From truth to computability. II.

DOI10.1016/J.TCS.2007.01.004zbMATH Open1118.03021arXivcs/0501031OpenAlexW4213193997WikidataQ56768693 ScholiaQ56768693MaRDI QIDQ2373705FDOQ2373705

Giorgi Japaridze

Publication date: 16 July 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Abstract: Computability logic is a formal theory of computational tasks and resources. Formulas in it represent interactive computational problems, and "truth" is understood as algorithmic solvability. Interactive computational problems, in turn, are defined as a certain sort games between a machine and its environment, with logical operators standing for operations on such games. Within the ambitious program of finding axiomatizations for incrementally rich fragments of this semantically introduced logic, the earlier article "From truth to computability I" proved soundness and completeness for system CL3, whose language has the so called parallel connectives (including negation), choice connectives, choice quantifiers, and blind quantifiers. The present paper extends that result to the significantly more expressive system CL4 with the same collection of logical operators. What makes CL4 expressive is the presence of two sorts of atoms in its language: elementary atoms, representing elementary computational problems (i.e. predicates, i.e. problems of zero degree of interactivity), and general atoms, representing arbitrary computational problems. CL4 conservatively extends CL3, with the latter being nothing but the general-atom-free fragment of the former. Removing the blind (classical) group of quantifiers from the language of CL4 is shown to yield a decidable logic despite the fact that the latter is still first-order. A comprehensive online source on computability logic can be found at http://www.cis.upenn.edu/~giorgi/cl.html

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

Recommendations

• From truth to computability. I.
• Propositional computability logic I
• Propositional computability logic II
• Computability logic: giving Caesar what belongs to Caesar
• Towards applied theories based on computability logic

zbMATH Keywords

computability logicconstructive logicgame semanticsinteractive computationlinear logic

Mathematics Subject Classification ID

Applications of game theory (91A80) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Logic in computer science (03B70) Metamathematics of constructive systems (03F50) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Cites Work

• Introduction to computability logic
• In the beginning was game semantics
• Propositional computability logic I
• Introduction to Cirquent Calculus and Abstract Resource Semantics
• A game semantics for linear logic
• From truth to computability. I.
• Computability Logic: A Formal Theory of Interaction
• Propositional computability logic II

Cited In (14)

• A PSPACE-complete first-order fragment of computability logic
• Separating the basic logics of the basic recurrences
• Introduction to clarithmetic. I
• Toggling operators in computability logic
• Many concepts and two logics of algorithmic reduction
• Sequential operators in computability logic
• A new face of the branching recurrence of computability logic
• The intuitionistic fragment of computability logic at the propositional level
• From truth to computability. I.
• Build your own clarithmetic I: Setup and completeness
• The taming of recurrences in computability logic through cirquent calculus. II
• The taming of recurrences in computability logic through cirquent calculus. I
• Towards applied theories based on computability logic
• A propositional cirquent calculus for computability logic.

This page was built for publication: From truth to computability. II.

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