A simple decision procedure for one-variable implicational/negation formulae in intuitionist logic.
Storrs McCall · Notre Dame Journal of Formal Logic · 1962
Those who have agonized over the intuitionist theory of deduction, as I have, will perhaps welcome a simple decision procedure for implication/negation formulae containing only one variable CC-N-p formulae').The procedure consists essentially in showing every such formula to be equivalent to one of six non-mutually-equivalent forms.Since the intuitionist calculus admits of the replacement of equivalents, any C-N-p formula, or C'N'p portion of a more complex formula, may be replaced by one of these six forms.The six forms are the following: