The intuitionistic fragment of computability logic at the propositional level

DOI10.1016/J.APAL.2007.05.001MaRDI QIDQ2373697zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Giorgi Japaridze

Publication date 16 July 2007

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

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

zbMATH Keywords

computability logicconstructive logicgame semanticsinteractive computationintuitionistic logicKripke semantics

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Abstract: This paper presents a soundness and completeness proof for propositional intuitionistic calculus with respect to the semantics of computability logic. The latter interprets formulas as interactive computational problems, formalized as games between a machine and its environment. Intuitionistic implication is understood as algorithmic reduction in the weakest possible -- and hence most natural -- sense, disjunction and conjunction as deterministic-choice combinations of problems (disjunction = machine's choice, conjunction = environment's choice), and "absurd" as a computational problem of universal strength. See http://www.cis.upenn.edu/~giorgi/cl.html for a comprehensive online source on computability logic.

Recommendations

• Intuitionistic computability logic
• Propositional computability logic I
• From truth to computability. I.
• Introduction to computability logic
• The logic of interactive turing reduction

Cites work

• scientific article; zbMATH DE number 3222098 (Why is no real title available?)
• scientific article; zbMATH DE number 3346343 (Why is no real title available?)
• scientific article; zbMATH DE number 3190338 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• A game semantics for linear logic
• Computability logic: a formal theory of interaction
• Degrees of indeterminacy of games
• Explicit provability and constructive semantics
• From truth to computability. I.
• From truth to computability. II.
• Introduction to Cirquent Calculus and Abstract Resource Semantics
• Introduction to computability logic
• Intuitionistic computability logic
• Linear logic
• Propositional computability logic I
• Propositional computability logic II
• The logic of interactive turing reduction
• Zur Deutung der intuitionistischen Logik
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(26)

• The logic of interactive turing reduction
• Intuitionistic proofs without syntax
• Intuitionistic computability logic
• scientific article; zbMATH DE number 2209833 (Why is no real title available?)
• scientific article; zbMATH DE number 1873426 (Why is no real title available?)
• A PSPACE-complete first-order fragment of computability logic
• Separating the basic logics of the basic recurrences
• Many concepts and two logics of algorithmic reduction
• On abstract resource semantics and computability logic
• Propositional computability logic I
• The taming of recurrences in computability logic through cirquent calculus. II
• The taming of recurrences in computability logic through cirquent calculus. I
• Sequential operators in computability logic
• Build your own clarithmetic. I: Setup and completeness
• A new face of the branching recurrence of computability logic
• Computations in fragments of intuitionistic propositional logic
• Kripke semantics for the logic of problems and propositions
• Introduction to clarithmetic. I
• Propositional computability logic II
• Intuitionistic games: determinacy, completeness, and normalization
• Introduction to clarithmetic. II
• Infinitary classical logic: recursive equations and interactive semantics
• scientific article; zbMATH DE number 4125400 (Why is no real title available?)
• Toggling operators in computability logic
• Towards applied theories based on computability logic
• A propositional cirquent calculus for computability logic.

This page was built for publication: The intuitionistic fragment of computability logic at the propositional level

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