4
$\begingroup$

What about with cut?

And can the sequent calculus be thought of as natural deduction, but with the implication/universal quantifier introduction rules being made more explicit with contexts? Are there any alternative ways of making those rules explicit?

$\endgroup$
4
$\begingroup$

A complete answer to your question is likely to depend on the details of the particular natural deduction system and sequent proof system that you have in mind. In general, sequent systems with cut tend to be rather similar to natural deduction systems. Specifically, given a natural deduction system, one can set up a closely related sequent calculus, in which a sequent $\Gamma\implies\phi$ is provable if and only if the natural deduction system has a proof of $\phi$ with open (i.e., undischarged or uncanceled, depending on your terminology) assumptions $\Gamma$. In this situation, I would expect the complexity of sequent proofs and of natural deduction proofs to be very similar. A proof, or even a careful formulation of that fact would require looking closely at the axioms and rules of both systems, to see how closely each one simulates the other.

Cut elimination, on the other hand, can greatly increase the length of proofs. So I would expect natural deduction proofs to be considerably more efficient, in general, than cut-free sequent proofs.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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