updates to incompleteness chapter

Author: rzach

incompleteness/arithmetization-syntax/proofs-in-lk.tex

@@ -130,35 +130,35 @@
 
 \begin{prop}
 Suppose $\Gamma$ is a primitive recursive set of !!{sentence}s.  Then
-the relation $\fn{Pr}_\Gamma(x, y)$ expressing ``$x$ is the G\"odel
-number of a sentence~$!A$ and $y$ is the code of !!a{derivation}~$\Pi$
-of $\Gamma_0 \Sequent !A$ for some finite $\Gamma_0 \subseteq
-\Gamma$'' is primitive recursive.
+the relation $\fn{Pr}_\Gamma(x, y)$ expressing ``$x$ is the code of
+!!a{derivation}~$\Pi$ of $\Gamma_0 \Sequent !A$ for some finite
+$\Gamma_0 \subseteq \Gamma$ and $x$ is the G\"odel number of~$!A$'' is
+primitive recursive.
 \end{prop}
 
 \begin{proof}
-Suppose ``$x \in \Gamma$'' is given by the primitive recursive
-predicate~$R_\Gamma(x)$. We have to show that $\fn{Pr}_\Gamma(x, y)$
-which holds iff $x$ is the G\"odel number of a sentence~$!A$ and $y$
-is the code of an $\Log{LK}$-!!{derivation} with end sequent
+Suppose ``$y \in \Gamma$'' is given by the primitive recursive
+predicate~$R_\Gamma(y)$. We have to show that $\fn{Pr}_\Gamma(x, y)$
+which holds iff $y$ is the G\"odel number of a sentence~$!A$ and
+$x$~is the code of an $\Log{LK}$-!!{derivation} with end sequent
 $\Gamma_0 \Sequent !A$ is primitive recursive.
 
-By the previous proposition, the property $\fn{Deriv}(y)$ which holds
-iff $y$`is the code of a correct derivation~$\Pi$ in $\Log{LK}$ is
-primitive recursive.  If $y$ is such a code, then $(y)_1$ is the code
-of the end sequent of`$\Pi$, and so $((y)_1)_0$ is the code of the
-left side of the end sequent and $((y)_1)_1$ the right side. So we can
+By the previous proposition, the property $\fn{Deriv}()$ which holds
+iff $x$ is the code of a correct derivation~$\Pi$ in $\Log{LK}$ is
+primitive recursive.  If $x$ is such a code, then $(x)_1$ is the code
+of the end sequent of~$\Pi$, and so $((x)_1)_0$ is the code of the
+left side of the end sequent and $((x)_1)_1$ the right side. So we can
 express ``the right side of the end sequent of~$\Pi$ is~$!A$'' as
-$\len{((y)_1)_1} = 1 \land (((y)_1)_1)_0 = x$.  The left side of the
+$\len{((x)_1)_1} = 1 \land (((x)_1)_1)_0 = x$.  The left side of the
 end sequent of $\Pi$ is of course automatically finite, we just have
 to express that every sentence in it is in~$\Gamma$.  Thus we can
 define $\fn{Pr}_\Gamma(x, y)$ by
 \begin{align*}
 \fn{Pr}_\Gamma(x, y) \defiff {}&
-\fn{Sent}(x) \land \fn{Deriv}(y) \land {} \\
+\fn{Sent}(y) \land \fn{Deriv}(x) \land {} \\
 & \lforall[i <
-  \len{((y)_1)_0}][(((y)_1)_0)_i \in \Gamma] \land {}\\
-& \len{((y)_1)_1} = 1 \land (((y)_1)_1)_0 = x
+  \len{((x)_1)_0}][(((x)_1)_0)_i \in \Gamma] \land {}\\
+& \len{((x)_1)_1} = 1 \land (((x)_1)_1)_0 = x
 \end{align*}
 \end{proof}
 

incompleteness/incompleteness-provability/fixed-point-lemma.tex

@@ -11,10 +11,12 @@
 \olsection{The Fixed-Point Lemma}
 
 Let $\fn{diag}(y)$ be the computable (in fact, primitive recursive)
-function that does the following: if $y$ is the code of a formula
-$!B(x)$, $\fn{diag}(y)$ returns a code of $!B(\gn{!B(x)})$. If
-$\Obj{diag}$ were a function symbol in $\Th{T}$ representing the
-function $\fn{diag}$, we could take $!A$ to be the formula
+function that does the following: if $y$ is the G\"odel number of a
+formula~$!B(x)$, $\fn{diag}(y)$ returns the G\"odel number
+of~$!B(\gn{!B(x)})$. ($\gn{!B(x)}$ is the standard numeral of the
+G\"odel number of~$!B(x)$, i.e., $\num{\Gn{!B(x)}}$). If $\Obj{diag}$
+were a function symbol in $\Th{T}$ representing the function
+$\fn{diag}$, we could take $!A$ to be the formula
 $!B(\Obj{diag}(\gn{!B(\Obj{diag}(x))}))$. Notice that
 \begin{align*}
 \fn{diag}(\Gn{!B(\Obj{diag}(x))}) & = 

incompleteness/incompleteness-provability/introduction.tex

@@ -81,7 +81,7 @@
 \end{enumerate}
 But what happens when one takes the phrase ``yields falsehood when
 preceded by its quotation,'' and precedes it with a quoted version of
-itself? Then one has the original sentence! In short, the sentence
+itself? Then one has the original sentence!{} In short, the sentence
 asserts that it is false.
 
 \end{document}

incompleteness/incompleteness-provability/provability-conditions.tex

@@ -14,7 +14,7 @@
 induction axioms for all formulas. In other words, one adds to $\Th{Q}$
 axioms of the form
 \[
-(!A(0) \land \lforall[x][(!A(x) \lif !A(x+1))]) \lif \lforall[x][!A(x)]
+(!A(0) \land \lforall[x][(!A(x) \lif !A(x'))]) \lif \lforall[x][!A(x)]
 \]
 for every formula $!A$. Notice that this is really a {\em schema},
 which is to say, infinitely many axioms (and it turns out that
@@ -53,9 +53,9 @@
 entails\dots) Carrying out the details would be tedious and
 uninteresting, so here we will ask you to take it on faith the
 $\Th{PA}$ has the three properties listed above. A reasonable choice
-of $\Prov[PA](y)$ will also satisfy
+of $\OProv[PA](y)$ will also satisfy
 \begin{enumerate}
-\item[4.] If $\Th{PA}$ proves $\Prov[PA](\gn{!A})$, then $\Th{PA}$ proves
+\item[4.] If $\Th{PA}$ proves $\OProv[PA](\gn{!A})$, then $\Th{PA}$ proves
   $!A$.
 \end{enumerate}
 But we will not need this fact.

incompleteness/incompleteness-provability/second-incompleteness-thm.tex

@@ -43,13 +43,13 @@
 $!G_\Th{PA}$.
 
 But: we know that if $\Th{PA}$ is consistent, it doesn't prove
-$!G_\Th{PA}$!  So if $\Th{PA}$ is consistent, it can't prove
+$!G_\Th{PA}$!{}  So if $\Th{PA}$ is consistent, it can't prove
 $\OCon[PA]$.
 
 To make the argument more precise, we will let $!G_\Th{PA}$ be the
-G\"odel sentence and use properties 1--3 above to show that $\Th{PA}$
-proves $\OCon[PA] \lif !G_\Th{PA}$. This will show that $\Th{PA}$
-doesn't prove $\OCon[PA]$. Here is a sketch of the proof,
+G\"odel sentence for~$\Th{PA}$ and use properties 1--3 above to show
+that $\Th{PA}$ proves $\OCon[PA] \lif !G_\Th{PA}$. This will show that
+$\Th{PA}$ doesn't prove $\OCon[PA]$. Here is a sketch of the proof,
 in~$\Th{PA}$:
 \begin{align*}
 & !G_\Th{PA} \lif \lnot \OProv[PA](\gn{!G_\Th{PA}}) &\ & 
@@ -81,10 +81,13 @@
   \ollabel{thm:second-incompleteness-gen}
   Let $\Th{T}$ be any theory extending $\Th{Q}$ and let
   $\OProv[T](y)$ be any formula satisfying 1--3 for $\Th{T}$. Then
-  if $\Th{T}$ is consistent, then $\Th{T}$ does not prove $\lnot
-  \OProv[T](\gn{\eq[0][1]})$.
+  if $\Th{T}$ is consistent, then $\Th{T}$ does not prove~$\OCon[T]$.
 \end{thm}
 
+\begin{prob}
+Show that $\Th{Q}$ proves $\OCon[PA] \lif !G_{\Th{Q}}$.
+\end{prob}
+
 \begin{digress}
 The moral of the story is that no ``reasonable'' consistent theory for
 mathematics can prove its own consistency. Suppose $\Th{T}$ is a

incompleteness/incompleteness-provability/tarski-thm.tex

@@ -10,17 +10,14 @@
 
 \olsection{The Undefinability of Truth}
 
-Now, for the moment, we will set aside the notion of {\em proof} and
-consider the notion of {\em definability}. This notion depends on
-having a formal semantics for the language of arithmetic, and we have
-not covered semantic notions for this course. But the intuitions are
-not difficult. We have described a set of formulas and sentences in
-the language of arithmetic. The ``intended interpretation'' is to read
-such sentences as making assertions about the natural numbers, and
-such an assertion can be true or false. Let $\Struct{N}$ be the
-!!{structure} with domain $\Nat$ and the standard interpretation for
-the symbols in the langauge of arithmetic.  The $\Sat{N}{!A}$ means
-``$!A$ is true in the standard interpretation.''
+The notion of {\em definability} depends on having a formal semantics
+for the language of arithmetic.  We have described a set of formulas
+and sentences in the language of arithmetic. The ``intended
+interpretation'' is to read such sentences as making assertions about
+the natural numbers, and such an assertion can be true or false. Let
+$\Struct{N}$ be the !!{structure} with domain $\Nat$ and the standard
+interpretation for the symbols in the language of arithmetic.  Then
+$\Sat{N}{!A}$ means ``$!A$ is true in the standard interpretation.''
 
 \begin{defn}
   A relation $R(x_1,\dots,x_k)$ of natural numbers is {\em definable}
@@ -37,7 +34,7 @@
 case.)
 
 \begin{lem}
-Every computable relation is definable in $\Struct{N}$.
+Every computable relation is definable in~$\Struct{N}$.
 \end{lem}
 
 \begin{proof}
@@ -49,30 +46,24 @@
 ``representable in $\Th{Q}$''? The answer is no. For example:
 
 \begin{lem}
-Every c.e.\ set is definable in $\Struct{N}$.
+The halting relation is definable in $\Struct{N}$.
 \end{lem}
 
 \begin{proof}
-Suppose $S$ is the range of $!A_e$, i.e.
+Let $H$ be the halting relation, i.e.,
 \[
-S = \Setabs{x}{\lexists[y][T(\num e,x,y)]}.
+H = \Setabs{x}{\lexists[y][T(\num e, x, y)]}.
 \]
 Let $!D_T$ define $T$ in $\Struct{N}$. Then
 \[
-S = \Setabs{x}{\Sat{N}{\lexists[y][!D_T(\num e, \num x, y)]}},
+H = \Setabs{x}{\Sat{N}{\lexists[y][!D_T(\num e, \num x, y)]}},
 \]
-so $\lexists[y][!D_T(\num e, x, y)]$ defines~$S$ is $\Struct{N}$. 
+so $\lexists[y][!D_T(\num e, x, y)]$ defines~$H$ is $\Struct{N}$. 
 \end{proof}
 
-\begin{cor}
-$\Th{Q}$ is definable in arithmetic.
-\end{cor}
-
-So, more sets are definable in $\Struct{N}$. For example, it is not hard
-to see that complements of c.e.\ sets are also definable. The sets of
-numbers definable in $\Struct{N}$ are called, appropriately, the
-``arithmetically definable sets,'' or, more simply, the ``arithmetic
-sets.'' 
+\begin{prob}
+Show that $\Th{Q}$ is definable in arithmetic.
+\end{prob}
 
 What about $\Th{TA}$ itself? Is it definable in arithmetic? That
 is: is the set $\Setabs{\Gn{!A}}{\Sat{N}{!A}}$ definable in

incompleteness/representability-in-q/representing-relations.tex

@@ -36,7 +36,7 @@
 
 In the other direction, suppose $R(x_0,\dots,x_k)$ is computable. By
 definition, this means that the function $\chi_R(x_0,\dots,x_k)$ is
-computable. By Theorem~\olref[int]{thm:representable-iff-comp}, $\chi_R$ is
+computable. By \olref[int]{thm:representable-iff-comp}, $\chi_R$ is
 represented by a formula, say $!A_{\chi_R}(x_0,\dots,x_k,y)$. Let
 $!A_R(x_0,\dots,x_k)$ be the formula $!A_{\chi_R}(x_0,\dots,x_k,\num
 1)$. Then for any $n_0,\dots,n_k$, if $R(n_0,\dots,n_k)$ is true, then

incompleteness/representability-in-q/undecidability.tex

@@ -16,47 +16,46 @@
 $\Th{Q}$ would be decidable iff there were a computational procedure
 which decides, given a sentence~$A$ in the language of arithmetic,
 whether $\Th{Q} \Proves !A$ or not.  We can make this more precise by
-asking: Is the relation~$\fn{Prov}_{\Th{Q}}(x)$, which holds of~$x$
-iff $x$ is the G\"odel number of a sentence provable in~$\Th{Q}$,
+asking: Is the relation~$\fn{Prov}_{\Th{Q}}(y)$, which holds of~$y$
+iff $y$ is the G\"odel number of a sentence provable in~$\Th{Q}$,
 recursive?  The answer is: no. 
 
 \begin{thm}
 $\Th{Q}$ is undecidable, i.e., the relation 
 \[
-\fn{Prov}_{\Th{Q}}(x) \defiff \fn{Sent}(x) \land
-\lexists[y][\fn{Pr}_{\Th{Q}}(x, y)]
+\fn{Prov}_{\Th{Q}}(y) \defiff \fn{Sent}(y) \land
+\lexists[x][\fn{Pr}_{\Th{Q}}(x, y)]
 \]
 is not recursive.
 \end{thm}
 
 \begin{proof}
 Suppose it were.  Then we could solve the halting problem as follows:
 Given $e$ and $n$, we know that $\cfind{e}(n) \defined$ iff there is
-an~$s$ such that $T(e, x, s)$, where $T$ is Kleene's predicate from
-\olref[cmp][rec][nft]{thm:kleene-nf}. Since $\Char{T}$ is primitive
-recursive it is representable in~$\Th{Q}$ by a formula
-$!B_T(e,x,s,y)$, that is, $\Th{Q} \Proves !B_T(\num{e}, \num{x},
-\num{s}, \num{1})$ iff $T(e, x, s)$.  If $\Th{Q} \Proves !B_T(\num{e},
-\num{x}, \num{s}, \num{1})$ then also $\Th{Q} \Proves \Th{Q} \Proves
-\lexists[y][!B_T(\num{e}, \num{x}, y, \num{1})]$. If no such $s$
-exists, then $\Th{Q} \Proves \lnot !B_T(\num{e}, \num{x}, \num{s},
-\num{1})$ for every~$s$. Since $\Th{Q}$ is $\omega$-consistent,
-$\Th{Q} \Proves/ \lexists[y][!B_T(\num{e}, \num{x}, y, \num{1})]$.  In
-other words, $\Th{Q} \Proves \lexists[y][!B_T(\num{e}, \num{x}, y,
-  \num{1})]$ iff there is an $s$ such that $T(e, n, s)$, i.e., iff
-$\cfind{e}(n) \defined$.  From $e$ and~$n$ we can compute
-$\Gn{\lexists[y][!B_T(\num{e}, \num{n}, y, \num{1})]}$, let $g(e, n)$
-  be the primitive recursive function which does that. So
+an~$s$ such that $T(e, n, s)$, where $T$ is Kleene's predicate from
+\olref[cmp][rec][nft]{thm:kleene-nf}. Since $T$ is primitive recursive
+it is representable in~$\Th{Q}$ by a formula $!B_T$, that is, $\Th{Q}
+\Proves !B_T(\num{e}, \num{n}, \num{s})$ iff $T(e, n, s)$.  If $\Th{Q}
+\Proves !B_T(\num{e}, \num{n}, \num{s})$ then also $\Th{Q} \Proves
+\Th{Q} \Proves \lexists[y][!B_T(\num{e}, \num{n}, y)]$. If no such $s$
+exists, then $\Th{Q} \Proves \lnot !B_T(\num{e}, \num{n}, \num{s})$
+for every~$s$. Since $\Th{Q}$ is $\omega$-consistent, $\Th{Q} \Proves/
+\lexists[y][!B_T(\num{e}, \num{n}, y)]$.  In other words,
+$\Th{Q} \Proves \lexists[y][!B_T(\num{e}, \num{n}, y)]$ iff
+there is an $s$ such that $T(e, n, s)$, i.e., iff $\cfind{e}(n)
+\defined$.  From $e$ and~$n$ we can compute
+$\Gn{\lexists[y][!B_T(\num{e}, \num{n}, y)]}$, let $g(e, n)$
+be the primitive recursive function which does that. So
 \[
 h(e, n) = 
 \begin{cases}
 1 & \text{if $\fn{Pr}_{\Th{Q}}(g(e, n))$}\\
 0 & \text{otherwise}.
 \end{cases}
 \]
-This would show that $h$ is recursive if $\fn{Pr}_{\Th{Q}}$ is. But $h$ is not
-recursive, by \olref[cmp][rec][hlt]{thm:halting-problem}, so $\fn{Pr}_{\Th{Q}}$
-cannot be either.
+This would show that $h$ is recursive if $\fn{Pr}_{\Th{Q}}$ is. But
+$h$ is not recursive, by \olref[cmp][rec][hlt]{thm:halting-problem},
+so $\fn{Pr}_{\Th{Q}}$ cannot be either.
 \end{proof}
 
 \begin{cor}

open-logic-config.sty

@@ -470,21 +470,21 @@
 % - `\Prf`: the proof relation
 
 \DeclareDocumentCommand \Prf { o } { \mathrm{Pr}\IfNoValueTF {#1} {} {_\Th{#1}}}
-\DeclareDocumentCommand \OPrf { o } { \Obj{Pr}\IfNoValueTF {#1} {} {_\Th{#1}}}
+\DeclareDocumentCommand \OPrf { o } { \mathsf{Pr}\IfNoValueTF {#1} {} {_\Th{#1}}}
 
 % - `\Prov`: the provability relation
 
 \DeclareDocumentCommand \Prov { o } { \mathrm{Prov}\IfNoValueTF {#1} {} {_\Th{#1}}}
-\DeclareDocumentCommand \OProv { o } { \Obj{Prov}\IfNoValueTF {#1} {} {_\Th{#1}}}
+\DeclareDocumentCommand \OProv { o } { \mathsf{Prov}\IfNoValueTF {#1} {} {_\Th{#1}}}
 
 % - `\RProv`: the Rosser provability relation
 
 \DeclareDocumentCommand \RProv { o } { \mathrm{RProv}\IfNoValueTF {#1} {} {_\Th{#1}}}
-\DeclareDocumentCommand \ORProv { o } { \Obj{RProv}\IfNoValueTF {#1} {} {_\Th{#1}}}
+\DeclareDocumentCommand \ORProv { o } { \mathsf{RProv}\IfNoValueTF {#1} {} {_\Th{#1}}}
 
 % - `\OCon`: the consistency statement
 
-\DeclareDocumentCommand \OCon { o } { \Obj{Con}\IfNoValueTF {#1} {} {_\Th{#1}}}
+\DeclareDocumentCommand \OCon { o } { \mathsf{Con}\IfNoValueTF {#1} {} {_\Th{#1}}}
 
 % Typesetting commands for logical concepts
 % =========================================