Add section on \Sigma_1 completeness to the chapter on representability in Q.

Author: beastaugh

content/incompleteness/representability-in-q/representability-in-q.tex

@@ -25,6 +25,8 @@
 
 \olimport{representing-relations}
 
+\olimport{sigma1-completeness}
+
 \olimport{undecidability}
 
 \OLEndChapterHook

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}