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.

enter image description here

  • 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, 2016 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, 2016 at 4:42
  • In a world with 1 Tet and nothing else the premises are true and the conclusion false.
    – E...
    Aug 12, 2016 at 7:16

3 Answers 3


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

enter image description here

  • Would you be able to provide that counterexample. That would strengthen your answer and give the reader more information. Welcome to this SE! Nov 27, 2018 at 3:38
  • 1
    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. Nov 27, 2018 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.

You must log in to answer this question.

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