Section 07: Proof-theoretic concepts

Last updated
Save as PDF

Page ID: 31341

\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \) \( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)\(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\) \(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\)\(\newcommand{\AA}{\unicode[.8,0]{x212B}}\)

We will use the symbol ‘⊢’ to indicate that a proof is possible. This symbol is called the turnstile. Sometimes it is called a single turnstile, to underscore the fact that this is not the double turnstile symbol (⊨) that we used to represent semantic entailment in ch. 5.

When we write {\(\mathcal{A}\)₁,\(\mathcal{A}\)₂,...}⊢\(\mathcal{B}\), this means that it is possible to give a proof of \(\mathcal{B}\) with \(\mathcal{A}\)₁,\(\mathcal{A}\)₂,... as premises. With just one premise, we leave out the curly braces, so \(\mathcal{A}\) ⊢ \(\mathcal{B}\) means that there is a proof of \(\mathcal{B}\) with \(\mathcal{A}\) as a premise. Naturally, `\(\mathcal{C}\) means that there is a proof of \(\mathcal{C}\) that has no premises.

Often, logical proofs are called derivations. So \(\mathcal{A}\) ⊢ \(\mathcal{B}\) can be read as ‘\(\mathcal{B}\) is derivable from \(\mathcal{A}\).’

A theorem is a sentence that is derivable without any premises; i.e., \(\mathcal{T}\) is a theorem if and only if ⊢\(\mathcal{T}\).

It is not too hard to show that something is a theorem— you just have to give a proof of it. How could you show that something is not a theorem? If its negation is a theorem, then you could provide a proof. For example, it is easy to prove¬(\(Pa\)&¬\(Pa\)), which shows that (\(Pa\)&¬\(Pa\)) cannot be a theorem. For a sentence that is neither a theorem nor the negation of a theorem, however, there is no easy way to show this. You would have to demonstrate not just that certain proof strategies fail, but that no proof is possible. Even if you fail in trying to prove a sentence in a thousand different ways, perhaps the proof is just too long and complex for you to make out.

Two sentences \(\mathcal{A}\) and \(\mathcal{B}\) are provably equivalent if and only if each can be derived from the other; i.e., \(\mathcal{A}\)⊢\(\mathcal{B}\) and \(\mathcal{B}\)⊢\(\mathcal{A}\)

It is relatively easy to show that two sentences are provably equivalent— it just requires a pair of proofs. Showing that sentences are not provably equivalent would be much harder. It would be just as hard as showing that a sentence is not a theorem. (In fact, these problems are interchangeable. Can you think of a sentence that would be a theorem if and only if \(\mathcal{A}\) and \(\mathcal{B}\) were provably equivalent?)

The set of sentences {\(\mathcal{A}\)₁,\(\mathcal{A}\)₂,...} is provably inconsistent if and only if a contradiction is derivable from it; i.e., for some sentence \(\mathcal{B}\), {\(\mathcal{A}\)₁,\(\mathcal{A}\)₂,...} ⊢ \(\mathcal{B}\) and {\(\mathcal{A}\)₁,\(\mathcal{A}\)₂,...}⊢¬\(\mathcal{B}\).

It is easy to show that a set is provably inconsistent: You just need to assume the sentences in the set and prove a contradiction. Showing that a set is not provably inconsistent will be much harder. It would require more than just providing a proof or two; it would require showing that proofs of a certain kind are impossible.