Re: [isabelle] Schematic vars or universal bound vars in theorem?
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.
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.
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
I'm interested in certain non-applied math, but with Isabelle I take the
attitude that all math implemented in Isabelle is applied math, with the
application being the attempt to find out how powerful Isabelle is. If
no one successfully uses axioms on top of Isabelle/HOL, then that
potential power of Isabelle/HOL never gets demonstrated.
Church's logic was shown to be inconsistent. The possibility of that
happening is all part of the game.
Giving opinions. That's the easy part.
This archive was generated by a fusion of
Pipermail (Mailman edition) and