Révision 220 CSL17/arithmetic.tex
| arithmetic.tex (revision 220) | ||
|---|---|---|
| 1 | 1 |
\section{An arithmetic for the polynomial hierarchy}\label{sect:arithmetic}
|
| 2 | 2 |
%Our base language is $\{ 0, \succ{} , + , \times, \smsh , |\cdot| , \leq \}$.
|
| 3 |
Our base language is defined by the set of functions (and constants) symbols $\{ 0, \succ{} , + , \times, \smsh , |\cdot|, \hlf{}.\}$ and the set of predicate symbols
|
|
| 4 |
$\{\leq, \safe, \normal \}$. The intended meaning of $|x|$ is the length of $x$ seen as a binary string, and that of $\smash(x,y)$ is $2^{|x||y|}$, so a string of length $|x||y|+1$.
|
|
| 3 |
Our base language consists of constant and function symbols $\{ 0, \succ{} , + , \times, \smsh , |\cdot|, \hlf{}.\}$ and predicate symbols
|
|
| 4 |
$\{\leq, \safe, \normal \}$. The function symbols are interpreted in the intuitive way, with $|x|$ denoting the length of $x$ seen as a binary string, and $\smash(x,y)$ denoting $2^{|x||y|}$, so a string of length $|x||y|+1$.
|
|
| 5 |
We may write $\succ{0}(x)$ for $2\cdot x$, $\succ{1}(x)$ for $\succ{}(2\cdot x)$, and $\pred (x)$ for $\hlf{x}$, to better relate to the $\bc$ setting.
|
|
| 5 | 6 |
|
| 6 |
We use classical logic connectives $\neg$, $\cand$, $\cor$, $\forall$, $\exists$. The formula $A \cimp B$ will be a notation for $\neg A \cor B$. |
|
| 7 |
We will also use as shorthand notations: |
|
| 8 |
$$ (s=t) = (s\leq t) \cand (t\leq s), \quad (s\neq t) = \neg(s=t).$$ |
|
| 9 |
We call \textit{atomic formulas} formulas of the form $(s\leq t)$ or $(s=t)$.
|
|
| 10 |
As we are in classical logic, we will assume, without loss of generality, that formulas are in \textit{De Morgan normal form}, that is to say that in formulas negation can only occur on atomic formulas, and that there is not any occurrence of subformula of the form $\neg \neg A$.
|
|
| 7 |
We consider formulas of classical first-order logic, over $\neg$, $\cand$, $\cor$, $\forall$, $\exists$, along with usual shorthands and abbreviations. |
|
| 8 |
%The formula $A \cimp B$ will be a notation for $\neg A \cor B$. |
|
| 9 |
%We will also use as shorthand notations: |
|
| 10 |
%$$ (s=t) = (s\leq t) \cand (t\leq s), \quad (s\neq t) = \neg(s=t).$$ |
|
| 11 |
\textit{Atomic formulas} formulas are of the form $(s\leq t)$, for terms $s,t$.
|
|
| 12 |
We will assume, without loss of generality, that formulas are in \textit{De Morgan normal form}, that is to say that in formulas negation can only occur on atomic formulas, and that there is not any occurrence of a subformula of the form $\neg \neg A$.
|
|
| 13 |
We write $\exists x^{N_i} . A$ or $\forall x^{N_i} . A$ for $\exists x . (N_i (x) \cand A)$ and $\forall x . (N_i (x) \cimp A)$ respectively.
|
|
| 11 | 14 |
|
| 12 |
In the sequel $\succ{0}(x)$ stand for $2\cdot x$ and $\succ{1}(x)$ stand for $\succ{}(2\cdot x)$,
|
|
| 13 |
Now, let us describe the axioms we are considering.The $\basic$ axioms are as follows: |
|
| 14 |
\[ |
|
| 15 |
\begin{array}{l}
|
|
| 16 |
\safe (0) \\ |
|
| 17 |
\forall x^\safe . \safe (\succ{} x) \\
|
|
| 18 |
\forall x^\safe . 0 \neq \succ{} (x) \\
|
|
| 19 |
\forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) \\
|
|
| 20 |
\forall x^\safe . (x = 0 \cor \exists y^\safe.\ x = \succ{} y )\\
|
|
| 21 |
\forall x^\safe, y^\safe . \safe(x+y)\\ |
|
| 22 |
\forall u^\normal, x^\safe . \safe(u\times x) \\ |
|
| 23 |
\forall u^\normal , v^\normal . \safe (u \smsh v)\\ |
|
| 24 |
\forall u^\normal \safe(u) \\ |
|
| 25 |
\forall u^\safe \safe(\hlf{u})\\
|
|
| 26 |
\forall x^\safe \safe(|x|) |
|
| 27 |
\end{array}
|
|
| 28 |
\] |
|
| 29 |
%\patrick{did I type writly the 2 last axioms?}
|
|
| 30 | 15 |
|
| 31 |
and the list of axioms of Appendix \ref{appendix:arithmetic}, coming from \cite{Buss86book}.
|
|
| 16 |
The theories we introduce are directly inspired from bounded arithmetic, namely the theories $S^i_2$. |
|
| 17 |
We include a similar set of axioms for direct comparison, although in our setting these are not minimal. |
|
| 18 |
Indeed, $\#$ can be defined using induction in our setting. |
|
| 32 | 19 |
|
| 33 |
\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.}
|
|
| 20 |
The $\basic$ axioms of bounded arithmetic give the inductive definitions and interrelationships of the various function symbols. |
|
| 21 |
It also states the fundamental algebraic properties, i.e.\ $(0,\succ{ } )$ is a free algebra, and, for us, it will also give us certain `typing' information for our function symbols based on their $\bc$ specification, with safe inputs ranging over $\safe$ and normal ones over $\normal$.
|
|
| 22 |
\begin{definition}
|
|
| 23 |
[Basic theory] |
|
| 24 |
The theory $\basic$ consists of the axioms from Appendix \ref{appendix:arithmetic}.
|
|
| 25 |
\end{definition}
|
|
| 34 | 26 |
|
| 35 | 27 |
|
| 36 | 28 |
Notation: if $\vec t=t_0,\dots, t_k$, we will denote as $\safe(\vec t)$ the sequence of formulas $\safe(t_0),\dots, \safe(t_k)$. Similarly for $\normal(\vec t)$. |
| ... | ... | |
| 108 | 100 |
Let us refer to the axiom schema in \eqref{eqn:lind} as $\clind{\mathcal C}$, when $A \in \mathcal C$.
|
| 109 | 101 |
We will freely use this in place of polynomial induction whenever it is convenient. |
| 110 | 102 |
|
| 111 |
\begin{lemma}
|
|
| 112 |
[Sharply bounded lemma] |
|
| 113 |
\label{lem:sharply-bounded-recursion}
|
|
| 114 |
Let $f_A$ be the characteristic function of a predicate $A(u , \vec u ; \vec x)$. |
|
| 115 |
Then the characteristic functions of $\forall u \prefix v . A(u,\vec u ; \vec x)$ and $\exists u \prefix v . A(u , \vec u ; \vec x)$ are in $\bc(f_A)$. |
|
| 116 |
\end{lemma}
|
|
| 117 |
\begin{proof}
|
|
| 118 |
We give the $\forall$ case, the $\exists$ case being dual. |
|
| 119 |
The characteristic function $f(v , \vec u ; \vec x)$ is defined by predicative recursion on $v$ as: |
|
| 120 |
\[ |
|
| 121 |
\begin{array}{rcl}
|
|
| 122 |
f(0, \vec u ; \vec x) & \dfn & f_A (0 , \vec u ; \vec x) \\ |
|
| 123 |
f(\succ i v , \vec u ; \vec x) & \dfn & \cond ( ; f_A (\succ i v, \vec u ; \vec x) , 0 , f(v , \vec u ; \vec x) ) |
|
| 124 |
\end{array}
|
|
| 125 |
\] |
|
| 126 |
\end{proof}
|
|
| 127 | 103 |
|
| 128 |
Notice that $\prefix$ suffices to encode usual sharply bounded inequalities, |
|
| 129 |
since $\forall u \leq |t| . A(u , \vec u ; \vec x) \ciff \forall u \prefix t . A(|u|, \vec u ; \vec x)$. |
|
| 130 | 104 |
|
| 131 | 105 |
|
| 132 | 106 |
\subsection{Graphs of some basic functions}\label{sect:graphsbasicfunctions}
|
Formats disponibles : Unified diff