[isabelle-dev] Isabelle/HOL axiom "iff" is redundant
Brian Huffman
brianh at cs.pdx.edu
Thu Nov 12 15:57:32 CET 2009
On Thu, Nov 12, 2009 at 4:52 AM, Makarius <makarius at sketis.net> wrote:
> Anyway, can you still derive iff from a more conventional classical rule
> without equality?
I just had a go at this, and I don't think it's possible.
Using the classical axiom "P | ~ P", the proof attempt of iff reduces
to the following subgoals:
1. [| P; Q |] ==> P = Q
2. [| ~P; ~Q |] ==> P = Q
At this point we're stuck, since we don't know anything special about
equality on booleans beyond refl and subst. It seems that the
classical axiom "P | ~ P" (without axiom iff) is consistent with
models where equality on booleans is strictly stronger than
bi-implication.
- Brian
More information about the isabelle-dev
mailing list