Chapter 20 Proof-theoretic concepts

In this chapter we will introduce some new vocabulary. The following expression:

\mathscr{A}_{1},\mathscr{A}_{2},\ldots,\mathscr{A}_{n}\vdash\mathscr{C}

means that there is some proof which ends with $\mathscr{C}$ whose undischarged assumptions are among $\mathscr{A}_{1},\mathscr{A}_{2},\ldots,\mathscr{A}_{n}$ . When we want to say that it is not the case that there is some proof which ends with $\mathscr{C}$ from $\mathscr{A}_{1}$ , $\mathscr{A}_{2}$ , …, $\mathscr{A}_{n}$ , we write:

\mathscr{A}_{1},\mathscr{A}_{2},\ldots,\mathscr{A}_{n}\nvdash\mathscr{C}

The symbol ‘ $\vdash$ ’ is called the single turnstile. We want to emphasize that this is not the double turnstile symbol (‘ $\vDash$ ’) that we introduced in chapter 12 to symbolize entailment. The single turnstile, ‘ $\vdash$ ’, concerns the existence of proofs; the double turnstile, ‘ $\vDash$ ’, concerns the existence of valuations (or interpretations, when used for FOL). They are very different notions.

Armed with our ‘ $\vdash$ ’ symbol, we can introduce some more terminology. To say that there is a proof of $\mathscr{A}$ with no undischarged assumptions, we write: ${}\vdash\mathscr{A}$ . In this case, we say that $\mathscr{A}$ is a theorem .

$\mathscr{A}$ is a theorem if⁠f $\vdash\mathscr{A}$

To illustrate this, suppose we want to show that ‘ $\neg(A\wedge\neg A)$ ’ is a theorem. So we need a proof of ‘ $\neg(A\wedge\neg A)$ ’ which has no undischarged assumptions. However, since we want to prove a sentence whose main logical operator is a negation, we will want to start with a subproof within which we assume ‘ $A\wedge\neg A$ ’, and show that this assumption leads to contradiction. All told, then, the proof looks like this:

Line number	Subproof level	Formula	Justification
$1$	open subproof, 1	$A\wedge\neg A$	AS
$2$	1	$A$	$\wedge$ E $1$
$3$	1	$\neg A$	$\wedge$ E $1$
$4$	1	$\bot$	$\neg$ E $3$ , $2$
$5$	close subproof, 0	$\neg(A\wedge\neg A)$	$\neg$ I $1$ – $4$

We have therefore proved ‘ $\neg(A\wedge\neg A)$ ’ on no (undischarged) assumptions. This particular theorem is an instance of what is sometimes called the Law of Non-Contradiction.

To show that something is a theorem, you just have to find a suitable proof. It is typically much harder to show that something is not a theorem. To do 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. Perhaps you just didn’t try hard enough.

Here is another new bit of terminology:

Two sentences $\mathscr{A}$ and $\mathscr{B}$ are provably equivalent if⁠f each can be proved from the other; i.e., both $\mathscr{A}\vdash\mathscr{B}$ and $\mathscr{B}\vdash\mathscr{A}$ .

As in the case of showing that a sentence is a theorem, 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 is just as hard as showing that a sentence is not a theorem.

Here is a third, related, bit of terminology:

The sentences $\mathscr{A}_{1},\mathscr{A}_{2},\ldots,\mathscr{A}_{n}$ are jointly inconsistent if⁠f the contradiction $\bot$ can be proved from them, i.e., $\mathscr{A}_{1},\mathscr{A}_{2},\ldots,\mathscr{A}_{n}\vdash\bot$ . If they are not inconsistent , we call them jointly consistent .

It is easy to show that some sentences are inconsistent: you just need to prove the contradiction $\bot$ , assuming all the sentences as premises. Showing that some sentences are not inconsistent is much harder. It would require more than just providing a proof or two; it would require showing that no proof of a certain kind is possible.

This table summarizes whether one or two proofs suffice, or whether we must reason about all possible proofs.

	Yes	No
theorem?	one proof	all possible proofs
inconsistent?	one proof	all possible proofs
equivalent?	two proofs	all possible proofs
consistent?	all possible proofs	one proof

Practice exercises

A. Show that each of the following sentences is a theorem:

1.

$O\rightarrow O$
2.

$N\vee\neg N$
3.

$J\leftrightarrow[J\vee(L\wedge\neg L)]$
4.

$((A\rightarrow B)\rightarrow A)\rightarrow A$

B. Provide proofs to show each of the following:

1.

$C\rightarrow(E\wedge G),\neg C\rightarrow G\vdash G$
2.

$M\wedge(\neg N\rightarrow\neg M)\vdash(N\wedge M)\vee\neg M$
3.

$(Z\wedge K)\leftrightarrow(Y\wedge M),D\wedge(D\rightarrow M)\vdash Y\rightarrow Z$
4.

$(W\vee X)\vee(Y\vee Z),X\rightarrow Y,\neg Z\vdash W\vee Y$

C. Show that each of the following pairs of sentences are provably equivalent:

1.

$R\leftrightarrow E$ , $E\leftrightarrow R$
2.

$G$ , $\neg\neg\neg\neg G$
3.

$T\rightarrow S$ , $\neg S\rightarrow\neg T$
4.

$U\rightarrow I$ , $\neg(U\wedge\neg I)$
5.

$\neg(C\rightarrow D),C\wedge\neg D$
6.

$\neg G\leftrightarrow H$ , $\neg(G\leftrightarrow H)$

D. If you know that $\mathscr{A}\vdash\mathscr{B}$ , what can you say about $(\mathscr{A}\wedge\mathscr{C})\vdash\mathscr{B}$ ? What about $(\mathscr{A}\vee\mathscr{C})\vdash\mathscr{B}$ ? Explain your answers.

E. In this chapter, we claimed that it is just as hard to show that two sentences are not provably equivalent, as it is to show that a sentence is not a theorem. Why did we claim this? (Hint: think of a sentence that would be a theorem if⁠f $\mathscr{A}$ and $\mathscr{B}$ were provably equivalent.)