# Notes - Logic MT24, Example proofs in propositional logic

> Source: https://ollybritton.com/notes/uni/part-b/mt24/logic/notes/example-proofs-in-propositional-logic/ · Updated: 2025-06-12 · Tags: uni, notes

- [Course - Logic MT24](https://ollybritton.com/notes/uni/part-b/mt24/logic/)
	- [Notes - Logic MT24, Proofs in propositional logic](https://ollybritton.com/notes/uni/part-b/mt24/logic/notes/proofs-in-propositional-logic/)

### Flashcards
The proof system $L_0$ is over the language $\mathcal L_0 := \mathcal L_\text{prop}(\lnot, \to)$ and consists of:

**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 B")
- 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$.

Prove in $L_0$ (without using completeness or the deduction theorem) that for any $\phi \in \text{Form}(\mathcal L_0)$,
$$
\vdash (\phi \to \phi)
$$
::

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)**

Tips for remembering:

- Need only A1 and A2
- Helps to work backwards
- There is no point trying to use the proof of the deduction theorem to help (the proof relies on this result)

@example~

The proof system $L_0$ is over the language $\mathcal L_0 := \mathcal L_\text{prop}(\lnot, \to)$ and consists of:

> **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 B")
> - 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$.

Prove in $L_0$ (without using completeness or the deduction theorem) that for any $\phi, \psi \in \text{Form}(\mathcal L_0)$,
$$
\\{\psi, \lnot \psi\\} \vdash \phi
$$
::

1. $((\lnot \phi \to \psi) \to ((\lnot \phi \to \lnot \psi) \to \phi))$ **(A3 with $\alpha = \phi, \psi = \beta$)**
2. $\psi$ (**Hyp**)
3. $(\psi \to (\lnot \phi \to \psi))$ **(A1 with $\alpha = \psi, \beta = \lnot \phi$)**
4. $(\lnot \phi \to \psi)$ **(MP 2,3)**
5. $((\lnot \phi \to \lnot \psi) \to \phi$ **(MP 4,1)**
6. $\lnot \psi$ **(Hyp)**
7. $(\lnot \psi \to (\lnot \phi \to \lnot \psi))$ **(A1 with $\alpha = \lnot \psi, \beta = \lnot \phi$)**
8. $(\lnot \phi \to \lnot \psi)$ **(MP 6,7)**
9. $\phi$ **(MP 8,5)**

Tips for remembering:

- A3 definitely needs to be used, so it becomes a problem of deriving $(\lnot \phi \to \psi)$ and $(\lnot \phi \to \lnot \psi)$ from $\\{\psi, \lnot \psi\\}$ so that you can use MP twice
- But these two sub-results follow straightforwardly from A1 and MP

@example~

Suppose we have two proofs:

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

Can you give a proof of $\phi \to \alpha_m$?::

- $\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...

- A2: $((\phi \to (\alpha_k \to \alpha_m)) \to ((\phi \to \alpha_k) \to (\alpha_k \to \alpha_m)))$
- MP: $((\phi \to \alpha_k) \to (\phi \to \alpha_m))$
- MP: $(\phi \to \alpha_m)$

@example~

Show that there is no proof $\vdash (\phi \to \phi)$ in $\mathcal L_0$ which uses less than 5 lines.::

Any derivation of $(\phi \to \phi)$ in $\mathcal L_0$ must end with an application of MP on the last line, since $(\phi \to \phi)$ is not an instance of any of the axioms. So the derivation must look like:

- Line $i$: $\alpha$
- Line $j$: $(\alpha \to (\phi \to \phi))$
- Line $k$: $(\phi \to \phi)$

We show that either $i$ or $j$ must've also been obtained by MP, and hence that the proof used at least 5 lines.

Line $j$ is only an axiom if:

- It is an instance of A1, so $\alpha = \phi$
- It is an instance of A3, so $\alpha = (\lnot \phi \to \lnot \phi)$

But then in either case $\alpha$ is not an axiom. Hence $\alpha$ must've been obtained by MP. So either line $i$ or line $j$ was obtained by MP and the overall proof must have at least 5 lines.

@example~ @exam~

### Other examples
- Tautologies used in the proof that the Henkin construction for a complete witnessing $\mathcal L$-theory is a model:
	- $(\tau \to (\lnot \rho \to \lnot (\tau \to \rho)))$
	- $\lnot (\tau \to \rho) \to \tau$
	- $\lnot (\tau \to \rho) \to \lnot \rho$

---
Olly Britton — https://ollybritton.com. Machine-readable index: https://ollybritton.com/llms.txt