Chapter 41 Proofs and semantics

We have used two different turnstiles in this book. This:

means that there is some proof which ends with $𝒞$ and whose only undischarged assumptions are among ${𝒜}_1,{𝒜}_2,\mathrm{\dots },{𝒜}_n$. This is a proof-theoretic notion. By contrast, this:

means that no valuation (or interpretation) makes all of ${𝒜}_1,{𝒜}_2,\mathrm{\dots },{𝒜}_n$ true and $𝒞$ false. This concerns assignments of truth and falsity to sentences. It is a semantic notion.

It cannot be emphasized enough that these are different notions. But we can emphasize it a bit more: They are different notions.

Once you have internalised this point, continue reading.

Although our semantic and proof-theoretic notions are different, there is a deep connection between them. To explain this connection,we will start by considering the relationship between validities and theorems.

To show that a sentence is a theorem, you need only produce a proof. Granted, it may be hard to produce a twenty line proof, but it is not so hard to check each line of the proof and confirm that it is legitimate; and if each line of the proof individually is legitimate, then the whole proof is legitimate. Showing that a sentence is a validity, though, requires reasoning about all possible interpretations. Given a choice between showing that a sentence is a theorem and showing that it is a validity, it would be easier to show that it is a theorem.

Contrawise, to show that a sentence is not a theorem is hard. We would need to reason about all (possible) proofs. That is very difficult. However, to show that a sentence is not a validity, you need only construct an interpretation in which the sentence is false. Granted, it may be hard to come up with the interpretation; but once you have done so, it is relatively straightforward to check what truth value it assigns to a sentence. Given a choice between showing that a sentence is not a theorem and showing that it is not a validity, it would be easier to show that it is not a validity.

Fortunately, a sentence is a theorem if and only if it is a validity. As a result, if we provide a proof of $𝒜$ on no assumptions, and thus show that $𝒜$ is a theorem, i.e., $⊢𝒜$, we can legitimately infer that $𝒜$ is a validity, i.e., $\models 𝒜$. Similarly, if we construct an interpretation in which $𝒜$ is false and thus show that it is not a validity, i.e., $⊭𝒜$, it follows that $𝒜$ is not a theorem, i.e., $⊬𝒜$.

More generally, we have the following powerful result:

This shows that, whilst provability and entailment are different notions, they are extensionally equivalent. As such:

For this reason, you can pick and choose when to think in terms of proofs and when to think in terms of valuations/interpretations, doing whichever is easier for a given task. The table on the next page summarizes which is (usually) easier.

It is intuitive that provability and semantic entailment should agree. But—let us repeat this—do not be fooled by the similarity of the symbols ‘$\models$’ and ‘$⊢$’. These two symbols have very different meanings. The fact that provability and semantic entailment agree is not an easy result to come by.

In fact, demonstrating that provability and semantic entailment agree is, very decisively, the point at which introductory logic becomes intermediate logic.