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

Joao Marcos botocudo at
Sun Aug 29 12:41:28 EDT 2021

Hi, Revantha!

You might already have seen the answer written by my Master's student
Vitor Greati at your blog:

In this paper that we will present in TABLEAUX next week, in
particular, we study the complexity of proof-search procedures
associated to certain kinds of (two-dimensional) _analytic_
*Hilbert-style* systems (and we show that a large class of logical
matrices are axiomatisable using just this kind of systems).  It might
be worth a look!
On the same line, Vitor provides also other references in his response
to your post.

Best wishes,
Joao Marcos

> From: Revantha Ramanayake
> 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.
> Best wishes,
> Revantha Ramanayake
> <d.r.s.ramanayake at>


More information about the FOM mailing list