[isabelle-dev] Isabelle/HOL axiom "iff" is redundant
brianh at cs.pdx.edu
Wed Nov 11 18:57:09 CET 2009
While I'm on the subject of redundant axioms, consider this piece of HOL.thy:
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.
More information about the isabelle-dev