[isabelle-dev] Isabelle/HOL axiom "iff" is redundant

Makarius makarius at sketis.net
Thu Nov 12 13:52:38 CET 2009


On Wed, 11 Nov 2009, Brian Huffman wrote:

> While I'm on the subject of redundant axioms, consider this piece of HOL.thy:
>
> axioms
>  iff:          "(P-->Q) --> (Q-->P) --> (P=Q)"
>  True_or_False:  "(P=True) | (P=False)"
>
> Has anyone else noticed that axiom "True_or_False" implies axiom "iff"? 
> (You can just do a proof by cases on P and Q.) I actually did this proof 
> within a modified HOL.thy (some lemmas need to be proved in a different 
> order, but the bootstrapping still works).
>
> I'm guessing that the origins of this redundancy are historical---I 
> suppose that True_or_False was probably introduced later in the 
> development so that intuitionistic lemmas could be kept separate from 
> the classical ones.

Concerning experiments with HOL axiomatics, 
src/HOL/ex/Higher_Order_Logic.thy might be of some interest. I've always 
found it more aestical to introduce the stronger principles like the 
classical axiom as late as possible, even if some more basic things happen 
to follow from it later.

Anyway, can you still derive iff from a more conventional classical rule 
without equality?

Moreover, see src/HOL/Hilber_Classical.thy for proofs of tertium-non-datur 
derived from Hilbert Choice.


 	Makarius




More information about the isabelle-dev mailing list