A logical basis for constructive systems

DOI10.1093/LOGCOM/EXR009MaRDI QIDQ2893325zbMATH OpenOpenAlexFDO

Authors Giorgi Japaridze

Publication date 20 June 2012

Published in Journal of Logic and Computation (Search for Journal in Brave)

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

zbMATH Keywords

computability logicconstructive logicsefficiency logicsgame semanticsimplicit computational complexityinteractive computation

Mathematics Subject Classification ID

Complexity of computation (including implicit computational complexity) (03D15) Recursive functions and relations, subrecursive hierarchies (03D20) Abstract and axiomatic computability and recursion theory (03D75) Metamathematics of constructive systems (03F50)

Abstract: The work is devoted to Computability Logic (CoL) -- the philosophical/mathematical platform and long-term project for redeveloping classical logic after replacing truth} by computability in its underlying semantics (see http://www.cis.upenn.edu/~giorgi/cl.html). This article elaborates some basic complexity theory for the CoL framework. Then it proves soundness and completeness for the deductive system CL12 with respect to the semantics of CoL, including the version of the latter based on polynomial time computability instead of computability-in-principle. CL12 is a sequent calculus system, where the meaning of a sequent intuitively can be characterized as "the succedent is algorithmically reducible to the antecedent", and where formulas are built from predicate letters, function letters, variables, constants, identity, negation, parallel and choice connectives, and blind and choice quantifiers. A case is made that CL12 is an adequate logical basis for constructive applied theories, including complexity-oriented ones.

Review text

Computability logic was introduced by the author [Ann. Pure Appl. Logic 123, No. 1--3, 1--99 (2003; Zbl 1028.03025); in: Interactive computation. The new paradigm. Berlin: Springer. 183--223 (2006; \url{doi:10.1007/3-540-34874-3_9}); in: Logic, Epistemology, and the Unity of Science 15, 249--350 (2009; Zbl 1171.03015)] as an alternative to the classical semantics based on computability and game theory. The main idea is considering logical formulas as games played by a machine against its environment. In this article a way of measuring the complexity of a winning strategy for the machine is proposed. A sequent system CL12 is stated and its soundness and completeness with respect to the semantics based on polynomial-time computability is proved.

Recommendations

• Towards applied theories based on computability logic
• On the system CL12 of computability logic
• Introduction to clarithmetic. I
• Propositional computability logic I
• From truth to computability. I.

Cited in

(13)

• The taming of recurrences in computability logic through cirquent calculus. II
• The taming of recurrences in computability logic through cirquent calculus. I
• Introduction to clarithmetic. II
• Build your own clarithmetic. I: Setup and completeness
• A Logical Architecture of a Normative System
• Towards applied theories based on computability logic
• Introduction to clarithmetic. III
• NOTIONAL LOGIC OF SYSTEMS
• scientific article; zbMATH DE number 1390331 (Why is no real title available?)
• Intuitionistic computability logic
• scientific article; zbMATH DE number 5060081 (Why is no real title available?)
• Introduction to clarithmetic. I
• A propositional cirquent calculus for computability logic.

This page was built for publication: A logical basis for constructive systems

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