nLab minor scale

Idea

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.

Definition

In terms of multiplicative conjunction and disjunction

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$,

$$a \otimes b = b \otimes a$$

$$\bot \otimes a = \bot$$

$$a \otimes \top = a$$

$$a \oplus b = b \oplus a$$

$$\bot \oplus a = a$$

$$a \oplus \top = \top$$

In terms of linear implication

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$

In terms of zoom operations

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$,

$$(\bot \vert a)^\wedge = \bot$$

$$(\bot \vert a)^\vee = a$$

$$(a \vert \top)^\wedge = a$$

$$(a \vert \top)^\vee = \top$$

In terms of central dilatations

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$,

$$(\odot \vert a)^\dagger = a$$

$$(\top \vert (\top \vert a))^\dagger = \top$$

$$(\bot \vert (\bot \vert a))^\dagger = \bot$$

$\bot$-zooming can be defined as

$$a^\vee \coloneqq ((a \vert (\odot \vert \top))^\dagger)^\dagger$$

$\top$-zooming can be defined as

$$a^\wedge \coloneqq (((\bot \vert \odot) \vert a)^\dagger)^\dagger$$

Multiplicative conjunction can be defined as

$$a \otimes b \coloneqq (a \vert b)^\wedge$$

Multiplicative disjunction can be defined as

$$a \oplus b \coloneqq (a \vert b)^\vee$$

Linear implication can be defined as

$$a \multimap b \coloneqq a^\bullet \oplus b$$

Other operations

The binary operation additive conjunction is defined as

$$a \wedge b \coloneqq a \otimes (a^\bullet \oplus b)$$

and additive disjunction is defined as

$$a \vee b \coloneqq a \oplus (a^\bullet \otimes b)$$

The binary operation dilatation is defined as

$$a\vartriangleleft b \coloneqq ((a^\bullet \vert \bot)\oplus b)^\wedge$$

or as

$$a\vartriangleleft b \coloneqq ((a^\bullet \vert \top)\otimes b)^\vee$$

Defining operations in terms of other operations

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$

Additional possible equational axioms

Here is a list of other possible equational axioms that a minor scale might satisfy:

• the scale identities: for all $a$ and $b$ in $M$,

$$a \otimes b = (a^\vee \otimes b^\wedge) \vert (a^\wedge \otimes b^\vee)$$

$$a \oplus b = (a^\wedge \oplus b^\vee) \vert (a^\vee \oplus b^\wedge)$$

The rest of the axioms follow from the scale identities:

• $\top$ is a fixed point of $(-)^\vee$:

$$\top^\vee = \top$$

• $\bot$ is a fixed point of $(-)^\wedge$:

$$\bot^\wedge = \bot$$

• the axiom of compensation: for all $a$ in $M$,

$$a = a^\vee \vert a^\wedge$$

• the axioms of central distributivity: for all $a$ in $M$,

$$a \otimes \odot = a^\wedge \vert \bot$$

$$a \oplus \odot = a^\vee \vert \top$$

• the axiom of balance: for all $a$ and $b$ in $M$,

$$a \vert (a \multimap b) = b \vert (b \multimap a)$$

• the disjunction property: for all $a$ and $b$ in $M$,

$$(a \rightarrowtail b) \vee (b \rightarrowtail a) = \top$$

• the coalgebra equation: for all $a$ in $M$,

$$a^\vee \vee (a^\wedge)^\bullet = \top$$

• associativity of multiplicative conjunction: for all $a$, $b$, and $c$ in $M$

$$a \otimes (b \otimes c) = (a \otimes b) \otimes c$$

• associativity of multiplicative disjunction: for all $a$, $b$, and $c$ in $M$

$$a \oplus (b \oplus c) = (a \oplus b) \oplus c$$

• the various lattice axioms for $(M,\top,\bot,\wedge,\vee)$: for all $a$, $b$, and $c$ in $M$,

$$a \wedge a = a$$

$$a \wedge b = b \wedge a$$

$$a \wedge (b \wedge c) = (a \wedge b) \wedge c$$

$$\top \wedge a = a$$

$$a \vee a = a$$

$$a \vee b = b \vee a$$

$$a \vee (b \vee c) = (a \vee b) \vee c$$

$$\bot \vee a = a$$

$$a \wedge (a \vee b) = a$$

$$a \vee (a \wedge b) = a$$

• for all $a$ and $b$ in $M$,

$$(a \otimes b) \rightarrowtail (a^\wedge \vert b^\wedge) = \top$$

• for all $a$ and $b$ in $M$,

$$(a \oplus b) \leftarrowtail (a^\vee \vert b^\vee) = \bot$$

Properties

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$.

Examples

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.

Related concepts

• symmetric closed midpoint algebra

• scale

• linear logic

• centipede mathematics

References

• Peter Freyd, Algebraic real analysis, Theory and Applications of Categories, Vol. 20, 2008, No. 10, pp 215-306 (tac:20-10)