Logic MT24, Proofs in propositional logic

Here $\mathcal L _ 0 := \mathcal L _ \text{prop}(\lnot, \to)$.

Axioms: Any formula of the following form, where $\alpha, \beta, \gamma \in \text{Form}(\mathcal L _ 0)$:

• A1: $(\alpha \to (\beta \to \alpha))$ (“if A, then anything implies A”)
• A2: $((\alpha \to (\beta \to \gamma)) \to ((\alpha \to \beta) \to (\alpha \to \gamma)))$ (“if A shows that B implies C, then if A implies B, A also implies C”)
• A3: $((\lnot \alpha \to \beta) \to ((\lnot \alpha \to \lnot \beta) \to \alpha)))$ (“contradiction”)

Rules of inference:

• Modus ponens (MP): For any $\phi, \psi \in \text{Form}(\mathcal L _ 0)$, from $\phi$ and $(\phi \to \psi)$ infer $\psi$.

There is a sequence of $\mathcal L _ 0$ formulaus $\phi _ 1, \ldots, \phi _ n$ with $\phi _ n = \phi$ such that for each $i \le n$, at least one of the following holds:

• (A1-A3): $\phi _ i$ is an axiom
• (Hyp): $\phi _ i \in \Gamma$
• (MP): $\phi _ k = (\phi _ j \to \phi _ i)$ for some $j, k < i$

\[\emptyset \vdash \phi\]

so $\phi$ is a theorem of $L _ 0$, i.e. $\phi$ is provable from no hypotheses.

\[\vdash \phi\]

• $\mathcal L _ 0$ is $\text{Form}(\mathcal L [\lnot, \to])$
• $L _ 0$ is $\mathcal L _ 0$ with a proof system

$L _ 0$ is sound, i.e. suppose:

• $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$
• $\phi \in \text{Form}(\mathcal L _ 0)$
• $\Gamma \vdash \phi$

Then:

• $\Gamma \models \phi$.

We prove the following for all $m$:

If $\phi$ has a proof of length $m$ from $\Gamma$ in $L _ 0$, then $\Gamma \models \phi$. $(\star)$

Induct on $m$. In the base case, $m = 0$. This is immediate as no proof has length $0$.

In the inductive step, we can assume $m \ge 1$ and ($\star$) holds for all $m’ < m$. Suppose $\alpha _ 1, \ldots, \alpha _ m$ is a proof in $L _ 0$. We want to show that $\Gamma \models \alpha _ m$. There are several cases:

Case 1: $\alpha _ m$ is an axiom. By truth tables, the axioms are logically valid, so $\Gamma \models \alpha _ m$.

Case 2: $\alpha _ m \in \Gamma$. Then $\Gamma \models \alpha _ m$ is immediate.

Case 3: $\alpha _ m$ is obtained by MP. Hence $\exists i, j < m$ and $\alpha _ j = (\alpha _ i \to \alpha _ m)$. By the inductive hypothesis, since $\alpha _ i, \ldots, \alpha _ i$ is a proof of length $i < m$, we have $\Gamma \models \alpha _ i$. Similarly, $\Gamma \models \alpha _ j$, i.e. $\Gamma \models (\alpha _ i \to \alpha _ m)$.

Then by the lemma which says:

Suppose $\Gamma$ is a set of formulas and $\psi$, $\phi$ are formulas (not necessarily in $\Gamma$). Then:

\[\Gamma \cup \\{\psi\\} \models \phi \text{ iff } \Gamma \models (\psi \to \phi)\]

$\{\alpha _ i, (\alpha _ i \to \alpha _ m)\} \models \alpha _ m$. But then by the transitivity of “$\models$”, $\Gamma \models \alpha _ m$, as required.

Any theorem of $L _ 0$ is logically valid.

Suppose:

• $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$
• $\phi, \psi \in \text{Form}(\mathcal L _ 0)$

Then:

• If $\Gamma \cup \{\phi \} \vdash \psi$, then $\Gamma \vdash (\phi \to \psi)$

---

…or, equivalently the result could be stated as…

• $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$
• $\phi, \psi \in \text{Form}(\mathcal L _ 0)$
• $\Gamma \cup \{\phi \} \vdash \psi$

Then:

• $\Gamma \vdash (\phi \to \psi)$

We prove the family of statements

If $\psi$ has a proof of length $m$ from $\Gamma \cup \{\phi\}$ in $L _ 0$, then $\Gamma \vdash (\phi \to \psi)$. $(\star)$

Induct on $m$. Suppose that $\alpha _ 1, \ldots, \alpha _ m$ is a proof in $L _ 0$ from $\Gamma \cup \{\phi\}$. We want to show that $\Gamma \vdash (\phi \to \alpha _ m)$, assuming inductively that $\Gamma \vdash (\phi \to \alpha _ i)$ for all $i < m$. There are several cases:

Case 1: $\alpha _ m$ is an axiom. Then $\emptyset \vdash (\phi \to \alpha _ m)$ by the following proof:

1. Axiom: $\alpha _ m$
2. A1: $(\alpha _ m \to (\phi \to \alpha _ m))$
3. MP1, 2: $(\phi \to \alpha _ m)$

But as $\emptyset \subseteq \Gamma$, $\Gamma \vdash (\phi \to \alpha _ m)$.

Case 2: $\alpha _ m \in \Gamma \cup \{\phi\}$. If $\alpha _ m \in \Gamma$, then the proof in case 1 goes through almost exactly the same, except line 1 is a hypothesis rather than an axiom.

1. Hypothesis: $\alpha _ m$
2. A1: $(\alpha _ m \to (\phi \to \alpha _ m))$
3. MP1, 2: $(\phi \to \alpha _ m)$

If instead $\alpha _ m = \phi$, then we have to prove $(\phi \to \phi)$ in $\Gamma$. But this has a short proof:

1. $(\phi \to ((\phi \to \phi) \to \phi))$ (A1 with $\alpha = \phi, \beta = (\phi \to \phi)$)
2. $((\phi \to ((\phi \to \phi) \to \phi)) \to ((\phi \to (\phi \to \phi)) \to (\phi \to \phi)))$ (A2 with $\alpha = \phi, \beta = (\phi \to \phi), \gamma = \phi$)
3. $((\phi \to (\phi \to \phi)) \to (\phi \to \phi))$ (MP 2,1)
4. $(\phi \to (\phi \to \phi))$ (A1 with $\alpha, \beta = \phi$)
5. $(\phi \to \phi)$ (MP 4, 3)

Case 3: $\alpha _ m$ is obtained by MP for earlier $\alpha _ j, \alpha _ k$. So there are $j, k < m$ such that $\alpha _ j = (\alpha _ k \to \alpha _ m)$. By the inductive hypothesis:

• $\Gamma \vdash (\phi \to \alpha _ k)$
• $\Gamma \vdash (\phi \to \alpha _ j)$, i.e. $\Gamma \vdash (\phi \to (\alpha _ k \to \alpha _ m))$.

We can glue these two proofs together to form a proof for $\Gamma \vdash \alpha _ m$:

Suppose:

\[\beta_1, \ldots, \beta_{r-1}, (\phi \to \alpha_k)\]

is a length-$r$ proof of $\Gamma \vdash (\phi \to \alpha _ k)$ from $\Gamma$ and

\[\gamma_1, \ldots, \gamma_{s-1}, (\phi \to (\alpha_k \to \alpha_m))\]

is a length-$s$ proof of $\Gamma \vdash (\phi \to (\alpha _ k \to \alpha _ m))$ from $\Gamma$. But then:

\[\beta_1, \ldots, \beta_{r-1}, (\phi \to \alpha_k), \gamma_1, \ldots, \gamma_{s-1}, (\phi \to (\alpha_k \to \alpha_m))\]

followed by

\[\begin{aligned} &((\phi \to (\alpha_k \to \alpha_m)) \to ((\phi \to \alpha_k) \to (\phi \to \alpha_m))), \\\\ &((\phi \to \alpha_k) \to (\phi \to \alpha_m)), \\\\ &(\phi \to \alpha_m) \end{aligned}\]

is a proof of $(\phi \to \alpha _ m)$ in $L _ 0$ from $\Gamma$.

Let $\beta _ 1, \ldots, \beta _ {r-1}, (\phi \to \psi)$ be the proof of $(\phi \to \psi)$ from $\Gamma$. Then

\[\beta_1, \ldots, \beta_{r-1}, (\phi \to \psi), \phi, \psi\]

Gives $\Gamma \cup \phi \vdash \psi$, where MP is used in the last step.

@important~

• No, the deduction theorem only states that if $\Gamma \cup \{ \phi \} \vdash \psi$, then $\Gamma \vdash \phi \to \psi$.
• The converse is true also, but this is not part of the deduction theorem.

If $\Gamma \cup \{\lnot \phi\} \vdash \chi$ and $\Gamma \cup \{\lnot \phi\} \vdash \lnot \chi$, then $\Gamma \vdash \phi$.

@extra~

By the deduction theorem, we have that

• $\Gamma \vdash (\lnot \phi \to \chi)$, and
• $\Gamma \vdash (\lnot \phi \to \lnot \chi)$

But by A3 we have that

• $(\lnot \phi \to \chi) \to ((\lnot \phi \to \lnot \chi) \to \phi)$

Hence by two uses of MP, $\Gamma \vdash \phi$, as required.

@extra~

Suppose:

• $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$
• $\phi \in \text{Form}(\mathcal L _ 0)$
• $\Gamma \models \phi$

Then:

• $\Gamma \vdash \phi$

\[\Gamma \models \phi \text{ iff } \Gamma \vdash \phi\]

There exists $\chi \in \text{Form}(\mathcal L _ 0)$ such that

\[\Gamma \vdash \chi \text{ and } \Gamma \vdash \lnot \chi\]

• $\mathcal L _ 0$ is sound, so anything proved from $\emptyset$ must be a logical validity
• If $\mathcal L _ 0$ were inconsistent, it could prove $\chi$ and $\lnot \chi$ for some $\chi$
• But both of these would have to be logical validities, however no formula and it’s negation can be both logically valid
• Therefore $\emptyset$ is consistent

$\Gamma \vdash \phi$ implies $\Gamma \cup \{\lnot \phi\}$ inconsistent:

Suppose $\Gamma \cup \{\lnot \phi\}$ is inconsistent, so that

\[\Gamma \cup \\{\lnot \phi\\} \vdash \chi \text{ and } \Gamma \cup \\{\lnot \phi\\} \vdash \lnot \chi\]

for some $\chi$. But then by the deduction theorem,

\[\Gamma \vdash (\lnot \phi \to \chi) \text{ and } \Gamma \vdash (\lnot \phi \to \lnot \chi)\]

so

\[((\lnot \phi \to \chi) \to ((\lnot \phi \to \lnot \chi) \to \phi))\]

is an instance of the axiom A3. By modus ponens twice, we can conclude $\Gamma \vdash \phi$ (this is effectively a proof of the contradiction lemma).

$\Gamma \cup \{\lnot \phi\}$ inconsistent implies $\Gamma \vdash \phi$:

Suppose $\Gamma \vdash \phi$. Then $\Gamma \cup \{\lnot \phi\}$ is inconsistent, since $\Gamma \cup \{\lnot \phi\} \vdash \phi$ and $\Gamma \cup \{\lnot \phi\} \vdash \lnot \phi$.

$\Gamma \vdash \phi$ iff $\Gamma \cup \{\lnot \phi\}$ is inconsistent.

$\Gamma \models \phi$ iff $\Gamma \cup \{\lnot \phi\}$ is unsatisfiable.

1. $\Gamma$ is consistent (you can’t prove a statement and it’s negation)
2. For every $\phi \in \text{Form}(\mathcal L _ 0)$, either $\Gamma \vdash \phi$ or $\Gamma \vdash \lnot \phi$.

Suppose:

• $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$ is consistent
• $\phi \in \text{Form}(\mathcal L _ 0)$

Then either:

• $\Gamma \cup \{\phi\}$ is consistent, or
• $\Gamma \cup \{\lnot \phi\}$ is consistent.

Consider the contrapositive. If $\Gamma \cup \{\phi\}$ and $\Gamma \cup \{\lnot \phi\}$ are both inconsistent, then by the lemma that says

$\Gamma \vdash \phi$ iff $\Gamma \cup \{\lnot \phi\}$ is inconsistent.

we have both $\Gamma \vdash \phi$ and $\Gamma \vdash \lnot \phi$. But then $\Gamma$ is inconsistent, a contradiction.

---

Alternative proof: Suppose $\Gamma \not\vdash \phi$, then $\Gamma \cup \{\lnot \phi\}$ is consistent by the lemma that says

$\Gamma \vdash \phi$ iff $\Gamma \cup \{\lnot \phi\}$ is inconsistent.

Otherwise, $\Gamma \vdash \phi$. Suppose for a contradiction that $\Gamma \cup \{\phi\}$ is not consistent, then

• $\Gamma \cup \{\phi\} \vdash \chi$ implies $\Gamma \vdash (\phi \to \chi)$ by the deduction theorem.
• $\Gamma \cup \{\phi\} \vdash \lnot\chi$ implies $\Gamma \vdash (\phi \to \lnot\chi)$ by the deduction theorem.

But then $\Gamma \vdash \phi$ implies by modus ponens that both $\Gamma \vdash \chi$ and $\Gamma \vdash \lnot \chi$, a contradiction since $\Gamma$ is assumed to be consistent.

In other words, either $\Gamma$ proves $\varphi$ or it doesn’t.

• If it does prove $\varphi$, then $\Gamma \cup \{ \lnot \varphi \}$ is consistent.
• If it doesn’t prove $\varphi$, then $\Gamma \cup \{ \varphi \}$ is consistent.

Suppose:

• $\Gamma \subseteq \text{Form}(\mathcal L _ 0)$ is consistent

Then:

• There exists a complete $\Gamma’ \supseteq \Gamma$

Note that $\text{Form}(\mathcal L _ 0) = \{\phi _ 0, \phi _ 1, \ldots\}$ is countable. Construct a chain of consistent sets like so:

\[\Gamma = \Gamma_0 \subseteq \Gamma_1 \subseteq \cdots\]

where:

$\Gamma _ 0 := \Gamma$ and given a consistent $\Gamma _ n$, let

\[\Gamma_{n+1} := \begin{cases} \Gamma_n \cup \\{\phi_n\\} &\text{ if } \Gamma_n \cup \\{\phi_n\\} \text{ is consistent} \\\\ \Gamma_n \cup \\{\lnot \phi_n \\} &\text{otherwise} \end{cases}\]

Then consider

\[\Gamma' := \bigcup^\infty_{n = 0} \Gamma_n\]

Then $\Gamma’$ is consistent: if $\Gamma’ \vdash \chi$ and $\Gamma’ \vdash \lnot \chi$, then proofs witnessing this use only finitely many formulas from $\Gamma’$, so for some $n$,

\[\Gamma_n \vdash \chi\]

and

\[\Gamma_n \vdash \lnot \chi\]

which contradicts the consistency of $\Gamma _ n$. And by construction $\Gamma’$ is complete.

For (1), consistency of $\Gamma$ handles the forward direction and completeness handles the backwards direction.

For (2):

• Forward direction: Suppose $\Gamma \vdash (\psi \to \chi)$ but that $\Gamma \vdash \psi$ and $\Gamma \not\vdash \chi$. But by MP, $\Gamma \vdash \chi$ contradicts consistency.
• Backwards direction: Suppose $\Gamma \not\vdash \psi$. Then $\Gamma \vdash \lnot\psi$ by (a). But then $\Gamma \vdash (\psi \to \chi)$ by the deduction theorem. If $\Gamma \vdash \chi$, then $\Gamma \vdash (\psi \to \chi)$ by A1 and MP.

(This result is used to show that if $\Gamma$ is complete then it is satisfiable, since these results let you prove that defining a valuation by $v(p _ i) = T$ if $\Gamma \vdash p _ i$ means that $v$ actually satisfies every formula in $\Gamma$).

\[\Gamma \text{ is complete} \implies \Gamma \text{ is satisfiable}\]

Define a valuation $v$ by:

\[v(p_i) = T \text{ iff } \Gamma \vdash p_i\]

We prove by induction of the length of any formula $\phi \in \text{Form}(\mathcal L _ 0)$:

\[v(\phi) = T \text{ iff } \Gamma \vdash \phi\]

There are several cases:

Case 1: $\phi = p _ i$ for some $i$. Then we are done by the definition of $v$.

Case 2: $\phi = \lnot \psi$. Then:

\[\begin{aligned} \tilde v(\phi) = T &\text{ iff } \tilde v(\psi) = F &&(\text{tt}\lnot) \\\\ &\text{ iff } \Gamma \not\vdash \psi &&(\text{by inductive hypothesis}) \\\\ &\text{ iff } \Gamma \vdash \lnot \psi &&(\text{by completeness}) \\\\ &\text{ iff } \Gamma \vdash \phi \end{aligned}\]

Case 3: $\phi = (\psi \to \chi)$. Then:

\[\begin{aligned} \tilde v(\phi) = T &\text{ iff } \tilde v(\psi) = F \text{ or } \tilde v(\chi) = T &&(\text{tt}\lnot) \\\\ &\text{ iff } \Gamma \not\vdash \psi \text{ or } \Gamma \vdash \chi &&(\text{by inductive hypothesis}) \\\\ &\text{ iff } \Gamma \vdash (\psi \to \chi) &&(\text{by completeness}) \\\\ &\text{ iff } \Gamma \vdash \phi \end{aligned}\]

as required.

\[\Gamma \text{ consistent} \iff \Gamma\text{ satisfiable}\]

• Forward direction: If $\Gamma$ is consistent, it extends to a complete set, which is satisfiable, and hence $\Gamma$ is also satisfiable
• Backward direction: If $\Gamma$ is inconsistent, then $\Gamma \vdash \chi$ and $\Gamma \vdash \lnot \chi$, then $\Gamma \models \chi$ and $\Gamma \models \lnot \chi$ by soundness. But no valuation can satisfy both $\chi$ and $\lnot \chi$.

\[\begin{aligned} \Gamma \models \phi &\stackrel1\implies \Gamma \cup \\{\lnot \phi\\} \text{ unsatisfiable} \\\\ &\stackrel2\implies \Gamma \cup \\{\lnot \phi\\} \text{ inconsistent} \\\\ &\stackrel3\implies \Gamma \vdash \phi \end{aligned}\]

where each of the implications follow from:

• (1): Immediate.
• (2): The result that if $\Sigma \subseteq \text{Form}(\mathcal L _ 0)$ is consistent, then it is satisfiable. The proof for this first shows that $\Sigma$ extends to a complete set of formulas $\Sigma’$, which is satisfiable. If $\Sigma’ \supseteq \Sigma$ is satisfiable, it follows that $\Sigma$ is also satisfiable.
• (3): Can consider a proof by contradiction in $L _ 0$.