Before I get to the question, could a moderator let me know if it's OK to cross post this on the philosophy site? I suspect those coming from a mathematical background will answer differently than those coming at this from a philosophy background.

The question is this, is Analytic/Semantic Tableaux (ST), also know as the Truth Tree Method, when used in the context of determining whether or not a sequent is semantically valid, a semantic or a syntactic method?

This discussion came up in the context of Classical Predicate/Quantificational/First-Order Logic (QL), and, unless otherwise stated, I will be referring to ST wrt QL. As ST can be used for other things, I'm only referring to its use as a decision-procedure for determining semantic validity.

So what do I mean by "syntactic"?

Syntactic refers broadly to the grammar of a language, logical or otherwise. Wrt to QL it refers specifically to 2 things. Firstly, it refers to the rules that allow us to construct well formed formulas (WFFs). Secondly, it refers to the proof theory of QL. The proof theory of QL is composed of the introduction and elimination rules inherited from Propositional Logic, and the universal, existential, and, potentially, identity introduction and elimination rules. The rules together are known as inference rules and allow us to take a set of premises and derive a conclusion. This process is known as a proof and is denoted in sequent form using the single turnstile - ⊢. This process isn't dependent on meaning, truth, etc., though it could be said to define, in a way, what the connectives mean.

What do I mean be semantic?

Semantics broadly deals with what things mean. Wrt to QL, and in the context of this discussion, it refers specifically to 2 things. Firstly, it refers to the interpretation ($\Im$), namely what the domain is, what the predicates and relations refer to, and what the names refer to. Secondly, it refers to truth assignments. Truth in QL is relative in that it depends on the interpretation. Roughly speaking, a predicate is a subset of the domain and a subject-predicate sentence is true if the subject is a member of the predicate subset and false if it isn't. For example -

$\begin{array}{lrl}\Im & D:& \{0, 1\}\\& F:& \{1\}\\& a:& 1\\& b:& 0\\\end{array}$

$Fa$ would be true under this interpretation, and $Fb$ would be false.

What do I mean when I say a sequent is semantically valid?

A sequent is semantically valid if and only if there exists no way for the premises to be true and the conclusion false. Keep in mind what "truth" means wrt to QL. We denote a semantically valid sequent using the double turnstile - ⊨.

Which brings us to ST and whether it's a semantic method. The development rules of ST take the WFFs that are the premises and the conclusion of a sequent, breaks them down into their constituent parts and assigns truth values to each constituent part. The process delineates all the appropriate ways that this can be done, and, as such, allows us to determine if a sequent is semantically valid, invalid, or, in the case of an infinite tree, undecidable. It does this very simply by looking to see if it's possible for the premises to be true while the conclusion is false. Another way to think about what ST is doing is that it's delineating the general properties that applicable $\Im$s must have. As polyadic QL is semi-decidable there exist some invalid sequents that can't be shown to be invalid via this, or any other, algorithm. In these cases we need to use human creativity to come up with a counterexample, also known as an Invalidating QL Interpretation (IQLI).

Now some of the ST development rules are syntactic, e.g., Universal Instantiation (UIN) and Existential Instantiation (EIN). But, as the process is exhaustively testing for semantic validity by assigning truth values, by assigning meaning, I contend that it is a semantic method, not a syntactic method. We're showing that a sequent is semantically valid through a process that assigns meaning.

In a practical sense, syntactic methods and semantic methods serve different purposes and can do different things. A syntactic method takes a set of premises, a set that may be empty, and churns out the conclusions that can be reached from those premises. We don't need to know what those conclusions are ahead of time, we can use a syntactic method to search for them. Semantic methods on the other hand can tell us if an entire argument is valid in QL, but we can't use it to derive novel conclusions. If we know what the entire argument is, though, it's really easy and fast to check it, and soundness and completeness guarantee that all semantically valid sequents are syntactically provable and vice versa. The Lowenheim-Skolem Theorem, which allows us to use the natural numbers for our domains, predicates, etc., makes it really easy to come up with models and counterexamples too, which makes ST the main way things get proved in QL (at least when we know what we want to prove).

  • $\begingroup$ The Method of analytic tableaux is a decision procedure for sentential logic, and a proof procedure for formulae of first-order logic. $\endgroup$ Commented Jul 8, 2021 at 6:54
  • $\begingroup$ I do cover that it gets used as the most common method of proving sequents :) Being sound and complete allows us to play pretty fast and loose with the tools we use. $\endgroup$
    – Ten O'Four
    Commented Jul 8, 2021 at 7:07

1 Answer 1


One can regard the method of analytic tableaux as an idiosyncratic (but often convenient!) alternative syntax for the one-sided Gentzen system (sequent calculus). I have yet to see anyone argue that the classic sequent calculi are semantic methods: on the contrary, they are usually regarded as the most syntactic of the syntactic methods.

The correspondence between tableaux and sequents is presented in many textbooks: for those who already know tableaux, but not sequent calculus, I recommend Chapter 11 of Raymond Smullyan's First-order logic.

  • $\begingroup$ Gentzen goes considerably further than a basic test of semantic validity, though. As such, a counterexample to your argument would be "polyadic QL is undecidable, therefore monadic QL is undecidable". Out of interest, are you viewing all structure as syntactic? Is an interpretation a syntactic structure to you? Or does it become syntactic when it's generalised? The test I'm asking about could be interpreted as the general form of the meaning, and what form is allowable depends on the form of the sequent. "Helping your uncle, Jack, off a horse", changes depending on "," use, etc. $\endgroup$
    – Ten O'Four
    Commented Jul 8, 2021 at 8:32
  • $\begingroup$ Thanks for the paper! I don't suppose you could point me at the second group they mention that looked to add in semantic elements? Maybe add it to your answer too? That would really help me with how different peeps are viewing what's what. $\endgroup$
    – Ten O'Four
    Commented Jul 8, 2021 at 8:39

You must log in to answer this question.

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