
\documentclass[11pt]{article}
\usepackage{latexsym}
\usepackage{amssymb,amsmath}
\usepackage{bussproofs}
\usepackage{textcomp}
\usepackage{arcs}  % Used for \overarc command

\def\sequent{\,\mbox{\Large$\boldsymbol\rightarrow$}\,}
\def\limplies{{\rightarrow}}
\newcommand{\inftype}[2]{{\it #1:#2}}
\def\fCenter{\sequent}
\newcommand{\vect}[1]{{\bf #1}}
\newcommand{\highcap}{\overarc{\ \ }}
\newcommand{\Len}{\text{Len}}
\newcommand{\Seq}{\text{Seq}}
\newcommand{\N}{\mathbb{N}}

\def\studentName{Andy Parrish}
\def\lectureDate{Friday, May 4, 2012}

\begin{document}

\begin{center}
\bf Math 260A --- Mathematical Logic --- Scribe Notes \\
\bf UCSD --- Spring Quarter 2012 \\
\bf Instructor: Sam Buss \\[1ex]
\bf Notes by: \studentName{} \\
\bf \lectureDate \\
\end{center}

\section{Quantifier Complexity and Bounded Quantifiers}

So far we have used ordinary quantifiers $\forall$ and $\exists$.
In order to study quantifier complexity, we now introduce bounded
versions, defined here:
\[
(\forall y \le t) A(y) \leftrightarrow (\forall y) (y \le t \rightarrow A(y))
\]
\[
(\exists y \le t) A(y) \leftrightarrow (\exists y) (y \le t \wedge A(y))
\]
where $t$ is a term not involving $y$.

Define a formula to be $\Delta_0$ if all of its quantifiers are bounded.

We further define a sequence of classes of formulas.
\begin{itemize}
\item A $\Sigma_1$ formula has the form
  $(\exists y_1) \ldots (\exists y_k) \varphi(\vec{x}, \vec{y})$,
  where $\varphi$ is $Delta_0$.
\item A $\Pi_1$ formula has the form
  $(\forall y_1) \ldots (\forall y_k) \varphi(\vec{x}, \vec{y})$,
  where $\varphi$ is $Delta_0$.
\item A $\Sigma_2$ formula has the form
  $(\exists \vec{y}) (\forall \vec{z}) \varphi(\vec{x}, \vec{y}, \vec{z})$,
  where $\varphi$ is $Delta_0$. Equivalently, it has the form
  $\exists \vec{y} \psi(\vec{x}, \vec{y})$, where $\psi$ is $\Pi_1$.
\item Inductively, a formula is $\Sigma_n$ if it has the form
  $\exists \vec{y} \varphi(\vec{x}, \vec{y})$, where $\varphi$ is $\Pi_{n-1}$.
\item $\Pi_n$ is defined dually.
\end{itemize}

\paragraph{Note} In each of the above, we may take any of the quantifier blocks
to be empty so that, for example, $\Sigma_n \subseteq \Sigma_{n+1}$.

We now consider restricted induction axioms. If $\Phi$ is a class of formulas
(such as $\Delta_0$ or $\Sigma_3$), the $\Phi$ induction axioms are
\[
\{ A(0) \rightarrow (\forall x) (A(x) \rightarrow A(Sx)) \rightarrow (\forall x) A(x) : A \in \Phi \}.
\]

Denote by $I \Phi$ the axiom system $Q_{\le} + \Phi$-induction
axioms\footnote{It is possible to redefine the axioms of $Q_{\le}$
to use only bounded quantifiers.}
For example, $I \Delta_0$ allows induction on all $\Delta_0$ formulas. Last time
we showed that $I \Delta_0$ proves $x+y = y+x$.

We define Peano Arithmetic = $PA = \bigcup I \Sigma_n = \bigcup I \Pi_n$.


More generally, we define classes $\Sigma_n^+$ and $\Pi_n^+$. $\Sigma_2$,
for example, includes formulas of the form
$(\forall u \le t) \exists y \forall z \varphi(u, x, y, z)$,
where $\varphi$ is $\Delta_0$. Simply put, you get a $\Sigma_n^+$ formula
by taking any $\Sigma_n$ formula and inserting bounded quantifiers wherever
you like --- including inside of a quantifier block.

\subsection*{Collection property / replacement property}
The following is valid in $\N$:
\begin{equation}\label{eq:replacement}
(\forall y \le t) (\exists z) \varphi(y, z) \rightarrow
  (\exists u) (\forall y \le t) (\exists z \le u) \varphi(y, z).
\end{equation}
This serves to put a uniform bound on the $z$-values, which is possible
since there are only finitely many $y$ values being considered.

If $\varphi$ is in $\Sigma_n$ (for example), then \ref{eq:replacement}
is called a $\Sigma_n$-replacement axiom.

\paragraph{Theorem} Any $\Sigma_n^+$ formula is equivalent to a $\Sigma_n$
formula, and any $\Pi_n^+$ formula is equivalent to a $\Pi_n$ formula.

We prove the statement for $\Sigma_n^+$, and $\Pi_n^+$ follows dually.

Since the converse to \ref{eq:replacement} is trivial, we will instead show
both directions. We work by induction on $n$.\footnote{You may find yourself
asking: ``Are we allowed to do induction here?'' Remember: we are doing
induction ourselves, not in a restricted proof system.}

We take the inverse of the axiom, so we'll instead show:
\[
(\exists y \le t) \forall z \psi(y, z) \leftrightarrow
  \forall u \exists y \le t \forall z \le u \psi(y,z),
\]
where $\psi = \lnot \phi$.

Thus it is enough to show that, if $\chi \in \Sigma_n$, then so are
$(\forall y \le t) \chi$ and $(\exists y \le t) \chi$.

Since $\chi \in \Sigma_n$, it has the form $\exists z_1 \ldots \exists z_k \psi(y, \vec{z})$.
Thus we have
\[
\begin{array}{rcl}
(\forall y \le t) & \leftrightarrow & (\forall y \le t) \exists z_1 \ldots \exists z_k \psi(y, \vec{z}) \\
    & \leftrightarrow & (\exists u) (\forall y \le t) (\exists z_1 \le u) \exists z_2 \ldots
      \exists z_k \psi(y, \vec{z}) \\
    & \leftrightarrow & (\exists u) (\forall y \le t) \exists z_2 \ldots \exists z_k
      (\exists z_1 \le u) \psi(y, \vec{z}). \\
    & \leftrightarrow & [repeat $k-1$ times] \\
    & \leftrightarrow & (\exists u') (\forall y \le t) (\exists z_1 \le u') \ldots (\exists z_k \le u')
      \psi(y, \vec{z}). \\
\end{array}
\]

Note that the last portion of this formula,
$(\exists z_1 \le u') \ldots (\exists z_k \le u') \psi(y, \vec{z})$,
is a $\Pi_{n-1}^+$ formula, so the induction hypothesis gives us an equivalent
$\Pi_{n-1}$ formula $\psi'(y, \vec{u})$. This formula can now absorb the
$(\forall y \le t)$. Adding on the $(\exists u')$ on the front leaves us with
a $\Sigma_n$ formula, as desired.


\subsection*{Extending languages}

We often use $I \Delta_0$ as our base theory. This can prove statements
like $x+y=y+x$, which we proved earlier using quantifier-free induction.

Our language is only $\{0, S, +, \cdot, \le\}$, but we will also want
function symbols. We extend by conservative definitions, for example
\[
z | x \leftrightarrow \exists u (z \cdot u = x)
\]
and
\[
Prime(x) \leftrightarrow x \neq 1 \wedge (\forall z) (z | x \rightarrow z=1 \vee z=x).
\]
These definitions are fine, but we should be mindful of unbounded quantifiers.
In both cases, we can (and should) replace them with bounded quantifiers ---
both $u$ and $z$ may be bounded by $x$ without changing the meaning.

\paragraph{Definition}
A predicate $R(x_1, \ldots, x_k) \subseteq \N^k$ is $\Delta_0$ if there is a
$\Delta_0$ formula $\phi(\vec{x})$ so that
\[
\N \vDash \forall \vec{x} (R(\vec{x}) \leftrightarrow \phi(\vec{x})).
\]

\paragraph{Definition}
Let $T$ be a theory.
Let $R$ be as above. Then $T(R)$ is the theory $T$ in the language
of $T$ plus symbol $R$, whose axioms are the axioms of $T$, along
with the axiom $Defn_R := \forall \vec{x} (R(\vec{x}) \leftrightarrow \phi(\vec{x}))$.

\paragraph{Theorem} \ \newline
({\it a}) $T(R)$ is a conservative extension of $T$. \newline
({\it b}) Let $T$ be a theory from $I \Delta_0, I \Sigma_n, I \Pi_n$.
  Any bounded (ie $\Delta_0$) formula $\psi$ of $T(R)$ is $T(R)$-provably
  equivalent to a bounded formula $\chi$ in the language of $T$.

\paragraph{Proof} \ \newline
We showed ({\it a}) last quarter. \newline
For ({\it b}), find $\chi$ by replacing each instance of $R(\vec{t})$ in $\psi$
by $\phi(\vec{t})$. This maintains the quantifier complexity,
since $\phi$ is $\Delta_0$.

Note: if $\psi$ is $\Sigma_n$, so is $\chi$, independent of the theory
we're working in.


\end{document} 