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.
There are various fragments of linear logic that contain the multiplicative conjunction. For instance, multiplicative linear logic (MLL) contains $\otimes$ along with its unit $\mathbf{1}$ and also the multiplicative disjunction $\parr$ and its unit $\bot$ and the linear negation $(-)^\bot$. While multiplicative intuitionistic linear logic (MILL) contains $\otimes$ and $\mathbf{1}$ along with the linear implication $\multimap$.
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 November 12, 2019 at 09:19:00. See the history of this page for a list of all contributions to it.