I've been working on this and I can't seem to figure out what exactly is going wrong can anyone help?
0
1
Okay, you are clearly on track here.
Now, you introduced term c to act as a witness for an existential, so thus you need to discharge it through Existential Elimination (not FO con).
|_ Ex (P(x) ^ Ay (P(y) -> y=x) ) Premise
| |_ [a,b] P(a) ^ P(b) Assumption (arbitrary)
| | |_ [c] P(c) ^ Ay (P(y) -> y=c) Assumption (witness to existance)
| | | P(a) Conjunction Elimination
| | | P(b) Conjunction Elimination
| | | Ay (P(y) -> y=c) Conjunction Elimination
| | | P(a) -> a=c Universal Elimination
| | | P(b) -> b=c Universal Elimination
| | | a=c Conditional Elimination
| | | b=c Conditional Elimination
| | | a=b Equality Elimination
| | a=b Existential Elimination (null quantification)
| Ax Ay ((P(x) ^ P(y)) -> x=y) Universal Introduction
Note, if your checker doesn't allow two universals to be introduced in one step, then do it in two.
|_ Ex (P(x) ^ Ay (P(y) -> x=y)) Premise
| |_ [a] Assumption
| | |_ [b] P(a) ^ P(b) Assumption
| | | |_ [c] P(c) ^ Ay (P(y) -> c=y) Assumption
| | | | : Rhubarb Rhubarb
| | | | a=b Equality Elimination
| | | a=b Existential Elimination
| | Ay ((P(a) ^ P(y)) -> a=y) Universal Introduction
| Ax Ay ((P(x) ^ P(y)) -> x=y) Universal Introduction
... or maybe in three. I prefer this format because, despite adding a step and a context, it clearly distinguishes between raising an assumption using an arbitrary term, and assuming a witness exists.
|_ Ex (P(x) ^ Ay (P(y) -> x=y)) Premise
| |_ [a] Assumption
| | |_ [b] Assumption
| | | |_ P(a) ^ P(b) Assumption
| | | | |_ [c] P(c) ^ Ay (P(y) -> c=y) Assumption
| | | | | : Rhubarb Rhubarb
| | | | | a=b Equality Elimination
| | | | a=b Existential Elimination
| | | (P(a) ^ P(b)) -> a=b Conditional Introduction
| | Ay ((P(a) ^ P(y)) -> a=y) Universal Introduction
| Ax Ay ((P(x) ^ P(y)) -> x=y) Universal Introduction
