Talk:Sequent calculus
From LLWiki
(Difference between revisions)
(→Two-sided sequent calculus: new section) |
(→Equivalences: update comment) |
||
| (9 intermediate revisions by 3 users not shown) | |||
| Line 1: | Line 1: | ||
| − | == Quantifiers == |
+ | == Equivalences == |
| − | The presentation does not seem to be completely uniform concerning quantifiers: are first-order quantifiers taken into account? It would be nice. |
+ | Equivalences might deserve a specific page (maybe merged with [[isomorphism]]s and [[equiprovability]]?). |
| − | A few related points: |
+ | 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. |
| − | * 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) |
||
| − | == Two-sided sequent calculus == |
+ | -- [[User:Olivier Laurent|Olivier Laurent]] 10:39, 15 March 2009 (UTC) |
| − | |||
| − | 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) |
||
Latest revision as of 22:01, 25 April 2013
[edit] Equivalences
Equivalences might deserve a specific page (maybe merged with isomorphisms and equiprovability?).
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.
-- Olivier Laurent 10:39, 15 March 2009 (UTC)
