Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

\section{An arithmetic for the polynomial hierarchy}

%Our base language is $\{ 0, \succ{} , + , \times, \smsh , |\cdot| , \leq \}$. 

 $\{\leq, \safe, \normal \}$.

We use classical logic connectives $\neg$, $\cand$, $\cor$, $\forall$, $\exists$. The formula $A \cimp B$ will be a notation for $\neg A \cor B$.

We will also use as shorthand notations:

We call \textit{atomic formulas} formulas of the form $(s\leq t)$ or $(s=t)$.

 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$.

Now, let us describe the axioms we are considering.The $\basic$ axioms are as follows:

\[

\begin{array}{l}

\forall x^\safe, y^\safe . \safe(x+y)\\

\forall u^\normal, x^\safe . \safe(u\times x) \\

\forall u^\normal , v^\normal . \safe (u \smsh v)\\

\end{array}

\]

\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.}