Formalizing the Decision Procedure

There are many ways to present the tableau decision procedure formally. In Nuprl we have looked at two of them [9,14]. Caldwell's account [9] is based on the approach in [14].

The methods referred to above can also be extended to the full set of connectives and to a notion of propositional proof derived from the internal definition of Proof. The details of how to do this are in [5].

Define PropSeq as a subtype of Term and PropProof as a subtype of Proof. Informally these are the definitions.

Definition: PropSeq = {$s\!:$ Sequent | hypotheses of s are variable declarations, the goal of s is a proposition built from $\&, \vee, \Rightarrow, \: False$ using the declared variables.}

PropProof = {$p\!:Proo\!f \vert$ the goal of p is PropSeq and all rules are primitive and are rules of the classical propositional calculus.}

As an abbreviation let P or not mean $P \vee \neg P$, then based on the proof method in [5,14] we can constructively prove:

Theorem (dp):

$$% latex2html id marker 2853 \forall s:{\sf PropSeq. \; ( {\boldmath\exists} p:PropProof.root(p)=s)} \mbox{or not}$$

Given a sequent $H \vdash G$ which is propositional, we have that the computable function extracted from dp, called here extract(dp), decides whether or not there is a propositional proof.