Introduction to clarithmetic. II
type: Item
instance of: scholarly article
title: Introduction to clarithmetic. II
zbMATH Open document ID: 1343.03045
author: Giorgi Japaridze
published in: Information and Computation
publication date: 2016-03-10T00:00:00Z
full work available at URL: https://arxiv.org/abs/1004.3236
reviewed by: Saeed Salehi
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 03F50
zbMATH DE Number: 6553705
zbMATH Keywords: computability logic
zbMATH Keywords: game semantics
zbMATH Keywords: Peano arithmetic
zbMATH Keywords: constructive theories
zbMATH Keywords: interactive computation
zbMATH Keywords: bounded arithmetic
zbMATH Keywords: implicit computational complexity
MaRDI profile type: Publication
OpenAlex ID: W1879353470
arXiv ID: 1004.3236
cites work: Q3800030
cites work: Bounded arithmetic for NC, ALogTIME, L and NL
cites work: Introduction to computability logic
cites work: The logic of interactive turing reduction
cites work: Intuitionistic computability logic
cites work: The intuitionistic fragment of computability logic at the propositional level
cites work: In the beginning was game semantics
cites work: Towards applied theories based on computability logic
cites work: Introduction to clarithmetic. I
cites work: A logical basis for constructive systems
DOI: 10.1016/J.IC.2016.02.002
Recommended article: Introduction to clarithmetic. III
Recommended article: On a Theory for AC0 and the Strength of the Induction Scheme
Recommended article: Introduction to clarithmetic. I
Recommended article: Build your own clarithmetic II: Soundness
Recommended article: Build your own clarithmetic I: Setup and completeness
Recommended article: Q4035308
Recommended article: Propositional computability logic I
Recommended article: Q4395609
Recommended article: Arithmetics based on computability logic
Recommended article: Soundness and completeness of the cirquent calculus system CL6 for computability logic
review text: This is Part II of a series of three papers, whose Part I was [the author, ibid. 209, No. 10, 1312--1354 (2011; Zbl 1243.03075)] and Part III was [the author, Ann. Pure Appl. Logic 165, No. 1, 241--252 (2014; Zbl 1303.03089)]. Giving the good news that Part I is self-contained, the author warns that ``this article fully and heavily relies on the terminology, notation, conventions and technical results of its predecessor, with which the reader is assumed to be well familiar.''NEWLINENEWLINE``The present paper constructs three new \textbf{CL12}-based systems: \textbf{CLA5}, \textbf{CLA6}, \textbf{CLA7} and proves their soundness and extensional completeness with respect to polynomial space computability, elementary recursive time (and/or space) computability, and primitive recursive time (and/or space) computability, respectively. While \textbf{CLA4} was already simple enough, the above three systems are even more so. All of them only need \(\sqcap x\sqcup y (y=x+1)\) as a single extra-Peano axiom. As before, the only logical rule is LC. And the induction rule (the only nonlogical rule) of each of these systems is \(\{F(0), F(x)\rightarrow F(x+1)\}\vdash\{F(x)\}\). The three systems differ from each other only in what (if any) conditions are imposed on the formula \(F(x)\) of induction. In \textbf{CLA5}, as in \textbf{CLA4}, \(F(x)\) is required to be polynomially bounded. \textbf{CLA6} relaxes this requirement and allows \(F(x)\) to be an exponentially bounded formula. \textbf{CLA7} takes this trend towards relaxation to an extreme and imposes no restrictions on \(F(x)\) whatsoever. This way, unlike \textbf{CLA4}, \textbf{CLA5} and \textbf{CLA6}, theory \textbf{CLA7} is no longer in the realm of bounded arithmetics.''
description: scientific article; zbMATH DE number 6553705