Notes - Logic MT24, Proofs in first-order logic

Axioms:

• 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”)
• A4: $(\forall x _ i \alpha \to \alpha[t/x _ i])$ if $\alpha[t/x _ i]$ is defined (“for all really means for all”)
• A5: $(\forall x _ i (\alpha \to \beta) \to (\alpha \to \forall x _ i \beta))$ if $x _ i \notin \text{Free}(\alpha)$ (“like blowing sand across a sticky surface”)
• A6: $x _ i \doteq x _ i$ (“equality is reflexive”)
• A7: $(x _ i \doteq x _ j \implies x _ j \doteq x _ i)$ (“equality is symmetric”)
• A8: $(x _ i \doteq x _ j \to (\alpha \to \alpha[x _ j/x _ i]))$ if $\alpha$ is atomic (“equal really means equal”)

Rules:

• MP (Modus Ponens): From $\alpha$ and $(\alpha \to \beta)$, infer $\beta$.
• Gen (Generalisation): For any variable $x _ k$, from $\alpha$ infer $\forall x _ k \alpha$.

There is a sequence of $\mathcal L$-formulas (a derivation or proof) $\phi _ 1, \ldots, \phi _ n$ with $\phi _ n = \phi$ such that for each $i \le n$, at least one of the following holds:

• ($A1$-$A8$) $\phi _ i$ is an axiom
• ($\text{Hyp}$) $\phi _ i \in \Sigma$
• $(\text{MP})$ $\phi _ k = (\phi _ j \to \phi _ i)$ for some $j, k < i$
• $(\text{Gen})$ $\phi _ i = \forall x _ k \phi _ j$ for some $j < i$ and some $k \in \mathbb N$

Suppose:

• $\Sigma \subseteq \text{Sent}(\mathcal L)$
• $\phi \in \text{Form}(\mathcal L)$

Then:

\[\Sigma \vdash \phi \implies \Sigma \models \phi\]

Recall the axioms and rules of inference for proofs in first-order logic:

• Axioms:
  • 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”)
  • A4: $(\forall x _ i \alpha \to \alpha[t/x _ i])$ if $\alpha[t/x _ i]$ is defined (“for all really means for all”)
  • A5: $(\forall x _ i (\alpha \to \beta) \to (\alpha \to \forall x _ i \beta))$ if $x _ i \notin \text{Free}(\alpha)$ (“like blowing sand across a sticky surface”)
  • A6: $x _ i \doteq x _ i$ (“equality is reflexive”)
  • A7: $(x _ i \doteq x _ j \implies x _ j \doteq x _ i)$ (“equality is symmetric”)
  • A8: $(x _ i \doteq x _ j \to (\alpha \to \alpha[x _ j/x _ i]))$ if $\alpha$ is atomic (“equal really means equal”)
• Rules:
  • MP (Modus Ponens): From $\alpha$ and $(\alpha \to \beta)$, infer $\beta$.
  • Gen (Generalisation): For any variable $x _ k$, from $\alpha$ infer $\forall x _ k \alpha$.

We induct on the length of the proof. Each of the axioms forms a base case:

• A1-3: These are tautologies and therefore logically valid, as they are for proofs in propositional logic.
• A4: This follows from the result that says “for any formula $\phi$ and term $t$ where $\phi[t/x _ i]$ is defined, $\models (\forall x _ i \phi \to \phi[t/x _ i])$”.
• A5: This follows from the result that says “if $x _ i$ has no free occurrence in $\alpha$, then: $\models (\forall x _ i (\alpha \to \beta) \to (\alpha \to \forall x _ i \beta))$”.
• A6-7: Immediate by reflexivity and symmetry of equality.
• A8: Slightly more complicated:

Let $\mathcal M$ be a $\mathcal L$-structure and $a$ an assignment in $\mathcal M$ such that

\[\mathcal M \models_a x_i \doteq x_j\]

and

\[\mathcal M \models_a \alpha\]

where $\alpha$ is atomic. We aim to show that $\mathcal M \models _ a \alpha[x _ j / x _ i]$.

By the definitions, we have that $a(x _ i) = a(x _ j)$, so

\[\tilde a(t[x_j / x_i]) = \tilde a(t)\]

for any term $t$, by induction on the length of $t$.

Suppose $\alpha = P(t _ 1, \ldots, t _ k)$. Then

\[\begin{aligned} M \models_a \alpha &\implies (\tilde a(t_1), \ldots, \tilde a(t_k)) \in P^\mathcal M \\\\ &\implies (\tilde a(t_1[x_j / x_i]), \ldots, \tilde a(t_k[x_j/x_i])) \in P^\mathcal M \\\\ &\implies \mathcal M \models_a P(t_1[x_j/x_i], \ldots, t_k[x_j / x_i]) \\\\ &\implies \mathcal M \models_a \alpha[x_j / x_i] \end{aligned}\]

as required, and a similar argument can be made for $\alpha$ of the form $t _ 1 \doteq t _ 2$.

Finally, the rules $\text{MP}$ and $\text{Gen}$ preserve the property of being a logical consequence of $\Sigma$:

• MP: For any $\mathcal M$ and $a$, if $\mathcal M \models _ a \alpha$ and $\mathcal M \models _ a (\alpha \to \beta)$, then $\mathcal M \models _ a \beta$. Hence if $\Sigma \models \alpha$ and $\Sigma \models (\alpha \to \beta)$, then $\Sigma \models \beta)$ by induction.
• Gen: Suppose $\Sigma \models \psi$, we want to show $\Sigma \models \forall x _ i \psi$. Recall that the elements of $\Sigma$ are sentences. Let $\mathcal M$ be such that $\mathcal M \models \Sigma$, and let $a$ be an assignment on $\mathcal M$. We want to show $\mathcal M \models _ a \forall x _ i \psi$. Let $a^\star \sim _ i a$, we want to show that $\mathcal M \models _ {a^\star} \psi$. Since $\Sigma \models \psi$, we have $\mathcal M \models _ {a’}$ for any assignment $a’$, and so in particular for $a^\star$.

All inductive steps are done, so the result follows.

Suppose:

• $\mathcal L$ is a first-order language
• $\Sigma \subseteq \text{Sent}(\mathcal L)$
• $\tau \in \text{Sent}(\mathcal L)$
• $\Sigma \cup \{\tau\} \vdash \phi$

Then:

• $\Sigma \vdash (\tau \to \phi)$

Proceed almost identically to the deduction theorem for propositional logic for uses of $\text{MP}$ and the axioms. To handle a use of $\text{Gen}$, e.g. deriving $\forall x _ i \chi$ from $\chi$, it suffices to show:

If $\Sigma \vdash (\tau \to \chi)$ then $\Sigma \vdash (\tau \to \forall x _ i \chi)$

But since

\[(\forall x_i (\tau \to \chi) \to (\tau \to \forall x_i \chi))\]

is an instance of A5 as $x _ i \notin \text{Free}(\tau) = \emptyset$, so the claim follows by Gen and MP.

---

Proof of deduction theorem for propositional logic:

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 $\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 $\{\} \subseteq \Gamma$, $\Gamma \vdash (\phi \to \alpha _ m)$.

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

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

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

If $\phi$ is a tautology of $\mathcal L$, then $\vdash \phi$ (and hence we can freely introduce tautologies in $K(\mathcal L)$).

Suppose $\phi$ results from substituting $\psi _ i$ for $p _ i$ in the propositional tautology $\tau$.

By the completeness of $L _ 0$, there is a proof

\[\tau_1, \ldots, \tau_{n-1}, \tau\]

of $\alpha$ in $L _ 0$. Since A1, A2, A3 and MP are in $K(\mathcal L)$, substituting $\psi _ i$ for $p _ i$ in each $\tau _ i$ yields a proof

\[\phi_1, \ldots, \phi_{n-1}, \phi\]

of $\phi$ in $K(\mathcal L)$.

A set $\Sigma \subseteq \text{Sent}(\mathcal L)$ of $\mathcal L$-sentences.

There does not exist $\chi \in \text{Sent}(\mathcal L)$ such that both:

• $\Sigma \vdash \chi$, and
• $\Sigma \vdash \lnot\chi$

It has a model, i.e. there exists a $\mathcal L$-structure $\mathcal M$ such that $\mathcal M \models \Sigma$.

• Suppose $\Sigma \vdash \chi$ and $\Sigma \vdash \lnot \chi$
• $(\chi \to (\lnot \chi \to \phi))$ is a tautology for any $\phi$
• Therefore $\Sigma \vdash \phi$

• $\Sigma \vdash \tau$ iff $\Sigma \cup \{\lnot \tau\}$ is inconsistent (use deduction theorem)
• $\Sigma \models \tau$ iff $\Sigma \cup \{\lnot \tau\}$ is unsatisfiable (straightforward)
• $\Sigma$ is consistent iff it is satisfiable (backward direction by soundness, forward direction is tricky).

• $\Sigma$ is consistent, and
• For any $\tau \in \text{Sent}(\mathcal L)$, either:
  • $\Sigma \vdash \tau$, or
  • $\Sigma \vdash \lnot \tau$.