Uniform Heyting Arithmetic
Ulrich Berger, Wilfried Buchholz and Helmut Schwichtenberg

Abstract
We present an extension of Heyting Arithmetic in finite types called \emph{Uniform Heyting Arithmetic} that allows for the extraction of optimized programs from constructive and classical proofs. The system has two sorts of first-order quantifiers: ordinary quantifiers governed by the usual rules, and uniform quantifiers subject to stronger variable conditions expressing roughly that the quantified object is not computationally used in the proof. We combine a Kripke-style Friedman/Dragalin translation which is inspired by work of Coquand and Hofmann and a variant of the refined A-translation due to Buchholz, Schwichtenberg and the author to extract programs from a rather large class of classical first-order proofs while keeping explicit control over the levels of recursion and the decision procedures for predicates used in the extracted program.

Bib entry


@article{Berger0y,
   AUTHOR = {Berger, U.},
   TITLE = "Uniform {H}eyting {A}rithmetic",
   JOURNAL = "{A}nnals of {P}ure and {A}pplied {L}ogic",
   YEAR = "to appear"
}

Draft copy: [pdf] [ps]