Logic & Programming

Basic Arithmetic (BA) is the theory obtained by putting the usual axioms of Peano or Heyting Arithmetic atop of Basic Predicate Calculus (BQC). BQC can be seen as intuitionistic predicate calculus (IQC) with a weakened form of implication, or as geometric logic with the addition of a restricted form of implication. Essentially, the form of implications allowed is the following one: the right hand side of an implication can never be a disjunction or an existential quantification, while the left hand side must be a disjunction or an existential quantification.

The paper shows that every provably total function in BA is definable by a geometric formula and is primitive recursive. However, not all primitive recursive functions are provably total in BA. The paper investigates three extensions of BA for which the classes of provably total functions and primitive recursive functions coincide: – BA with the axiom $\neg\top\Rightarrow\bot$ – BA with the cancellation law $x+y=x+z \Rightarrow y=z$ – BA with cut-off subtraction $x\leq y \Rightarrow x\dot- y = 0$

Moreover, the authors investigate the status of the Matiyasevich-Robinson-Davis-Putnam (MRDP) theorem on the existence of Diophantine equations equivalent to $\Sigma_1$ formulas for BA and the three extensions: only the first of the extensions above satisfies this theorem.

The paper is rich with additional results and methodology. It develops the meta-theory of Kripke models of BA. It recalls the realizability interpretations used previously in the context of BA. And it makes a link to the theory I$\Sigma_1$ which also has the property that the classes of provable total and primitive recursive functions coincide.

Comment here: @danko@mamot.fr Follow using the Fediverse ID: @danko@blog.iaddg.net