2
$\begingroup$

First at all, I am new at proof theory, so excuse this perhaps redundant question.

I am wondering what is the 'most appropriate' definition of a proof in a sequent calculus (e.g. LK). Proofs as trees or proofs as sequences of sequents?

Does one of the representations have advantages in proofs about the calculus (I am especially thinking of induction on proof length, etc.)?

1 Answers 1

3

Both are fine. Note that we can think of linear format (i.e. sequence of sequents) as a DAG, and the tree version is a special case of the DAG version.

The main advantage is that we can use a sequent multiple times in a proof. The main place where this is interesting is in proof complexity where we are interested in the size of the propositional proofs. However even in that case it is often possible to prove that the DAG version does not provide a superpolynomial improvement over the tree version (i.e. one can convert a DAG proof into a tree proof with polynomial blowup in size of the proof).

In proof complexity the DAG is the standard version and the tree version is denoted by adding a $*$ superscript. For example, the tree version of bounded-depth Frege (a propositional proof system equivalent to $PK$) is denoted by $bdFrege^*$.

In classical proof theory it doesn't matter that much which definition you use for $LK$. Both are fine, however I think the tree version is the more standard one (it seems to be the one used in proof theory textbooks).