Notations

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(→‎Rule names: implicit R for one-sided)
 
(8 intermediate revisions by 4 users not shown)
Line 52: Line 52:
 
* First order quantification: <math>\forall x A</math> with substitution <math>A[t/x]</math>
  
* First order quantification: <math>\forall x A</math> with substitution <math>A[t/x]</math>
 
* Second order quantification: <math>\forall X A</math> with substitution <math>A[B/X]</math>
  
* Second order quantification: <math>\forall X A</math> with substitution <math>A[B/X]</math>
−
* Quantification of arbitrary order (mainly first or second): <math>\forall\alpha A</math> with substitution <math>A[\tau/\alpha]</math>
 +
* Quantification of arbitrary order (mainly first or second): <math>\forall\xi A</math> with substitution <math>A[\tau/\xi]</math>
   
 
=== Rule names ===
  
=== Rule names ===
Line 58: Line 58:
 
Name of the connective, followed by some additional information if required, followed by "L" for a left rule or "R" for a right rule. This is for a two-sided system, "R" is implicit for one-sided systems.
  
Name of the connective, followed by some additional information if required, followed by "L" for a left rule or "R" for a right rule. This is for a two-sided system, "R" is implicit for one-sided systems.
 
For example: <math>\wedge_1 \text{add} L</math>.
  
For example: <math>\wedge_1 \text{add} L</math>.
  +
  +
== Semantics ==
  +
  +
=== [[Coherent spaces]] ===
  +
* Web of the space <math>X</math>: <math>\web X</math>
  +
* Coherence relation of the space <math>X</math>: large <math>\coh_X</math> and strict <math>\scoh_X</math>
  +
  +
=== [[Finiteness spaces]] ===
  +
* Web of the finiteness space <math>\mathcal A</math>: <math>\web{\mathcal A}</math>
  +
* Finiteness structure of the space <math>\mathcal A</math>: <math>\mathfrak F(\mathcal A)</math> (we use <tt>\mathfrak</tt>, which is consistent with the fact that <math>\finpowerset{\web{\mathcal A}}\subseteq \mathfrak F(\mathcal A) \subseteq\powerset{\web{\mathcal A}}</math>).
  +
  +
  +
== [[A formal account of nets|Nets]] ==
  +
  +
* The free ports of a net <math>R</math>: <math>\mathrm{fp}(R)</math>.
  +
* The result of the connection of two nets <math>R</math> and <math>R'</math>, given the partial bijection <math>f:\mathrm{fp}(R)\pinj \mathrm{fp}(R')</math>: <math>R\bowtie_f R'</math>.
  +
* The number of loops in the resulting net: <math>\Inner{R}{R'}_f</math> (includes the loops already present in <math>R</math> and <math>R'</math>).
  +
  +
== Miscellaneous ==
  +
  +
* [[Isomorphism]]: <math>A\cong B</math>
  +
* injection: <math>A\hookrightarrow B</math>
  +
* partial injection: <math>A\pinj B</math>

Latest revision as of 12:56, 6 September 2012

Contents

[edit] Logical systems

For a given logical system such as MLL (for multiplicative linear logic), we consider the following variations:

Notation Meaning Connectives
MLL propositional without units X,{\tens},{\parr}
MLLu propositional with units only \one,\bot,{\tens},{\parr}
MLL0 propositional with units and variables X,\one,\bot,{\tens},{\parr}
MLL1 first-order without units X\vec{t},{\tens},{\parr},\forall x A,\exists x A
MLL01 first-order with units X\vec{t},\one,\bot,{\tens},{\parr},\forall x A,\exists x A
MLL2 second-order propositional without units X,{\tens},{\parr},\forall X A,\exists X A
MLL02 second-order propositional with units X,\one,\bot,{\tens},{\parr},\forall X A,\exists X A
MLL12 first-order and second-order without units X\vec{t},{\tens},{\parr},\forall x A,\exists x A,\forall X A,\exists X A
MLL012 first-order and second-order with units X\vec{t},\one,\bot,{\tens},{\parr},\forall x A,\exists x A,\forall X A,\exists X A

[edit] Formulas and proof trees

[edit] Formulas

  • First order quantification: \forall x A with substitution A[t / x]
  • Second order quantification: \forall X A with substitution A[B / X]
  • Quantification of arbitrary order (mainly first or second): \forall\xi A with substitution A[τ / ξ]

[edit] Rule names

Name of the connective, followed by some additional information if required, followed by "L" for a left rule or "R" for a right rule. This is for a two-sided system, "R" is implicit for one-sided systems. For example: \wedge_1 \text{add} L.

[edit] Semantics

[edit] Coherent spaces

  • Web of the space X: \web X
  • Coherence relation of the space X: large \coh_X and strict \scoh_X

[edit] Finiteness spaces

  • Web of the finiteness space \mathcal A: \web{\mathcal A}
  • Finiteness structure of the space \mathcal A: \mathfrak F(\mathcal A) (we use \mathfrak, which is consistent with the fact that \finpowerset{\web{\mathcal A}}\subseteq \mathfrak F(\mathcal A) \subseteq\powerset{\web{\mathcal A}}).


[edit] Nets

  • The free ports of a net R: fp(R).
  • The result of the connection of two nets R and R', given the partial bijection f:\mathrm{fp}(R)\pinj \mathrm{fp}(R'): R\bowtie_f R'.
  • The number of loops in the resulting net: \Inner{R}{R'}_f (includes the loops already present in R and R').

[edit] Miscellaneous

Retrieved from "http://llwiki.ens-lyon.fr/mediawiki/index.php?title=Notations&oldid=573"
Personal tools