The Journal of Symbolic Logic

Research Article

The logic of interactive turing reduction

Giorgi Japaridze

Villanova University, Department of Computing Sciences, 800 Lancaster Avenue, Villanova, PA 19085, USA. E-mail: URL:;japaridz/


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.

(Received December 28 2005)

Key words and phrases

  • Computability logic;
  • Intuitionistic logic;
  • Interactive computation;
  • Game semantics