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

[Tobias Nipkow]

This is more subtle. I copied the axioms from Mike Gordon's TR 68.
Neither of us seems to have noticed the redundancy.

If you look at "HOL done right" by John Harrison, he does not seem to
comment on the redundancy either but sets the system up a bit
differently: he includes "iff" (IMP_ANTISYM_RULE) as an axiom, but
derives True_or_False (BOOL_CASES_AX) from the axiom for SOME. He
comments he wants to delay the point at which the system becomes
classical and introduces the SOME operator later. That must be the
reason why he does not get rid of IMP_ANTISYM_RULE as well.

Coming back to Isabelle/HOL: there seems no reason to have "iff" as an
axiom since we are unashamedly classical from the beginning. (We delay
SOME, so we cannot derive True_or_False from it.) I have no objection to
a removal of this axiom.

Tobias

Brian Huffman wrote:
> Hello again,
> 
> 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.
> 
> - Brian
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev