2

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

  • 1
    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
2

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)] ).

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.