nLab Heyting scale

Contents

Contents

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 MM with a Heyting implication operation ()():M×MM(-)\rightarrow(-):M \times M \to M such that

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

  • for all aa in MM, a(a)=a \wedge (a \rightarrow \bot) = \bot

  • for all aa and bb in MM, ((ab)) =(a) (b) ((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.

References

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

Last revised on June 2, 2021 at 15:14:21. See the history of this page for a list of all contributions to it.