The intuitionistic fragment of computability logic at the propositional level

DOI10.1016/J.APAL.2007.05.001zbMATH Open1143.03014DBLPjournals/apal/Japaridze07arXivcs/0602011OpenAlexW1980921829WikidataQ56765868 ScholiaQ56765868MaRDI QIDQ2373697FDOQ2373697

Authors: Giorgi Japaridze 

Publication date: 16 July 2007

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

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.

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

Recommendations

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

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)

Cites Work

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

Cited In (26)

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

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)