Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4661964 | Annals of Pure and Applied Logic | 2014 | 12 Pages |
Abstract
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.
Keywords
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
Giorgi Japaridze,