Towards applied theories based on computability logic

DOI10.2178/JSL/1268917495MaRDI QIDQ3570163zbMATH OpenOpenAlexFDO

Authors Giorgi Japaridze

Publication date 24 June 2010

Published in Journal of Symbolic Logic (Search for Journal in Brave)

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

zbMATH Keywords

computability logicconstructive logicsgame semanticsPeano arithmetic

Mathematics Subject Classification ID

Logic in computer science (03B70) First-order arithmetic and fragments (03F30) Metamathematics of constructive systems (03F50)

Abstract: Computability logic (CL) (see http://www.cis.upenn.edu/~giorgi/cl.html) is a recently launched program for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth that logic has more traditionally been. Formulas in it represent computational problems, "truth" means existence of an algorithmic solution, and proofs encode such solutions. Within the line of research devoted to finding axiomatizations for ever more expressive fragments of CL, the present paper introduces a new deductive system CL12 and proves its soundness and completeness with respect to the semantics of CL. Conservatively extending classical predicate calculus and offering considerable additional expressive and deductive power, CL12 presents a reasonable, computationally meaningful, constructive alternative to classical logic as a basis for applied theories. To obtain a model example of such theories, this paper rebuilds the traditional, classical-logic-based Peano arithmetic into a computability-logic-based counterpart. Among the purposes of the present contribution is to provide a starting point for what, as the author wishes to hope, might become a new line of research with a potential of interesting findings -- an exploration of the presumably quite unusual metatheory of CL-based arithmetic and other CL-based applied systems.

Recommendations

• From truth to computability. I.
• Propositional computability logic I
• Computability logic: giving Caesar what belongs to Caesar
• From truth to computability. II.
• A logical basis for constructive systems

Cites work

• Cirquent Calculus Deepened
• Computability logic: a formal theory of interaction
• From truth to computability. I.
• From truth to computability. II.
• Introduction to Cirquent Calculus and Abstract Resource Semantics
• Introduction to computability logic
• Many concepts and two logics of algorithmic reduction
• Propositional computability logic I
• Propositional computability logic II
• Sequential operators in computability logic
• The intuitionistic fragment of computability logic at the propositional level
• The logic of interactive turing reduction

Cited in

(16)

• Many concepts and two logics of algorithmic reduction
• The taming of recurrences in computability logic through cirquent calculus. I
• The countable versus uncountable branching recurrences in computability logic
• Applicative theories for logarithmic complexity classes
• From truth to computability. II.
• Introduction to clarithmetic. II
• A logical basis for constructive systems
• On the system CL12 of computability logic
• Build your own clarithmetic. I: Setup and completeness
• Introduction to clarithmetic. III
• Separating the basic logics of the basic recurrences
• scientific article; zbMATH DE number 2101985 (Why is no real title available?)
• Arithmetics base on computability logic
• Toggling operators in computability logic
• Introduction to clarithmetic. I
• A new face of the branching recurrence of computability logic

This page was built for publication: Towards applied theories based on computability logic

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