The logical system used in this post is first-order logic.

I’ve been reading Introduction to Logic: Predicate Logic, 2nd edition by Howard Pospesel, and I have some questions concerning a truth tree. In chapter 9 on page 114, question 6(a) poses the following. “Prove by the proof and truth-tree methods that the symbolization of this sentence is a logical truth: There is someone such that if he or she makes a donation to charity, then everyone makes such a donation. (domain: people)”. I agree that this statement is a logical truth. However, my symbolization involves a nested quantifier, which was not used in the book prior to this problem. Let Dx mean x makes a donation to charity. Then my symbolization is: ∃x (Dx → ∀yDy). My questions are:

  1. Is my symbolization correct?
  2. Is there an alternate symbolization that does not use nested quantifiers?
  3. Is my two-sided truth tree correct? (see attached below)
  4. For sequents with nested quantifiers without relational predicates, are truth trees an effective method? Is so, how would ⊢ ∃x (Dx → ∀yEy) ever terminate?

Thanks for any help or input you can provide! The last question bugs me because Pospesel never seems to get anything wrong, yet he claims on page 168 that truth trees are effective for sequents with only monadic predicates. I hope I can get my thinking straightened out.

Thank you!

Two-Sided Truth Tree

  • 1
    Your formula sounds correct with an non-empty domain of FOL and this is actually the famous Drinker paradox: is a theorem of classical predicate logic that can be stated as "There is someone in the pub such that, if he is drinking, then everyone in the pub is drinking." It was popularised by the mathematical logician Raymond Smullyan. As for your truth-tree's effectiveness for sequents with only monadic predicates, this is due to the well-known decidability of monadic fragment of FOL without function symbols... Jul 24, 2022 at 17:12
  • The formula is correctly written, but in order to prove that it is a tautology you have to start with the negation of the formula: the truth-tree method works by contradiction: showing that the negation of the formula is unsatisfiable, we may conclude that the formula is a tautology. Jul 25, 2022 at 8:57


You must log in to answer this question.

Browse other questions tagged .