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

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

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.

Regards,
GB






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