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
inconsistent.

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
things.

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.

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.
This sounds all very risky ;) "a person" (as in *a single* person), "slight modification", "no inconsistency shows up".

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
different.
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).

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,

chris






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.