2
$\begingroup$

In Gentzen's sequent calculus, a formal proof is described by a tree, with each node representing the sequent obtained from the child(ren) by applying a given inference rule.

If no inference rule has more than one premise, such a tree becomes a sequence: in a 1957 paper, Craig devised Linear Reasoning to pursue such an idea; an evolution of this approach (seemingly related to Craig's famous interpolation theorem, by the way) is exposed in the standard First-Order Logic textbook by Smullyan (chapter XVII in my edition).

The corresponding theorems, however, pose various restrictions: for example, on the form of the sentences involved.

Is linear reasoning possible in more general cases?

For example, is there a sequent calculus giving linear proofs and being simultaneously complete (and sound, of course) for classical first order logic? Or, on the contrary, is there some result limiting similar ambitions?

P.S.: I know about deep inference, so let us restrict to `standard' sequent calculi.


Background

When faced with the task of formalizing sequent calculus on a set theoretical proof assistant (Mizar), I felt trees would have been not so easy to actually work with, so I devised alternative frameworks. It worked, in the sense that one can manage not to ever mention trees and still carry on a great deal of results; however, they are still morally there, hence the question arose naturally.

$\endgroup$

1 Answer 1

2
$\begingroup$

By "linear" do you mean (following Smullyan and Craig) that all rules have one premise? If so, I have nothing to add. But if you're willing to relax this requirement, there's another sense of "linear reasoning" that can be found in discussions of linear refinements of resolution. Linearity in this context means that every application of resolution is such that one of the (two) premises was derived immediately before the conclusion. Here one deals with trees, but of a very limited kind. There are completeness theorems for such restrictions of resolution (see, e.g., Donald Loveland's Automated Theorem Proving: A Logical Basis).

$\endgroup$
1
  • $\begingroup$ You may also consider working wit prenex formulas rather than arbitrary formulas. One can then formulate tableau rules that avoid branching. See, e.g., chapter 10 section 2 of Smullyan's First-Order Logic. $\endgroup$ Jan 15, 2013 at 12:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.