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.