标题：Introduction to clarithmetic III
作者机构：[Japaridze, G] School of Computer Science and Technology, Shandong University, Middle Shunhua Road, Jinan, Shandong 25101, China, Department of Comput 更多
通讯作者地址：[Japaridze, G]Villanova Univ, Dept Comp Sci, 800 Lancaster Ave, Villanova, PA 19085 USA.
来源：Annals of Pure and Applied Logic
关键词：03D75;03F30;03F50;68T30;Computability logic;Constructive theories;Game semantics;Interactive computation;Peano arithmetic
摘要：The present paper constructs three new systems of clarithmetic (arithmetic based on computability logic): 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 τ-time solution for some PA-provably recursive function τ 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.