# language logic and proof chapter 12 question 49 and question 50

I've been working on this and I can't seem to figure out what exactly is going wrong can anyone help?  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
``````
• Thank you so much that makes so much more sense now! – jessie Nov 27 '18 at 2:54