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
