Soundness and Completeness: Bridging Model and Proof

Two Conceptions of Consequence

Let's formalise the two notions of consequence that Hamkins introduced. Given a set of premises $T$ and a conclusion $\varphi$:

• Model-Theoretic Consequence ($T\models \varphi$): We say $\varphi$ is a model-theoretic consequence of $T$ if and only if every model that makes all sentences in $T$ true also makes $\varphi$ true. This is a semantic notion. It's about truth preservation across all relevant "possible worlds" or interpretations. It corresponds to the idea of a necessary connection between premises and conclusion.

• Proof-Theoretic Consequence ($T⊢\varphi$): We say $\varphi$ is a proof-theoretic consequence of $T$ if and only if there is a formal proof (a finite sequence of formulas) of $\varphi$ starting from the premises in $T$ and the axioms of our logical system, using only the allowed rules of inference. This is a syntactic notion. It's about formal derivability. It corresponds to the idea of a justified or demonstrable connection.

The crucial philosophical question is: what is the relationship between $\models$ and $⊢$? Do our formal proof systems correctly capture the a-historical, abstract relation of necessary truth preservation?

The Bridge: Soundness and Completeness

Soundness and completeness theorems provide the answer for a given logical system. They act as a two-way bridge connecting the syntactic world of proofs with the semantic world of truth.

To understand what these theorems state and why they are so significant, we will return to the Hamkins video, which offers a particularly clear philosophical exposition.

Let's break down these two key properties.

Soundness: Proofs Don't Lie

A proof system is sound if, whenever you can prove $\varphi$ from $T$, it is also the case that $\varphi$ is a model-theoretic consequence of $T$.

Soundness guarantees that our proof system is truth-preserving. It cannot lead us from true premises to a false conclusion. As Hamkins notes, this is a basic "sanity check" for any proof system. If a system allows you to prove things that aren't actually valid, it's not a system of logic but a generator of fallacies. Proving soundness is typically straightforward: one just has to check that the axioms are valid and that each rule of inference preserves validity.

Completeness: All Truths Are Provable

A proof system is complete if, whenever $\varphi$ is a model-theoretic consequence of $T$, you can also prove $\varphi$ from $T$.

Completeness is, as Hamkins puts it, "incredible". It guarantees that our proof system is strong enough to capture every valid argument. It states that for every abstract semantic validity, which involves a truth-preserving relationship across an infinity of potential models, there exists a corresponding finite, concrete, syntactic object: a proof.

This provides a profound philosophical reassurance: if an argument is valid, its validity is not some ineffable mystery. It is demonstrable. In Hamkins's words, "everything that's true is true for a reason—namely, the proof."

When a logic has a sound and complete proof system (as first-order logic does), the two notions of consequence coincide:

This means that derivability and validity are extensionally equivalent. They are two different ways of characterising the very same relation.

Philosophical Significance and Deeper Analysis

The fact that for first-order logic, $⊢$ and $\models$ coincide is one of the most important metatheoretical results in modern logic. Its philosophical significance is immense.

1. Unifying Rival Philosophies of Logic

As we've discussed, the proof-theoretic and model-theoretic accounts are backed by different philosophical perspectives.

• The proof-centered approach highlights the epistemic aspects of logic. A proof provides justification and understanding. This view is often favoured by anti-realists, who are skeptical of abstract entities like models and want to ground meaning in knowable, verifiable procedures.
• The model-centered approach is closer to a realist or Platonist perspective. It defines consequence in terms of truth in abstract mathematical structures, independent of our ability to know or prove it.

The soundness and completeness theorems show that, at least for first-order logic, these two rival perspectives are not in conflict. They perfectly align. The class of arguments whose conclusions can be formally derived is exactly the same as the class of arguments whose conclusions are necessarily true if their premises are.

2. The Compactness Theorem

One of the most powerful consequences of the completeness theorem is the Compactness Theorem for first-order logic. As Hamkins explained in the video, it states that if a sentence $\varphi$ is a logical consequence of an infinite set of premises $T$, then it must be a consequence of some finite subset of $T$.

The reasoning is elegant and highlights the syntax-semantics bridge:

1. Assume $T\models \varphi$.
2. By the completeness theorem, it follows that $T⊢\varphi$.
3. By the definition of a proof, any proof is a finite object and can therefore only use a finite number of premises from $T$. Let this finite subset be $T_0$. So, we have $T_0⊢\varphi$.
4. By the soundness theorem, it follows that $T_0\models \varphi$.

This is a profound result about the semantic world (about models and truth) that is derived almost trivially by taking a detour through the syntactic world of finite proofs.

3. Justifying Model Theory: Kreisel's Squeezing Argument

One worry about model theory is that it is based in set theory. All models are sets. But what if the "real world" or some other relevant domain isn't a set (e.g., the collection of all sets is a proper class, not a set)? If so, model-theoretic validity ($\models$) might not correctly capture intuitive validity.

Georg Kreisel devised a "squeezing argument" that uses the completeness theorem to show that, for first-order logic, this worry is unfounded. The argument, which you just read about in the SEP article, goes like this:

Let's denote:

• $D$: the set of deductively valid arguments (those with a proof).
• $V$: the set of model-theoretically valid arguments (true in all set-based models).
• $Val$: the set of intuitively valid arguments (true in all possible structures, whether sets or not).

We can establish three relationships:

1. $D\subseteq Val$: Our proof system is intuitively sound. A proof provides an undeniable justification.
2. $Val\subseteq V$: Any argument that holds in all possible structures must, in particular, hold in all set-based structures (since sets are just one type of structure).
3. $V\subseteq D$: This is the completeness theorem.

Putting these together, we have $D\subseteq Val\subseteq V\subseteq D$. This forces all three sets to be identical: $D=Val=V$. Therefore, the standard set-theoretic definition of logical consequence perfectly captures the intuitive notion of validity for first-order logic.

4. The Limits of Equivalence: Tarski's Argument

Despite this beautiful equivalence, is it the whole story? Alfred Tarski argued that the model-theoretic account is ultimately more fundamental. His argument hinges on the fact that some intuitively correct patterns of inference cannot be captured by any standard, finitary proof system.

Tarski's point is that our intuitive notion of consequence is not necessarily compact. The $\omega$-rule is a prime example: from the infinite set of premises $\{P(0),P(1),P(2),\dots \}$, we intuitively want to conclude $\forall n:P(n)$, provided we also know that $0,1,2,\dots$ are all the numbers there are.

• This inference is semantically valid in the intended model of arithmetic.
• However, it cannot be captured by a standard proof system, because any proof can only use a finite number of premises. No finite subset of $\{P(0),P(1),P(2),\dots \}$ entails $\forall n:P(n)$.

Tarski argued that this shows the superiority of the model-theoretic account, which can easily handle such infinitary consequences, over any proof-theoretic account based on finite derivations. This reveals a lasting tension, suggesting that while $⊢$ and $\models$ are equivalent for first-order logic, the semantic notion $\models$ may have a claim to being more general and fundamental.

Conclusion

Today we have analysed the relationship between the two great traditions in logic—the proof-theoretic and the model-theoretic—by examining the theorems that connect them.

Key Takeaways:

• Two Worlds: Logical consequence can be understood syntactically ($T⊢\varphi$, provability) or semantically ($T\models \varphi$, truth-preservation).
• The Bridge: For first-order logic, soundness and completeness theorems establish that these two notions are extensionally equivalent.
  • Soundness ($⊢⟹\models$) guarantees that our proof methods are truthful.
  • Completeness ($\models ⟹⊢$) guarantees that our proof methods are powerful enough to capture all validities.
• Philosophical Significance: This equivalence is not merely a technical result.
  • It reconciles rival philosophical accounts of logic (epistemic/anti-realist vs. metaphysical/realist).
  • It yields powerful semantic tools like the Compactness Theorem from syntactic considerations.
  • It can be used to justify the adequacy of set-theoretic model theory for capturing intuitive validity via Kreisel's squeezing argument.
• Persistent Tension: The alignment is not perfect. Tarski's argument concerning non-compact inferences like the $\omega$-rule suggests that the semantic conception of consequence might be the more fundamental one. Furthermore, this perfect alignment breaks down for more expressive systems like second-order logic, which are sound but not complete, raising deep questions about their status as 'logic'.

Preview of the Next Lesson:

Our entire discussion today has been situated within the framework of classical logic, which assumes a realist conception of truth. The law of the excluded middle—that every proposition is either true or false—is a cornerstone of this framework. But what if we challenge this from the outset?

In our next lesson, we will begin our study of intuitionism. We will analyse Brouwer's philosophical case against the law of excluded middle, which is based on a radically different, constructive view of mathematical truth. This will lead us to a logic where truth is identified not with correspondence to reality, but with the existence of a proof, shifting the foundations of logic squarely into the proof-theoretic camp.