Sequent calculus - Revision history

Olivier Laurent: /* Equivalence */ Link to List of equivalences

2013-10-28T14:46:27Z

‎Equivalence: Link to List of equivalences

Emmanuel Beffara: /* Reversibility */ mention focalization

2012-08-31T21:21:59Z

‎Reversibility: mention focalization

Olivier Laurent: /* Variations */ Mix

2011-02-21T15:09:55Z

‎Variations: Mix

Emmanuel Beffara: /* Sequents and proofs */

2010-12-09T14:30:46Z

‎Sequents and proofs

Olivier Laurent: /* Exponential rules */ multiplexing

2009-03-19T20:40:19Z

‎Exponential rules: multiplexing

Olivier Laurent: /* Variations */ multi-fonctorial promotion and digging

2009-03-19T20:05:37Z

‎Variations: multi-fonctorial promotion and digging

Olivier Laurent: /* Sequents and proofs */ additional context in promotion rules

2009-03-19T19:39:19Z

‎Sequents and proofs: additional context in promotion rules

Olivier Laurent: /* Fundamental equivalences */ pointer to the lattice of exponential modalities

2009-03-14T15:39:42Z

‎Fundamental equivalences: pointer to the lattice of exponential modalities

Emmanuel Beffara: Markup and a typo

2009-03-14T14:43:50Z

Markup and a typo

Emmanuel Beffara: Made the two-sided system the reference one, presenting the one-sided system as a simplification

2009-03-10T15:30:23Z

Made the two-sided system the reference one, presenting the one-sided system as a simplification

Show changes

@@ Line 453: / Line 453: @@
 Any pair of connectives that has the same rules as <math>\tens/\parr</math> is
 equivalent to it, the same holds for additives, but not for exponentials.
 == Properties of proofs ==

@@ Line 625: / Line 625: @@
 cuts, since in the case of <math>\with</math> we duplicated a part of the
 original proof.}}
 == One-sided sequent calculus ==

← Older revision		Revision as of 15:09, 21 February 2011
Line 795:		Line 795:
	* [[Intuitionistic linear logic]] is the two-sided system where the right-hand side is constrained to always contain exactly one formula (with a few associated restrictions).		* [[Intuitionistic linear logic]] is the two-sided system where the right-hand side is constrained to always contain exactly one formula (with a few associated restrictions).
	* Similar restrictions are used in various [[semantics]] and [[proof search]] formalisms.		* Similar restrictions are used in various [[semantics]] and [[proof search]] formalisms.
		+
		+	=== Mix rules ===
		+
		+	It is quite common to consider [[Mix\|mix rules]]:
		+	<math>
		+	\LabelRule{\rulename{Mix}_0}
		+	\NulRule{\vdash}
		+	\DisplayProof
		+	\qquad
		+	\AxRule{\Gamma \vdash \Delta}
		+	\AxRule{\Gamma' \vdash \Delta'}
		+	\LabelRule{\rulename{Mix}_2}
		+	\BinRule{\Gamma,\Gamma' \vdash \Delta,\Delta'}
		+	\DisplayProof
		+	</math>

@@ Line 192: / Line 192: @@
 \DisplayProof
 </math> &emsp; <math>
-\AxRule{ \Gamma \vdash, A \Delta }
+\AxRule{ \Gamma \vdash A, \Delta }
-\AxRule{ \Gamma \vdash, B \Delta }
+\AxRule{ \Gamma \vdash B, \Delta }
 \LabelRule{ \with_R }
-\BinRule{ \Gamma, A \with B \vdash \Delta }
+\BinRule{ \Gamma \vdash A \with B, \Delta }
 \DisplayProof
 </math>

@@ Line 750: / Line 750: @@
 === Exponential rules ===
-The promotion rule, on the right-hand side for example,
+* The promotion rule, on the right-hand side for example,
 <math>
 \AxRule{ \oc A_1, \ldots, \oc A_n \vdash B, \wn B_1, \ldots, \wn B_m }
@@ Line 774: / Line 774: @@
 Note that digging violates the subformula property.
 === Non-symmetric sequents ===

← Older revision		Revision as of 20:05, 19 March 2009
Line 747:		Line 747:

	== Variations ==		== Variations ==
		+
		+	=== Exponential rules ===
		+
		+	The promotion rule, on the right-hand side for example,
		+	<math>
		+	\AxRule{ \oc A_1, \ldots, \oc A_n \vdash B, \wn B_1, \ldots, \wn B_m }
		+	\LabelRule{ \oc_R }
		+	\UnaRule{ \oc A_1, \ldots, \oc A_n \vdash \oc B, \wn B_1, \ldots, \wn B_m }
		+	\DisplayProof
		+	</math>
		+	can be replaced by a ''multi-functorial'' promotion rule
		+	<math>
		+	\AxRule{ A_1, \ldots, A_n \vdash B, B_1, \ldots, B_m }
		+	\LabelRule{ \oc_R \rulename{mf}}
		+	\UnaRule{ \oc A_1, \ldots, \oc A_n \vdash \oc B, \wn B_1, \ldots, \wn B_m }
		+	\DisplayProof
		+	</math>
		+	and a ''digging'' rule
		+	<math>
		+	\AxRule{ \Gamma \vdash \wn\wn A, \Delta }
		+	\LabelRule{ \wn\wn}
		+	\UnaRule{ \Gamma \vdash \wn A, \Delta }
		+	\DisplayProof
		+	</math>,
		+	without modifying the provability.
		+
		+	Note that digging violates the subformula property.
		+
		+	=== Non-symmetric sequents ===

	The same remarks that lead to the definition of the one-sided calculus can		The same remarks that lead to the definition of the one-sided calculus can

@@ Line 225: / Line 225: @@
 \DisplayProof
 </math> &emsp; <math>
-\AxRule{ \oc A_1, \ldots, \oc A_n \vdash B }
+\AxRule{ \oc A_1, \ldots, \oc A_n \vdash B ,\wn B_1, \ldots, \wn B_m }
 \LabelRule{ \oc_R }
-\UnaRule{ \oc A_1, \ldots, \oc A_n \vdash \oc B }
+\UnaRule{ \oc A_1, \ldots, \oc A_n \vdash \oc B ,\wn B_1, \ldots, \wn B_m }
 \DisplayProof
 </math>
@@ Line 246: / Line 246: @@
 \DisplayProof
 </math> &emsp; <math>
-\AxRule{ A \vdash \wn B_1, \ldots, \wn B_n }
+\AxRule{ \oc A_1, \ldots, \oc A_n, A \vdash \wn B_1, \ldots, \wn B_m }
 \LabelRule{ \wn_L }
-\UnaRule{ \wn A \vdash \wn B_1, \ldots, \wn B_n }
+\UnaRule{ \oc A_1, \ldots, \oc A_n, \wn A \vdash \wn B_1, \ldots, \wn B_m }
 \DisplayProof
 </math>

@@ Line 428: / Line 428: @@
 \wn\oc\wn\oc A \linequiv \wn\oc A </math> &emsp; <math>
 \wn\oc \bot \linequiv \bot </math>
 * Commutation of quantifiers (<math>\zeta</math> does not occur in <math>A</math>):
 *: <math>

@@ Line 303: / Line 303: @@
 An alternative presentation would be to define a sequent as a finite sequence
 of formulas and to add the exchange rules:
 : <math>
 \AxRule{ \Gamma_1, A, B, \Gamma_2 \vdash \Delta }
 \LabelRule{\rulename{exchange}_L}
@@ Line 332: / Line 332: @@
 Negation is involutive:
 : <math>A\linequiv A\biorth</math>
 Duality between connectives:
 {|
 |-
@@ Line 376: / Line 375: @@
 === Fundamental equivalences ===
-* Associativity, commutativity, neutrality: <br> <math>
+* Associativity, commutativity, neutrality:
 A \tens (B \tens C) \linequiv (A \tens B) \tens C </math> &emsp; <math>
 A \tens B \linequiv B \tens A </math> &emsp; <math>
-A \tens \one \linequiv A </math> <br> <math>
+A \tens \one \linequiv A </math>
 A \parr (B \parr C) \linequiv (A \parr B) \parr C </math> &emsp; <math>
 A \parr B \linequiv B \parr A </math> &emsp; <math>
-A \parr \bot \linequiv A </math> <br> <math>
+A \parr \bot \linequiv A </math>
 A \plus (B \plus C) \linequiv (A \plus B) \plus C </math> &emsp; <math>
 A \plus B \linequiv B \plus A </math> &emsp; <math>
-A \plus \zero \linequiv A </math> <br> <math>
+A \plus \zero \linequiv A </math>
 A \with (B \with C) \linequiv (A \with B) \with C </math> &emsp; <math>
 A \with B \linequiv B \with A </math> &emsp; <math>
 A \with \top \linequiv A </math>
-* Idempotence of additives: <br> <math>
+* Idempotence of additives:
 A \plus A \linequiv A </math> &emsp; <math>
 A \with A \linequiv A </math>
-* Distributivity of multiplicatives over additives: <br> <math>
+* Distributivity of multiplicatives over additives:
 A \tens (B \plus C) \linequiv (A \tens B) \plus (A \tens C) </math> &emsp; <math>
-A \tens \zero \linequiv \zero </math> <br> <math>
+A \tens \zero \linequiv \zero </math>
 A \parr (B \with C) \linequiv (A \parr B) \with (A \parr C) </math> &emsp; <math>
 A \parr \top \linequiv \top </math>
-* Defining property of exponentials: <br> <math>
+* Defining property of exponentials:
 \oc(A \with B) \linequiv \oc A \tens \oc B </math> &emsp; <math>
 \oc\top \linequiv \one </math>
-* Monoidal structure of exponentials: <br> <math>
+*: <math>
 \oc A \tens \oc A \linequiv \oc A </math> &emsp; <math>
-\oc \one \linequiv \one </math> <br> <math>
+\oc \one \linequiv \one </math>
 \wn A \parr \wn A \linequiv \wn A </math> &emsp; <math>
 \wn \bot \linequiv \bot </math>
-* Digging: <br> <math>
+* Digging:
 \oc\oc A \linequiv \oc A </math> &emsp; <math>
-\wn\wn A \linequiv \oc A </math>
+\wn\wn A \linequiv \wn A </math>
-* Other properties of exponentials: <br> <math>
+* Other properties of exponentials:
 \oc\wn\oc\wn A \linequiv \oc\wn A </math> &emsp; <math>
 \oc\wn \one \linequiv \one </math>
-* Commutation of quantifiers (<math>\zeta</math> does not occur in <math>A</math>): <br> <math>
+*: <math>
 \exists \xi. \exists \psi. A \linequiv \exists \psi. \exists \xi. A </math> &emsp; <math>
 \exists \xi.(A \plus B) \linequiv \exists \xi.A \plus \exists \xi.B </math> &emsp; <math>
 \exists \zeta.(A\tens B) \linequiv A\tens\exists \zeta.B </math> &emsp; <math>
-\exists \zeta.A \linequiv A </math> <br> <math>
+\exists \zeta.A \linequiv A </math>
 \forall \xi. \forall \psi. A \linequiv \forall \psi. \forall \xi. A </math> &emsp; <math>
 \forall \xi.(A \with B) \linequiv \forall \xi.A \with \forall \xi.B </math> &emsp; <math>
@@ Line 433: / Line 432: @@
 Any pair of connectives that has the same rules as <math>\tens/\parr</math> is
 equivalent to it, the same holds for additives, but not for exponentials.
 == Properties of proofs ==
@@ Line 623: / Line 618: @@
 The inference rules are essentially the same except that the left hand side of
 sequents is kept empty:
-* Identity group:<br><math>
+* Identity group:
 \LabelRule{\rulename{axiom}}
 \NulRule{ \vdash A\orth, A }
@@ Line 634: / Line 629: @@
 \DisplayProof
 </math>
-* Multiplicative group:<br><math>
+* Multiplicative group:
 \AxRule{ \vdash \Gamma, A }
 \AxRule{ \vdash \Delta, B }
@@ Line 655: / Line 650: @@
 \DisplayProof
 </math>
-* Additive group:<br><math>
+* Additive group:
 \AxRule{ \vdash \Gamma, A }
 \LabelRule{ \plus_1 }
@@ Line 676: / Line 671: @@
 \DisplayProof
 </math>
-* Exponential group:<br><math>
+* Exponential group:
 \AxRule{ \vdash \Gamma, A }
 \LabelRule{ d }
@@ Line 697: / Line 692: @@
 \DisplayProof
 </math>
-* Quantifier group (in the <math>\forall</math> rule, <math>\xi</math> must not occur free in <math>\Gamma</math>):<br><math>
+* Quantifier group (in the <math>\forall</math> rule, <math>\xi</math> must not occur free in <math>\Gamma</math>):
 \AxRule{ \vdash \Gamma, A[t/x] }
 \LabelRule{ \exists^1 }