The intuitionistic fragment of computability logic at the propositional level
- 作者：Giorgi Japaridze
- 关键词：Computability logic ; Intuitionistic logic ; Constructive logic ; Interactive computation ; Game semantics
- 刊名：Annals of Pure and Applied Logic
- 出版年：2007
- 期刊代码：4_01680072
- 类别：cp
- 出版时间：July 2007
- 卷：147
- 期：3
- 页码：187-227
- 文件大小：720 K
摘要
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.