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

[Alexander Krauss]

Brian Huffman wrote:
> 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.

Probably one can simply interpret bool as a three-element set {True, 
False, AlsoTrue}, where AlsoTrue behaves just like True under the 
propositional connectives, but they are not equal.

Alex