Talk:Sequent calculus

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(Quantifiers: subformula of <math>\forall X A</math>)
(Equivalences: update comment)
 
(10 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)
* Define immediate subformula of <math>\forall X A</math> as <math>A</math>?
 
-- [[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)

Personal tools