Révision 172
| CSL17/arithmetic.tex (revision 172) | ||
|---|---|---|
| 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 |
Our base language is $\{ 0, \succ{} , + , \times, \smsh , |\cdot| , \leq \}$.
|
|
| 3 | 3 |
|
| 4 | 4 |
The $\basic$ axioms are as follows: |
| 5 | 5 |
\[ |
| 6 | 6 |
\begin{array}{l}
|
| 7 | 7 |
\safe (0) \\ |
| 8 |
\succ 0 = 0 \\ |
|
| 9 |
\safe (x) \cimp \safe (\succ i x) \\ |
|
| 8 |
\forall x^\safe . \safe (\succ{} x) \\
|
|
| 9 |
\forall x^\safe . 0 \neq \succ{} (x) \\
|
|
| 10 |
\forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) \\
|
|
| 11 |
\forall x^\safe . (x = 0 \cor \exists y^\safe.\ x = \succ{} y )
|
|
| 10 | 12 |
\end{array}
|
| 11 | 13 |
\] |
| 14 |
\anupam{in fact, we use essentially the same language, so just take Buss' Basic axioms after proper typing. Should also add the symbol $\hlf{\cdot}$ for binary predecessor then we have the full language of bounded arithmetic.}
|
|
| 12 | 15 |
|
| 16 |
|
|
| 17 |
|
|
| 18 |
\begin{definition}
|
|
| 19 |
[Derived functions and notations] |
|
| 20 |
We write $1,2,3,\dots$ for the terms $\succ{} 0, \succ{} \succ{} 0, \succ{} \succ{} \succ{} 0 \dots$, and frequently omit the $\times$ symbol.
|
|
| 21 |
We define the functions $\succ 0 x , \succ 1 x$ as $2 x$ and $2x +1$ respectively. |
|
| 22 |
\end{definition}
|
|
| 23 |
|
|
| 13 | 24 |
(Here use a variation of S12 with sharply bounded quantifiers and safe quantifiers) |
| 14 | 25 |
|
| 15 | 26 |
Use base theory + sharply bounded quantifiers. |
| 16 | 27 |
|
| 17 |
\anupam{Perhaps use prefix quantifier instead of sharply bounded (a la Ignatovic?), since plays nicer with sharply bounded lemma?}
|
|
| 18 | 28 |
|
| 19 | 29 |
|
| 20 | 30 |
|
| CSL17/ph-macros.tex (revision 172) | ||
|---|---|---|
| 25 | 25 |
|
| 26 | 26 |
\newcommand{\prefix}{\preccurlyeq}
|
| 27 | 27 |
|
| 28 |
\newcommand{\charfn}[2]{\chi^{#1}_{#2}}
|
|
| 28 | 29 |
\newcommand{\wit}[2]{\mathit{wit}^{#1}_{#2}}
|
| 29 | 30 |
\newcommand{\Wit}[2]{\mathit{Wit}^{#1}_{#2}}
|
| 30 | 31 |
\newcommand{\dfn}{:=}
|
| ... | ... | |
| 34 | 35 |
\renewcommand{\epsilon}{\varepsilon}
|
| 35 | 36 |
\newcommand{\pred}{p}
|
| 36 | 37 |
\renewcommand{\succ}[1]{s_{#1}}
|
| 38 |
\newcommand{\hlf}[1]{\lfloor \frac{#1}{2}\rfloor}
|
|
| 37 | 39 |
\newcommand{\cond}{C}
|
| 38 | 40 |
\newcommand{\smsh}{\#}
|
| 39 | 41 |
\newcommand{\pair}[3]{\langle ; #1,#2 , #3 \rangle}
|
| 42 |
\newcommand{\eq}{\textsc{eq}}
|
|
| 43 |
\newcommand{\leqfn}{\textsc{leq}}
|
|
| 40 | 44 |
|
| 41 | 45 |
|
| 42 |
\newcommand{\safe}{{S}}
|
|
| 43 |
\newcommand{\normal}{N}
|
|
| 46 |
\newcommand{\safe}{{N_0}}
|
|
| 47 |
\newcommand{\normal}{{N_1}}
|
|
| 44 | 48 |
|
| 45 | 49 |
\newcommand{\pv}{\mathit{PV}}
|
| 46 | 50 |
\newcommand{\pvbci}[1]{\pv^{#1}_{\mathrm{BC}}}
|
| CSL17/soundness.tex (revision 172) | ||
|---|---|---|
| 7 | 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 | 8 |
\end{theorem}
|
| 9 | 9 |
|
| 10 |
For this we will use length-bounded witnessing. |
|
| 11 | 10 |
|
| 11 |
|
|
| 12 |
The main problem for soundness is that we have predicates, for example equality, that take safe arguments in our theory but do not formally satisfy the polychecking lemma for $\mubc$ functions. |
|
| 13 |
For this we will use length-bounded witnessing, borrowing a similar idea from Bellantoni's previous work \cite{Bellantoni95}.
|
|
| 14 |
|
|
| 15 |
\begin{definition}
|
|
| 16 |
[Length bounded basic functions] |
|
| 17 |
We define \emph{length-bounded equality}, $\eq(l;x,y)$ as the characteristic function of the predicate:
|
|
| 18 |
\[ |
|
| 19 |
x \mode l = y \mode l |
|
| 20 |
\] |
|
| 21 |
\end{definition}
|
|
| 22 |
|
|
| 23 |
\anupam{Do we need the general form of length-boundedness? E.g. the $*$ functions from Bellantoni's paper? Put above if necessary. Otherwise just add sequence manipulation functions as necessary.}
|
|
| 24 |
|
|
| 25 |
Notice that $\eq$ is a polymax bounded polyomial checking function on its normal input, and so can be added to $\mubc$ without problems. |
|
| 26 |
|
|
| 27 |
\begin{definition}
|
|
| 28 |
[Length bounded characteristic functions] |
|
| 29 |
We define $\mubci{}$ programs $\charfn{}{A} (l , \vec u; \vec x)$, parametrised by a formula $A(\vec u ; \vec x)$, as follows.
|
|
| 30 |
% If $A$ is a $\Pi_{i}$ formula then:
|
|
| 31 |
\[ |
|
| 32 |
\begin{array}{rcl}
|
|
| 33 |
\charfn{}{s\leq t} (l, \vec u ; \vec x, w) & \dfn & \leqfn(;s,t) \\
|
|
| 34 |
\smallskip |
|
| 35 |
\charfn{}{s=t} (l, \vec u ; \vec x, w) & \dfn & \eq(;s,t) \\
|
|
| 36 |
\smallskip |
|
| 37 |
\charfn{}{\neg A} (l, \vec u ; \vec x, w) & \dfn & \neg (;\charfn{}{A}(l , \vec u ; \vec x)) \\
|
|
| 38 |
\smallskip |
|
| 39 |
\charfn{}{A\cor B} (l, \vec u ; \vec x , w) & \dfn & \cor (; \charfn{}{A} (\vec u ; \vec x , w), \charfn{}{B} (\vec u ;\vec x, w) ) \\
|
|
| 40 |
\smallskip |
|
| 41 |
\charfn{}{A\cand B} (l, \vec u ; \vec x , w) & \dfn & \cand(; \charfn{}{A} (\vec u ; \vec x , w), \charfn{}{B} (\vec u ;\vec x, w) ) \\
|
|
| 42 |
\smallskip |
|
| 43 |
\charfn{}{\exists x^\safe . A(x)} (l, \vec u ;\vec x, w) & \dfn & \begin{cases}
|
|
| 44 |
1 & \exists x^\safe . \charfn{}{A(x)} (\vec u ;\vec x , x, w) = 1 \\
|
|
| 45 |
0 & \text{otherwise}
|
|
| 46 |
\end{cases} \\
|
|
| 47 |
\smallskip |
|
| 48 |
\charfn{\vec u; \vec x}{\forall x^\safe . A(x)} (l, \vec u ;\vec x , w) & \dfn &
|
|
| 49 |
\begin{cases}
|
|
| 50 |
0 & \exists x^\sigma. \charfn{}{ A(x)} (\vec u; \vec x , x) = 0 \\
|
|
| 51 |
1 & \text{otherwise}
|
|
| 52 |
\end{cases}
|
|
| 53 |
\end{array}
|
|
| 54 |
\] |
|
| 55 |
\end{definition}
|
|
Formats disponibles : Unified diff