Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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

Regards

share|improve this question

1 Answer 1

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

share|improve this answer

Your Answer

 
discard

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.