# Is Analytic/Semantic Tableaux a Semantic Method?

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

• The Method of analytic tableaux is a decision procedure for sentential logic, and a proof procedure for formulae of first-order logic. Commented Jul 8, 2021 at 6:54
• 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. Commented Jul 8, 2021 at 7:07