[isabelle-dev] Isabelle/HOL axiom "iff" is redundant
Makarius
makarius at sketis.net
Thu Nov 12 13:52:38 CET 2009
On Wed, 11 Nov 2009, Brian Huffman wrote:
> 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.
Concerning experiments with HOL axiomatics,
src/HOL/ex/Higher_Order_Logic.thy might be of some interest. I've always
found it more aestical to introduce the stronger principles like the
classical axiom as late as possible, even if some more basic things happen
to follow from it later.
Anyway, can you still derive iff from a more conventional classical rule
without equality?
Moreover, see src/HOL/Hilber_Classical.thy for proofs of tertium-non-datur
derived from Hilbert Choice.
Makarius
More information about the isabelle-dev
mailing list