# Fitch Proof - Logic LPL 13.11

I am currently doing questions for my course from LPL Chapter 13.11. I have posted the screenshot of what I am trying to do. I am quite stuck and I can not think of a way to get to ~Tet(a). Any hint and help would be really appreciated. • Welcome to Philosophy.SE! Are you sure this is right? From the two premises, it does not follow that there is an x with ~Tet(x): the premises are true also when for all x Tet(x) holds. – user2953 Aug 12 '16 at 4:37
• Yes, after like an hour of thinking I am really questioning whether this is a typo :/ But this is straight out of the textbook. – mehryar Aug 12 '16 at 4:42
• In a world with 1 Tet and nothing else the premises are true and the conclusion false. – Eliran Aug 12 '16 at 7:16

This must be a typo in the text book: in the case that ∀x: Tet(x) ∧ ¬Cube(x) the premises are both true (provided there is at least one x), but the conclusion obviously does not hold.

However, you can prove that the promises entail ∃x: Tet(x).

Its purposely not suppose to work out. I would recommend using Taskis world to make something like this to prove it wrong • Would you be able to provide that counterexample. That would strengthen your answer and give the reader more information. Welcome to this SE! – Frank Hubeny Nov 27 '18 at 3:38
• The counter example is there in the image: When the domian is of several tetrahedrons and nothing else, then the premises are both satisfied but the existance of a non-tetrahedron is not satisfied. – Graham Kemp Nov 27 '18 at 3:54

When you introduce a new term `a`, don't use a completely different term `b`. You introduced it for a reason.

You appear to be trying rules at random hoping to hit on something. Examing the premises and target conclusions.

`````` |  Ax (Cube(x) v Tet(x))    Premise
|_ Ex ~Cube(x)              Premise
|  :
|  Ex Tet(x)                Somehow
``````

[Note: presumably the target should be `Ex Tet(x)` because `Ex ~Tet(x)` is not entailed by the premises. ]

Your premises are an existential and a universal of a disjunction and your target is another existential. That suggests some of the rules of inference you might need are Existential Elimination, Universal Elimination, Disjunction Elimination, and Existential Introduction.

`````` |  Ax (Cube(x) v Tet(x))    Premise
|_ Ex ~Cube(x)              Premise
|  |_ [a] ~Cube(a)          Assumption
|  |  Cube(a) v Tet(a)      Universal Elimination
|  |  :
|  |  Tet(a)                Disjunction Elimination
|  |  Ex Tet(x)             Existential Introduction
|  Ex Tet(x)                Existential Elimination
``````

Disjunction Elimination is a Proof by Cases: You require two subproofs, assuming in turn the left and right cases of the disjunction, and deriving the conclusion in each. In the right case it is trivial (the desired conclusion is the assumption). In the left case the assumption contradicts an earlier assumption, so you may use the principle of explosion (what your proof checker names "contradiction elimination").

``````  1.|  Ax (Cube(x) v Tet(x))    Premise
2.|_ Ex ~Cube(x)              Premise
3.|  |_ [a] ~Cube(a)          Assumption
4.|  |  Cube(a) v Tet(a)      Universal Elimination (1)
5.|  |  |_ Cube(a)            Assumption
6.|  |  |  #                  Contradiction Introduction (3,5)
7.|  |  |  Tet(a)             Contradiction Elimination  (6) (ex falso quodlibet)
8.|  |  +
9.|  |  |_ Tet(a)             Assumption
10.|  |  Tet(a)                Disjunction Elimination (4,5-7,9-9)
11.|  |  Ex Tet(x)             Existential Introduction (10)
12.|  Ex Tet(x)                Existential Elimination (2,3-11)
``````

[ You should notice that the original conclusion `Ex ~Tet(x)` just could not be reached from this point. If you assume Tet(a) and have no active contradictions, then ~Tet(a) cannot be derived. ]

So ends the lesson.