The intuitionistic fragment of computability logic at the propositional level

Annals of Pure and Applied Logic 147 (3):187-227 (2007)
  Copy   BIBTEX

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 , and “absurd” as a computational problem of universal strength

Categories

Keywords

Reprint years

DOI

10.1016/j.apal.2007.05.001

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,990

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

The Logic of Interactive Turing Reduction.Giorgi Japaridze - 2007 - Journal of Symbolic Logic 72 (1):243 - 276.
On the computational content of intuitionistic propositional proofs.Samuel R. Buss & Pavel Pudlák - 2001 - Annals of Pure and Applied Logic 109 (1-2):49-64.
Introduction to computability logic.Giorgi Japaridze - 2003 - Annals of Pure and Applied Logic 123 (1-3):1-99.
Normalization, Soundness and Completeness for the Propositional Fragment of Prawitz’ Ecumenical System.Luiz Carlos Pereira & Ricardo Oscar Rodriguez - 2017 - Revista Portuguesa de Filosofia 73 (3-4):1153-1168.
Soundness and completeness of the Cirquent calculus system CL6 for computability logic.Wenyan Xu & Sanyang Liu - 2012 - Logic Journal of the IGPL 20 (1):317-330.
A secondary semantics for Second Order Intuitionistic Propositional Logic.Mauro Ferrari, Camillo Fiorentini & Guido Fiorino - 2004 - Mathematical Logic Quarterly 50 (2):202-210.
The complexity of the disjunction and existential properties in intuitionistic logic.Sam Buss & Grigori Mints - 1999 - Annals of Pure and Applied Logic 99 (1-3):93-104.
Doing logic by computer: interpolation in fragments of intuitionistic propositional logic.Lex Hendriks - 2000 - Annals of Pure and Applied Logic 104 (1-3):97-112.
The taming of recurrences in computability logic through cirquent calculus, Part I.Giorgi Japaridze - 2013 - Archive for Mathematical Logic 52 (1-2):173-212.
Completeness of Second-Order Intuitionistic Propositional Logic with Respect to Phase Semantics for Proof-Terms.Yuta Takahashi & Ryo Takemura - 2019 - Journal of Philosophical Logic 48 (3):553-570.

Analytics

Added to PP
2013-12-30

Downloads
21 (#729,174)

6 months
4 (#1,006,062)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

In the Beginning was Game Semantics?Giorgi Japaridze - 2009 - In Ondrej Majer, Ahti-Veikko Pietarinen & Tero Tulenheimo (eds.), Games: Unifying Logic, Language, and Philosophy. Dordrecht, Netherland: Springer Verlag. pp. 249--350.
Towards applied theories based on computability logic.Giorgi Japaridze - 2010 - Journal of Symbolic Logic 75 (2):565-601.
Separating the basic logics of the basic recurrences.Giorgi Japaridze - 2012 - Annals of Pure and Applied Logic 163 (3):377-389.

View all 6 citations / Add more citations

References found in this work

Explicit provability and constructive semantics.Sergei N. Artemov - 2001 - Bulletin of Symbolic Logic 7 (1):1-36.
A game semantics for linear logic.Andreas Blass - 1992 - Annals of Pure and Applied Logic 56 (1-3):183-220.
Introduction to computability logic.Giorgi Japaridze - 2003 - Annals of Pure and Applied Logic 123 (1-3):1-99.

View all 6 references / Add more references