Re: [isabelle] Schematic vars or universal bound vars in theorem?
What you describe is all possible without using axioms (which are
usually just used to initially set up a logic like HOL in Isabelle).
Just use a locale that has all your "axioms" as assumptions and inside
this locale you can work as if you had introduced the axioms. However,
you avoid the risk of anything outside the locale being effected. E.g.,
when adding inconsistent axioms to HOL the combination is just
inconsistent (and because of this risk I would not build on any theory
with "unnecessary" axioms). Defining a locale with inconsistent
assumptions just means that the locale itself is useless but does not
effect the whole logic.
The bottom line: avoid using axioms (as long as you are not setting up a
new object logic for Isabelle).
On 07/22/2012 03:29 PM, Gottfried Barrow wrote:
On 7/21/2012 1:32 PM, Makarius wrote:
On Wed, 18 Jul 2012, Gottfried Barrow wrote:
It's my healthy paranoia kicking in here. I'm using axioms, so I'm
trying to use everything I know right now to keep from being
The best way is not to use axioms then. In mathematics you define new
things by using old ones, and then prove the desired properties.
Sometimes you work with abstract theories, but that corresponds to a
locale or class definition in Isabelle/HOL, not axiomatization.
I'll try to make a short sales speech here to spin the pro-axiom side of
Suppose there are 10 standard axioms for a language of FOL that have
held up for many years. Then there's no more risk in using those axioms
than there's ever been.
Right, but combining those axioms with others (say those of HOL) is a risk.
This sounds all very risky ;) "a person" (as in *a single* person),
"slight modification", "no inconsistency shows up".
Suppose a person implements those axioms on top of Isabelle/HOL with a
slight modification, and others build a lot of standard math on top of
those axioms, and no inconsistency shows up.
What you describe is not using HOL as a meta-language to reason about
another standard logic (which is a reasonable thing to do), but
extending HOL itself by additional axioms (which I would consider risky).
The scenario I just described would be completely beneficial to
Isabelle/HOL as a product. What's done as HOL is just HOL, where HOL is
obviously very useful. But if HOL is used as a meta-language to
implement another standard logic on top of it, in a way that's
reasonably pure, which might require axioms to do, then that's something
If you use HOL to reason about another logic, you will *define* (not
axiomatize) the formulas of this logic as HOL-type and also define its
semantics by HOL-functions. In that way you can talk *about* the other
logic *in* HOL.
just my 2 cents,
This archive was generated by a fusion of
Pipermail (Mailman edition) and