# LPL ( language proof and logic) - FITCH - 14.12

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

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?

• 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

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