The logic of interactive Turing reduction

TL;DR

This paper establishes a soundness and completeness proof for the implicative fragment of intuitionistic calculus within computability logic, interpreting intuitionistic implication as an interactive reduction, thus generalizing Turing reducibility to interactive computational tasks.

Contribution

It provides a formal proof connecting intuitionistic logic with computability logic, introducing a generalized notion of reducibility for interactive computational problems.

Findings

Proof of soundness and completeness for the implicative fragment

Interpretation of intuitionistic implication as interactive reduction

Generalization of Turing reducibility to interactive tasks

Abstract

The paper gives a soundness and completeness proof for the implicative fragment of intuitionistic calculus with respect to the semantics of computability logic, which understands intuitionistic implication as interactive algorithmic reduction. This concept -- more precisely, the associated concept of reducibility -- is a generalization of Turing reducibility from the traditional, input/output sorts of problems to computational tasks of arbitrary degrees of interactivity. See http://www.cis.upenn.edu/~giorgi/cl.html for a comprehensive online source on computability logic.