Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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.


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.

share|improve this question

1 Answer 1

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).

share|improve this answer
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. –  jessealama Jan 15 '13 at 12:08

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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