3

what's wrong with the last line in my proof? i can't understand the error on line 21 enter image description here

i wrote the important line of the proof :

18 - ∀z (Cube(z) → (z = c ∨ z = f))

19 - ∃y (Cube(c) ∧ Cube(y) ∧ c ≠ y)

20 - ∃y (Cube(c) ∧ Cube(y) ∧ c ≠ y) ∧ ∀z (Cube(z) → (z = c ∨ z = f))

21 - ∃x ∃y (Cube(x) ∧ Cube(y) ∧ x ≠ y ∧ ∀z (Cube(z) → (z = x ∨ z = y)))

EDIT

NOW IT WORK BUT I CAN'T USE FO CON. HOW CAN I WROTE THE SAME LINE WITHOUT USE FO CON?

enter image description here

  • 1
    21 has an existential quant more than 20: this need a new ∃-intro... – Mauro ALLEGRANZA Dec 28 '17 at 8:59
  • @MauroALLEGRANZA i tried but it doesn't work. can you tell me what line i have to select? – Taioli Francesco Dec 28 '17 at 9:19
  • From 20 to 21 the z=f has been rewritten as z=y. Whu ? – Mauro ALLEGRANZA Dec 28 '17 at 9:26
  • @MauroALLEGRANZA it's a mine error because the ∃-quant doesn't take the ∀z part. How can include the ∀z(..) inside the ∃ intro in the line 20? – Taioli Francesco Dec 28 '17 at 9:33
  • @MauroALLEGRANZA i edit the question – Taioli Francesco Dec 28 '17 at 12:17
4

18 - ∀z (Cube(z) → (z = c ∨ z = f))

19 - (Cube(c) ∧ Cube(y) ∧ c ≠ y) ∧ ∀z (Cube(z) → (z = c ∨ z = f)) --- from 4 and 18 by ∧-intro

20 - ∃x ∃y [(Cube(x) ∧ Cube(y) ∧ x ≠ y) ∧ ∀z (Cube(z) → (z = x ∨ z = y))] --- from 19 by ∃-intro twice

20 is derived under the two assumptions 3 and 4 made for two ∃-elim's with terms c and f. They are not present in 20; thus, we can safely conclude with 20 by ∃-elim twice, discharging temporary assumptions 3 and 4.

Conclusion:

1, 2 ⊢ ∃x ∃y [(Cube(x) ∧ Cube(y) ∧ x ≠ y) ∧ ∀z (Cube(z) → (z = x ∨ z = y))]

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.