Introduction to clarithmetic III

TL;DR

This paper introduces three new systems of clarithmetic based on computability logic, each with different levels of completeness and constructiveness, linking logical theorems to PA-provable computability.

Contribution

It constructs and analyzes CLA8, CLA9, and CLA10, establishing their soundness and completeness relative to various notions of PA-provable computability.

Findings

CLA8 is sound and extensionally complete for PA-provably recursive time computability.

CLA9 is sound and intensionally complete for constructively PA-provable computability.

CLA10 is sound and intensionally complete for PA-provable computability without constructiveness.

Abstract

The present paper constructs three new systems of clarithmetic (arithmetic based on computability logic --- see http://www.cis.upenn.edu/~giorgi/cl.html): CLA8, CLA9 and CLA10. System CLA8 is shown to be sound and extensionally complete with respect to PA-provably recursive time computability. This is in the sense that an arithmetical problem A has a t-time solution for some PA-provably recursive function t iff A is represented by some theorem of CLA8. System CLA9 is shown to be sound and intensionally complete with respect to constructively PA-provable computability. This is in the sense that a sentence X is a theorem of CLA9 iff, for some particular machine M, PA proves that M computes (the problem represented by) X. And system CLA10 is shown to be sound and intensionally complete with respect to not-necessarily-constructively PA-provable computability. This means that a sentence X is a theorem of CLA10 iff PA proves that X is computable, even if PA does not "know" of any particular machine M that computes X.