Intuitionistic computability logic
arXiv:cs/0411008
Abstract
Computability logic (CL) is a systematic formal theory of computational tasks and resources, which, in a sense, can be seen as a semantics-based alternative to (the syntactically introduced) linear logic. With its expressive and flexible language, where formulas represent computational problems and "truth" is understood as algorithmic solvability, CL potentially offers a comprehensive logical basis for constructive applied theories and computing systems inherently requiring constructive and computationally meaningful underlying logics. Among the best known constructivistic logics is Heyting's intuitionistic calculus INT, whose language can be seen as a special fragment of that of CL. The constructivistic philosophy of INT, however, has never really found an intuitively convincing and mathematically strict semantical justification. CL has good claims to provide such a justification and hence a materialization of Kolmogorov's known thesis "INT = logic of problems". The present paper contains a soundness proof for INT with respect to the CL semantics. A comprehensive online source on CL is available at http://www.cis.upenn.edu/~giorgi/cl.html
References in corpus (3)
Cited by in corpus (14)
- Sequential operators in computability logic
- Computability Logic: a formal theory of interaction
- The intuitionistic fragment of computability logic at the propositional level
- 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
- Introduction to clarithmetic I
- A logical basis for constructive systems
- On the system CL12 of computability logic
- Ptarithmetic
- Implementing program extraction from CL1-proofs
- Aspects of an internal logic for persistence