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
