From 3686a22e56d86830eecd64822b19dbe1f3e94e91 Mon Sep 17 00:00:00 2001
From: Benedict Eastaugh <benedict@eastaugh.net>
Date: Thu, 26 Jun 2025 16:07:57 +0200
Subject: [PATCH 1/2] Add section on \Sigma_1 completeness to the chapter on
 representability in Q.

---
 .../representability-in-q.tex                 |   2 +
 .../sigma1-completeness.tex                   | 329 ++++++++++++++++++
 2 files changed, 331 insertions(+)
 create mode 100644 content/incompleteness/representability-in-q/sigma1-completeness.tex

diff --git a/content/incompleteness/representability-in-q/representability-in-q.tex b/content/incompleteness/representability-in-q/representability-in-q.tex
index 378cd66f..bfbf416a 100644
--- a/content/incompleteness/representability-in-q/representability-in-q.tex
+++ b/content/incompleteness/representability-in-q/representability-in-q.tex
@@ -25,6 +25,8 @@
 
 \olimport{representing-relations}
 
+\olimport{sigma1-completeness}
+
 \olimport{undecidability}
 
 \OLEndChapterHook
diff --git a/content/incompleteness/representability-in-q/sigma1-completeness.tex b/content/incompleteness/representability-in-q/sigma1-completeness.tex
new file mode 100644
index 00000000..037cda18
--- /dev/null
+++ b/content/incompleteness/representability-in-q/sigma1-completeness.tex
@@ -0,0 +1,329 @@
+% Part: incompleteness
+% Chapter: representability-in-q
+% Section: sigma1-completeness
+
+\documentclass[../../../include/open-logic-section]{subfiles}
+
+\begin{document}
+
+\olfileid{inc}{inp}{s1c}
+\olsection{\texorpdfstring{$\Sigma_1$}{Sigma-1} completeness}
+
+Despite the incompleteness of $\Th{Q}$ and its consistent, axiomatizable
+extensions, we have seen that $\Th{Q}$ does prove many basic facts about
+numerals. In fact, this can be extended quite considerably. To understand
+the scope of what can be proved in $\Th{Q}$, we introduce the notions of
+$\Delta_0$, $\Sigma_1$, and $\Pi_1$ !!{formula}s. Roughly speaking, a
+$\Sigma_1$ !!{formula} is one of the form $\lexists{x}!A(x)$, where $!A$
+is constructed using only Boolean connectives and bounded quantifiers.
+We shall show that if $!A$ is a correct $\Sigma_1$ sentence, then
+$\Th{Q} \Proves !A$ (\olref{thm:sigma1-completeness}).
+
+\begin{defn}
+\ollabel{defn:correct-frm}
+A sentence $!A$ is \emph{correct} if $\Struct{N} \Entails !A$.
+\end{defn}
+
+\begin{defn}
+\ollabel{defn:bd-quant}
+A \emph{bounded existential !!{formula}} is one of the form
+$\lexists[x][(x < t \land !A(x))]$ where $t$ is any term, which we
+conventionally write as $\bexists{x < t}{!A(x)}$.
+%
+A \emph{bounded universal !!{formula}} is one of the form
+$\lforall[x][(x < t \lif !A(x))]$ where $t$ is any term, which we
+conventionally write as $\bforall{x < t}{!A(x)}$.
+\end{defn}
+
+\begin{defn}
+\ollabel{defn:delta0-sigma1-pi1-frm}
+A !!{formula} $!B$ is $\Delta_0$ if it is built up from atomic
+!!{formula}s using only Boolean connectives and bounded quantification.
+%
+A !!{formula} $!A$ is $\Sigma_1$ if $!A \ident \lexists[x][!B(x)]$
+where $!B$ is $\Delta_0$.
+%
+A !!{formula} $!C$ is \emph{generalized $\Sigma_1$} if it can be
+constructed from $\Delta_0$ !!{formula}s using only conjunction,
+disjunction, implication, bounded universal quantification, and
+unbounded existential quantification.
+%
+A formula $!A$ is $\Pi_1$ if $!A \ident \lforall[x][!B(x)]$
+where $!B$ is $\Delta_0$.
+%
+A !!{formula} $!C$ is \emph{generalized $\Pi_1$} if it can be
+constructed from $\Delta_0$ !!{formula}s using only conjunction,
+disjunction, implication, bounded existential quantification, and
+unbounded universal quantification.
+\end{defn}
+
+\begin{lem}
+\ollabel{lem:q-proves-clterm-id} Suppose $t$ is a closed term such that
+$\Assign{t}{N} = n$. Then $\Th{Q} \Proves \eq[t][\num n]$.
+\end{lem}
+
+\begin{proof}
+We prove this by induction on the complexity of $t$. For the base case,
+${\Obj 0}^\Struct{N} = 0$, and $\Th{Q} \Proves \eq[\Obj 0][\num 0]$
+since $\num 0 \ident \Obj 0$.
+%
+For the inductive case, let $t_1$ and $t_2$ be terms such that
+$t_1^\Struct{N} = n_1$, $t_2^\Struct{N} = n_2$,
+$\Th{Q} \Proves \eq[t_1][\num n_1]$, and
+$\Th{Q} \Proves \eq[t_2][\num n_2]$.
+
+Then $(t_1')^\Struct{N} = n_1 + 1$, and we have that $\Th{Q} \Proves
+\eq[t_1'][{\num n_1}']$ by the first-order rules for identity applied
+to the induction hypothesis and the !!{formula}
+$\eq[\num{n_1}'][\num{n_1}']$,
+so we have $\Th{Q} \Proves \eq[t_1'][\num{n_1 + 1}]$
+by the definition of numerals.
+
+For sums we have
+$$
+      (t_1 + t_2)^\mathfrak{N}
+    = t_1^\mathfrak{N} + t_2^\mathfrak{N}
+    = n_1 + n_2.
+$$
+By the induction hypothesis and the rules for identity,
+$\Th{Q} \Proves \eq[t_1 + t_2][\num n_1 + t_2]$, and then
+$\Th{Q} \Proves \eq[t_1 + t_2][\num n_1 + \num n_2]$
+by a second application of the rules for identity.
+By \olref[inc][req][bre]{lem:q-proves-add},
+$\Th{Q} \Proves \eq[\num n_1 + \num n_2][\num{n_1 + n_2}]$,
+so $\Th{Q} \Proves \eq[t_1 + t_2][\num{n_1 + n_2}]$.
+
+Similar reasoning also works for $\times$, using
+\olref[inc][req][bre]{lem:q-proves-mult}.
+%
+Since this exhausts the closed terms of arithmetic, we have that
+$\Th{Q} \Proves \eq[t][\num n]$ for all closed terms $t$ such that
+$t^\Struct{N} = n$.
+\end{proof}
+
+\begin{prob}
+Prove in detail the part of \olref{lem:q-proves-clterm-id}
+involving $\times$.
+\end{prob}
+
+\begin{lem}
+\ollabel{lem:atomic-completeness}
+Suppose $t_1$ and $t_2$ are closed terms. Then
+\begin{enumerate}
+\item If $t_1^\Struct{N} = t_2^\Struct{N}$,
+    then $\Th{Q} \Proves \eq[t_1][t_2]$.
+\item If $t_1^\Struct{N} \neq t_2^\Struct{N}$,
+    then $\Th{Q} \Proves \eq/[t_1][t_2]$.
+\item If $t_1^\Struct{N} < t_2^\Struct{N}$,
+    then $\Th{Q} \Proves t_1 < t_2$.
+\item If $t_2^\Struct{N} \leq t_1^\Struct{N}$,
+    then $\Th{Q} \Proves \lnot(t_1 < t_2)$.
+\end{enumerate}
+\end{lem}
+
+\begin{proof}
+Given terms $t_1$ and $t_2$, we fix $n = t_1^\mathfrak{N}$ and
+$m = t_2^\mathfrak{N}$.
+
+Suppose $!A \ident t_1 = t_2$. By \olref{lem:q-proves-clterm-id},
+$\Th{Q} \Proves \eq[t_1][\num n]$ and $\Th{Q} \Proves \eq[t_2][\num n]$.
+If $n = m$, then $\Th{Q} \Proves \eq[\num n][\num m]$ and hence
+$\Th{Q} \Proves \eq[t_1][t_2]$ by the transitivity of identity.
+If $n \neq m$ then $\Th{Q} \Proves \eq/[\num n][\num m]$,
+and by the transitivity of identity again,
+$\Th{Q} \Proves \eq/[t_1][t_2]$.
+
+Now let $!A \ident t_1 < t_2$. For both cases, we rely on axiom $!Q_8$,
+which states that $x < y \leftrightarrow \lexists[z][\eq[z' + x][y]]$
+for all $x,y$.
+
+Suppose $\Sat{N}{t_1 < t_2}$. Then there exists some $k \in \Nat$
+such that $n + k + 1 = m$. By \olref{lem:q-proves-clterm-id},
+$\Th{Q} \Proves \eq[t_1][\num n]$ and $\Th{Q} \Proves \eq[t_2][\num m]$,
+and by the first part of this lemma,
+$\Th{Q} \Proves \eq[\num n + {\num k}'][\num m]$.
+By the transitivity of identity it follows that
+$\Th{Q} \Proves \eq[{\num k}' + t_1][t_2]$,
+so $\Th{Q} \Proves \lexists[z][\eq[z' + t_1][t_2]]$.
+By the right-to-left direction of $!Q_8$, $\Th{Q} \Proves t_1 < t_2$.
+
+Suppose instead that $\Sat/{N}{t_1 < t_2}$, i.e.\ $m \leq n$.
+%
+We work in $\Th{Q}$ and assume that $t_1 < t_2$. By the left-to-right
+direction of $!Q_8$, there is some $z$ such that $\eq[z' + t_1][t_2]$.
+Since $\Th{Q} \Proves \eq[t_1][\num n]$ and
+$\Th{Q} \Proves \eq[t_2][\num m]$, $\eq[z' + \num n][\num m]$.
+%
+By an external induction on $m$ using $!Q_5$,
+$\eq[z' + \num{n - m}][\Obj 0]$.
+If $m = n$ then $\eq/[z'][\Obj 0]$, giving a contradiction via $!Q_3$.
+If $m < n$ then $\eq[(z' + \num{n - m - 1})'][\Obj 0]$ by $!Q_5$ again,
+giving a contradiction via $!Q_3$.
+So $\Th{Q} \Proves \lnot(t_1 < t_2)$.
+\end{proof}
+
+\begin{lem}
+\ollabel{lem:boolean-completeness}
+Suppose $!A$ and $!B$ are either atomic !!{formula}s,
+or are built up from atomic !!{formula}s using only
+Boolean connectives.
+\begin{enumerate}
+\item If $(!A \land !B)$ is correct,
+    then $\Th{Q} \Proves (!A \land !B)$.
+%
+\item If $\lnot(!A \land !B)$ is correct,
+    then $\Th{Q} \Proves \lnot(!A \land !B)$.
+%
+\item If $(!A \lor !B)$ is correct,
+    then $\Th{Q} \Proves (!A \lor !B)$.
+%
+\item If $\lnot(!A \lor !B)$ is correct,
+    then $\Th{Q} \Proves (!A \lor !B)$.
+%
+\item If $\lnot !A$ is correct,
+    then $\Th{Q} \Proves \lnot !A$.
+\end{enumerate}
+\end{lem}
+
+\begin{proof}
+We prove this by induction on formula complexity.
+%
+\begin{enumerate}
+\item Suppose $(!A \land !B)$ is correct, so $!A$ and $!B$
+are correct. By the induction hypothesis, $\Th{Q} \Proves !A$
+and $\Th{Q} \Proves !B$, so $\Th{Q} \Proves (!A \land !B)$
+by logic.
+%
+\item Suppose $\lnot(!A \land !B)$ is correct, so either
+$\lnot !A$ or $\lnot !B$ are correct. For concreteness, and
+without loss of generality, suppose the former. Then
+$\Th{Q} \Proves \lnot !A$ by the induction hypothesis, and
+hence $\Th{Q} \Proves \lnot(!A \land !B)$ by logic.
+%
+\item Suppose $(!A \lor !B)$ is correct, so either
+$!A$ is correct or $!B$ is correct. Suppose the former.
+Then by the induction hypothesis $\Th{Q} \Proves !A$, and
+hence $\Th{Q} \Proves (!A \lor !B)$ by logic.
+%
+\item Suppose $\lnot(!A \lor !B)$ is correct, so $\lnot !A$
+and $\lnot !B$ are correct. Then $\Th{Q} \Proves \lnot !A$
+and $\Th{Q} \Proves \lnot !B$ by the induction hypothesis.
+Consequently, $\Th{Q} \Proves \lnot(!A \land !B)$ by logic.
+%
+\item Suppose $\lnot !A$ is correct, so $!A$ is not correct
+and $\Th{Q} \not\Proves !A$. Either $!A$ is atomic or $!A$
+has the form $\lnot\lnot !B$, $\lnot(!B \land !C)$, or
+$\lnot(!B \lor !C)$. If $!A$ is atomic then by
+\olref{lem:atomic-completeness}, $\Th{Q} \Proves \lnot !A$.
+The other cases are dealt with above, except $\lnot\lnot !B$.
+By logic this is provably equivalent (in $\Th{Q}$) to $!B$,
+which is correct since $\lnot !A \ident \lnot\lnot !B$ is
+correct, so by the induction hypothesis we have that
+$\Th{Q} \Proves \lnot !A$.
+\end{enumerate}
+\end{proof}
+
+\begin{lem}
+\ollabel{lem:bounded-quant-equiv}
+Suppose $!A$ is a !!{formula}. Then
+\begin{enumerate}
+\item $\Th{Q} \Proves \bforall{x<t}{!A(x)}$ iff $\Th{Q} \Proves
+    !A(\num 0) \land \dotsc \land !A(\num{t^\Struct{N}-1})$.
+\item $\Th{Q} \Proves \bexists{x<t}{!A(x)}$ iff $\Th{Q} \Proves
+    !A(\num 0) \lor \dotsc \lor !A(\num{t^\Struct{N}-1})$.
+\end{enumerate}
+\end{lem}
+
+\begin{proof}
+    We prove the case for the bounded universal quantifier.
+    If $t^\Struct{N} = 0$ then the left-hand side of the
+    equivalence is provable in $\Th{Q}$, because there is no
+    $x<\num 0$ by \olref[inc][req][min]{lem:less-zero}.
+    Similarly, we can take an empty disjunction to be simply
+    $\ltrue$, which is also provable in $\Th{Q}$.
+    %
+    We therefore suppose that $t^\Struct{N} = k+1$ for some
+    natural number $k$. By \olref{lem:q-proves-clterm-id} we
+    can assume that we are working with a formula of the form
+    $\bforall{x<\num{k+1}}{!A(x)}$.
+    
+    Suppose that $\Th{Q} \Proves \bforall{x<\num{k+1}}{!A(x)}$,
+    and let $n \leq k$. Since $\Th{Q} \Proves \num n < \num{k+1}$
+    by \olref{lem:atomic-completeness}, it follows by logic that
+    $\Th{Q} \Proves !A(\num n)$. Applying this fact $k+1$ times
+    for each $n \leq k$, we get that $\Th{Q} \Proves !A(\num 0)
+    \land \dotsc \land !A(\num k)$ as desired.
+    
+    For the other direction, suppose that $\Th{Q} \Proves
+    !A(\num 0) \land \dotsc \land !A(\num k)$. Working in
+    $\Th{Q}$, suppose that $x < \num{k+1}$.
+    By \olref[inc][req][min]{lem:less-nsucc} we have that
+    $x = \num 0 \lor \dotsc \lor x = \num k$, so by logic it
+    follows that $!A(x)$, and hence the universal claim
+    $\bforall{x<\num{k+1}}!A(x)$ follows.
+    
+    The proof of the equivalence for bounded existentially
+    quantified formulas is similar.
+\end{proof}
+
+\begin{prob}
+Give a detailed proof of the existential case in
+\olref{lem:bounded-quant-equiv}.
+\end{prob}
+
+\begin{lem}
+\ollabel{lem:delta0-completeness}
+If $!A$ is a correct $\Delta_0$ sentence,
+then $\Th{Q} \Proves !A$.
+\end{lem}
+
+\begin{proof}
+By induction on !!{formula} complexity.
+%
+Suppose $!A$ is a correct atomic formula. Then
+$\Th{Q} \vdash !A$ by \olref{lem:atomic-completeness}.
+%
+If $!A$ is a Boolean combination of correct $\Delta_0$
+formulas, we apply \olref{lem:boolean-completeness}.
+%
+If $!A$ has the form $\bforall{x<t}!B(x)$,
+then $\Th{Q} \Proves \bforall{x<t}!B(x) \liff
+!B(\num 0) \land \dotsc !B(\num{t^\Struct{N}-1})$ by
+\olref{lem:bounded-quant-equiv}. By the induction
+hypothesis, if $!B(\num n)$ is correct for all
+$n < t^\Struct{N}$ then $\Th{Q} \Proves !B(\num 0)
+\land \dotsc !B(\num t-1)$, so $\Th{Q} \Proves
+\bforall{x<t}!B(x)$. The case for bounded existential
+quantification parallels this one.
+\end{proof}
+
+\begin{thm}
+\ollabel{thm:sigma1-completeness}
+If $!A$ is a correct $\Sigma_1$ sentence,
+then $\Th{Q} \Proves !A$.
+\end{thm}
+
+\begin{proof}
+Let $\lexists{x}!A(x)$ be a correct $\Sigma_1$ sentence.
+By correctness there exists a natural number $n$ and a
+variable assignment $s$ such that $s(x) = n$ and
+$\Struct{N},s \Entails !A(x)$. By standard facts about
+the satisfaction relation it follows that
+$\Struct{N} \Entails !A(\num n)$. But $!A(\num n)$ is a
+$\Delta_0$ formula, so by \olref{lem:delta0-completeness}
+we have that $\Th{Q} \Proves !A(\num n)$, and hence by
+logic we also have that $\Th{Q} \Proves \exists{x}!A(x)$.
+\end{proof}
+
+Note that $\Sigma_1$ !!{formula}s are not closed under Boolean
+operations. For example, $\OProv[\Th{PA}](x)$ is a $\Sigma_1$
+!!{formula} but $\lnot\OProv[\Th{PA}](x)$ is not. One can show that
+there is a $\Sigma_1$ sentence $!B$ such that
+$\Th{PA} \Proves \lnot!B \liff !G_\Th{PA}$.
+Since, if $\Th{PA}$ is consistent, $\Th{PA} \Proves/ !G_\Th{PA}$
+by the first incompleteness theorem, $\Th{PA} \Proves/ \lnot!B$ and
+a fortiori $\Th{Q} \Proves/ \lnot!B$. $\lnot!B$ is therefore not a
+$\Sigma_1$ !!{formula}, since this would contradict
+\olref{thm:sigma1-completeness}.
+
+\end{document}

From f443135c8ac2393ab67c8f6846cbfbaa842c03e6 Mon Sep 17 00:00:00 2001
From: Benedict Eastaugh <benedict@eastaugh.net>
Date: Fri, 27 Jun 2025 17:11:38 +0200
Subject: [PATCH 2/2] Tidy up Sigma_1 completeness proof.

---
 .../representability-in-q.tex                 |   4 +-
 .../sigma1-completeness.tex                   | 205 ++++++++----------
 2 files changed, 90 insertions(+), 119 deletions(-)

diff --git a/content/incompleteness/representability-in-q/representability-in-q.tex b/content/incompleteness/representability-in-q/representability-in-q.tex
index bfbf416a..4e932152 100644
--- a/content/incompleteness/representability-in-q/representability-in-q.tex
+++ b/content/incompleteness/representability-in-q/representability-in-q.tex
@@ -25,10 +25,10 @@
 
 \olimport{representing-relations}
 
-\olimport{sigma1-completeness}
-
 \olimport{undecidability}
 
+\olimport{sigma1-completeness}
+
 \OLEndChapterHook
 
 \end{document}
diff --git a/content/incompleteness/representability-in-q/sigma1-completeness.tex b/content/incompleteness/representability-in-q/sigma1-completeness.tex
index 037cda18..3ef99d43 100644
--- a/content/incompleteness/representability-in-q/sigma1-completeness.tex
+++ b/content/incompleteness/representability-in-q/sigma1-completeness.tex
@@ -15,14 +15,10 @@
 the scope of what can be proved in $\Th{Q}$, we introduce the notions of
 $\Delta_0$, $\Sigma_1$, and $\Pi_1$ !!{formula}s. Roughly speaking, a
 $\Sigma_1$ !!{formula} is one of the form $\lexists{x}!A(x)$, where $!A$
-is constructed using only Boolean connectives and bounded quantifiers.
-We shall show that if $!A$ is a correct $\Sigma_1$ sentence, then
-$\Th{Q} \Proves !A$ (\olref{thm:sigma1-completeness}).
-
-\begin{defn}
-\ollabel{defn:correct-frm}
-A sentence $!A$ is \emph{correct} if $\Struct{N} \Entails !A$.
-\end{defn}
+is constructed using only propositional connectives and bounded
+quantifiers. We shall show that if $!A$ is a $\Sigma_1$ !!{sentence}
+which is true in $\Struct{N}$, then $\Th{Q} \Proves !A$
+(\olref{thm:sigma1-completeness}).
 
 \begin{defn}
 \ollabel{defn:bd-quant}
@@ -38,23 +34,14 @@
 \begin{defn}
 \ollabel{defn:delta0-sigma1-pi1-frm}
 A !!{formula} $!B$ is $\Delta_0$ if it is built up from atomic
-!!{formula}s using only Boolean connectives and bounded quantification.
+!!{formula}s using only propositional connectives and bounded
+quantification.
 %
 A !!{formula} $!A$ is $\Sigma_1$ if $!A \ident \lexists[x][!B(x)]$
 where $!B$ is $\Delta_0$.
 %
-A !!{formula} $!C$ is \emph{generalized $\Sigma_1$} if it can be
-constructed from $\Delta_0$ !!{formula}s using only conjunction,
-disjunction, implication, bounded universal quantification, and
-unbounded existential quantification.
-%
-A formula $!A$ is $\Pi_1$ if $!A \ident \lforall[x][!B(x)]$
+A !!{formula} $!A$ is $\Pi_1$ if $!A \ident \lforall[x][!B(x)]$
 where $!B$ is $\Delta_0$.
-%
-A !!{formula} $!C$ is \emph{generalized $\Pi_1$} if it can be
-constructed from $\Delta_0$ !!{formula}s using only conjunction,
-disjunction, implication, bounded existential quantification, and
-unbounded universal quantification.
 \end{defn}
 
 \begin{lem}
@@ -162,67 +149,6 @@
 So $\Th{Q} \Proves \lnot(t_1 < t_2)$.
 \end{proof}
 
-\begin{lem}
-\ollabel{lem:boolean-completeness}
-Suppose $!A$ and $!B$ are either atomic !!{formula}s,
-or are built up from atomic !!{formula}s using only
-Boolean connectives.
-\begin{enumerate}
-\item If $(!A \land !B)$ is correct,
-    then $\Th{Q} \Proves (!A \land !B)$.
-%
-\item If $\lnot(!A \land !B)$ is correct,
-    then $\Th{Q} \Proves \lnot(!A \land !B)$.
-%
-\item If $(!A \lor !B)$ is correct,
-    then $\Th{Q} \Proves (!A \lor !B)$.
-%
-\item If $\lnot(!A \lor !B)$ is correct,
-    then $\Th{Q} \Proves (!A \lor !B)$.
-%
-\item If $\lnot !A$ is correct,
-    then $\Th{Q} \Proves \lnot !A$.
-\end{enumerate}
-\end{lem}
-
-\begin{proof}
-We prove this by induction on formula complexity.
-%
-\begin{enumerate}
-\item Suppose $(!A \land !B)$ is correct, so $!A$ and $!B$
-are correct. By the induction hypothesis, $\Th{Q} \Proves !A$
-and $\Th{Q} \Proves !B$, so $\Th{Q} \Proves (!A \land !B)$
-by logic.
-%
-\item Suppose $\lnot(!A \land !B)$ is correct, so either
-$\lnot !A$ or $\lnot !B$ are correct. For concreteness, and
-without loss of generality, suppose the former. Then
-$\Th{Q} \Proves \lnot !A$ by the induction hypothesis, and
-hence $\Th{Q} \Proves \lnot(!A \land !B)$ by logic.
-%
-\item Suppose $(!A \lor !B)$ is correct, so either
-$!A$ is correct or $!B$ is correct. Suppose the former.
-Then by the induction hypothesis $\Th{Q} \Proves !A$, and
-hence $\Th{Q} \Proves (!A \lor !B)$ by logic.
-%
-\item Suppose $\lnot(!A \lor !B)$ is correct, so $\lnot !A$
-and $\lnot !B$ are correct. Then $\Th{Q} \Proves \lnot !A$
-and $\Th{Q} \Proves \lnot !B$ by the induction hypothesis.
-Consequently, $\Th{Q} \Proves \lnot(!A \land !B)$ by logic.
-%
-\item Suppose $\lnot !A$ is correct, so $!A$ is not correct
-and $\Th{Q} \not\Proves !A$. Either $!A$ is atomic or $!A$
-has the form $\lnot\lnot !B$, $\lnot(!B \land !C)$, or
-$\lnot(!B \lor !C)$. If $!A$ is atomic then by
-\olref{lem:atomic-completeness}, $\Th{Q} \Proves \lnot !A$.
-The other cases are dealt with above, except $\lnot\lnot !B$.
-By logic this is provably equivalent (in $\Th{Q}$) to $!B$,
-which is correct since $\lnot !A \ident \lnot\lnot !B$ is
-correct, so by the induction hypothesis we have that
-$\Th{Q} \Proves \lnot !A$.
-\end{enumerate}
-\end{proof}
-
 \begin{lem}
 \ollabel{lem:bounded-quant-equiv}
 Suppose $!A$ is a !!{formula}. Then
@@ -244,8 +170,8 @@
     %
     We therefore suppose that $t^\Struct{N} = k+1$ for some
     natural number $k$. By \olref{lem:q-proves-clterm-id} we
-    can assume that we are working with a formula of the form
-    $\bforall{x<\num{k+1}}{!A(x)}$.
+    can assume that we are working with a !!{formula} of the
+    form $\bforall{x<\num{k+1}}{!A(x)}$.
     
     Suppose that $\Th{Q} \Proves \bforall{x<\num{k+1}}{!A(x)}$,
     and let $n \leq k$. Since $\Th{Q} \Proves \num n < \num{k+1}$
@@ -263,7 +189,7 @@
     $\bforall{x<\num{k+1}}!A(x)$ follows.
     
     The proof of the equivalence for bounded existentially
-    quantified formulas is similar.
+    quantified !!{formula}s is similar.
 \end{proof}
 
 \begin{prob}
@@ -273,57 +199,102 @@
 
 \begin{lem}
 \ollabel{lem:delta0-completeness}
-If $!A$ is a correct $\Delta_0$ sentence,
-then $\Th{Q} \Proves !A$.
+If $!A$ is a $\Delta_0$ !!{sentence} which is true in
+$\Struct{N}$, then $\Th{Q} \Proves !A$.
 \end{lem}
 
 \begin{proof}
-By induction on !!{formula} complexity.
+We prove this by induction on !!{formula} complexity.
+%
+The base case is given by \olref{lem:atomic-completeness},
+so we move to the induction step. For simplicity we split
+the case of negation into subcases depending on the
+structure of the !!{formula} to which the negation is
+applied.
+
+\begin{enumerate}
+\item Suppose $(!A \land !B)$ is true in $\Struct{N}$,
+so $!A$ and $!B$ are true in $\Struct{N}$.
+By the induction hypothesis, $\Th{Q} \Proves !A$ and
+$\Th{Q} \Proves !B$,
+so $\Th{Q} \Proves (!A \land !B)$ by logic.
+%
+\item Suppose $\lnot (!A \land !B)$ is true in $\Struct{N}$,
+so either $\lnot !A$ or $\lnot !B$ is true in $\Struct{N}$.
+Without loss of generality, suppose the former. By the
+induction hypothesis $\Th{Q} \Proves \lnot !A$, and hence
+$\Th{Q} \Proves \lnot (!A \land !B)$ by logic.
+%
+\item Suppose $(!A \lor !B)$ is true in $\Struct{N}$, so
+either $!A$ is true in $\Struct{N}$ or $!B$ is true in
+$\Struct{N}$. Without loss of generality, suppose the former
+holds. By the induction hypothesis $\Th{Q} \Proves !A$, and
+hence $\Th{Q} \Proves (!A \lor !B)$ by logic.
 %
-Suppose $!A$ is a correct atomic formula. Then
-$\Th{Q} \vdash !A$ by \olref{lem:atomic-completeness}.
+\item Suppose $\lnot(!A \lor !B)$ is true in $\Struct{N}$,
+so $\lnot !A$ and $\lnot !B$ are true in $\Struct{N}$.
+Then $\Th{Q} \Proves \lnot !A$ and $\Th{Q} \Proves \lnot !B$
+by the induction hypothesis. Consequently,
+$\Th{Q} \Proves \lnot(!A \lor !B)$ by logic.
 %
-If $!A$ is a Boolean combination of correct $\Delta_0$
-formulas, we apply \olref{lem:boolean-completeness}.
+\item Suppose that $\bforall{x<t}!A(x)$ is true in
+$\Struct{N}$, where $t$ is a closed term. By the induction
+hypothesis and logic, if $!A(\num n)$ is true in $\Struct{N}$
+for all $n < t^\Struct{N}$ then $\Th{Q} \Proves
+!A(\num 0) \land \dots \land !A(\num{t^\Struct{N}-1})$.
+By \olref{lem:bounded-quant-equiv} it follows that
+$\Th{Q} \Proves \bforall{x<t}!A(x)$.
 %
-If $!A$ has the form $\bforall{x<t}!B(x)$,
-then $\Th{Q} \Proves \bforall{x<t}!B(x) \liff
-!B(\num 0) \land \dotsc !B(\num{t^\Struct{N}-1})$ by
-\olref{lem:bounded-quant-equiv}. By the induction
-hypothesis, if $!B(\num n)$ is correct for all
-$n < t^\Struct{N}$ then $\Th{Q} \Proves !B(\num 0)
-\land \dotsc !B(\num t-1)$, so $\Th{Q} \Proves
-\bforall{x<t}!B(x)$. The case for bounded existential
-quantification parallels this one.
+\item The case for the bounded existential quantifier, where
+we have a !!{sentence} of the form $\bexists{x < t}!A(x)$,
+is similar to that for the bounded universal quantifier.
+%
+\item Suppose that $\lnot \bforall{x<t}!A(x)$ is true in
+$\Struct{N}$, where $t$ is a closed term. This !!{sentence}
+is equivalent to the !!{sentence} $\bexists{x<t}\lnot!A(x)$,
+with the equivalence derivable in $\Th{Q}$, so we may apply
+the reasoning for bounded existential quantifiers.
+%
+\item Similarly, suppose that $\lnot \bexists{x<t}!A(x)$ is
+true in $\Struct{N}$, where $t$ is a closed term. This
+!!{sentence} is equivalent in $\Th{Q}$ to
+$\bforall{x<t}\lnot!A(x)$, and so we may apply the reasoning
+for bounded universal quantifiers.
+%
+\item Finally, suppose $\lnot !A$ is true in $\Struct{N}$.
+The only cases remaining are when $!A$ is atomic and when
+$\lnot !A \ident \lnot\lnot !B$ for some $\Delta_0$
+!!{sentence} $!B$. If $!A$ is atomic then by
+\olref{lem:atomic-completeness}, $\Th{Q} \Proves \lnot !A$.
+If $\lnot !A \ident \lnot\lnot !B$, then by logic it is
+provably equivalent in $\Th{Q}$ to $!B$, which is true in
+$\Struct{N}$ since $\lnot !A$ is true in $\Struct{N}$.
+By the induction hypothesis we therefore have that
+$\Th{Q} \Proves \lnot !A$.
+\end{enumerate}
 \end{proof}
 
+\begin{prob}
+Give a detailed proof of the existential case in
+\olref{lem:delta0-completeness}.
+\end{prob}
+
 \begin{thm}
 \ollabel{thm:sigma1-completeness}
-If $!A$ is a correct $\Sigma_1$ sentence,
-then $\Th{Q} \Proves !A$.
+If $!A$ is a $\Sigma_1$ !!{sentence} which is true in
+$\Struct{N}$, then $\Th{Q} \Proves !A$.
 \end{thm}
 
 \begin{proof}
-Let $\lexists{x}!A(x)$ be a correct $\Sigma_1$ sentence.
-By correctness there exists a natural number $n$ and a
-variable assignment $s$ such that $s(x) = n$ and
+If $\lexists{x}!A(x)$ is a $\Sigma_1$ !!{sentence} which
+is true in $\Struct{N}$, then there exists a natural number
+$n$ and a variable assignment $s$ such that $s(x) = n$ and
 $\Struct{N},s \Entails !A(x)$. By standard facts about
 the satisfaction relation it follows that
 $\Struct{N} \Entails !A(\num n)$. But $!A(\num n)$ is a
-$\Delta_0$ formula, so by \olref{lem:delta0-completeness}
+$\Delta_0$ !!{formula}, so by \olref{lem:delta0-completeness}
 we have that $\Th{Q} \Proves !A(\num n)$, and hence by
 logic we also have that $\Th{Q} \Proves \exists{x}!A(x)$.
 \end{proof}
 
-Note that $\Sigma_1$ !!{formula}s are not closed under Boolean
-operations. For example, $\OProv[\Th{PA}](x)$ is a $\Sigma_1$
-!!{formula} but $\lnot\OProv[\Th{PA}](x)$ is not. One can show that
-there is a $\Sigma_1$ sentence $!B$ such that
-$\Th{PA} \Proves \lnot!B \liff !G_\Th{PA}$.
-Since, if $\Th{PA}$ is consistent, $\Th{PA} \Proves/ !G_\Th{PA}$
-by the first incompleteness theorem, $\Th{PA} \Proves/ \lnot!B$ and
-a fortiori $\Th{Q} \Proves/ \lnot!B$. $\lnot!B$ is therefore not a
-$\Sigma_1$ !!{formula}, since this would contradict
-\olref{thm:sigma1-completeness}.
-
 \end{document}