Talk:Sequent calculus - Revision history

Olivier Laurent: /* Equivalences */ update comment

2013-04-25T20:01:20Z

‎Equivalences: update comment

Olivier Laurent: /* Equivalences */ pointer to provable formulas

2012-04-19T17:35:52Z

‎Equivalences: pointer to provable formulas

Samuel Mimram: /* Equivalences */

2009-03-23T18:55:59Z

‎Equivalences

Olivier Laurent: /* Equivalences */

2009-03-15T10:39:16Z

‎Equivalences

Olivier Laurent: /* Equivalences */ new section

2009-03-14T15:47:54Z

‎Equivalences: new section

Olivier Laurent: /* Two-sided sequent calculus */ closed topic

2009-03-14T15:46:10Z

‎Two-sided sequent calculus: closed topic

Olivier Laurent: /* Quantifiers */ closed topic

2009-03-14T15:45:43Z

‎Quantifiers: closed topic

Emmanuel Beffara: /* Quantifiers */

2009-01-21T16:07:12Z

‎Quantifiers

Olivier Laurent: /* Quantifiers */ indentation

2009-01-17T17:13:00Z

‎Quantifiers: indentation

Emmanuel Beffara: /* Quantifiers */

2009-01-17T16:10:10Z

‎Quantifiers

← Older revision		Revision as of 20:01, 25 April 2013
Line 2:		Line 2:

	Equivalences might deserve a specific page (maybe merged with [[isomorphism]]s and [[equiprovability]]?).		Equivalences might deserve a specific page (maybe merged with [[isomorphism]]s and [[equiprovability]]?).
−
−	This is also redundant with the principles described in [[semantics]].

	We might imagine a page or some pages giving a collection of [[Provable formulas\|valid principles]] of linear logic (with appropriate proofs) and specifying which ones correspond to implications, equivalences or isomorphisms.		We might imagine a page or some pages giving a collection of [[Provable formulas\|valid principles]] of linear logic (with appropriate proofs) and specifying which ones correspond to implications, equivalences or isomorphisms.

@@ Line 5: / Line 5: @@
 This is also redundant with the principles described in [[semantics]].
-We might imagine a page or some pages giving a collection of valid principles of linear logic (with appropriate proofs) and specifying which ones correspond to implications, equivalences or isomorphisms.
+We might imagine a page or some pages giving a collection of [[Provable formulas|valid principles]] of linear logic (with appropriate proofs) and specifying which ones correspond to implications, equivalences or isomorphisms.
 -- [[User:Olivier Laurent|Olivier Laurent]] 10:39, 15 March 2009 (UTC)

@@ Line 1: / Line 1: @@
 == Equivalences ==
-Equivalences might deserve a specific page (maybe merged with [[isomorphim]]s and [[equiprovability]]?).
+Equivalences might deserve a specific page (maybe merged with [[isomorphism]]s and [[equiprovability]]?).
 This is also redundant with the principles described in [[semantics]].

← Older revision		Revision as of 10:39, 15 March 2009
Line 3:		Line 3:
	Equivalences might deserve a specific page (maybe merged with [[isomorphim]]s and [[equiprovability]]?).		Equivalences might deserve a specific page (maybe merged with [[isomorphim]]s and [[equiprovability]]?).

−	-- [[User:Olivier Laurent\|Olivier Laurent]] 15:47, 14 March 2009 (UTC)	+	This is also redundant with the principles described in [[semantics]].
		+
		+	We might imagine a page or some pages giving a collection of valid principles of linear logic (with appropriate proofs) and specifying which ones correspond to implications, equivalences or isomorphisms.
		+
		+	-- [[User:Olivier Laurent\|Olivier Laurent]] 10:39, 15 March 2009 (UTC)

← Older revision	Revision as of 15:47, 14 March 2009
Line 1:	Line 1:
	+	== Equivalences ==
	+
	+	Equivalences might deserve a specific page (maybe merged with [[isomorphim]]s and [[equiprovability]]?).
	+
	+	-- [[User:Olivier Laurent\|Olivier Laurent]] 15:47, 14 March 2009 (UTC)

← Older revision		Revision as of 15:46, 14 March 2009
Line 1:		Line 1:
−	== Two-sided sequent calculus ==
−
−	I think the terminology "two-sided sequent calculus" should be used for the system where all the connectives are involved and all the rules are duplicated (with respect to the one-sided version) and negation is a connective.
−
−	In this way, we obtain the one-sided version from the two-sided one by:
−	* quotient the formulas by de Morgan laws and get negation only on atoms, negation is defined for compound formulas (not a connective)
−	* fold all the rules by <math>\Gamma\vdash\Delta \mapsto {}\vdash\Gamma\orth,\Delta</math>
−	* remove useless rules (negation rules become identities, almost all the rules appear twice)
−
−	A possible name for the two-sided system presented here could be "two-sided positive sequent calculus".
−
−	-- [[User:Olivier Laurent\|Olivier Laurent]] 21:34, 15 January 2009 (UTC)

← Older revision		Revision as of 15:45, 14 March 2009
Line 1:		Line 1:
−	== Quantifiers ==
−
−	The presentation does not seem to be completely uniform concerning quantifiers: are first-order quantifiers taken into account? It would be nice.
−
−	A few related points:
−	* Why a distinction between atomic formulas and propositional variables?
−	* Some mixing between <math>\forall x A</math> and <math>\forall X A</math>. I tried to propose a [[notations#formulas\|convention]] on that point, but it does not match here with the use of <math>\alpha</math> for atoms.
−	* Define immediate subformula of <math>\forall X A</math> as <math>A</math>?
−	-- [[User:Olivier Laurent\|Olivier Laurent]] 18:37, 14 January 2009 (UTC)
−
−	:I improved the uniformity for quantifiers: the full system with first and second order quantification is described, only predicate variables with first-order arguments are not described.
−	:The distinction between atomic formulas and propositional variables is because there are systems with atomic formulas that are not propositional variables but fixed predicates like equalities.
−	:I found <math>\alpha</math> to be a used notation for atomic formulas in other texts, so I used <math>\xi,\psi,\zeta</math> instead for arbitrary variables.
−
−	:Using substitution in the definition of subformulas is questionable, but if the only immediate subformula of <math>\forall\xi.A</math> is <math>A</math>, then the ''subformula'' property does not hold.
−
−	:''Edit:'' Well... my bad. The subformula property does hold if the only immediate subformula of <math>\forall\xi.A</math> is <math>A</math>, substitution is necessary only for <math>\exists\xi.A</math>. I changed it.
−
−	:-- [[User:Emmanuel Beffara\|Emmanuel Beffara]]
−
	== Two-sided sequent calculus ==		== Two-sided sequent calculus ==

← Older revision		Revision as of 16:07, 21 January 2009
Line 14:		Line 14:

	:Using substitution in the definition of subformulas is questionable, but if the only immediate subformula of <math>\forall\xi.A</math> is <math>A</math>, then the ''subformula'' property does not hold.		:Using substitution in the definition of subformulas is questionable, but if the only immediate subformula of <math>\forall\xi.A</math> is <math>A</math>, then the ''subformula'' property does not hold.
		+
		+	:''Edit:'' Well... my bad. The subformula property does hold if the only immediate subformula of <math>\forall\xi.A</math> is <math>A</math>, substitution is necessary only for <math>\exists\xi.A</math>. I changed it.

	:-- [[User:Emmanuel Beffara\|Emmanuel Beffara]]		:-- [[User:Emmanuel Beffara\|Emmanuel Beffara]]

@@ Line 1: / Line 1: @@
 == Quantifiers ==
-:The presentation does not seem to be completely uniform concerning quantifiers: are first-order quantifiers taken into account? It would be nice.
+The presentation does not seem to be completely uniform concerning quantifiers: are first-order quantifiers taken into account? It would be nice.
-I improved the uniformity for quantifiers: the full system with first and second order quantification is described, only predicate variables with first-order arguments are not described.
+A few related points:
-The distinction between atomic formulas and propositional variables is because there are systems with atomic formulas that are not propositional variables but fixed predicates like equalities.
+* Why a distinction between atomic formulas and propositional variables?
-I found <math>\alpha</math> to be a used notation for atomic formulas in other texts, so I used <math>\xi,\psi,\zeta</math> instead for arbitrary variables.
+* Some mixing between <math>\forall x A</math> and <math>\forall X A</math>. I tried to propose a [[notations#formulas|convention]] on that point, but it does not match here with the use of <math>\alpha</math> for atoms.
-Using substitution in the definition of subformulas is questionable, but if the only immediate subformula of <math>\forall\xi.A</math> is <math>A</math>, then the ''subformula'' property does not hold.
+:I improved the uniformity for quantifiers: the full system with first and second order quantification is described, only predicate variables with first-order arguments are not described.
--- [[User:Emmanuel Beffara|Emmanuel Beffara]]
+:Using substitution in the definition of subformulas is questionable, but if the only immediate subformula of <math>\forall\xi.A</math> is <math>A</math>, then the ''subformula'' property does not hold.
 == Two-sided sequent calculus ==