Notations

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(Semantics: Notations for finiteness spaces)
m (Finiteness spaces: justify the notation of fniiteness structures)
Line 66: Line 66:
   
 
=== [[Finiteness spaces]] ===
 
=== [[Finiteness spaces]] ===
* Web of the space <math>\mathcal A</math>: <math>\web {\mathcal A}</math>
+
* 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>
+
* 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>).

Revision as of 15:48, 6 July 2009

Contents

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

Formulas and proof trees

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[τ / ξ]

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.

Semantics

Coherent spaces

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

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}}).
Personal tools