Hypersequent

Last updated August 18, 2024

In mathematical logic, the hypersequent framework is an extension of the proof-theoretical framework of sequent calculi used in structural proof theory to provide analytic calculi for logics that are not captured in the sequent framework. A hypersequent is usually taken to be a finite multiset of ordinary sequents, written

{\frac {\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Sigma \Rightarrow A\qquad \Omega _{1}\Rightarrow \Theta _{1}\mid \dots \mid \Omega _{m}\Rightarrow \Theta _{m}\mid \Pi \Rightarrow B}{\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Omega _{1}\Rightarrow \Theta _{1}\mid \dots \mid \Omega _{m}\Rightarrow \Theta _{m}\mid \Sigma \Rightarrow B\mid \Pi \Rightarrow A}}

or the modal splitting rule for the modal logic S5:^[1]

{\frac {\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Box \Sigma ,\Theta \Rightarrow \Box \Pi ,\Omega }{\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Box \Sigma \Rightarrow \Box \Pi \mid \Theta \Rightarrow \Omega }}

Hypersequent calculi have been used to treat modal logics, intermediate logics, and substructural logics. Hypersequents usually have a formula interpretation, i.e., are interpreted by a formula in the object language, nearly always as some kind of disjunction. The precise formula interpretation depends on the considered logic.

Formal definitions and propositional rules

Formally, a hypersequent is usually taken to be a finite multiset of ordinary sequents, written

\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}

The sequents making up a hypersequent consist of pairs of multisets of formulae, and are called the components of the hypersequent. Variants defining hypersequents and sequents in terms of sets or lists instead of multisets are also considered, and depending on the considered logic the sequents can be classical or intuitionistic. The rules for the propositional connectives usually are adaptions of the corresponding standard sequent rules with an additional side hypersequent, also called hypersequent context. E.g., a common set of rules for the functionally complete set of connectives $\{\bot ,\to \}$ for classical propositional logic is given by the following four rules:

{\frac {}{{\mathcal {G}}\mid \Gamma ,p\Rightarrow p,\Delta }}

{\frac {}{{\mathcal {G}}\mid \Gamma ,\bot \Rightarrow \Delta }}

{\frac {{\mathcal {G}}\mid \Gamma ,B\Rightarrow \Delta \qquad {\mathcal {G}}\mid \Gamma \Rightarrow A,\Delta }{{\mathcal {G}}\mid \Gamma ,A\to B\Rightarrow \Delta }}

${\frac {{\mathcal {G}}\mid \Gamma ,A\Rightarrow B,\Delta }{{\mathcal {G}}\mid \Gamma \Rightarrow A\to B,\Delta }}$

Due to the additional structure in the hypersequent setting, the structural rules are considered in their internal and external variants. The internal weakening and internal contraction rules are the adaptions of the corresponding sequent rules with an added hypersequent context:

{\frac {{\mathcal {G}}\mid \Gamma \Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma ,\Sigma \Rightarrow \Delta ,\Pi }}

${\frac {{\mathcal {G}}\mid \Gamma ,A,A\Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma ,A\Rightarrow \Delta }}$

${\frac {{\mathcal {G}}\mid \Gamma \Rightarrow A,A,\Delta }{{\mathcal {G}}\mid \Gamma \Rightarrow A,\Delta }}$

The external weakening and external contraction rules are the corresponding rules on the level of hypersequent components instead of formulae:

${\frac {\mathcal {G}}{{\mathcal {G}}\mid \Gamma \Rightarrow \Delta }}$

${\frac {{\mathcal {G}}\mid \Gamma \Rightarrow \Delta \mid \Gamma \Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma \Rightarrow \Delta }}$

Soundness of these rules is closely connected to the formula interpretation of the hypersequent structure, nearly always as some form of disjunction. The precise formula interpretation depends on the considered logic, see below for some examples.

Main examples

Modal logics

Hypersequents have been used to obtain analytic calculi for modal logics, for which analytic sequent calculi proved elusive. In the context of modal logics the standard formula interpretation of a hypersequent

\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}

is the formula

\Box (\bigwedge \Gamma _{1}\to \bigvee \Delta _{1})\lor \dots \lor \Box (\bigwedge \Gamma _{n}\to \bigvee \Delta _{n})

Here if $\Gamma$ is the multiset $A_{1},\dots ,A_{n}$ we write $\Box \Gamma$ for the result of prefixing every formula in $\Gamma$ with $\Box$ , i.e., the multiset $\Box A_{1},\dots ,\Box A_{n}$ . Note that the single components are interpreted using the standard formula interpretation for sequents, and the hypersequent bar $\mid$ is interpreted as a disjunction of boxes. The prime example of a modal logic for which hypersequents provide an analytic calculus is the logic S5. In a standard hypersequent calculus for this logic^[1] the formula interpretation is as above, and the propositional and structural rules are the ones from the previous section. Additionally, the calculus contains the modal rules

{\frac {{\mathcal {G}}\mid \Box \Gamma \Rightarrow A}{{\mathcal {G}}\mid \Box \Gamma \Rightarrow \Box A}}

${\frac {{\mathcal {G}}\mid \Gamma ,A\Rightarrow \Delta }{{\mathcal {G}}\mid \Gamma ,\Box A\Rightarrow \Delta }}$

${\frac {{\mathcal {G}}\mid \Box \Gamma ,\Sigma \Rightarrow \Box \Delta ,\Pi }{{\mathcal {G}}\mid \Box \Gamma \Rightarrow \Box \Delta \mid \Sigma \Rightarrow \Pi }}$

Admissibility of a suitably formulated version of the cut rule can be shown by a syntactic argument on the structure of derivations or by showing completeness of the calculus without the cut rule directly using the semantics of S5. In line with the importance of modal logic S5, a number of alternative calculi have been formulated.^[2]^[3]^[1]^[4]^[5]^[6]^[7] Hypersequent calculi have also been proposed for many other modal logics.^[6]^[7]^[8]^[9]

Intermediate logics

Hypersequent calculi based on intuitionistic or single-succedent sequents have been used successfully to capture a large class of intermediate logics, i.e., extensions of intuitionistic propositional logic. Since the hypersequents in this setting are based on single-succedent sequents, they have the following form:

\Gamma _{1}\Rightarrow A_{1}\mid \dots \mid \Gamma _{n}\Rightarrow A_{n}

The standard formula interpretation for such an hypersequent is

(\bigwedge \Gamma _{1}\to A_{1})\lor \dots \lor (\bigwedge \Gamma _{n}\to A_{n})

Most hypersequent calculi for intermediate logics include the single-succedent versions of the propositional rules given above and a selection of the structural rules. The characteristics of a particular intermediate logic are mostly captured using a number of additional structural rules. E.g., the standard calculus for intermediate logic LC, sometimes also called Gödel–Dummett logic, contains additionally the so-called communication rule:^[1]

{\frac {\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Sigma \Rightarrow A\qquad \Omega _{1}\Rightarrow \Theta _{1}\mid \dots \mid \Omega _{m}\Rightarrow \Theta _{m}\mid \Pi \Rightarrow B}{\Gamma _{1}\Rightarrow \Delta _{1}\mid \dots \mid \Gamma _{n}\Rightarrow \Delta _{n}\mid \Omega _{1}\Rightarrow \Theta _{1}\mid \dots \mid \Omega _{m}\Rightarrow \Theta _{m}\mid \Sigma \Rightarrow B\mid \Pi \Rightarrow A}}

Hypersequent calculi for many other intermediate logics have been introduced,^[1]^[10]^[11]^[12] and there are very general results about cut elimination in such calculi.^[13]

Substructural logics

As for intermediate logics, hypersequents have been used to obtain analytic calculi for many substructural logics and fuzzy logics.^[1]^[13]^[14]

History

The hypersequent structure seem to have appeared first in ^[2] under the name of cortege, to obtain a calculus for the modal logic S5. It seems to have been developed independently in ^[3], also for treating modal logics, and in the influential ^[1], where calculi for modal, intermediate and substructural logics are considered, and the term hypersequent is introduced.

Related Research Articles

In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axioms as much as possible to express the logical laws of deductive reasoning.

In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology instead of an unconditional tautology. Each conditional tautology is inferred from other conditional tautologies on earlier lines in a formal argument according to rules and procedures of inference, giving a better approximation to the natural style of deduction used by mathematicians than to David Hilbert's earlier style of formal logic, in which every line was an unconditional tautology. More subtle distinctions may exist; for example, propositions may implicitly depend upon non-logical axioms. In that case, sequents signify conditional theorems in a first-order language rather than conditional tautologies.

In logic, a substructural logic is a logic lacking one of the usual structural rules, such as weakening, contraction, exchange or associativity. Two of the more significant substructural logics are relevance logic and linear logic.

In quantum mechanics and quantum field theory, the propagator is a function that specifies the probability amplitude for a particle to travel from one place to another in a given period of time, or to travel with a certain energy and momentum. In Feynman diagrams, which serve to calculate the rate of collisions in quantum field theory, virtual particles contribute their propagator to the rate of the scattering event described by the respective diagram. Propagators may also be viewed as the inverse of the wave operator appropriate to the particle, and are, therefore, often called (causal) Green's functions.

In physics, the Hamilton–Jacobi equation, named after William Rowan Hamilton and Carl Gustav Jacob Jacobi, is an alternative formulation of classical mechanics, equivalent to other formulations such as Newton's laws of motion, Lagrangian mechanics and Hamiltonian mechanics.

In mathematical logic, structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof, a kind of proof whose semantic properties are exposed. When all the theorems of a logic formalised in a structural proof theory have analytic proofs, then the proof theory can be used to demonstrate such things as consistency, provide decision procedures, and allow mathematical or computational witnesses to be extracted as counterparts to theorems, the kind of task that is more often given to model theory.

In proof theory, the semantic tableau, also called an analytic tableau, truth tree, or simply tree, is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic. An analytic tableau is a tree structure computed for a logical formula, having at each node a subformula of the original formula to be proved or refuted. Computation constructs this tree and uses it to prove or refute the whole formula. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure for modal logics.

In quantum physics, the scattering amplitude is the probability amplitude of the outgoing spherical wave relative to the incoming plane wave in a stationary-state scattering process. At large distances from the centrally symmetric scattering center, the plane wave is described by the wavefunction

In physics, the Polyakov action is an action of the two-dimensional conformal field theory describing the worldsheet of a string in string theory. It was introduced by Stanley Deser and Bruno Zumino and independently by L. Brink, P. Di Vecchia and P. S. Howe in 1976, and has become associated with Alexander Polyakov after he made use of it in quantizing the string in 1981. The action reads:

In logic, a rule of inference is admissible in a formal system if the set of theorems of the system does not change when that rule is added to the existing rules of the system. In other words, every formula that can be derived using that rule is already derivable without that rule, so, in a sense, it is redundant. The concept of an admissible rule was introduced by Paul Lorenzen (1955).

In rotordynamics, the rigid rotor is a mechanical model of rotating systems. An arbitrary rigid rotor is a 3-dimensional rigid object, such as a top. To orient such an object in space requires three angles, known as Euler angles. A special rigid rotor is the linear rotor requiring only two angles to describe, for example of a diatomic molecule. More general molecules are 3-dimensional, such as water, ammonia, or methane.

In theoretical physics, the Wess–Zumino model has become the first known example of an interacting four-dimensional quantum field theory with linearly realised supersymmetry. In 1974, Julius Wess and Bruno Zumino studied, using modern terminology, dynamics of a single chiral superfield whose cubic superpotential leads to a renormalizable theory. It is a special case of 4D N = 1 global supersymmetry.

In mathematics and philosophy, Łukasiewicz logic is a non-classical, many-valued logic. It was originally defined in the early 20th century by Jan Łukasiewicz as a three-valued modal logic; it was later generalized to n-valued as well as infinitely-many-valued (ℵ₀-valued) variants, both propositional and first order. The ℵ₀-valued version was published in 1930 by Łukasiewicz and Alfred Tarski; consequently it is sometimes called the Łukasiewicz–Tarski logic. It belongs to the classes of t-norm fuzzy logics and substructural logics.

In fluid mechanics and mathematics, a capillary surface is a surface that represents the interface between two different fluids. As a consequence of being a surface, a capillary surface has no thickness in slight contrast with most real fluid interfaces.

In statistical decision theory, where we are faced with the problem of estimating a deterministic parameter (vector) $from observations an estimator is called minimax if its maximal risk is minimal among all estimators of . In a sense this means that is an estimator which performs best in the worst possible case allowed in the problem.$

<span class="mw-page-title-main">Variance gamma process</span> Concept in probability

In the theory of stochastic processes, a part of the mathematical theory of probability, the variance gamma (VG) process, also known as Laplace motion, is a Lévy process determined by a random time change. The process has finite moments, distinguishing it from many Lévy processes. There is no diffusion component in the VG process and it is thus a pure jump process. The increments are independent and follow a variance-gamma distribution, which is a generalization of the Laplace distribution.

In mathematical physics, the Belinfante–Rosenfeld tensor is a modification of the stress–energy tensor that is constructed from the canonical stress–energy tensor and the spin current so as to be symmetric yet still conserved.

The Maxwell–Bloch equations, also called the optical Bloch equations describe the dynamics of a two-state quantum system interacting with the electromagnetic mode of an optical resonator. They are analogous to the Bloch equations which describe the motion of the nuclear magnetic moment in an electromagnetic field. The equations can be derived either semiclassically or with the field fully quantized when certain approximations are made.

In theoretical physics, more specifically in quantum field theory and supersymmetry, supersymmetric Yang–Mills, also known as super Yang–Mills and abbreviated to SYM, is a supersymmetric generalization of Yang–Mills theory, which is a gauge theory that plays an important part in the mathematical formulation of forces in particle physics. It is a special case of 4D N = 1 global supersymmetry.

A non-normal modal logic is a variant of modal logic that deviates from the basic principles of normal modal logics.

References

1 2 3 4 5 6 7 Avron, Arnon (1996). "The method of hypersequents in the proof theory of propositional non-classical logics". Logic: From Foundations to Applications. pp. 1–32. ISBN 978-0-19-853862-2.
1 2 Mints, Grigori (1971). "On some calculi of modal logic". Proc. Steklov Inst. Of Mathematics. 98: 97–122.
1 2 Pottinger, Garrell (1983). "Uniform, cut-free formulations of T, S4 and S5 (abstract)". J. Symb. Log. 48 (3): 900.
↑ Poggiolesi, Francesca (2008). "A cut-free simple sequent calculus for modal logic S5" (PDF). Rev. Symb. Log. 1: 3–15. doi:10.1017/S1755020308080040. S2CID 37437016.
↑ Restall, Greg (2007). Dimitracopoulos, Costas; Newelski, Ludomir; Normann, Dag; Steel, John R (eds.). "Proofnets for S5: Sequents and circuits for modal logic". Logic Colloquium 2005. Lecture Notes in Logic. 28: 151–172. doi:10.1017/CBO9780511546464.012. hdl: 11343/31712 . ISBN 9780511546464.
1 2 Kurokawa, Hidenori (2014). "Hypersequent Calculi for Modal Logics Extending S4". New Frontiers in Artificial Intelligence. Lecture Notes in Computer Science. Vol. 8417. pp. 51–68. doi:10.1007/978-3-319-10061-6_4. ISBN 978-3-319-10060-9.
1 2 Lahav, Ori (2013). "From Frame Properties to Hypersequent Rules in Modal Logics". 2013 28th Annual ACM–IEEE Symposium on Logic in Computer Science . pp. 408–417. doi:10.1109/LICS.2013.47. ISBN 978-1-4799-0413-6. S2CID 221813.
↑ Indrzejczak, Andrzej (2015). "Eliminability of cut in hypersequent calculi for some modal logics of linear frames". Information Processing Letters . 115 (2): 75–81. doi:10.1016/j.ipl.2014.07.002.
↑ Lellmann, Björn (2016). "Hypersequent rules with restricted contexts for propositional modal logics". Theor. Comput. Sci. 656: 76–105. doi: 10.1016/j.tcs.2016.10.004 .
↑ Ciabattoni, Agata; Ferrari, Mauro (2001). "Hypersequent calculi for some intermediate logics with bounded Kripke models". J. Log. Comput. 11 (2): 283–294. doi:10.1093/logcom/11.2.283.
↑ Ciabattoni, Agata; Maffezioli, Paolo; Spendier, Lara (2013). Galmiche, Didier; Larchey-Wendling, Dominique (eds.). "Hypersequent and Labelled Calculi for Intermediate Logics". Tableaux 2013: 81–96.
↑ Baaz, Matthias; Ciabattoni, Agata; Fermüller, Christian G. (2003). "Hypersequent Calculi for Gödel Logics – A Survey". J. Log. Comput. 13 (6): 835–861. CiteSeerX 10.1.1.8.5319 . doi:10.1093/logcom/13.6.835.
1 2 Ciabattoni, Agata; Galatos, Nikolaos; Terui, Kazushige (2008). "From Axioms to Analytic Rules in Nonclassical Logics". 2008 23rd Annual IEEE Symposium on Logic in Computer Science. pp. 229–240. CiteSeerX 10.1.1.405.8176 . doi:10.1109/LICS.2008.39. ISBN 978-0-7695-3183-0. S2CID 7456109.
↑ Metcalfe, George; Olivetti, Nicola; Gabbay, Dov (2008). Proof theory for fuzzy logics. Springer, Berlin.

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[:0-1] 1 2 3 4 5 6 7 Avron, Arnon (1996). "The method of hypersequents in the proof theory of propositional non-classical logics". Logic: From Foundations to Applications. pp. 1–32. ISBN 978-0-19-853862-2.

[:4-2] 1 2 Mints, Grigori (1971). "On some calculi of modal logic". Proc. Steklov Inst. Of Mathematics. 98: 97–122.

[:5-3] 1 2 Pottinger, Garrell (1983). "Uniform, cut-free formulations of T, S4 and S5 (abstract)". J. Symb. Log. 48 (3): 900.

[4] Poggiolesi, Francesca (2008). "A cut-free simple sequent calculus for modal logic S5" (PDF). Rev. Symb. Log. 1: 3–15. doi:10.1017/S1755020308080040. S2CID 37437016.

[5] Restall, Greg (2007). Dimitracopoulos, Costas; Newelski, Ludomir; Normann, Dag; Steel, John R (eds.). "Proofnets for S5: Sequents and circuits for modal logic". Logic Colloquium 2005. Lecture Notes in Logic. 28: 151–172. doi:10.1017/CBO9780511546464.012. hdl: 11343/31712 . ISBN 9780511546464.

[:1-6] 1 2 Kurokawa, Hidenori (2014). "Hypersequent Calculi for Modal Logics Extending S4". New Frontiers in Artificial Intelligence. Lecture Notes in Computer Science. Vol. 8417. pp. 51–68. doi:10.1007/978-3-319-10061-6_4. ISBN 978-3-319-10060-9.

[:2-7] 1 2 Lahav, Ori (2013). "From Frame Properties to Hypersequent Rules in Modal Logics". 2013 28th Annual ACM–IEEE Symposium on Logic in Computer Science . pp. 408–417. doi:10.1109/LICS.2013.47. ISBN 978-1-4799-0413-6. S2CID 221813.

[8] Indrzejczak, Andrzej (2015). "Eliminability of cut in hypersequent calculi for some modal logics of linear frames". Information Processing Letters . 115 (2): 75–81. doi:10.1016/j.ipl.2014.07.002.

[9] Lellmann, Björn (2016). "Hypersequent rules with restricted contexts for propositional modal logics". Theor. Comput. Sci. 656: 76–105. doi: 10.1016/j.tcs.2016.10.004 .

[10] Ciabattoni, Agata; Ferrari, Mauro (2001). "Hypersequent calculi for some intermediate logics with bounded Kripke models". J. Log. Comput. 11 (2): 283–294. doi:10.1093/logcom/11.2.283.

[11] Ciabattoni, Agata; Maffezioli, Paolo; Spendier, Lara (2013). Galmiche, Didier; Larchey-Wendling, Dominique (eds.). "Hypersequent and Labelled Calculi for Intermediate Logics". Tableaux 2013: 81–96.

[12] Baaz, Matthias; Ciabattoni, Agata; Fermüller, Christian G. (2003). "Hypersequent Calculi for Gödel Logics – A Survey". J. Log. Comput. 13 (6): 835–861. CiteSeerX 10.1.1.8.5319 . doi:10.1093/logcom/13.6.835.

[:3-13] 1 2 Ciabattoni, Agata; Galatos, Nikolaos; Terui, Kazushige (2008). "From Axioms to Analytic Rules in Nonclassical Logics". 2008 23rd Annual IEEE Symposium on Logic in Computer Science. pp. 229–240. CiteSeerX 10.1.1.405.8176 . doi:10.1109/LICS.2008.39. ISBN 978-0-7695-3183-0. S2CID 7456109.

[14] Metcalfe, George; Olivetti, Nicola; Gabbay, Dov (2008). Proof theory for fuzzy logics. Springer, Berlin.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]