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

\section{A two-sorted arithmetic for the polynomial hierarchy}

\newcommand{\nb}[1]{{\color{blue} NB: #1}}

%\newtheorem{theorem}{Theorem}

%\newtheorem{proposition}[theorem]{Proposition}

%\newtheorem{lemma}[theorem]{Lemma}

%

%

%\theoremstyle{definition}

%\newtheorem{definition}[theorem]{Definition}

\newcommand{\wit}[2]{\mathit{wit}^{#1}_{#2}}

\newcommand{\Wit}[2]{\mathit{Wit}^{#1}_{#2}}

\newcommand{\dfn}{:=}

\newcommand{\seqar}{\rightarrow}

\newcommand{\proves}{\vdash}

\newcommand{\safe}{\sigma}

\newcommand{\normal}{\nu}

\newcommand{\pv}{\mathit{PV}}

\newcommand{\pvbci}[1]{\pv^{#1}_{\mathrm{BC}}}

\newcommand{\mubci}[1]{\mu\mathrm{BC}^{#1}}

\newcommand{\bc}{\mathrm{BC}}

\newcommand{\fphi}[1]{\Box_{#1}}

	\newcommand{\ph}{\mathbf{PH}}

	\newcommand{\pspace}{\mathbf{PSPACE}}

	\newcommand{\fpspace}{\mathbf{FPSPACE}}

	\newcommand{\ptime}{\mathbf{P}}

	\newcommand{\fptime}{\mathbf{FP}}

	\newcommand{\nc}{\mathbf{NC}}

	\newcommand{\ac}{\mathbf{AC}}

	\newcommand{\exptime}{\mathbf{EXP}}

\newcommand{\cnot}{\neg}

\newcommand{\cimp}{\supset}

\newcommand{\cor}{\vee}

\newcommand{\cand}{\wedge}

\newcommand{\ciff}{\equiv}

\section{Introduction}

\label{sect:intro}

(Perhaps copy intro from DICE?)

\section{Conclusions}

\section{Preliminaries}

We introduce the polynomial hierarchy and its basic properties, then the Bellantoni characterisation.

\subsection{Polynomial hierarchy}

(include closure properties)

\subsection{Bellantoni's characterisation using predicative minimisation}

(perhaps compare with Cobham's using limited recursion)

\input{arithmetic}

\section{An extension of Bellantoni's theory PV for PH}

PVBC+FCA+ safe induction characterises PH

\subsection{Delineating levels using function ranks}