Correspondences between Classical, Intuitionistic and Uniform Provability

TL;DR

This paper analyzes the relationships between classical, intuitionistic, and uniform provability, characterizing when classical provability implies intuitionistic provability and exploring reductions to uniform provability.

Contribution

It provides a detailed characterization of when classical and intuitionistic provability entail uniform provability and examines reductions via negation assumptions.

Findings

Classical provability entails intuitionistic provability under specific inference rule conditions.

Certain versions of abstract logic programming languages are identified as the richest in classical and intuitionistic logic.

Reduction of classical and intuitionistic provability to uniform provability is possible by adding negation of the target formula.

Abstract

Based on an analysis of the inference rules used, we provide a characterization of the situations in which classical provability entails intuitionistic provability. We then examine the relationship of these derivability notions to uniform provability, a restriction of intuitionistic provability that embodies a special form of goal-directedness. We determine, first, the circumstances in which the former relations imply the latter. Using this result, we identify the richest versions of the so-called abstract logic programming languages in classical and intuitionistic logic. We then study the reduction of classical and, derivatively, intuitionistic provability to uniform provability via the addition to the assumption set of the negation of the formula to be proved. Our focus here is on understanding the situations in which this reduction is achieved. However, our discussions indicate the structure of a proof procedure based on the reduction, a matter also considered explicitly elsewhere.