[isabelle-dev] Isabelle/HOL axiom "iff" is redundant

[Brian Huffman]

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