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

\documentclass[a4paper]{article}

\usepackage{amsmath}

\usepackage{amsthm}

\usepackage{amssymb}

\usepackage{microtype}

\usepackage[dvipsnames]{xcolor}

\usepackage{hyperref}

\bibliographystyle{plainurl}% the recommended bibstyle

\usepackage[lutzsyntax]{virginialake}

\input{ph-macros}

\begin{document}

\title{An implicit characterisation of the polynomial hierarchy in an unbounded arithmetic}

\author{Patrick Baillot}

\author{Anupam Das}

\maketitle

\begin{abstract}

We consider extensions of theories based on the Bellantoni-Cook function algebra for polynomial time functions ($\fptime$) by induction principles without bounds on quantifiers. Instead, we limit quantification to `safe' arguments and show that the provably total functions are just those of the functional polynomial hierarchy ($\fph$). Our witness extraction proof relies on \emph{free-cut elimination} in the logic, making use of the \emph{witness function method}, due to Buss, rather than realisability and Dialectica approaches more common in implicit complexity. Our results closely resemble analogous ones from bounded arithmetic, only for an unbounded setting, and the proof generalises those for previous approaches characterising $\fptime$ via ramified theories.

%\patrick{Remove: We present further comparisons to the bounded arithmetic setting and give tiered arithmetic theories analogous to the Si2 and Vi hierarchies of bounded arithmetic.}

\end{abstract}

%\begin{abstract}

%We consider extensions of equational theories based on the Bellantoni-Cook function algebra for FPTIME by induction principles without bounds on quantifiers. Instead, we limit quantification to 'safe' variables and show that the provably total functions are just those of FPH. This closely resembles analogous results from bounded arithmetic, only for an unbounded setting, and the proof generalises those for previous approaches characterising FPTIME via the Bellantoni-Cook framework. We present further comparisons to the bounded arithmetic setting and give two-sorted arithmetic theories analogous to the Si2 and Vi hierarchies of bounded arithmetic.

% \end{abstract}

\input{intro}

\input{preliminaries}

%\input{sequence-coding}

\input{arithmetic}

\input{soundness}

\input{completeness}

%\input{further}

\input{conclusions}

%\subparagraph*{Acknowledgements.}

%

%I want to thank \dots

%%

%% Bibliography

%%

%% Either use bibtex (recommended),

%\newpage

\bibliographystyle{alpha}

\bibliography{ph-biblio}

%% .. or use the thebibliography environment explicitely

\newpage

\appendix

%%\input{pv-theories}

\input{appendix-sequent-calculus}

\end{document}