0

I've been working on this and I can't seem to figure out what exactly is going wrong can anyone help? enter image description here

enter image description here

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
  • Thank you so much that makes so much more sense now! – jessie Nov 27 '18 at 2:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.