1

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

5
  • 1
    21 has an existential quant more than 20: this need a new ∃-intro... Dec 28, 2017 at 8:59
  • @MauroALLEGRANZA i tried but it doesn't work. can you tell me what line i have to select? Dec 28, 2017 at 9:19
  • From 20 to 21 the z=f has been rewritten as z=y. Whu ? Dec 28, 2017 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? Dec 28, 2017 at 9:33
  • @MauroALLEGRANZA i edit the question Dec 28, 2017 at 12:17

1 Answer 1

3

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

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .