# Results about logics that were new with proof systems other than sequent calculus

Lew Gordeew lew.gordeew at uni-tuebingen.de
Sun Aug 29 02:19:36 EDT 2021

There are novel ideas and methods of *proof compression* in sequent
calculus and especially in (Prawitz') natural deduction, as follows.

Given any "huge" proof produce an equivalent "small" proof of the same
conclusion (sequent or formula, respectively).

Principal applications deal with computational proof complexity, see
e.g. my recent presentation "On Proof Theory in Computational
Complexity" at Logic Colloquium 2021:

slide).

Nested proof systems dealing with Tarski's relation algebra are
exposed in my chapter "Proof Systems in Relation Algebra":

Best,
LG

Zitat von Revantha Ramanayake <revantha at logic.at>:

> Dear colleagues,
>
> Many new results and new insights about classical and non-classical
> logics have been obtained using the sequent calculus, e.g. Gentzen's
> consistency argument; interpolation; decidability, complexity; etc.
>
> I would like to identify results and insights *about logics* that
> were *new*, and that were obtained using proof systems---other than
> the sequent calculus---that utilised some notion of analyticity / a
> restriction of proof space such as the subformula property. I am
> interested across all logics and all sorts of proof systems like
> hypersequent, nested, labelled, display, proof nets, deep inference
> based. Here I am viewing a logic as a set of formulas.
>
> I would be pleased to see your thoughts and references ! You could
> comment on my post at the The Proof Theory Blog (link below), reply
> here, or write to me directly.
>