Been stuck on this question for awhile now and I just don't know how to get Cube(x) so that I can use ^ intro with Cube(x) and ∀y (Cube(y) → y = a) and then use ∃ intro to get the conclusion. This is what I have so far.enter image description here

This is the original question if needed (14.11). enter image description here

1 Answer 1


Hint: Universal elimination can be to any term in the context, which includes the assumed witness for the existential.

|_ Ex Ay (Cube(y)<->y=x)                Premise
|  |_ [a] Ay (Cube(y)<->y=a)            Assumption
|  |  Cube(a)<->a=a                     Universal Elimination
|  |  :
|  |  :
|  |  Ex (Cube(x) & Ay (Cube(y)->y=x))  Existential Introduction
|  Ex (Cube(x) & Ay (Cube(y)->y=x))     Existential Elimination

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .