[isabelle-dev] Isabelle/HOL axiom "iff" is redundant
Alexander Krauss
krauss at in.tum.de
Thu Nov 12 16:05:07 CET 2009
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
More information about the isabelle-dev
mailing list