Model-Theoretic vs. Proof-Theoretic Consequence

1. The Core Distinction: Syntax vs. Semantics

At the heart of the distinction between proof theory and model theory is a more fundamental one: the distinction between syntax and semantics.

• Syntax refers to the formal properties of a language: its symbols, grammar, and the rules for manipulating those symbols. It is concerned with the form of expressions, not their meaning.
• Semantics refers to the meaning of those expressions and the truth of statements. It connects the language to the world or to abstract structures.

In logic, this plays out as a distinction between what is provable (a syntactic notion) and what is true (a semantic notion).

To get a clear overview of this crucial dichotomy, please watch the first few minutes of the following video by mathematician and philosopher Joel David Hamkins. He provides an excellent chart that contrasts syntactic and semantic concepts.

As the video illustrates, we have two parallel worlds of concepts. The question of logical consequence can be asked in either world.

Let's now explore each of these conceptions in more detail.

2. The Model-Theoretic Conception: Consequence as Truth-Preservation

The model-theoretic account defines logical consequence in terms of truth. It aims to formalize the intuitive idea that a valid argument is one where it's impossible for the premises to be true and the conclusion false. The key innovation is to define "impossible" as "true in no model".

A model is a mathematical structure that provides a specific interpretation of the non-logical terms of our language. For a standard first-order language, a model consists of a domain of objects and an interpretation function that assigns members of the domain to constants, relations on the domain to predicates, and so on.

Logical consequence ($\models$) is then defined as follows:
A conclusion $\varphi$ is a model-theoretic consequence of a set of premises $\Gamma$ (written $\Gamma \models \varphi$) if and only if there is no model in which every sentence in $\Gamma$ is true and $\varphi$ is false.

In short: truth is preserved from premises to conclusion across all possible interpretations.

To deepen your understanding of this approach, please read the following section from the Stanford Encyclopedia of Philosophy.

The model-theoretic view has a strong philosophical appeal. It aligns with a realist conception of truth, where the truth of a statement depends on how things are in some reality (represented by the model), independent of our knowledge or ability to prove it.

3. The Proof-Theoretic Conception: Consequence as Derivability

The proof-theoretic account takes a different starting point. Instead of talking about truth and models, it focuses on the formal process of deduction. It captures the idea that a valid argument is one where the conclusion can be reached from the premises through a series of small, self-evidently correct steps.

A deductive system consists of a set of axioms (starting formulas) and rules of inference (rules for deriving new formulas from old ones, like Modus Ponens). A proof (or derivation) is a finite sequence of formulas, where each formula is either a premise, an axiom, or follows from previous formulas by a rule of inference.

Logical consequence ($⊢$) is then defined as follows:
A conclusion $\varphi$ is a proof-theoretic consequence of a set of premises $\Gamma$ (written $\Gamma ⊢\varphi$) if and only if there is a proof of $\varphi$ starting from the premises in $\Gamma$.

In short: the conclusion is formally derivable from the premises.

Now, please read the next section of the same encyclopedia entry.

As the text suggests, the proof-theoretic view is often favored by philosophical anti-realists or constructivists. From this perspective, the meaning of logical connectives isn't given by truth tables (which refer to an external reality), but by their rules of use in proofs (e.g., introduction and elimination rules). A statement is "true" just in case it is provable.

4. Bridging the Gap: Soundness and Completeness

We now have two distinct, rigorously defined notions of logical consequence: $\models$ and $⊢$. One is semantic, about truth in models; the other is syntactic, about formal proofs. The central question of metatheory is: how do they relate?

The answer lies in two of the most important theorems in modern logic.

• A proof system is sound if whatever is provable is also a model-theoretic consequence.
  $\text{If }\Gamma ⊢\varphi ,\text{ then }\Gamma \models \varphi .$
  Soundness means our proof system is reliable; it won't lead us from truth to falsehood. It only proves valid arguments.

• A proof system is complete if whatever is a model-theoretic consequence is also provable.
  $\text{If }\Gamma \models \varphi ,\text{ then }\Gamma ⊢\varphi .$
  Completeness means our proof system is powerful enough; it can prove every valid argument.

For first-order logic, Kurt Gödel proved in 1929 that there are deductive systems that are both sound and complete.
Gödel's Completeness Theorem: For first-order logic, $\Gamma ⊢\varphi$ if and only if $\Gamma \models \varphi$.

This is a profound result. It shows that the syntactic notion of formal proof perfectly captures the semantic notion of truth-preservation across all models. The two different worlds—syntax and semantics—are perfectly aligned.

Let's return to the Hamkins video to explore the significance of these properties.

The philosophical upshot of soundness and completeness is immense. They show that for first-order logic, the two perspectives coincide in extension. However, it's crucial to remember that they remain conceptually distinct. One defines consequence via truth, the other via proof. As we will see later in the course, for other logics (like second-order logic), this perfect correspondence breaks down, and the choice between a proof-theoretic or model-theoretic account becomes a substantive philosophical decision.

Conclusion

This lesson concludes our initial survey of the philosopher's toolkit. We have distinguished between the two fundamental ways of understanding logical consequence, which will be a recurring theme throughout the rest of our course.

Key Takeaways:

• Model-theoretic consequence ($\models$) is a semantic notion defined as truth-preservation across all models. It formalizes the idea of "no counterexample" and aligns with a realist philosophy of truth.
• Proof-theoretic consequence ($⊢$) is a syntactic notion defined as derivability in a formal deductive system. It formalizes the idea of a step-by-step argument and aligns with an anti-realist or constructivist philosophy of meaning and justification.
• Soundness and Completeness theorems (for a given logic) establish the relationship between these two notions. For first-order logic, Gödel's completeness theorem shows they are equivalent ($⊢⟺\models$), a powerful result that bridges the syntactic and semantic worlds.

Preview of the Next Lesson:

Having assembled our conceptual toolkit, we are now ready to begin our historical journey. We will start with the figure who looms large over modern philosophy: Immanuel Kant. In the next lesson, we will explore Kant's view of logic as a completed, formal science and his famous distinction between analytic and synthetic judgments. This will provide the crucial philosophical backdrop against which the logical revolutions of Boole and Frege took place.