Search code examples
logicproof

Prove ¬(¬a = a)


This looks like such an easy problem but still can't figure it out. How do I prove ¬(¬a = a)?

No given premises.

I got this so far (in Fitch):

proof so far

This is a subproof where I assume the negation of my goal and then try to reach the absurd/contradiction so I can state the negation of my assumption, which would be my goal.

Thanks in advance!


Solution

  • Looking at your screenshot I'd say your =Intro introduces a variable a (that is, a is an object of the domain, rather than a predicate).

    I say this because

    1. in all books I've read, the =Intro rule is used for objects rather than predicates, and

    2. for predicates, equals is expressed as "if and only if" which is typically written as ↔ and not =.

    So, in other words, the only sensible interpretation of ¬(¬a = a) is that = binds harder than ¬, and the whole formula should be interpreted as ¬(¬(a = a)).

    Now you should be able to

    1. introduce a = a
    2. assume the contrary: ¬(a = a)
    3. arrive at a contradiction, ⊥, based on 1. and 2.
    4. Use ¬Intro on 2 and 3 to get ¬(¬(a = a)).