Introduction to clarithmetic. III

DOI10.1016/J.APAL.2013.07.012zbMATH Open1303.03089arXiv1008.0770OpenAlexW2041255875MaRDI QIDQ392285FDOQ392285

Authors: Giorgi Japaridze 

Publication date: 13 January 2014

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1008.0770

Recommendations

• Introduction to clarithmetic. I
• From truth to computability. I.
• Introduction to clarithmetic. II
• Towards applied theories based on computability logic
• Build your own clarithmetic. I: Setup and completeness

zbMATH Keywords

computability logicconstructive theoriesgame semanticsinteractive computationPeano arithmetic

Mathematics Subject Classification ID

Logic in computer science (03B70) First-order arithmetic and fragments (03F30) Metamathematics of constructive systems (03F50) Abstract and axiomatic computability and recursion theory (03D75)

Cites Work

• Introduction to clarithmetic. II
• A logical basis for constructive systems
• Introduction to clarithmetic. I

Cited In (6)

• A PSPACE-complete first-order fragment of computability logic
• Introduction to clarithmetic. II
• Introduction to clarithmetic. I
• Build your own clarithmetic. I: Setup and completeness
• Build your own clarithmetic. II: Soundness
• The taming of recurrences in computability logic through cirquent calculus. I

This page was built for publication: Introduction to clarithmetic. III

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q392285)