symmetric monoidal (∞,1)-category of spectra
The idea of a minor scale comes from Peter Freyd, in his attempt to give an algebraic (in the sense of universal algebra) description of the real interval, which he believed to be more fundamental than the real numbers themselves in analysis.
Certain minor scales are models of multiplicative linear logic.
Minor scales are an example of centipede mathematics; a lot of this page will be determining which of Freyd’s results in Algebraic Real Analysis still applies in minor scales and possible weakenings of the scale identity axiom.
Note: The terms multiplicative conjunction, multiplicative disjunction, linear implication, reverse linear implication, additive conjunction, and additive disjunction used in this page come from scales, which are algebraic models of multiplicative-additive linear logics. While the same operations may be defined in the same way in minor scales as in scales, the operations may no longer correspond to any linear logic at all, and are simply defined to reduce syntactical complexity in equational sentences and axioms.
A minor scale is a symmetric closed midpoint algebra $(M,\vert, \odot, (-)^\bullet, \bot, \top)$ with two binary operations $(-)\otimes(-):M\times M\to M$ called multiplicative conjunction and $(-)\oplus(-):M\times M\to M$ called multiplicative disjunction such that for all $a$ in $M$,
Note: linear implication is usually denoted using $\multimap$. We use $\rightarrowtail$ instead because there is no left-pointing $\multimap$ in LaTeX? for the dual linear implication, while there is $\leftarrowtail$
From $\rightarrowtail$ one could define the zoom operators.
$\bot$-zooming can be defined as
$a^\vee \coloneqq a^\bullet \rightarrowtail a$
$\top$-zooming can be defined as
$a^\wedge \coloneqq (a \rightarrowtail a^\bullet)^\bullet$
A minor scale is a symmetric closed midpoint algebra $(M,\vert, \odot, (-)^\bullet, \bot, \top)$ with two functions $(-)^\wedge:M\to M$ called $\top$-zooming and $(-)^\vee:M\to M$ called $\bot$-zooming such that for all $a$ in $M$,
A minor scale is a symmetric closed midpoint algebra $(M,\vert, \odot, (-)^\bullet, \bot, \top)$ with a function $(-)^\dagger:M\to M$ called central dilatation such that for all $a$ in $M$,
$\bot$-zooming can be defined as
$\top$-zooming can be defined as
Multiplicative conjunction can be defined as
Multiplicative disjunction can be defined as
Linear implication can be defined as
The binary operation additive conjunction is defined as
and additive disjunction is defined as
The binary operation dilatation is defined as
or as
Multiplication conjunction, multiplicative disjunction, $\top$-zooming, $\bot$-zooming, linear implication, and dual linear implication can all be defined in terms of each other, $\vert$, and $(-)^\bullet$.
operation | $a \otimes b$ | $a \oplus b$ | $a^\wedge$ | $a^\vee$ | $a \leftarrowtail b$ | $a \rightarrowtail b$ |
---|---|---|---|---|---|---|
$a \otimes b$ | $a \otimes b$ | $(a^\bullet \oplus b^\bullet)^\bullet$ | $(a\vert b)^\wedge$ | $((a^\bullet \vert b^\bullet)^\vee)^\bullet$ | $a^\bullet \leftarrowtail b$ | $(a \rightarrowtail b^\bullet)^\bullet$ |
$a \oplus b$ | $(a^\bullet \otimes b^\bullet)^\bullet$ | $a \oplus b$ | $((a^\bullet \vert b^\bullet)^\wedge)^\bullet$ | $(a \vert b)^\vee$ | $(a \leftarrowtail b^\bullet)^\bullet$ | $a^\bullet \rightarrowtail b$ |
$a^\wedge$ | $a \otimes a$ | $(a^\bullet \oplus a^\bullet)^\bullet$ | $a^\wedge$ | $((a^\bullet)^\vee)^\bullet$ | $a^\bullet \leftarrowtail a$ | $(a \rightarrowtail a^\bullet)^\bullet$ |
$a^\vee$ | $(a^\bullet \otimes a^\bullet)^\bullet$ | $a \oplus a$ | $((a^\bullet)^\wedge)^\bullet$ | $a^\vee$ | $(a \leftarrowtail a^\bullet)^\bullet$ | $a^\bullet \rightarrowtail a$ |
$a \leftarrowtail b$ | $a^\bullet \otimes b$ | $(a \oplus b^\bullet)^\bullet$ | $(a^\bullet \vert b)^\wedge$ | $((a \vert b^\bullet)^\vee)^\bullet$ | $a \leftarrowtail b$ | $(a^\bullet \rightarrowtail b^\bullet)^\bullet$ |
$a \rightarrowtail b$ | $(a \otimes b^\bullet)^\bullet$ | $a^\bullet \oplus b$ | $((a \vert b^\bullet)^\wedge)^\bullet$ | $(a^\bullet \vert b)^\vee$ | $(a^\bullet \leftarrowtail b^\bullet)^\bullet$ | $a \rightarrowtail b$ |
Here is a list of other possible equational axioms that a minor scale might satisfy:
The rest of the axioms follow from the scale identities:
Every minor scale with $\bot = \top$ is trivial.
$\bot$ is a fixed point of $(-)^\vee$ and $\top$ is a fixed point of $(-)^\wedge$.
As a minor scale is a closed midpoint algebra, a minor scale has a partial order $\leq$. If $a \leq b$, then $a \multimap b = \top$.
The currying of $\vartriangleleft$ results in a dilatation at an element $(-)\vartriangleleft:M\to (M\to M)$. For every element $a$ in $M$, dilatation at $a$ is a retraction of contraction at $a$: $(a\vartriangleleft) \circ (a\vert) = id_M$, where $id_M$ is the identity function on $M$.
The unit interval with $a \vert b \coloneqq \frac{a + b}{2}$, $\odot = \frac{1}{2}$, $a^\bullet = 1 - a$, $\bot = 0$, $\top = 1$, $a \otimes b = max(a + b - 1,0)$, $a \oplus b = min(a + b,1)$, $a^\wedge = max(2a - 1,0)$ and $a^\vee = min(2a,1)$ is an example of a minor scale.
The set of truth values in Girard’s linear logic is a minor scale.
Last revised on June 3, 2021 at 16:01:05. See the history of this page for a list of all contributions to it.