Proof search
Jan von Plato · Cambridge University Press eBooks · 2014
The construction of derivations in Gentzen's tree form is awkward: One would have to know, more or less, how the final tree has to look before one can start. So one looks at the assumptions, and one looks at the conclusion, and one tries to figure a way from the former to the latter. The good aspects of the tree form include that once you have the tree, its structure is transparent. We shall modify a bit natural deduction, to get a logical calculus that supports proof search better. The starting point is the change in Section 3.4 in which all E -rules were written with an arbitrary conclusion. Consider any formula C in a derivation tree. The assumptions it depends on can be listed, and let them be A 1 ,…, A n . If you take the part of the tree that is determined by the chosen formula C , you geta subderivation of the original derivation. To be precise, to get a correct derivation tree you have to delete the labels from above those assumptions that have not been closed at the stage in which formula C is concluded. The subderivation establishes a derivability relation, namely A 1 ,…, A n ⊢ C . It will be convenient to have a name for the thing a derivability relation establishes: Expressions of the form A 1 ,…, A n ⊢ C are called sequents. The name stems from the arrangement of formulas in a sequence in the antecedent , left part of a sequent.