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

[Brian Huffman]

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