Talk:Structural proof theory

Sections on Display Logic and Calculus of Structures don't belong

The sections on Display Logic and Calculus of Structures don't belong here. Instead, there should be a section on extensions to Gentzen-style sequent calculi based on the generalization of syntatic elements of sequents, which could link to separate pages about these systems, if needed.

The purpose of these extensions is to provide structural proof theory for many non-classical logics that sequent calculi is not adequate for.

For example, sequent calculi have been extended in the following ways (as categorised by F. Paoli, with some additions by R. Rothenberg):

• Mulitple Sequent Systems - such as
  • High-order Sequents (sequents of sequents), K. Doŝen and later P. Schröder-Heister
  • Hypersequents (lists of multisets of sequents), A. Avron, (with similar work by E.W. Beth, G. Pottinger, G. Sambin)
• Multi-Sided Sequents - when sides of sequent assumed to correspond with true/false as with semantic tableau, so multi-sided systems used for finite-valued logics by Rousseau, Takahashi
• Multi-Arrow Systems - sequent arrow generalised, useful for fuzzy logics with ≤ and < relations as arrows, M. Baaz, A. Ciabattoni
• Multi-Comma Systems - structural connectives designating multiple kinds of commas, e.g. N. Belnap (Display Logic), G. Mints, Dunn
• Multi-Level Inference - allows inference as levels other than outmost level, e.g. deep inference or calculus of structures
• Multi-Formula Systems - allows annotation of formulae or other aspects of the sequent with "labels" and "relations". Kanger, Maslov, then later D. M. Gabbay, Blackburn. Can be seen as extending the notion of what a logical formula is.

Many systems combine these, e.g. tree hypersequents combine multiple sequent systems with multi-level systems, or relational hypersequents being combination of multiple sequent systems and multi-arrow systems.

Also note that semantic tableau can be viewed as an alternative notation for sequents, according to M. Fitting. —Preceding unsigned comment added by 94.173.19.247 (talk) 14:54, 29 December 2010 (UTC)

By all means, {{sofixit}}. There is a dearth of qualified editors in logic around here. Tijfo098 (talk) 13:13, 7 April 2011 (UTC)

Examples of proof calculi which are not analytic?

It is written: "structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof". Isn't proof theory essentially structural in this sense? What are examples of proof calculi that do not support a notion of analytic proofs? For instance, Hilbert systems are analytic too (their normal proofs are the normal forms of their interpretation as combinators via the correspondence between Hilbert systems and combinatory logic. Hugo Herbelin (talk) 22:55, 13 January 2017 (UTC)

@Hugo Herbelin: The point of structural proof theory is to be able to do semantics with it and provide a basis for the kind of thing model theory is used for. It's tricky to do this kind of thing with combinatory logic: how does the fact that you only need to consider normal forms help you to prove consistency of propositional logic? It's also the case that a calculus might fail to have analytic proofs for all theorems: there are a number of formulations of S5 in vanilla sequent calculus with cut, but I don't believe it is possible to find one that allow cut-elimination. — Charles Stewart (talk) 20:36, 20 March 2019 (UTC)