Why should we care about syntactic proofs if we can show semantically that statements are true?

Question

I am talking about classical logic here.

I admit this might be a naive question, but as far as I understand it: Syntactic entailment means there is a proof using the syntax of the language, while on the other hand semantic entailment does not care about the syntax, it simply means that a statement must be true if a set of other statements are also true.

That being said, isn't semantic entailment sufficient to know whether or not a statement is true? Why do we need syntactic proofs?

Granted I know that in the case of boolean logic, proving statements by truth tables gets intractable very fast, but in essence, isn't semantic entailment "superior"? As it does not rely on how we construct the grammar?

Thank you

Edit: Suppose it wasn't the case that finding a satisfying assignment to an arbitrary boolean statement is an exponentially increasing problem, then would we even need syntactic entailment?

Answer 1

First of all, let me set the terminology straight:

By a syntactic proof ($\vdash$) we mean a proof operating purely on a set of rules that manipulate strings of symbols, without making reference to semantic notions such as assignment, truth, model or interpretation. A syntactic proof system is one that says, for example, "If you have $A$ written on one line and $B$ on another line, then you are allowed to write the symbols $A \land B$ on a line below that." Examples of syntactic proof systems are Hilbert-style calculi, sequent calculi and natural deduction in their various flavors, or tableaus aka truth trees.

By a semantic proof ($\vDash$) we mean a proof operating on the semantic notions of the language, such as assignment, truth, model or interpretation. Examples of semantic proofs are truth tables, presentation of (counter) models, or arguments in plain text (along the lines of "Suppose $A \to B$ is true under a given assignment. Then it is the case that either ...").

Furthermore, the term "entailment" is usually understood as a purely semantic notion ($\vDash$), while the syntactic counterpart ($\vdash$) is normally referred to as derivability.

(The division "$\vDash$ $\approx$ semantics $\approx$ models and $\vdash$ $\approx$ syntax $\approx$ proofs" is oversimplifying matters a bit -- proof theoretic semantics, for example, argues that a semantics can be established in terms of formal (= "syntactic") proofs rather than just by model-theoretic considerations, but for the sake of this explanation, let's keep this more simple two-fold distinction up.)

I'm clarifying this because the way you set out things is not entirely accurate:

Syntactic entailment means there is a proof using the syntax of the language

In a way yes, the syntax of a logic is always relevant when talking about notions such as entailment or derivability -- but what is the crucial feature that makes us call this notion syntactic? It isn't that the syntax of the language is involved in establishing entailment or derivability relations. The crucial feature is that the set of rules we use is purely syntactic, i.e. merely operating on strings of symbols, without making explicit reference to meaning.

while on the other hand semantic entailment does not care about the syntax

That's not quite accurate -- in order to establish the truth value of a formula and hence notions such as validity or entailment, we have to investigate the syntax of a formula in order to determine any truth value at all. After all, truth is defined inductively on the structure (= the syntax) of formulas: "$[[A \land B]]_v = \text{ true iff } [[A]]_v = \text{ true and } [[B]]_v = \text{true}...$" If we didn't care about syntax, then we couldn't talk about semantics at all.

---

Now to your actual question:

Why should we care about syntactic proofs if we can show semantically that statements are true?

The short answer is: Because syntactic proofs are often a lot easier.

For propositional logic, the world is still relatively innocent: We can just write down a truth table, look at the truth value at each formula and decide whether or not it is the case that all the lines where the columns of all of the premises have a "true" also have the conclusion column as "true". As you point out, this procedure quickly explodes for formulas with many propositional variables, but it's still a deterministic procedure that's doable in finite time.

We could also present a natural language proof arguing in terms of truth assignments. This can be a bit more cumbersome, but might be more instructive, and is still comparatively handleable for the relatively simple language and interpretation of propositional logic.

But things get worse when we go into first-order logic. Here we are confronted with formulas that quantify over models whose domains are potentially infinite. Even worse, in contrast to propositional logic where the number of assignments (~= interpretations) is always finite and completely determined by the number of propositional variables, the structures (~= interpretations) in which a first-order formula might or might not be true are unlimited in size and shape. That is, not only can the structures themselves be infinite, but we are now facing an infinite amount of structures in which our formulas can be interpreted in the first place. Simply writing down a truth table will no longer work for the language of predicate logic, so determining the truth value -- and hence semantic properties and relations such as validity and entailment -- is no longer a simple, finite procedure for predicate logic.

So if we want to present a semantic proof, we have to resort to arguments about the structures that a formula does or does not satisfy. This is where an interesting duality enters:

• To prove that

  • an existentially quantified semantic meta-statement is true (For example "The formula $\phi$ is satisfiable", i.e. "There exists a model of $\phi$) or
  • a universally quantified semantic meta-statement is false (For example $\not \vDash \phi$, "The formula $\phi$ is not valid", i.e. "It is not the case that all structures satisfy $\phi$)

  it suffices to provide one (counter)model and we're done: If we find just one structure in which $\phi$ is true then we know that $\phi$ is satisfiable, and conversely, if we find one structure in which $\phi$ is not true then we know that $\phi$ is not valid.

Analogously, to prove that

• an existentially quantified object-language formula ($\exists x ...$) is true in a structure or
• a universally quantified object-language formula ($\forall x ...$) is false in a structure,

it suffices to find one element in the structure's domain that provides an example for the existentially quantified formula or, respectively, a counterexample to the universal quantification and we're done.

However,

• to prove that

  • a universally quantified semantic meta-statement is true (For example $\vDash \phi$, "The formula $\phi$ is valid", i.e. "All structures satisfy $\phi$), or
  • an existentially quantified semantic meta-statement is false (For example "The formula $\phi$ is unsatisfiable", i.e. "There exists no model of $\phi$),

  we are suddenly faced with the difficult task of making a claim about all possible structures. We can not simply list them, as there are infinitely many of them, so all we can do is write a natural-language text arguing over the possible truth values of formulas, eventually showing that all structures must succeed or fail to fulfill a certain requirement.

  Analogously, to prove that

  • an universally quantified object-language formula ($\forall x ...$) is true in a structure or
  • an existentially quantified object-language formula ($\exists x ...$) is false in a structure,

  we have to iterate over all the elements in the structure's domain. If the domain is finite, we are lucky and can simply go through all of the possible values (although this may take quite some time if the domain is large enough), but if it is infinite, there is no way we can ever get done if we just brute force check the formula for the elements one after the other.

This is a rather unpleasant situation, and exactly the point where syntactic proofs come in very handy.

Recall the definition of entailment:

$\Gamma \vDash \phi$ iff all interpretations that satisfy all formulas in $\Gamma$ also satisfy $\phi$

or equivalently

$\Gamma \vDash \phi$ iff there is no interpretation that satisfies all formulas in $\Gamma$ but not $\phi$.

This is precisely the kind of universal quantification that makes purely semantic proofs difficult: We would have to establish a proof over the infinity of all the possible structures to check whether the semantic entailment relation does or does not hold.
But now look at the definition of syntactic derivability:

$\Gamma \vdash \phi$ iff there is a derivation with premises from $\Gamma$ and conclusion $\phi$.

The nasty universal quantifier suddenly became an existential one! Rather than having to argue over all the possible structures, it now suffices to show just one syntactic derivation and we're done. (The same applies to the case where we don't have any premises, i.e. $\vDash \phi$ ("$\phi$ is valid" = "true in all structures" vs. $\vdash \phi$ (= "$\phi$ is derivable" = "there is a derivation with no open assumptions and $\phi$ as the conclusion). This is an enormous advantage -- call it "superior" if you want.

Now we have a kind of disparity: For some things semantics is hard whereas syntax is easy, so how can we use this disparity for good?
Luckily, in the case of classical logic, we are equipped with soundness and completeness:

Soundness: If $\Gamma \vdash \phi$, then $\Gamma \vDash \phi$ -- if we found a syntactic derivation, then we know that the entailment holds semantically.

Completeness: If $\Gamma \vDash \phi$, then $\Gamma \vdash \phi$ -- if a semantic entailment holds, then we can find a syntactic derivation.

While any reasonable derivation system will be sound w.r.t. to the language's semantics, completeness is a non-trivial and very powerful result: If we want to prove a semantic entailment, by completeness we know that there must be a syntactic derivation, so we can go find just one such derivation, and as soon as we do, soundness ensures us that this is indeed a proof that the entailment holds semantically. Hence, we can use syntactic proofs to avoid cumbersome semantic arguments that involve meta-logical quantification over all structures. This is pretty neat.

Now note how things turn around for the syntactic calculus:

• To prove that
• a universally quantified syntactic meta-statement is true or an existentially quantified syntactic meta-statement is false (For example $\not \vdash \phi$, "The formula $\phi$ is underivable", i.e. "There is no derivation with conclusion $\phi$"/"All attempts to find a derivation with conclusion $\phi$ eventually fail)

we would have to argue over all possible syntactic proofs, which can again be difficult.

Now we can apply the soundness and completeness results in the other direction: If we want to show that a formula is not derivable, then by contraposition on completeness we know it is not valid (because if it were, then by completeness there would be a derivation), so we can carry out a semantic proof by providing just one counter-model to the validity of $\phi$ and we're almost done; because then again by contraposition on soundness, we can be sure that if the formula is not valid, there will be no derivation (because if there were a derivation for something that is not semantically valid, our system would be unsound), so we have our proof of the underivability without needing to argue over hypothetical derivations that can't exist.

And this is precisely how the aforementioned duality comes about:

--------------------------------------------------------------------------------
            semantic                          syntactic
--------------------------------------------------------------------------------
positive    ⊨                                 ⊢                                 
            universal quantif.                existential quantif.
            ("all structures"/                ("there is a derivation"/
             "no structure such that not")     "not all derivations fail")
            => difficult 🙁                   => easy 🙂

negated     ⊭                                 ⊬                                 
            negated universal quantif.        negated existential quantif.
            ("not all structures"/            ("there is no syntactic proof"/
             "there exists a counter-model")    "all attempts at proofs fail")
            => easy 🙂                        => difficult 🙁
--------------------------------------------------------------------------------

Thanks to soundness and completeness, the duality of semantic and a syntactic proofs can help us bridge the difficult parts:

• $\vDash$ ("all structures" -- difficult) $\ \xrightarrow{\text{completeness}}\ $ $\vdash$ ("some derivation" -- easy) $\ \xrightarrow{\text{soundness}}\ $ $\vDash$
• $\not \vdash$ ("no derivation" -- difficult) $\ \xrightarrow{\text{contrapos. completeness}}\ $ $\not \vDash$ ("some countermodel" -- easy) $\ \xrightarrow{\text{contrapos. soundness}}\ $ $\not \vdash$

Putting these bridges into the picture from before:

------------------------------------------------------------------------------
            semantic                         syntactic
------------------------------------------------------------------------------

                        completeness     
                        ------------->   
positive    🙁 ⊨                            ⊢ 🙂
                        <-------------      
                          soundness

                    contrapos. completeness
                   <-----------------------
negated     🙂 ⊭                            ⊬ 🙁
                   ----------------------->
                     contrapos. soundness
------------------------------------------------------------------------------

I think the existence of syntactic calculi already is wonderful enough simply for the mathematical beauty of this symmetry.

Answer 2

The main reason to care about syntactic proofs is that they are crucial to the foundations of mathematics. If you are (say) formulating axioms for set theory which you will use as the foundation for all of mathematics, you need an unambiguous notion of proof that relies on an absolute minimum of background concepts (since you're trying to build all of the rest of math from this). Syntactic proofs are perfect for this: they're just finite strings of symbols that follows certain simple rules. Semantic proofs, on the other hand, only make sense once you already have a powerful metatheory that can reason about things like models. This is pretty useless for foundational purposes, since it just pushes the foundational question back to the metatheory.

To put it another way, let's say you're working with ZFC as your metatheory, as is standard in modern mathematics. If you want to study some first-order theory, you don't really need syntactic proofs--you can just always use semantic reasoning. But what is a semantic proof? It's just a syntactic proof in your ZFC metatheory, talking about models of your first-order theory within the first-order language of set theory.

---

On the flip side, I would emphasize that if you don't care about foundations and are just happily doing model theory within ZFC, there is pretty much no reason to ever think about syntactic proofs.* Although lemontree mentioned in their answer that syntactic proofs give an easier way to reason about all models, that's not really accurate, because you can just imitate the steps of a syntactic proof in semantic terms. For instance, typically one of the inference rules you can use in syntactic proofs is that if you have $\varphi$ and $\psi$ you can deduce $\varphi\wedge\psi$. Well, guess what? You can do this in semantic proofs too! If you have a model that satisfies both $\varphi$ and $\psi$, then it also satisfies $\varphi\wedge\psi$, by definition of satisfaction. Similarly, all the other syntactic inference rules can be trivially translated into semantic arguments.

_{*OK, this is a bit of an exaggeration. Even if you aren't doing foundations, you might still care about syntactic proofs for similar reasons as in foundations, namely their finitary nature. So for instance, if you have a finitely axiomatizable theory which you know (perhaps by semantic means) is complete, then using syntactic proofs (and the completeness theorem) you can deduce that there exists an algorithm that decides whether any sentence is in the theory.}

Answer 3

The good news is that for first-order logic we have the soundness and completeness theorems: For any first-order theory $T$, and any sentence $\sigma$ in the same language, $T \models \sigma$ if and only if $T \vdash \sigma$. That is, semantic and syntactic truth are equivalent.

In light of that theorem, you could, if you wish, focus entirely on semantic truth (as is sometimes done by model theorists) or entirely on syntactic truth (as is sometimes done by proof theorists). Each area has its own questions and techniques, but they are closely linked, so there is also opportunity for mixing the two.

One direct consequence of the completeness theorem is the compactness theorem, which is absolutely central to first-order model theory. It says that if every finite subset of some theory $T$ has a model, then $T$ itself has a model. You can prove this by observing that if $T$ had no model then you could write a proof of a contradiction from $T$. Since every proof is finite, only finitely many statements from $T$ are needed in your proof, so there must be a finite subset of $T$ that proves a contradiction, and hence has no models. (It's possible to prove compactness by methods that feel more semantic, like ultraproducts, but the proof sketched here is the first one that many people see).

Answer 4

The accepted answer is good and expansive, but let me try to distill the key point a bit:

How do you justify that a semantic proof is correct?

A “semantic proof” must still be a proof, in some rigorous checkable sense. If I claim I’ve got a semantic proof and you challenge it, how do we chase it down to a clear criterion for correctness? By breaking it down into minimal basic steps, and agreeing on what the valid basic steps are. In other words, we are agreeing on some syntactic notion of proof for the metatheory, and then exhibiting the semantic proof as a syntactic proof for the metathory. So in summary:

Every sufficiently rigorous notion of proof must be, at base, syntactic. A “semantic proof” means “a proof in the syntax of the metatheory, about the object theory” — so it still depends on a notion of syntactic proof.

---

Regarding your edit:

Suppose it wasn't the case that finding a satisfying assignment to an arbitrary boolean statement is an exponentially increasing problem, then would we even need syntactic entailment?

Semantics by finitary boolean assignment only covers the specific case of classical propositional logic. For this restricted case, it is more reasonable to suggest taking the semantics as primitive, since the semantics is just as simple and finitist as the syntax.

However, propositional logic isn’t expressive enough to do serious mathematics in it: mathematics requires quantification. For systems with quantification, like first-order predicate logic, the semantics are not finitist, so reasoning about them requires a non-trivial metatheory, and we’re back to the regress above: a rigorous notion of “semantic proof” depends on already having some rigorous notion of proof for the metatheory.

Answer 5

Others have already pointed out that although you can 'get away with' truth tables to verify the truth of a tautology in propositional logic, and do not need a so-called 'syntactic' deductive system for that, we need a 'syntactic' proof system for first-order logic (FOL), because it is impossible to use only truth tables.

I wish to elaborate more on that. Firstly, there is a wide variety of deductive systems for first-order logic, but in my opinion you only need to learn one of them to be able to not only understand but also reconstruct almost all the others, specifically Fitch-style natural deduction for first-order logic. Note that there are many variants of Fitch-style systems for FOL, but they are all based on the idea of performing deduction in explicit visually structured contexts. For propositional logic, we need only the if-subcontext (introduced by the "If ..." header in my post). For FOL, we need only that plus the universal-subcontext (introduced by the "Given ..." header). For reference, here is another Fitch-style variant, but the differences are not important for now.

What is important is that for FOL, the universal-subcontext is extremely crucial to allowing the deductive system to work. A proof of a universal statement, namely of the form "$∀x∈S\ ( Q(x) )$" has to be carried out by introducing a subcontext in which we are given "$x∈S$" and then within that subcontext proving that "$Q(x)$" is true. The beautiful thing is that we do not have to reason about all members of $S$, but merely about a single arbitrarily given member $x$ of $S$. If we can prove that such a given $x$ satisfies $Q$, then we have effectively proven that every member of $S$ satisfies $Q$, because our proof does not depend on which $x∈S$ was given. This idea is captured by the ∀-intro rule, and is critical in allowing a finite syntactic object (a proof) to capture a potentially infinite semantic notion (truth for every member of $S$).

This 'potentially infinitary' semantics is also what makes it impossible to use truth-tables to find out the truth-value of a sentence in FOL. It turns out that no computer program can correctly determine whether or not a sentence in FOL is a tautology. (This is called the undecidability of FOL, and one way to show this is to prove that any such program can be used to construct a program that can solve the halting problem.) This implies that no systematic procedure (using truth tables or otherwise) can determine whether or not a sentence in FOL is a tautology. This makes FOL very unlike propositional logic, because truth-tables provide a systematic procedure of determining whether a propositional formula is a tautology or not.

Incidentally, even for propositional logic it can be argued that truth-tables are in fact syntactic proofs in disguise! A truth-table 'proof' is implicitly claiming that the shown rows represent all possible cases, and the evaluation of the formula's truth value in each row is implicitly performing a syntactic analysis of the formula to determine its truth-value. How do you 'know' that you have not missed a case? You syntactically observe that each possible assignment of truth-values is in the table. This is not much different from performing a Fitch-style proof of the following form:

A∨¬A.
If A:
  ...
  B.
If ¬A:
  ...
  B.
B.

Same thing here, the only way to know whether a formal proof is correct is to syntactically observe that each step is permitted by the deductive rules. One can therefore say that the method of using truth-tables for propositional logic is actually just a primitive syntactic deductive system. It merely appears semantic, but you are definitely not dealing with real truth-values, and only playing with syntactic symbols for truth-values, often "0" and "1".

Answer 6

Are you talking about propositional logic or predicate calculus, aka first-order logic, or FOL? It makes a big difference regarding your question, why we care about $\vdash$ given that it's equivalent to $\models$:

1. In propositional logic truth tables give us an algorithm for determining whether $\models\phi$ holds, given $\phi$. There is no such algorithm for FOL (Godel proved here is no such algorithm). A counterexample suffices to show that $\not\models\phi$, but to verify $\models\phi$ "directly" would require that we look at infinitely many structures. In order to show $\models\phi$ we need some sort of logical argument to show that $\phi$ is true in every structure. Now if we want to __formalize_ this we need to give a precise definition f "some sort of logical argument"; that amounts to defining $\vdash$ or somethig very muuch like it.

In fact, even if $\models\phi$ is all we care about, typically or at least often verifying $\vdash\phi$ is the only way we have to verify $\models\phi$.

2. $\vdash$ is hugely important in proving things about logic. For example consider the Compactness Theorem:

CT: $\,\,\,\Gamma\models\phi$ if and only if $F\models\phi$ for some finite set $F\subset\Gamma$.

That's not at all obvious. But it's obvious that $\Gamma\vdash\phi$ implies $F\vdash\phi$ for some finite $F\subset\Gamma$, just because a proof of $\phi$ from $\Gamma$ has only finitely many steps, hence invokes only finitely many elements of $\Gamma$.

Answer 7

Here are two more reasons why syntactic proofs are interesting. (I figured I'd make this a separate post because it makes a completely different point than my other answer).

---

1. Syntactic proofs can help us capture better why, rather than just that, an argument is valid

While truth tables can tell us that a certain validity or entailment holds, they typically don't really tell us why. Sure, the entailment holds because the conclusion is true under all interpretations under which all the premises are true, but why is that? Truth tables (or arguments about valuations) don't usually give much insight into the patterns that underly logical reasoning.

The calculus of natural deduction has its name because it is intended to formalize how mathematicians would reason naturally in informal proofs. If you already know all about natural deduction, you can skip the next paragraph.

---

For instance, consider the following entailment: $A \lor B, B \to C \vDash A \lor C$.

Naturally, we would carry out a proof by cases on the disjunction in the first premise. There are two cases to consider:

1. $A$ holds. Then surely, either $A$ or $C$ holds, i.e. $A \lor C$. We can express this step of reasoning with a bar from the assumption to the new observation:
   $\dfrac{A}{A \lor C}$
2. $B$ holds. By the second premise, we know that if $B$, then $C$. The combination of these two pieces of knowledge allows to conclude us that $C$:
   $\dfrac{B \quad B \to C}{C}$
   Analogous to above, we may conclude that either $A$ or $C$:
   $\dfrac{\dfrac{B \quad B \to C}{C}}{A \lor C}$

Now we proved that in both cases, $A \lor C$ follows. We don't know which of the disjuncts is true, but we know that at least one is, so we can conclude $A \lor C$ for sure. At this point, the actual truth values of each of the disjuncts no longer matter, so we can discharge the temporary assumptions $A$ and $B$, and the final conclusion only depends on the premises $A \lor B$ and $B \to C$. Puzzling the first premise and the two subproofs together, we get the following structure of the entire argument:

$\dfrac{A \lor B \quad \dfrac{A\hspace{-6pt}\times}{A \lor C} \quad \dfrac{\dfrac{B\hspace{-7.5pt}\times \quad B \to C}{C}}{A \lor C} } {A \lor C}$

---

And that's precisely what a tree-style natural deduction looks like. This presentation reveals several insights about the way reason logically:

• Arguments can be composed stepwise from elementary rules of reasoning.
• The structure of an argument can be thought of as a tree shape, where we dissect and reassemble assumptions to new formulas to eventually reach a single conclusion.
• We can make local assumptions, for example in a proof by cases, and, under some conditions, later resolve the dependency on the assumptions and discharge them.

All of this a simple truth table can not provide -- but this is precisely the kind of issues that are interesting: The task of logic is not primarily to exhaustively list the valid theorems, but rather to investigate the elementary building blocks and structural properties of logical arguments.

---

While natural deduction is particularly suited to mimic the structure of intuitive reasoning, other syntactic calculi have their merits as well.

The tableau calculus may look like not more than a fancy truth table at first sight, but what makes it interesting is the ability to directly construct a (counter) model from an open branch. That way, we are provided with a formal means to analyze what structures make a particular formula satisfiable or invalid. This works even for predicate logic, where truth tables don't exist.

Sequent calculus provides a new perspective because it essentially makes inferences about inferences: The sequent rules express from which derivability claim we may infer another one.

And last but not least, syntactic proof systems are interesting on their own -- this is what proof theory studies. There are entire books out there just about natural deduction because there is a lot to say about the properties of proofs as mathematical objects, normalization being one important keyword.

---

2. Syntactic proof systems can be taught to computers

When talking about tableaus, it shouldn't be left unmentioned that they are a completely algorithmic, deterministic procedure and thus very straightforward to implement, thereby providing a computational mechanism for both theorem proving and model generation, at least in principle (though this procedure is among the quicker ones to blow up on larger formulas).

Among the tools employed in real-life computing, resolution and unificatoin are powerful procedures that can be expressed as a syntactic calculus.

Axiomatic systems in a Hilber-style manner due to their simplicity are particularly useful in carrying proofs about decidability and computability issues in theoretical computer science.

Truth tables may be straightforward to implement, but end at propositional logic, which is not very useful for many real-life problems, and that's where syntactic calculi come in handy.

The possibility to treat predicate logic with computers of course has its own perks. You can do theorem proving to verify mathematical arguments, software verification, SAT solving for configuration checkers, ..., and of course, again, the ifs and hows of doing mathematics with computers is interesting in itself for mathematics and theoretical computer science.