Build your own clarithmetic. I: Setup and completeness

DOI10.2168/LMCS-12(3:8)2016MaRDI QIDQ2974779zbMATH OpenFDO

Authors Giorgi Japaridze

Publication date 11 April 2017

Published in Logical Methods in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

bounded arithmeticcomputability logicgame semanticsimplicit computational complexityinteractive computationPeano arithmetic

Mathematics Subject Classification ID

Logic in computer science (03B70) Complexity of computation (including implicit computational complexity) (03D15) Abstract and axiomatic computability and recursion theory (03D75) First-order arithmetic and fragments (03F30) Metamathematics of constructive systems (03F50)

Abstract: Clarithmetics are number theories based on computability logic (see http://www.csc.villanova.edu/~japaridz/CL/ ). Formulas of these theories represent interactive computational problems, and their "truth" is understood as existence of an algorithmic solution. Various complexity constraints on such solutions induce various versions of clarithmetic. The present paper introduces a parameterized/schematic version CLA11(P1,P2,P3,P4). By tuning the three parameters P1,P2,P3 in an essentially mechanical manner, one automatically obtains sound and complete theories with respect to a wide range of target tricomplexity classes, i.e. combinations of time (set by P3), space (set by P2) and so called amplitude (set by P1) complexities. Sound in the sense that every theorem T of the system represents an interactive number-theoretic computational problem with a solution from the given tricomplexity class and, furthermore, such a solution can be automatically extracted from a proof of T. And complete in the sense that every interactive number-theoretic problem with a solution from the given tricomplexity class is represented by some theorem of the system. Furthermore, through tuning the 4th parameter P4, at the cost of sacrificing recursive axiomatizability but not simplicity or elegance, the above extensional completeness can be strengthened to intensional completeness, according to which every formula representing a problem with a solution from the given tricomplexity class is a theorem of the system. This article is published in two parts. The present Part I introduces the system and proves its completeness, while Part II is devoted to proving soundness.

Recommendations

• Build your own clarithmetic. II: Soundness
• Introduction to clarithmetic. I
• Introduction to clarithmetic. II
• Introduction to clarithmetic. III
• From truth to computability. II.

Cites work

• A cirquent calculus system with clustering and ranking
• A game semantics for linear logic
• A logical basis for constructive systems
• A new face of the branching recurrence of computability logic
• A new recursion-theoretic characterization of the polytime functions
• A new “feasible” arithmetic
• A PSPACE-complete first-order fragment of computability logic
• An arithmetic for non-size-increasing polynomial-time computation
• An arithmetic for polynomial-time computation
• Bounded linear logic: A modular approach to polynomial-time computability
• Build your own clarithmetic. II: Soundness
• Cirquent Calculus Deepened
• Computability logic: a formal theory of interaction
• Degrees of indeterminacy of games
• Existence and feasibility in arithmetic
• From formulas to cirquents in computability logic
• From truth to computability. I.
• From truth to computability. II.
• Higher type recursion, ramification and polynomial time
• scientific article; zbMATH DE number 3912375 (Why is no real title available?)
• scientific article; zbMATH DE number 4066875 (Why is no real title available?)
• scientific article; zbMATH DE number 1215494 (Why is no real title available?)
• scientific article; zbMATH DE number 1114016 (Why is no real title available?)
• scientific article; zbMATH DE number 1170091 (Why is no real title available?)
• scientific article; zbMATH DE number 806752 (Why is no real title available?)
• scientific article; zbMATH DE number 3399180 (Why is no real title available?)
• scientific article; zbMATH DE number 3190338 (Why is no real title available?)
• In the beginning was game semantics
• Interactive Computation
• Introduction to Cirquent Calculus and Abstract Resource Semantics
• Introduction to clarithmetic. I
• Introduction to clarithmetic. II
• Introduction to clarithmetic. III
• Introduction to computability logic
• Light linear logic
• Linear logic
• Logical foundations of proof complexity
• On abstract resource semantics and computability logic
• On the system CL12 of computability logic
• On the toggling-branching recurrence of computability logic
• Propositional computability logic I
• Propositional computability logic II
• Safe recursion with higher types and BCK-algebra
• Separating the basic logics of the basic recurrences
• Sequential operators in computability logic
• Soundness and completeness of the cirquent calculus system CL6 for computability logic
• The computational complexity of propositional cirquent calculus
• The countable versus uncountable branching recurrences in computability logic
• The intuitionistic fragment of computability logic at the propositional level
• The logic of interactive turing reduction
• The parallel versus branching recurrences in computability logic
• The realm of primitive recursion
• The taming of recurrences in computability logic through cirquent calculus. I
• The taming of recurrences in computability logic through cirquent calculus. II
• Toggling operators in computability logic
• Towards applied theories based on computability logic

Cited in

(5)

• Introduction to clarithmetic. II
• Build your own clarithmetic. II: Soundness
• Introduction to clarithmetic. III
• Arithmetics base on computability logic
• Introduction to clarithmetic. I

This page was built for publication: Build your own clarithmetic. I: Setup and completeness

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