Sean's changes #39

Author: seanrsinclair

computability/recursive-functions/bounded-minimization.tex

@@ -21,8 +21,8 @@
 \end{prop}
 
 \begin{proof}
-Note than there can be no~$x < y$ such that $R(x, \vec{z})$ since
-there is no $x < y$ at all.  So $m_R(x, 0) = 0$.
+Note than there can be no~$x < 0$ such that $R(x, \vec{z})$ since
+there is no $x < 0$ at all.  So $m_R(x, 0) = 0$.
 
 In case the bound is $y + 1$ we have three cases: (a) There is an $x <
 y$ such that $R(x, \vec{z})$, in which case $m_R(y+1, \vec{z}) =

incompleteness/arithmetization-syntax/coding-formulas.tex

@@ -16,15 +16,20 @@
 
 \begin{proof}
 The number $x$ is the G\"odel number of an atomic !!{formula} iff
+one of the following holds:
 \begin{enumerate}
-\item there are $n$, $j < x$, and $z < x$ such that for each $i < n$,
+\item There are $n$, $j < x$, and $z < x$ such that for each $i < n$,
   $\fn{Term}((z)_i)$ and
 \[
-x = \Gn{\Obj P^n_j(} \concat \fn{flatten}(z) \concat \Gn{)} \text{, or}
+x = \Gn{\Obj P^n_j(} \concat \fn{flatten}(z) \concat \Gn{)}.
 \]
-\item there are $z_1, z_2 < x$ such that $x = z_1 \concat \Gn{\eq}
-  \concat \eq z_2$ and $\fn{Term}(z_1)$ and $\fn{Term}(z_2)$.
-% Missing the case for bottom
+\item There are $z_1, z_2 < x$ such that $\fn{Term}(z_1)$,
+  $\fn{Term}(z_2)$, and 
+\[
+x = z_1 \concat \Gn{\eq} \concat z_2.
+\]
+  \tagitem{prvFalse}{$x = \Gn{\lfalse}$.}{}
+  \tagitem{prvTrue}{$x = \Gn{\ltrue}$.}{}
 \end{enumerate}
 \end{proof}
 

incompleteness/arithmetization-syntax/coding-symbols.tex

@@ -42,9 +42,8 @@
 \end{array}
 \]
 \item If $s$ is the $i$-th variable $\Obj x_i$, then $\scode s = \tuple{1, i}$.
-\item If $s$ is the $i$-th $n$-ary !!{constant}~$\Obj c_i^n$, then
-  $\scode s = \tuple{2, n, i}$.
-% n-ary constant symbols?
+\item If $s$ is the $i$-th !!{constant}~$\Obj c_i^n$, then
+  $\scode s = \tuple{2, i}$.
 \item If $s$ is the $i$-th $n$-ary !!{function}~$\Obj f_i^n$, then
   $\scode s = \tuple{3, n, i}$.
 \item If $s$ is the $i$-th $n$-ary !!{predicate}~$\Obj P_i^n$, then

incompleteness/incompleteness-provability/rosser-thm.tex

@@ -47,6 +47,13 @@
 doesn't prove $\lnot !R_\Th{T}$. (In other words, we don't need the
 assumption of $\omega$-consistency.)
 
+
+\end{document}
+
+% Following digression should only be included if
+% incompleteness/theories-computability/first-incompleteness.tex also
+% compiled.
+
 \begin{digress}
 % This comment doesn't make much sense, what are you trying to get at?
 By comparison to the proof of
@@ -57,5 +64,3 @@
 G\"odel-Rosser methods therefore have the advantage of making the
 independent statement perfectly clear.
 \end{digress}
-
-\end{document}

incompleteness/representability-in-q/introduction.tex

@@ -27,15 +27,14 @@
 (to be used in conjunction with the other axioms and rules of
 first-order logic with !!{identity}):
 \begin{enumerate}
-% Maybe add the quantifiers here.
-\item $x' = y' \lif x = y$
-\item $\eq/[0][x']$
-\item $\eq/[x][0] \lif \lexists[y][\eq[x][y']]$
-\item $x+0 = x$
-\item $x+ y' = (x+y)'$
-\item $x \times 0 = 0$
-\item $x \times y' = x \times y + x$
-\item $x < y \liff \lexists[z][(z' + x) = y]$
+\item $\lforall[x][\lforall[y][x' = y' \lif x = y]]$
+\item $\lforall[x][\eq/[0][x']]$
+\item $\lforall[x][\eq/[x][0] \lif \lexists[y][\eq[x][y']]]$
+\item $\lforall[x][(x+0) = x]$
+\item $\lforall[x][\lforall[y][(x+ y') = (x+y)']]$
+\item $\lforall[x][(x \times 0) = 0]$
+\item $\lforall[x][\lforall[y][(x \times y') = ((x \times y) + x)]]$
+\item $\lforall[x][\lforall[y][x < y \liff \lexists[z][(z' + x) = y]]]$
 \end{enumerate}
 For each natural number $n$, define the numeral $\bar n$ to be the
 term $0^{''\ldots'}$ where there are $n$ tick marks in all.