Uniform Provability in Classical Logic

TL;DR

This paper explores uniform provability in classical logic, identifying a fragment where it holds and proposing a goal-directed proof procedure that integrates mechanisms for disjunctive assumptions and hypotheticals.

Contribution

It introduces a modified fragment of classical logic where uniform provability is valid and develops a proof procedure that incorporates existing mechanisms for disjunctive information and hypotheticals.

Findings

Uniform provability holds in a specific fragment of classical logic.

A goal-directed proof procedure is outlined based on this fragment.

The procedure integrates mechanisms for disjunctive assumptions and hypotheticals.

Abstract

Uniform proofs are sequent calculus proofs with the following characteristic: the last step in the derivation of a complex formula at any stage in the proof is always the introduction of the top-level logical symbol of that formula. We investigate the relevance of this uniform proof notion to structuring proof search in classical logic. A logical language in whose context provability is equivalent to uniform provability admits of a goal-directed proof procedure that interprets logical symbols as search directives whose meanings are given by the corresponding inference rules. While this uniform provability property does not hold directly of classical logic, we show that it holds of a fragment of it that only excludes essentially positive occurrences of universal quantifiers under a modest, sound, modification to the set of assumptions: the addition to them of the negation of the formula being proved. We further note that all uses of the added formula can be factored into certain derived rules. The resulting proof system and the uniform provability property that holds of it are used to outline a proof procedure for classical logic. An interesting aspect of this proof procedure is that it incorporates within it previously proposed mechanisms for dealing with disjunctive information in assumptions and for handling hypotheticals. Our analysis sheds light on the relationship between these mechanisms and the notion of uniform proofs.