W2: Completeness

Remark on Question 2.5: ‘H’ is after Hilbert. There’s a trade-off between how many axioms and rules your system has (that is, how many nullary vs. non-nullary rules you have); H-style systems are those which push the trade-off much more towards axioms. Our system here is sort of the limit case, where all tautologies are axioms. This is decidable, but it’s equivalent to the satisfiability problem (just taking negations), so it’s not exactly practical.

Remark on Question 2.6: Some professional logicians have gotten this wrong in conversation, apparently! It’s a very cute question. Unexplored area of logic: what rules can you add to a system of logic with the rules (Tautology) and (Assumption) to get a complete proof system? Clearly, (MP) works, (MT) fails, and ($\wedge$Intro) obviously fails. (Project?)

The Completeness Theorem for First-Order Logic

Question 2.2

Show that any complete consistent set of ${\mathcal{L}}_1$-sentences is a theory.

Consider the following definitions, for $\Gamma \subseteq {\mathsf{Sent}}_1$ and $\varphi \in {\mathsf{Sent}}_1$.

• Completeness${}_1$: for all $\varphi$, $\Gamma ⊢\varphi$ or $\Gamma ⊢\neg \varphi$.
• Completeness${}_2$: for all $\varphi$, $\varphi \in \Gamma$ or $\neg \varphi \in \Gamma$.
• Inconsistency: for all $\varphi$, $\Gamma ⊢\varphi$.
• Theoryhood: for all $\varphi$, if $\Gamma ⊢\varphi$, then $\varphi \in \Gamma$.

With Completeness${}_1$, the claim doesn’t follow. (Informally: consider a theory $\Gamma$ that proves and so contains $(P\wedge Q)$. Now, $\Gamma \setminus \{P\}$ is not a theory, but proves just those things that $\Gamma$ proves, and so in particular is consistent and complete${}_1$.) Notice also that, for theories, completeness${}_1$ is equivalent to completeness${}_2$.

Assume that $\Gamma$ is complete${}_2$ and consistent. Then, for any $\varphi$ such that $\Gamma ⊢\varphi$, either (i) $\varphi \in \Gamma$ or (ii) $\neg \varphi \in \Gamma$. If (ii) $\neg \varphi \in \Gamma$, then $\Gamma ⊢\neg \varphi$, so $\Gamma$ is negation-inconsistent and so not consistent. So (i) $\varphi \in \Gamma$. So complete${}_2$ consistency implies theoryhood.

Question 2.3

Show that any maximal consistent set of ${\mathcal{L}}_1$-sentences is a complete theory.

Recall that $\Gamma$ is maximal consistent just in case $\Gamma$ is consistent, and for any $\varphi \notin \Gamma$, $\Gamma \cup \{\varphi \}$ is inconsistent. That is, if $\Gamma \cup \{\varphi \}$ is consistent, then $\varphi \in \Gamma$.

(Theory): As $\Gamma$ is consistent, $\Gamma ⊢\varphi$ implies that $\Gamma \cup \{\varphi \}$ is consistent, so (as $\Gamma$ is maximally consistent) $\varphi \in \Gamma$. So maximal consistency implies theoryhood.

(Complete): Suppose $\Gamma$ is not complete. Then there is some $\varphi$ such that $\Gamma /⊢\varphi$ and $\Gamma /⊢\neg \varphi$. But then $\Gamma \cup \{\varphi \}$ is consistent, so $\Gamma$ is not maximal consistent. So maximal consistency implies complete theoryhood.

Question 2.4

Prove one of the missing quantifier cases of Theorem 2.1.2. (Soundness of ND${}_{=}$). (You may choose which one.)

For ($\forall$Elim), the proof $\pi$ has the structure ${\pi }_1\cdots \forall \text{v}\varphi |\varphi [\text{c}/\text{v}]$, with $\mathsf{As}(\pi )=\mathsf{As}({\pi }_1)$. We have $\mathsf{As}(\pi ){⊢}_n^{\pi }\varphi [\text{c}/\text{v}]$. We fix an arbitrary $\mathcal{A}$ and assume $\mathcal{A}\models \chi$ for every $\chi \in \mathsf{As}(\pi )$; we need to show $\mathcal{A}\models \varphi [\text{c}/\text{v}]$. We have $\mathsf{As}({\pi }_1){⊢}_{<n}^{{\pi }_1}\forall \text{v}\varphi$, so by the IH $\mathsf{As}({\pi }_1)\models \forall \text{v}\varphi$. Since $\mathsf{As}(\pi )=\mathsf{As}({\pi }_1)$, $\mathcal{A}\models \forall \text{v}\varphi$. That is, for any variable assignment $\alpha$, $\min \{|\varphi {|}_{\mathcal{A}}^{\alpha [a/\text{v}]}:a\in D_{\mathcal{A}}\}=1$, so in particular $|\varphi [\text{c}/\text{v}]{|}_{\mathcal{A}}^{\alpha }=|\varphi {|}_{\mathcal{A}}^{\alpha [\text{c}/\text{v}]}=1$. So, $\mathcal{A}\models \varphi [\text{c}/\text{v}].$

Question 2.5

Let H be the deduction system for ${\mathcal{L}}_1$ with the following rules:

• (Assumption)
• ($\to$ Elim)

and the novel rule

• (Taut): where $\varphi$ is an ${\mathcal{L}}_1$-tautology, a labelled tree consisting of a single node, labelled with the sentence $\varphi$, constitutes a proof $\pi$ of $\varphi$ of the form $\varphi$ with $\mathsf{As}(\pi )=\varnothing$.

Show that H is sound and complete for the semantics of ${\mathcal{L}}_1$. You may use the soundness and completeness of ND${}_1$.

(Soundness): We want to show that if there is an H-proof $\pi$ such that $\Gamma {⊢}^{\pi }\varphi$ for $\varphi \in \mathsf{Sent}$ and $\Gamma \subseteq \mathsf{Sent}$, then for any ${\mathcal{L}}_1$-structure $\mathcal{A}$: if $\mathcal{A}\models \Gamma$, then $\mathcal{A}\models \varphi$.

We proceed by strong induction on length of proofs. If $\pi$ has length 1, then it consists of a single application of either (Assumption) or (Taut). In the first case, we have $\varphi \in \Gamma$, and so by definition $\mathcal{A}\models \varphi$ whenever $\mathcal{A}\models \Gamma$. In the second case, we have $\models \varphi$, and so (a fortiori) $\mathcal{A}\models \varphi$ whenever $\mathcal{A}\models \Gamma$.

Now assume (IH) that all H-proofs of less than length $k$ are sound. Then a length-$k$ proof is sound, as for $k>1$ the proof must consist of a terminal application of ($\to$Elim), which is a rule of ND${}_1$ (which we know is sound). So by strong induction of length of proofs, H is sound.

(Completeness): We want to show that if $\Gamma \models \varphi$ then $\Gamma {⊢}_{\text{H}}\varphi$. We have that if $\Gamma \models \varphi$, then $\Gamma {⊢}_{{\text{ND}}_1}\varphi$, so it suffices to show that if $\Gamma {⊢}_{{\text{ND}}_1}\varphi$ then $\Gamma {⊢}_{\text{H}}\varphi$. Suppose that there is an ND${}_1$-proof $\pi$ from $\Gamma$ to $\varphi$, and so in particular from $\mathsf{As}(\pi )$ to $\varphi$. We proceed by induction on number of assumptions. As $\pi$ must be finite, $\mathsf{As}(\pi )$ must have finite cardinality, say $n$. We number the assumptions of $\pi$ $a_1$, …, $a_n$.

Base case: if $n=0$, then $\models \varphi$, and so there is an H-proof of $\varphi$ consisting of a single application of (Taut).

Induction: now assume (IH) that for any ND${}_1$-proof of $\psi$ with $k$ assumptions, then there is an H-proof of $\psi$. Suppose there is a ND${}_1$-proof $\pi$ of $\varphi$ with $k+1$ assumptions. Applying ($\to$Intro), we can discharge $a_{k+1}$ to get a ND${}_1$-proof $\rho$ from $\mathsf{As}(\pi )\setminus \{a_{k+1}\}$ to $(a_{k+1}\to \varphi )$. So by (IH) there is an H-proof $\sigma$ from $\mathsf{As}(\pi )\setminus \{a_{k+1}\}$ to $(a_{k+1}\to \varphi )$. Now, we may apply (Assumption) and ($\to$Elim) to get an H-proof of $\varphi$ from $\mathsf{As}(\pi )$: $(a_{k+1})(\sigma [\mathsf{As}(\pi )\setminus \{a_{k+1}\}]\cdots (a_{k+1}\to \varphi ))|\varphi$

Question 2.7

Suppose that, in system H, ($\to$Elim) were replaced with the following version of modus tollens:

• (MT) Where ${\pi }_1$ is a proof of $\neg \varphi$ and ${\pi }_2$ is a proof of $\psi \to \varphi$, the labelled tree $\pi$ with the following structure constitutes a proof of $\neg \psi$: $({\pi }_1\cdots \neg \varphi )({\pi }_2\cdots \psi \to \varphi )|\neg \psi$ and $\mathsf{As}(\pi )=\mathsf{As}({\pi }_1)\cup \mathsf{As}({\pi }_2)$.

Call this system H*. Is H* complete for the semantics of ${\mathcal{L}}_1$? If so, provide a proof. If not, explain why and suggest a new rule (other than ($\to$Elim)) that could be added to H* to restore completeness.

H* is not complete, because (MT) only proves sentences of the form $\neg \psi$. So, for instance, it can’t prove that $\neg \neg P\models P$. We could add contraposition, and double-negation introduction/elimination.

Question 2.8

Let ${\mathcal{L}}_{!}$ be ${\mathcal{L}}_{=}$ enriched with a new quantifier $\exists !$, whose syntax is $\exists !\text{v}\varphi$ and whose intended interpretation is ‘there exists exactly one …‘. Provide precise semantic clauses for $\exists !$ and find introduction and elimination rules that could be added to ND${}_{=}$ to generate a system ND${}_{!}$ (with deducibility relation ${⊢}_{!}$) for ${\mathcal{L}}_{!}$. Show that ND${}_{!}$ is conservative over ND${}_{=}$ in the following sense: where $\varphi \in \mathsf{Sent}$ and $\Gamma \subseteq \mathsf{Sent}$, $\Gamma {⊢}_{!}\varphi$ only if $\Gamma ⊢\varphi$ (according to the standard ND${}_{=}$-derivability relation $⊢$).

Informally: we treat $\exists !\text{v}\varphi$ as abbreviating $\exists \text{u}\forall \text{w}(\varphi [\text{w}/\text{v}]\leftrightarrow \text{w}=\text{u})$, where $\text{u}$ and $\text{w}$ are variables with no instances in $\varphi$.

$|\exists !\text{v}\varphi {|}_{\mathcal{A}}^{\alpha }=1$ just in case there’s exactly one $\beta \stackrel{\text{v}}{\sim }\alpha$ such that $|\varphi {|}_{\mathcal{A}}^{\beta }=1$.

($\exists !$Intro): Where $\rho$ is a proof of $\exists \text{u}\forall \text{w}(\varphi [\text{w}/\text{v}]\leftrightarrow \text{w}=\text{u})$, with neither $\text{u}$ nor $\text{w}$ appearing in $\varphi$, the labelled tree $\pi$ with the following structure constitutes a proof of $\exists !\text{v}\varphi$: $\rho \cdots \exists \text{u}\forall \text{w}(\varphi [\text{w}/\text{v}]\leftrightarrow \text{w}=\text{u})|\exists !\text{v}\varphi$.

($\exists !$Elim): Where $\rho$ is a proof of $\exists !\text{v}\varphi$, with neither $\text{u}$ nor $\text{w}$ appearing in $\varphi$, the labelled tree $\pi$ with the following structure constitutes a proof of $\exists \text{u}\forall \text{w}(\varphi [\text{w}/\text{v}]\leftrightarrow \text{w}=\text{u})$: $\rho \cdots \exists !\text{v}\varphi |\exists \text{u}\forall \text{w}(\varphi [\text{w}/\text{v}]\leftrightarrow \text{w}=\text{u})$.

To show that ND${}_{!}$ is conservative over ND${}_{=}$, it suffices to show that whenever a terminal application of ($\exists !$Elim) results in $\psi \in \mathsf{Sent}$ on assumptions $\Delta \subseteq \mathsf{Sent}$, then there is a ND${}_{=}$ proof from $\Delta$ to $\psi$.

Notice that $\psi$ must have form $\exists \text{u}\forall \text{w}(\varphi [\text{w}/\text{v}]\leftrightarrow \text{w}=\text{u})$, and the node immediately above $\psi$ must have form $\exists !\text{v}\varphi$, with neither $\text{u}$ nor $\text{w}$ occurring in $\varphi$, and with $\varphi \in \mathsf{Sent}$.

But as $\Delta \subseteq \mathsf{Sent}$, an examination of what the ND${}_{=}$ rules can(not) produce shows that there must be some above application of ($\exists !$Intro) resulting in a node of the form $\exists !\text{v}\varphi$ (this node is necessarily the one immediately above the root node). But then the node immediately above that one must have form $\exists {\text{u}}^{\prime }\forall {\text{w}}^{\prime }(\varphi [{\text{w}}^{\prime }/\text{v}]\leftrightarrow {\text{w}}^{\prime }={\text{u}}^{\prime })$, with neither \textbf{u}’ nor \textbf{w}’ occurring in $\varphi$.

But clearly $\exists {\text{u}}^{\prime }\forall {\text{w}}^{\prime }(\varphi [{\text{w}}^{\prime }/\text{v}]\leftrightarrow {\text{w}}^{\prime }={\text{u}}^{\prime })\models \exists \text{u}\forall \text{w}(\varphi [\text{w}/\text{v}]\leftrightarrow \text{w}=\text{u})$; so by completeness of ND${}_{=}$ there is a proof from the former to the latter, with which we may replace the intermediate steps in the ND${}_{!}$-proof of the latter to obtain a ND${}_{=}$-proof from assumptions $\Delta$ to $\psi$.