Propositional calculus

Propositional calculus#

\(\newcommand{\vd}{\vdash}\) \(\newcommand{\dvd}{\models}\) \(\newcommand{\imp}{\Rightarrow}\)

First, we define propositions. A primitive proposition should be regarded simply as a symbol, e.g. \(p, q\) or \(r,\) which can be combined with other symbols using a special \(\imp\) symbol, to obtain new composite propositions.

Definition 113 (Proposition)

Let \(P\) be a set of primitive propositions, (e.g. \(p, q, r\)). The set of propositions, written as \(L\) or \(L(P)\) is defined inductively by

If \(p \in P,\) then \(p \in L.\)
\(\perp \in L,\) where \(\perp\) is a proposition read as “false.”
If \(p, q \in L,\) then \((p \imp q) \in L.\)

Equivalently, if \(P\) is a primitive set of propositions, then

\[\begin{split}\begin{align} L_0 &= \{\perp\} \cup P \\ L_{n+1} &= L_n \cup \{(p \imp q): p, q \in L_n\} \end{align}\end{split}\]

and \(L = L_0 \cup L_1 \cup L_2 \cup \dots.\)

We now define logical symbols, which should be understood as shorthand for particular propositions that are written in terms of the \(\perp\) and \(\imp\) symbols.

Definition 114 (Logical symbols)

We define the symbols \(\neg, \wedge, \vee\) as

\[\begin{split}\begin{align} \neg p &= p \imp \perp \\ p \wedge q &= \neg (p \imp \neg q) \\ p \vee q &= (\neg p) \imp q \\ \end{align}\end{split}\]

where \(p, q \in L.\)

Semantic entailment#

By themselves, propositions are meaningless. Semantic entailment assigns truth values to propositions, where we declare each proposition to either be “true” or “false” according to a valuation function.

Definition 115 (Valuation)

A valuation on \(L\) is a function \(v: L \to \{0, 1\},\) such that

\[\begin{split}\begin{equation} v(\perp) = 0,~~ v(p \imp q) = \begin{cases} 0 & \text{ if } v(p) = 1, v(q) = 0, \\ 1 & \text{ otherwise }. \\ \end{cases} \end{equation}\end{split}\]

We interpret \(v(p)\) to be the truth value of \(p,\) with \(0\) and \(1\) denoting “false” and “true” respectively. A valuation is uniquely determined by the value it takes on the primitive propositions, since all other propositions in the language are constructed from the primitive ones. In addition, given the values of a valuation function on the primitive propositions, we can extend this to a (unique) valuation on the entire language.

Lemma 47 (Equivalent valuations and extension to valuation)

Suppose \(P\) is a set of primitive propositions, and \(L\) is the set of propositions derived from it. Then

If \(v\) and \(v'\) are valuations with \(v(p) = v'(p)\) for all \(p \in P,\) then \(v = v'.\)
For any function \(w: P \to \{0, 1\},\) we can extend it to a valuation \(v: L \to \{0, 1\}\) such that \(v(p) = w(p)\) for all \(p \in P.\)

We now define the notion of tautology, i.e. a proposition that is true under all possible valuations on the primitive propositions.

Definition 116 (Tautology)

We say \(t\) is a tautology, written \(\models t,\) if \(v(t) = 1\) for any valuation \(v: L \to \{0, 1\}.\)

To show that a statement is a tautology, we can use a truth table, which is a big table that summarises the value that a valuation function takes on each proposition for each inductive step. We can write out all possible starting combinations of truth values on \(P,\) and the resulting propositions in \(L,\) until we determine the value of the proposition we are after. If the value of this proposition is true for any starting combination of truth values of \(P,\) then it is a tautology.

We can now define semantic entailment. Informally a set of propositions \(S\) (the assumptions) entails a proposition \(t\) if for any valuation that is true on the assumptions is also true on \(t.\)

Definition 117 (Semantic entailment)

For \(S \subseteq L, t \in L\) we say \(S\) entails \(t,\) \(S\) semantically implies \(t\) or \(S \models t,\) if for any \(v\) such that \(v(s) = 1\) for all \(s \in S,\) we have \(v(t) = 1.\)

We define truth of a proposition under a valuation function, in terms of the value that this takes on the proposition.

Definition 118 (Truth and model)

If \(v(t) = 1,\) then we say that \(t\) is true in \(v,\) or \(v\) is a model of \(t.\) For \(S \subseteq L,\) a valuation \(v\) is a model of \(S\) if \(v(s) = 1\) for all \(s \in S.\)

Syntactic implication#

The second notion we study is syntactic valuation. While semantic implication captures the idea of truthfulness, syntactic implication captures the idea of a proof. We will set up our definitions so that a set of propositions \(S\) (the assumptions) syntactically implies a proposition \(t\) if there is a proof of \(t\) from \(S.\) We have not yet defined a notion of proof though. A proof will turn out to be a finite sequence of propositions with some particular requirements. Before defining proofs we define the proof axioms and the modus ponens rule.

Definition 119 (Proof axioms and modus ponens)

We define the following three proof axioms

\(p \imp (q \imp p),\)
\((p \imp (q \imp r)) \imp ((p \imp q) \imp (p \imp r)),\)
\((\neg \neg p) \imp p.\)

We define the deduction rule of modus ponens as: from \(p\) and \(p \imp q\) we can deduce \(q.\)

We can now define proofs and syntactic entailment.

Definition 120 (Proof and syntactic entailment)

For any \(S \subseteq L,\) a proof of \(t\) from \(S\) is a finite sequence \(t_1, t_2, \dots, t_n\) of propositions, with \(t_n = t,\) such that each \(t_i\) is one of the following:

An axiom;
A member of \(S\);
A proposition \(t_i\) such that there exist \(j, k < i\) with \(t_j\) being \(t_k \imp t_i.\)

If there is a proof of \(t\) from \(S,\) we say that \(S\) proves, or syntactically entails \(t,\) written \(S \vdash t.\) If \(\emptyset \vdash t,\) we say \(t\) is a theorem and write \(\vdash t.\) In a proof of \(t\) from \(S,\) \(t\) is the conclusion and \(S\) is the set of hypothesis or premises.

Example 15 (\(p \imp p\) is a theorem)

We have that \(\vd p \imp p,\) that is, \(p \imp p\) is a theorem.

Generally, writing proofs as that in Example 15 can get cumbersome. The following theorem can help a lot to shorten our informal proofs.

Theorem 102 (Deduction theorem)

Let \(S \subseteq L\) and \(p, q \in L.\) Then \(S \vdash (p \imp q)\) if and only if \(S \cup \{p\} \vdash q.\)

Completeness#

Here we show one of the main results of this section. We will show that semantic entailment is equivalent to syntactic entailment. In other words, a proposition is semantically entailed by a set of assumptions if and only if it can be proved from those assumptions. We will break down this proof into two parts: the soundness theorem and the adequacy theorem.

Soundness#

The soundness theorem shows that syntactic entailment implies semantic entailment. It is called the soundness theorem because it demonstrates that our proof axioms are sound: if a of a proposition exists, then this proposition is true under our notion of semantic entailment. In other words, we can prove only those propositions that are true.

Theorem 103 (Soundness theorem)

If \(S \vd t,\) then \(S \dvd t.\)

Adequacy#

The second part of the completeness theorem is the adequacy, which shows that semantic implication implies syntactic implication. It is called the adequacy theorem because it shows that our definition of is adequate for capturing all logical truths in the system: if a proposition is true, then there exists a (formal) proof for it, so our definition of proof is adequate for proving all logical truths.

This is a bit more involved than the soundness theorem. We break this down into intermediate results. First, we define consistent propositions.

Definition 121 (Consistent)

A set of propositions \(S \subseteq L\) is inconsistent if \(S \vd \perp.\) S is consistent if it is not inconsistent.

Next, we show the following useful lemma. Given a set of consistent assumptions and a new proposition \(p,\) then at least one of \(p\) and \(\neg p\) can be added to the propositions while preserving consistency.

Lemma 48 (Consistent assumptions can be extended)

For consistent \(S \subseteq L\) and \(p \in L,\) at least one of \(S \cup \{p\}\) and \(S \cup \{\neg p\}\) is consistent.

Now we show the main intermediate result for proving adequacy. If a set of assumptions is consistent, then it has a model. Equivalently, if it does not have a model, then it is inconsistent.

Theorem 104 (Model existence)

Let \(L\) be a countable set of propositions. If \(S \dvd \perp,\) then \(S \vd \perp.\) In other words, if \(S\) has no model, then \(S\) is inconsistent. Equivalently, if \(S\) is consistent, then \(S\) has a model.

Proof: Model existence

Assume \(L\) is countable and list it as \(\{t_1, t_2, \dots\}.\) Let \(S \subseteq L\) be consistent and define \(S_0 = S.\) Then by Lemma 48, at least one of \(S \cup \{t_1\}\) and \(S \cup \{\neg t_1\}\) is consistent. Define \(S_1\) to be the consistent one. Then, let \(S_2\) be \(S_1 \cup \{t_2\}\) or \(S_1 \cup \{\neg t_2\},\) such that \(S_2\) is consistent, and continue inductively.

Set \(\bar{S} = S_0 \cup S_1 \cup \dots.\) Then \(p \in \bar{S}\) or \(\neg p \in \bar{S}\) for each \(p \in L\) by construction. Also, we know that \(\bar{S}\) is consistent: if \(\bar{S} \vd \perp,\) then since proofs are finite, there is some \(S_n\) that contains all the assumptions used in the proof of \(\bar{S} \vd \perp.\) Hence \(S_n \vd \perp,\) but we know that all \(S_n\) are consistent. Finally, we check that \(\bar{S}\) is deductively closed: if \(\bar{S} \vd \perp,\) we must have \(p \in \bar{S}\) because otherwise we would have \(\neg p \in \bar{S},\) which would be a contradiction.

Finally, we show that \(\bar{S}\) has a model. Define \(v: L \to \{0, 1\}\) by

\[\begin{split}\begin{equation} v(p) = \begin{cases} 1 & \text{ if } p \in \bar{S} \\ 0 & \text{ otherwise. } \end{cases} \end{equation}\end{split}\]

Since \(\bar{S}\) is deductively closed, we only need to show that \(v\) is indeed a valuation. By Definition 115, for \(v\) to be a valuation it needs to satisfy a condition on \(v(\perp)\) and a condition on \(v(p \imp q).\) First, we have \(v(\perp) = 0,\) since \(\perp \not \in \bar{S}\) because \(\bar{S}\) is consistent. Second, we check \(v(p \imp q)\) for each possible combination of values that \(v\) can take on \(p\) and \(q.\)

Case 1: Suppose \(v(p) = 0.\) Then by the definition of \(v,\) we have \(p \not \in \bar{S}\) and \(\neg p \in \bar{S}.\) We want to show that \(p \imp q \in \bar{S}.\)

Now, note that to show \(p \imp q \in \bar{S}\) it suffices to show \(\neg p \vd p \imp q.\) This is because if \(\neg p \vd p \imp q,\) then since \(\bar{S} \vd \neg p,\) we have \(\bar{S} \vd p \imp q.\) We can show this by noting that

\(\vd \perp \imp (\neg q \imp \perp)\) by axiom 1.
\(\vd \perp \imp (\neg \neg q)\) by the definition of negation.
\(\perp \vd \neg \neg q\) by the deduction theorem.
\(\{p, \neg p\} \vd \neg \neg q.\)
\(\{p, \neg p\} \vd q\) by axiom 3.
\(\neg p \vd p \imp q\) by the deduction theorem.

We conclude that \(\neg p \vd p \imp q,\) which implies \(\bar{S} \vd p \imp q,\) so \(p \imp q \in \bar{S}\) and \(v(p \imp q) = 1\) as required.

Case 2: Suppose \(v(p) = 1, v(q) = 0.\) Then, \(p \in \bar{S}, q \not \in \bar{S}.\) We want to show that \(p \imp q \not \in \bar{S}.\) Suppose instead that \(p \imp q \in \bar{S}.\) Then, \(\bar{S} \perp p \imp q\) and since \(p \in \bar{S},\) then by modus ponens we have \(\bar{S} \per q\) which means \(q \in \bar{S},\) which is a contradiction. Therefore \(p \imp q \not \in \bar{S}\) and \(v(p \imp q) = 0\) as required.

Case 3: Suppose \(v(p) = 1, v(q) = 1.\) Then, \(p \in \bar{S}, q \in \bar{S}.\) We want to show that \(p \imp q \in \bar{S}.\) By the axiom 1, we have \(\perp q \imp (p \imp q),\) and by the deduction theorem we have \(q \perp (p \imp q).\) Since \(\bar{S} \perp q,\) we have \(\bar{S} \perp (p \imp q),\) and since \(\bar{S}\) is deductively closed, we have \(p \imp q \in \bar{S}.\) We conclude that \(v(p \imp q) = 1\) as required.

This covers all possible cases for \(v\) on \(p\) and \(q,\) so we conclude \(v\) is a valuation on \(L\) such that \(v(s) = 1\) for all \(s \in \bar{S},\) so \(v\) is a model of \(\bar{S},\) and also of \(S.\) So \(S\) has a model.

We can now use the model existence theorem to prove the adequacy theorem.

Theorem 105 (Adequacy theorem)

Let \(S \subseteq L, t \in L.\) Then \(S \models t\) implies \(S \vd t.\)

Completeness and compactness#

We can now combine the soundness and adequacy theorems to prove the completness theorem.

Theorem 106 (Completeness theorem)

Let \(S \subseteq L\) and \(t \in L.\) Then \(S \models t\) if and only if \(S \vd t.\)

A useful corollary of the completeness theorem is the compactness theorem. This says that for any logical truth, there is a finite set of assumptions that proves it.

Theorem 107 (Compactness theorem)

Let \(S \subseteq L\) and \(t \in L\) with \(S \models t.\) Then, there is some finite \(S' \subseteq S\) with \(S' \models t.\)

Another useful corollary of the completeness theorem is the decidability theorem. This says that given a finite set of assumptions and a proposition, there exists a procedure that determines whether this statement can be proved from the assumptions, in finite time.

Theorem 108 (Decidability theorem)

Let \(S \subseteq L\) be a finite set and \(t \in L.\) Then, there exists an algorithm that determines, in finite and bounded time, whether or not \(S \vd t.\)