Talk:Sequent calculus
From LLWiki
(Difference between revisions)
(Dealing with quantifiers) |
(→Equivalences: update comment) |
||
(11 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. |
+ | -- [[User:Olivier Laurent|Olivier Laurent]] 10:39, 15 March 2009 (UTC) |
− | -- [[User:Olivier Laurent|Olivier Laurent]] 18:37, 14 January 2009 (UTC) |
Latest revision as of 21: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)