The intuitionistic fragment of computability logic at the propositional level
arXiv:cs/0602011 · doi:10.1016/j.apal.2007.05.001
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.
References in corpus (8)
- Introduction to Cirquent Calculus and Abstract Resource Semantics
- Propositional computability logic I
- Computability Logic: a formal theory of interaction
- From truth to computability I
- Propositional Computability Logic II
- Intuitionistic computability logic
- From truth to computability II
- The logic of interactive Turing reduction
Cited by in corpus (19)
- Sequential operators in computability logic
- Many concepts and two logics of algorithmic reduction
- The taming of recurrences in computability logic through cirquent calculus, Part I
- Toggling operators in computability logic
- From formulas to cirquents in computability logic
- Introduction to clarithmetic II
- In the beginning was game semantics
- Towards applied theories based on computability logic
- A new face of the branching recurrence of computability logic
- A logical basis for constructive systems
- Introduction to clarithmetic I
- On the system CL12 of computability logic
- The taming of recurrences in computability logic through cirquent calculus, Part II
- Separating the basic logics of the basic recurrences
- A Galois connection between classical and intuitionistic logics. I: Syntax
- Elementary-base cirquent calculus I: Parallel and choice connectives
- Build your own clarithmetic I: Setup and completeness
- Ptarithmetic
- Implementing program extraction from CL1-proofs