nLab Heyting scale

Idea

The idea of a Heyting scale comes from Peter Freyd.

Definition

In terms of Heyting implication

A Heyting scale or chromatic scale is a scale $M$ with a Heyting implication operation $(-)\rightarrow(-):M \times M \to M$ such that

• $(\bot \rightarrow \bot)^\bullet = \bot$

• for all $a$ in $M$, $a \wedge (a \rightarrow \bot) = \bot$

• for all $a$ and $b$ in $M$, $((a \wedge b) \rightarrow \bot)^\bullet = (a \rightarrow \bot)^\bullet \wedge (b \rightarrow \bot)^\bullet$

In terms of support

…

Properties

Every Heyting scale with $\bot = \top$ is trivial.

Relation to Girard’s linear logic

…

Examples

The set of truth values in Girard’s linear logic is a Heyting scale.

Related concepts

• scale

• linear logic

References

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