In this talk I will present a theorem justifying an intuitive semantical interpretation of rules of sequent proof systems. This theorem is based on the one hand on a generalization of Lindenbuam maximalization theorem and on the other hand on a general semantical theory of bivaluations, not necessarily truth-functional, originally developed by Newton da Costa for paraconsistent systems. I will show that this theorem gives a better understanding of sequent calculus and that it can fruitfully be applied to a wide class of logical systems providing instantaneous completeness results. This is a typical example of work in the line of the universal logic project, of which I will say a few words.

Reference: Logica Universalis, Special Double Issue – Scope of Logic Theorems. Volume 8, Issue 3-4, December 2014.