[isabelle-dev] Isabelle/HOL axiom "iff" is redundant
krauss at in.tum.de
Wed Nov 11 23:09:59 CET 2009
> Has anyone else noticed that axiom "True_or_False" implies axiom
> "iff"? (You can just do a proof by cases on P and Q.)
Here the case seems a little different, as eq_reflection is probably not
involved (or is it?). So maybe this is really redundant, but I am not sure.
> 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.
This seems like a sensible explanation... Was there ever a non-classical
HOL? At least in the "known history" the axioms were always sitting
there, side by side:
More information about the isabelle-dev