computer-sciencefirst-order-logicfitch-proofs

Deriving Cube(a) from Cube(a) <-> a = a (Fitch)


I'm trying to prove something in Fitch and i'm stuck on one step, i have:

1.  Cube(a) <-> a = a

and i want to derive 2. Cube(a) from that.

I know it's possible because i can use Ana Con on 2. and selecting 1. as premise and it says it's valid.
Is there anyone who can tell me how to do this without using Ana Con?


Solution

  • (I don't have a copy of Fitch and have never used it, so take this with a pinch of salt. But I'm pretty sure it's right.)

    First get just "a=a" using =Intro. (You don't need any premises.) Then take that plus your 1. and apply <->Elim to get Cube(a).