Révision 168
| CSL17/arithmetic.tex (revision 168) | ||
|---|---|---|
| 1 | 1 |
\section{An arithmetic for the polynomial hierarchy}
|
| 2 |
Our base language is $\{ 0, \succ 0, \succ 1, \pred, + , \times, \smsh , |\cdot| , \leq \}$.
|
|
| 2 | 3 |
|
| 4 |
|
|
| 3 | 5 |
(Here use a variation of S12 with sharply bounded quantifiers and safe quantifiers) |
| 4 | 6 |
|
| 5 | 7 |
Use base theory + sharply bounded quantifiers. |
| 6 | 8 |
|
| 7 | 9 |
\anupam{Perhaps use prefix quantifier instead of sharply bounded (a la Ignatovic?), since plays nicer with sharply bounded lemma?}
|
| 8 | 10 |
|
| 11 |
|
|
| 12 |
|
|
| 9 | 13 |
\begin{definition}
|
| 10 | 14 |
[Quantifier hierarchy] |
| 11 | 15 |
We define: |
| ... | ... | |
| 15 | 19 |
\end{itemize}
|
| 16 | 20 |
\end{definition}
|
| 17 | 21 |
|
| 22 |
|
|
| 23 |
\anupam{Collection principles for prenexing? Otherwise need to add closure under sharply bounded quantifiers.}
|
|
| 24 |
|
|
| 25 |
|
|
| 18 | 26 |
\begin{definition}
|
| 19 | 27 |
Define the theory $\arith^i$ consisting of the following axioms: |
| 20 | 28 |
\begin{itemize}
|
| 21 | 29 |
\item $\basic$; |
| 22 | 30 |
\item $\cpind{\Sigma^\safe_i } $:
|
| 23 |
\item $\forall \vec x \in \normal . \exists y \in \safe . A \cimp \forall \vec x \in \normal .\exists y\in \normal . A$ (raising) . |
|
| 24 | 31 |
\end{itemize}
|
| 32 |
and an inference rule: |
|
| 33 |
\[ |
|
| 34 |
\dfrac{\forall \vec x^\normal . \exists y^\safe . A }{ \forall \vec x^\normal .\exists y^\normal . A}
|
|
| 35 |
\] |
|
| 25 | 36 |
\end{definition}
|
| 37 |
\anupam{In induction,for inductive cases, need $u\neq 0$ for $\succ 0$ case.}
|
|
| 26 | 38 |
|
| 27 |
|
|
| 28 | 39 |
\begin{lemma}
|
| 29 | 40 |
[Sharply bounded lemma] |
| 30 | 41 |
Let $f_A$ be the characteristic function of a predicate $A(u , \vec u ; \vec x)$. |
| ... | ... | |
| 42 | 53 |
\end{proof}
|
| 43 | 54 |
|
| 44 | 55 |
Notice that $\prefix$ suffices to encode usual sharply bounded inequalities, |
| 45 |
since $\forall u \leq |t| . A(u , \vec u ; \vec x) \ciff \forall u \prefix t . A(|u|, \vec u ; \vec x)$. |
|
| 56 |
since $\forall u \leq |t| . A(u , \vec u ; \vec x) \ciff \forall u \prefix t . A(|u|, \vec u ; \vec x)$. |
|
| 57 |
|
|
| 58 |
|
|
| 59 |
\subsection{Graphs of some basic functions}
|
|
| 60 |
Todo: $+1$, |
|
| 61 |
|
|
| 62 |
\subsection{Encoding sequences in the arithmetic}
|
|
| 63 |
\todo{}
|
|
| 64 |
|
|
| 65 |
\anupam{Assume we have a $\Sigma^\safe_1$ predicate $\beta(i,x,y)$, expressing that the $i$th element of the sequence $x$ is $y$, such that $\arith^1 \proves \forall i^\normal , x^\safe . \exists ! y^\safe . \beta (i,x,y)$.}
|
|
| 66 |
|
|
| 67 |
|
|
| 68 |
\subsection{A sequent calculus presentation}
|
|
| 69 |
\todo{Write out usual first-order sequent calculus}
|
|
| 70 |
|
|
| 71 |
\subsection{Free-cut free normal form of proofs}
|
|
| 72 |
\todo{State theorem, with references (Takeuti, Cook-Nguyen) and present the important corollaries for this work.}
|
|
| CSL17/ph-macros.tex (revision 168) | ||
|---|---|---|
| 20 | 20 |
\newcommand{\pind}{\mathit{PIND}}
|
| 21 | 21 |
\newcommand{\cind}[1]{#1\text{-}\ind}
|
| 22 | 22 |
\newcommand{\cpind}[1]{#1\text{-}\pind}
|
| 23 |
\renewcommand{\min}{\mathit{MIN}}
|
|
| 24 |
\newcommand{\cmin}[1]{#1\text{-}\min}
|
|
| 23 | 25 |
|
| 24 | 26 |
\newcommand{\prefix}{\preccurlyeq}
|
| 25 | 27 |
|
| ... | ... | |
| 31 | 33 |
|
| 32 | 34 |
\renewcommand{\epsilon}{\varepsilon}
|
| 33 | 35 |
\newcommand{\pred}{p}
|
| 34 |
\renewcommand{\succ}[1]{s_i}
|
|
| 36 |
\renewcommand{\succ}[1]{s_{#1}}
|
|
| 35 | 37 |
\newcommand{\cond}{C}
|
| 38 |
\newcommand{\smsh}{\#}
|
|
| 36 | 39 |
|
| 37 | 40 |
\newcommand{\safe}{{S}}
|
| 38 | 41 |
\newcommand{\normal}{N}
|
| CSL17/further.tex (revision 168) | ||
|---|---|---|
| 1 |
\section{Further results}
|
|
| 1 |
\section{Further results}
|
|
| 2 |
|
|
| 3 |
\subsection{Equational theories}
|
|
| 4 |
\todo{Mention PVBC}
|
|
| 5 |
|
|
| 6 |
\subsection{Modal and second order theories}
|
|
| 7 |
\todo{Mention links with ramification/sortedness}
|
|
| CSL17/completeness.tex (revision 168) | ||
|---|---|---|
| 5 | 5 |
\begin{theorem}
|
| 6 | 6 |
\label{thm:completeness}
|
| 7 | 7 |
For every $\mubci{i-1}$ program $f(\vec u ; \vec x)$ (which is in $\fphi i$), there is a $\Sigma_i$ formula $A_f(\vec u, \vec x)$ such that $\arith^i$ proves $\forall \vec u \in \normal . \forall \vec x \in \safe. \exists ! y \in \safe . A_f(\vec u , \vec x , y )$ and $\Nat \models \forall \vec u , \vec x. A(\vec u , \vec x , f(\vec u ; \vec x))$.
|
| 8 |
\end{theorem}
|
|
| 8 |
\end{theorem}
|
|
| 9 |
|
|
| 10 |
The rest of this section is devoted to a proof of this theorem. |
|
| 11 |
We proceed by structural induction on a $\mubc{i-1} $ program, dealing with each case in the proceeding paragraphs.
|
|
| 12 |
|
|
| 13 |
\paragraph*{Predicative minimisation}
|
|
| 14 |
Suppose $f(\vec u ; \vec x)$ is defined as $\mu x^{+1} . g(\vec u ; \vec x , x) =_2 0$.
|
|
| 15 |
By definition $g$ is in $\mubci{i-2}$, and so by the inductive hypothesis there is a $\Sigma_{i-1}$ formula $A_g (\vec u , \vec x , x , y)$ computing the graph of $g$ such that,
|
|
| 16 |
\[ |
|
| 17 |
\arith^i \proves \forall \vec u^\normal . \forall \vec x^\safe , x^\safe . \exists ! y^\safe . A_g(\vec u , \vec x , x , y) |
|
| 18 |
\] |
|
| 19 |
Let us define $A_f(\vec u ; \vec x , z)$ as: |
|
| 20 |
\[ |
|
| 21 |
\begin{array}{rl}
|
|
| 22 |
&\left( |
|
| 23 |
z=0 \ \cand \ \forall x^\safe , y^\safe . (A_g (\vec u , \vec x , x, y) \cimp y=_2 1) |
|
| 24 |
\right) \\ |
|
| 25 |
\cor & \left( |
|
| 26 |
\begin{array}{ll}
|
|
| 27 |
z\neq 0 |
|
| 28 |
& \cand\ \forall y^\safe . (A_g (\vec u , \vec x , p z , y) \cimp y=_2 0 ) \\ |
|
| 29 |
& \cand\ \forall x^\safe < p z . \forall y^\safe . (A_g (\vec u , \vec x , x , y) \cimp y=_2 1) |
|
| 30 |
\end{array}
|
|
| 31 |
\right) |
|
| 32 |
\end{array}
|
|
| 33 |
\] |
|
| 34 |
Notice that $A_f$ is $\Pi_{i-1}$, since $A_g$ is $\Sigma_{i-1}$ and occurs only in negative context above, with additional safe universal quantifiers occurring in positive context.
|
|
| 35 |
In particular this means $A_f$ is $\Sigma_i$. |
|
| 36 |
|
|
| 37 |
Now, to prove totality of $A_f$, we rely on $\Sigma^\safe_{i-1}$-minimisation, which is a consequence of $\cpind{\Sigma^\safe_i}$:
|
|
| 38 |
|
|
| 39 |
\begin{lemma}
|
|
| 40 |
[Minimisation] |
|
| 41 |
$\arith^i \proves \cmin{\Sigma^\safe_{i-1}}$.
|
|
| 42 |
\end{lemma}
|
|
| 43 |
\begin{proof}
|
|
| 44 |
\todo{}
|
|
| 45 |
\end{proof}
|
|
| 46 |
|
|
| 47 |
Now, working in $\arith^i$, let $\vec u \in \normal , \vec x \in \safe$ and let us prove: |
|
| 48 |
\[ |
|
| 49 |
\exists !z^\safe . A_f(\vec u ; \vec x , z) |
|
| 50 |
\] |
|
| 51 |
Suppose that $\exists x^\safe , y^\safe . (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$. |
|
| 52 |
We can apply minimisation due to the lemma above to find the least $x\in \safe$ such that $\exists y^\safe . (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$, and we set $z = \succ 1 x$. |
|
| 53 |
\todo{verify $z\neq 0$ disjunct.}
|
|
| 54 |
|
|
| 55 |
Otherwise, we have that $\forall x^\safe , y^\safe . (A_g (\vec u , \vec x , x, y) \cimp y=_2 1)$ and so we can set $z=0$. |
|
| 56 |
|
|
| 57 |
|
|
| 58 |
\paragraph*{Predicative recursion on notation}
|
|
| 59 |
Now suppose that $f$ is defined by PRN: |
|
| 60 |
\[ |
|
| 61 |
\begin{array}{rcl}
|
|
| 62 |
f(0 , \vec u ; \vec x) & \dfn & g(\vec u ; \vec x) \\ |
|
| 63 |
f(\succ i u, \vec u ; \vec x) & \dfn & h_i( u , \vec u ; \vec x , f(u , \vec u ; \vec x)) |
|
| 64 |
\end{array}
|
|
| 65 |
\] |
|
| 66 |
|
|
| 67 |
\anupam{using $\beta(i,x,y)$ predicate for sequences: ``$i$th element of $x$ is $y$''. Provably total in $\arith^1$.}
|
|
| 68 |
|
|
| 69 |
Suppose we have $\Sigma^\safe_i$ formulae $A_g (\vec u ; \vec x,y)$ and $A_{h_i} (u , \vec u ; \vec x , y , z)$ computing the graphs of $g$ and $h_i$ respectively, provably total in $\arith^i$.
|
|
| 70 |
We define $A_f (u ,\vec u ; \vec x , y)$ as, |
|
| 71 |
\[ |
|
| 72 |
\exists w^\safe . \left( |
|
| 73 |
\begin{array}{ll}
|
|
| 74 |
& |
|
| 75 |
%Seq(z) \cand |
|
| 76 |
\exists y_0 . ( A_g (\vec u , \vec x , y_0) \cand \beta(0, w , y_0) ) \cand \beta(|u|, w,y ) \\ |
|
| 77 |
\cand & \forall k < |u| . \exists y_k , y_{k+1} . ( \beta (k, w, y_i) \cand \beta (k+1 ,w, y_{k+1}) \cand A_{h_i} (u , \vec u ; \vec x , y_k , y_{k+1}) )
|
|
| 78 |
\end{array}
|
|
| 79 |
\right) |
|
| 80 |
\] |
|
| 81 |
which is $\Sigma^\safe_i$ by inspection, and indeed defines the graph of $f$. |
|
| 82 |
|
|
| 83 |
To show totality, let $\vec u \in \normal, \vec x \in \safe$ and proceed by induction on $u \in \normal$. |
|
| 84 |
The base case, when $u=0$, is immediate from the totality of $A_g$, so for the inductive case we need to show: |
|
| 85 |
\[ |
|
| 86 |
\exists y^\safe . A_f (u , \vec u ; \vec x , y) |
|
| 87 |
\quad \seqar \quad |
|
| 88 |
\exists z^\safe . A_f (s_i u, \vec u ; \vec x , y) |
|
| 89 |
\] |
|
| 90 |
|
|
| 91 |
\anupam{here need to `add' element to the computation sequence. Need to do this earlier in the paper.}
|
|
| 92 |
|
|
| 93 |
\anupam{for inductive cases, need $u\neq 0$ for $\succ 0$ case.}
|
|
| 94 |
|
|
| 95 |
\paragraph*{Safe composition}
|
|
| 96 |
Now suppose that $f$ is defined by safe composition: |
|
| 97 |
\[ |
|
| 98 |
f(\vec u ; \vec x) \quad \dfn \quad g( \vec h(\vec u;) ; \vec h' (\vec u ; \vec x) ) |
|
| 99 |
\] |
|
| 100 |
|
|
| 101 |
By the inductive hypothesis, let us suppose that we have $\Sigma^\safe_i $ definitions $A_g , A_{h_i} , A_{h_j'} $ of the graphs of $g , h_i , h_j'$ respectively, which are provably total etc.
|
|
| 102 |
In particular, by Raising, we have that $\forall \vec u^\normal . \exists v^\normal . A_{h_i} (\vec u , v)$.
|
|
| 103 |
|
|
| 104 |
We define $A_f (\vec u , \vec x , z)$ defining the graph of $f$ as follows: |
|
| 105 |
\[ |
|
| 106 |
\exists \vec v^\normal . \exists \vec y^\safe . |
|
| 107 |
\left( |
|
| 108 |
\bigwedge\limits_i A_{h_i} (\vec u , v_i)
|
|
| 109 |
\wedge |
|
| 110 |
\bigwedge\limits_j A_{h_j'} (\vec u ; \vec x , y_j)
|
|
| 111 |
\wedge |
|
| 112 |
A_g ( \vec v , \vec y , z ) |
|
| 113 |
\right) |
|
| 114 |
\] |
|
| 115 |
The provable totality of $A_f$ follows from simple first-order reasoning, mostly cuts and basic quantifier manipulations. |
|
| 116 |
|
|
| 117 |
\todo{elaborate}
|
|
| 118 |
|
|
| 119 |
\paragraph*{Other cases}
|
|
| 120 |
\todo{}
|
|
| 121 |
|
|
| 122 |
|
|
| 123 |
|
|
| 124 |
|
|
| 125 |
|
|
| 126 |
|
|
| 127 |
|
|
| 128 |
|
|
| 129 |
|
|
| 130 |
|
|
| 131 |
|
|
| 132 |
|
|
| 133 |
|
|
| 134 |
|
|
| 135 |
|
|
| 136 |
|
|
| 137 |
|
|
| 138 |
|
|
| 139 |
|
|
| 140 |
|
|
| 141 |
|
|
| 142 |
|
|
| 143 |
|
|
| 144 |
|
|
| CSL17/soundness.tex (revision 168) | ||
|---|---|---|
| 1 | 1 |
\section{Soundness}
|
| 2 |
\label{sect:soundness}
|
|
| 3 |
|
|
| 4 |
The main result of this section is the following: |
|
| 5 |
|
|
| 6 |
\begin{theorem}
|
|
| 7 |
If $\arith^i$ proves $\forall \vec u^\normal . \forall \vec x^\safe . \exists y^\safe . A(\vec u ; \vec x , y)$ then there is a $\mubci{i-1}$ program $f(\vec u ; \vec x)$ such that $\Nat \models A(\vec u ; \vec x , f(\vec u ; \vec x))$.
|
|
| 8 |
\end{theorem}
|
|
| 9 |
|
|
| CSL17/preliminaries.tex (revision 168) | ||
|---|---|---|
| 46 | 46 |
\begin{enumerate}
|
| 47 | 47 |
\item The constant functions $\epsilon^k$ which takes $k$ arguments and outputs $\epsilon \in \Word$. |
| 48 | 48 |
\item The projection functions $\pi^{m,n}_k ( x_1 , \dots , x_m ; x_{m+1} , \dots, x_{m+n} ) := x_k$ for $n,m \in \Word$ and $1 \leq k \leq m+n$.
|
| 49 |
\item The successor functions $\succ_i ( ; x) := xi$ for $i = 0,1$.
|
|
| 49 |
\item The successor functions $\succ i ( ; x) := xi$ for $i = 0,1$.
|
|
| 50 | 50 |
\item The predecessor function $\pred (; x) := \begin{cases}
|
| 51 | 51 |
\epsilon & \mbox{ if } x = \epsilon \\
|
| 52 | 52 |
x' & \mbox{ if } x = x'i
|
| ... | ... | |
| 77 | 77 |
\[ |
| 78 | 78 |
\begin{array}{rcl}
|
| 79 | 79 |
f(0, \vec v ; \vec x) & := & g(\vec v ; \vec x) \\ |
| 80 |
f (\succ_i u , \vec v ; \vec x ) & := & h_i ( u , \vec v ; \vec x , f (u , \vec v ; \vec x) )
|
|
| 80 |
f (\succ i u , \vec v ; \vec x ) & := & h_i ( u , \vec v ; \vec x , f (u , \vec v ; \vec x) )
|
|
| 81 | 81 |
\end{array}
|
| 82 | 82 |
\] |
| 83 | 83 |
for $i = 0,1$, so long as the expressions are well-formed. % (i.e.\ in number/sort of arguments). |
| ... | ... | |
| 101 | 101 |
\[ |
| 102 | 102 |
\begin{array}{rcl}
|
| 103 | 103 |
f^j(0, \vec v ; \vec x) & := & g^j(\vec v ; \vec x) \\ |
| 104 |
f^j(\succ_i u , \vec v ; \vec x ) & := & h^j_i ( u , \vec v ; \vec x , \vec{f} (u , \vec v ; \vec x) )
|
|
| 104 |
f^j(\succ i u , \vec v ; \vec x ) & := & h^j_i ( u , \vec v ; \vec x , \vec{f} (u , \vec v ; \vec x) )
|
|
| 105 | 105 |
\end{array}
|
| 106 | 106 |
\] |
| 107 | 107 |
for $i = 0,1$, so long as the expressions are well-formed. |
Formats disponibles : Unified diff