余ハイティング代数

CSSのテストを兼ねて囲み記事にして書く。いずれにしても、携帯（タッチデバイス）では効かなくなる。

[補足]

(L, ∧, ∨, 1, 0)を分配束とする。束なので、∧も∨もベキ等可換で、ベキ等可換演算から導入される順序≦が、∧からでも∨からでも一致する（束の公理から）。1, 0は順序≦の最大元と最小元。

f_a(x) := x∧a で定義される単調写像が右随伴 g_a を持つとする。つまり、

• f_a(x) ≦ y ⇔ x ≦ g_a(y)
• あるいは、x∧a ≦ y ⇔ x ≦ a->y

これがハイティング代数の定義。

f_a(x) := x∨a で定義される単調写像が右随伴 g_a を持つとする。つまり、

• f_a(x) ≦ y ⇔ x ≦ g_a(y)
• あるいは、x∨a ≦ y ⇔ x ≦ y-a

これが余ハイティング代数の定義。
[/補足]