Finding Proofs in Fixed Finite Time

in Classical Propositional Logics

Abstract

M.W. Bunder
Mathematics Department
University of Wollongong

It is well known that proofs of theorems in intuitionistic implicational logic Hfi can be represented by combinators or by lambda terms. These are intertranslatable.

Proofs in subsystems of Hfi can also be represented by combinators, these are generated from the combinators representing the axioms of the logic. The question arises: what set of lambda terms corresponds to what set of combinators and how is this correspondence defined? This was answered in [1].

Given a formula of implicational logic we can find, by the Ben-Yelles Algorithm, a lambda term in long normal form which represents its proof, or a guarantee that the formula has no proof, within a fixed number of steps determined by the structure of the formula.

The algorithm and the guarantee of proofs or refutation in a fixed number of steps has been extended to a number of sublogics of Hfi in [2]. Anthony Dekker has produced a very efficient implementation of this in [4].

A new algorithm that is even more efficient has recently been produced in [3]. This provides us with simple decision procedures for many implicational logics including Rfi and also Hfi for which no decision procedure was known.

The work on the Ben-Yelles algorithm is now being extended to various subsystems of classical logic. Some of this is based on earlier joint work with Sachio Hirokawa and is being done jointly with Ramzy Rizkalla.

References

[1] Bunder, M.W. ?Lambda terms definable as combinators? University of Wollongong Department of Mathematics, Preprint Series No. 1/95.