Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.
Sign up to join this community
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.
This is the original question if needed (14.11).
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
