The intuitionistic fragment of computability logic at the propositional level

TL;DR

This paper establishes soundness and completeness for propositional intuitionistic calculus within computability logic, interpreting formulas as interactive computational problems and clarifying their logical connectives as problem operations.

Contribution

It provides the first formal proof connecting propositional intuitionistic logic with the semantics of computability logic, interpreting logical connectives as computational problem operations.

Findings

Soundness and completeness of propositional intuitionistic calculus proven

Formulas interpreted as interactive computational problems

Logical connectives correspond to problem operations

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.