# prove: ∃x ∃y (Cube(x) ∧ Cube(y) ∧ x ≠ y ∧ ∀z (Cube(z) → (z = x ∨ z = y)))

I need a formal (Fitch) first order logic proof for:

∃x ∃y (P(x) ∧ P(y) ∧ x ≠ y ∧ ∀z (P(z) → (z = x ∨ z = y)))

Given

∃x ∃y (P(x) ∧ P(y) ∧ x ≠ y)

∀x ∀y ∀z ((P(x) ∧ P(y) ∧ P(z)) → (x = y ∨ x = z ∨ y = z))

Any tips or help would be appreciated,

Bob Miller

• welcome to philosophy.SE! What have you tried so far? – Mr. Kennedy Mar 13 '17 at 1:40
• This is confusing to me. Say `P` is `is a dog?` and `x` is `Fido` (a dog) and `y` is `Rover` (also a dog). Then ∃x ∃y (P(x) ∧ P(y) ∧ x ≠ y) is valid. How can we then believe ∀z (P(z) → (z = x ∨ z = y)))? Are all dogs either Fido or Rover? What about poor Spot? The situation doesn't seem to get any better if `P` is `is a cubic number?`, as is implied by your title. There we can have `x=8` and `y=27` and yet still `z=64`. What am I missing? – Dan Bron Mar 13 '17 at 9:45
• Consider 2nd premise; with your example : (Dog(Fido) ∧ Dog(Rover) ∧ Dog(Spot)) → (Fido = Rover ∨ Fido = Spot ∨ Rover = Spot). But Fido = Rover is ruled out by 1st premise; thus we get : Fido = Spot ∨ Rover = Spot. – Mauro ALLEGRANZA Mar 13 '17 at 10:04
• @MauroALLEGRANZA But both `Fido = Spot` and `Rover = Spot` are false, so `Fido = Spot ∨ Rover = Spot` is false. So what is this whole proof telling us? I took the ∀z clause to be a conclusion based on the ∃x ∃y premise, but if it's also a premise, then what is the conclusion? What are we proving? – Dan Bron Mar 13 '17 at 10:10
• Why you conclude that both Fido = Spot and Rover = Spot are false ? You are assuming the existence of a third dog named Spot and you conclude that either Fido = Spot or Rover = Spot; thus, there is no "third dog". – Mauro ALLEGRANZA Mar 13 '17 at 10:21

Use -elim twice with 1st premise to get :

P(a) ∧ P(b) ∧ a ≠ b.

Use -elim with 2nd premise to get :

(P(a) ∧ P(b) ∧ P(z)) → (a = b ∨ a = z ∨ b = z).

Assume:

[A] P(z)

and unpack the first above to get :

¬ (a=b)

and the second above to get:

¬ (a=b) → (a = z ∨ b = z)

and by modus ponens (i.e. -elim) derive:

a = z ∨ b = z.

By -intro (Conditional Proof) we get:

P(z) → (a = z ∨ b = z),

discharging "temporary" assumption [A], and then ∀z [ P(z) → (a = z ∨ b = z)], by -intro (no z free in the premises or assumptions left).

Now by we "re-build":

P(a) ∧ P(b) ∧ a ≠ b ∧ ∀z [ P(z) → (a = z ∨ b = z)]

followed by -intro twice to get:

∃x∃y ( P(x) ∧ P(y) ∧ x ≠ y ∧ ∀z [ P(z) → (x = z ∨ y = z)] ).