natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
category with duals (list of them)
dualizable object (what they have)
ribbon category, a.k.a. tortile category
monoidal dagger-category?
In linear logic/linear type theory, one of the two linear versions of logical conjunction is called the multiplicative conjunction and usually denoted “$\otimes$”. The analogous connective in relevance logic is sometimes called the intensional conjunction or the fusion or cotenability, and sometimes denoted “$\circ$”.
The categorical semantics of the multiplicative conjunction is as the tensor product with respect to a (symmetric) monoidal category structure on the collection of types.
If one retains of all conjunctions in linear logic only the multiplicative conjunction, then one speaks of the fragment of linear logic called multiplicative linear logic or multiplicative intuitionistic linear logic or MILL for short. See also at linear type theory for more on this.
basic symbols used in logic
$\phantom{A}$symbol$\phantom{A}$ | $\phantom{A}$meaning$\phantom{A}$ |
---|---|
$\phantom{A}$$\in$ | $\phantom{A}$element relation |
$\phantom{A}$$\,:$ | $\phantom{A}$typing relation |
$\phantom{A}$$=$ | $\phantom{A}$equality |
$\phantom{A}$$\vdash$$\phantom{A}$ | $\phantom{A}$entailment / sequent$\phantom{A}$ |
$\phantom{A}$$\top$$\phantom{A}$ | $\phantom{A}$true / top$\phantom{A}$ |
$\phantom{A}$$\bot$$\phantom{A}$ | $\phantom{A}$false / bottom$\phantom{A}$ |
$\phantom{A}$$\Rightarrow$ | $\phantom{A}$implication |
$\phantom{A}$$\Leftrightarrow$ | $\phantom{A}$logical equivalence |
$\phantom{A}$$\not$ | $\phantom{A}$negation |
$\phantom{A}$$\neq$ | $\phantom{A}$negation of equality / apartness$\phantom{A}$ |
$\phantom{A}$$\notin$ | $\phantom{A}$negation of element relation $\phantom{A}$ |
$\phantom{A}$$\not \not$ | $\phantom{A}$negation of negation$\phantom{A}$ |
$\phantom{A}$$\exists$ | $\phantom{A}$existential quantification$\phantom{A}$ |
$\phantom{A}$$\forall$ | $\phantom{A}$universal quantification$\phantom{A}$ |
$\phantom{A}$$\wedge$ | $\phantom{A}$logical conjunction |
$\phantom{A}$$\vee$ | $\phantom{A}$logical disjunction |
$\phantom{A}$$\otimes$$\phantom{A}$ | $\phantom{A}$multiplicative conjunction$\phantom{A}$ |
$\phantom{A}$$\oplus$$\phantom{A}$ | $\phantom{A}$multiplicative disjunction$\phantom{A}$ |
Last revised on July 3, 2018 at 02:56:42. See the history of this page for a list of all contributions to it.