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

[Lew Gordeew]

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:

https://lc2021.pl/conf-data/LC2020/files/LC21_book_of_abstracts_links_02-08-2021.pdf, Contributed talk 37 (with  
slide).

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

https://link.springer.com/chapter/10.1007%2F978-3-7908-1828-4_13

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.
>
> https://prooftheory.blog/2021/08/23/new-results-about-logics-using-proof-systems-other-than-sequent-calculus/
>
> Best wishes,
>
> Revantha Ramanayake
> <d.r.s.ramanayake at rug.nl>