FOM: Refutation Theorem Proving and Natural Deduction?

[A.P. Hazen]

Steve Stevenson asked about the relations between Refutation Theorem
Proving (I take it that this refers to Resolution and similar methods, and
I am more familiar with Beth-Smullyan tableaux, but I think there are
relevant similarities).

>Is there any formal connection between the two trees so that one can
>be converted to the other (regardless of how hard that might be)?

-------Yes.  The refutation proving procedures tend to be closely related
to cut-free sequent calculi, and sequent calculi are transparently related
to natural deduction.
   The refutation proof procedure I know best is Beth-Smullyan tableaux
(done by hand rather than by computer: these systems are often used in
elementary logic teaching).  As usually presented, these systems have a
convention of "checking off" a formula after it has been used: checked-off
formulas don't have to be used again in further construction of the
tableau.  The correspondence to sequent calculi is that a line in the
sequent proof is a "frame" of a "motion picture" of the process of tableau
construction.
   In more detail: Alter the sequent rules so that sequents are
"left-sided": sequents all have null succedents.  This involves (i)
changing the axioms to the form p,-p ->  (ii) changing the rules for the
horseshoe connective so that negations in the antecedent play the role of
formulas in the succedent, and (iii) adding negative rules allowing, e.g.,
the inference of GAMMA, DELTA, -(A&B) -> from GAMMA, -A -> and DELTA, -B
->.  (The negative rules are classically obvious, but would also be used in
a sequent calculus for David Nelson's "Constructible Falsity" [JSL v. 14
(1949), pp. 16-26)] variant of intuitionistic logic.)
    When this is done, the construction of a tableau can be "depicted" by a
sequent proof in which the formulas occurring in each sequent are the
formulas occurring, NOT CHECKED OFF, on a branch of the tableau at some
stage of its construction.

>All the algorithms I know for setting up the refutation search require
>conversion to conjuntive normal form. Doesn't this require the
>excluded middle? Doesn't that make refutation style systems impossible
>for intuitionistic systems?
--------------------My impression is that many attempts at artificial
theorem proving for non-classical logics in effect use classical first
order logic.  First step: translate the (say, for example) intuitionistic
statement into a classical formula descrbing a Kripke Model, and then use
your classical theorem prover.  ATP, however, is NOT my area, so this is
just an outsider's impression.
    The sequent-calculus I described above as a labor-and-ink-intensive
variant of tableaux is sound on a constructive interpretation: cf. the
reference to David Nelson.  What this gives us is a sort of negation
interpretation: the tableau proof of a classical formula corresponds to an
intuitionistic proof of the double negation of a certain related formula.

Allen Hazen
Philosophy Department
University of Melbourne