Red cat の数学よもやま話・新装開店

はてなダイアリー「Red cat の数学よもやま話」から徐々にこちらに移行していきます。

直観主義論理の入り口~Heyting 代数~(その 10・最終回)

完備 Heyting 代数

Heyting 代数は束として完備であるとき, 完備 Heyting 代数(complete Heyting algebra)と言います. 良く cHa などと略されます.

同様に Boole 代数が束として完備であるとき, 完備 Boole 代数(complete Boole algebra, cBa)と言います.

既に見たように, Boole 代数は Heyting 代数なので, cBa は cHa になっていますが, 実は無限分配律
(\bigvee X) \wedge a = \bigvee (X \wedge a)
を満たす完備束 L は cHa となることが以下のように示されます. ただし X \subset L, a \in L に対して
X \wedge a = \{ x \wedge a | x \in X\}
と定義します.

P(a,b) = \{ x | x \wedge a \le b \} と置くとき, 完備性により \bigvee P(a,b) が存在します. このとき無限分配律が成り立つことにより
( \bigvee P(a,b) ) \wedge a = \bigvee(P(a,b) \wedge a) \le b
なので \bigvee P(a,b) \in P(a,b) が成り立ち, したがって \max P(a,b) が存在するので L は cHa.

Heyting 代数はなぜ直観主義論理への入り口なのか ?

今回, 「直観主義論理への入り口」と題して Heyting 代数を紹介してきましたが, なぜ Heyting 代数は直観主義論理への入り口なのでしょうか ?

既に見たように, (完備) Boole 代数では \neg \neg x = xx \vee \neg x = 1 と言った見慣れた式が成り立ちますが, (完備) Heyting 代数ではこれらの式は一般には成り立ちません.

古典論理は真偽値の集合を完備 Boole 代数に取ったものと考えられますが, もし, 真偽値の集合を完備 Heyting 代数に取ったらどうなるでしょうか ? そのような論理体系では, もはや排中律は成り立ちません.

これは一見すると少し変わった論理体系のように思えます. しかし, もう少し「人間的な」見方をすると, ある事柄 P について, P であることを確認する方法がなかったからと言って P ではないと言い切るのは自然でしょうか ?

このように, 実は排中律が成り立たない論理体系の方が実は人間の感覚により近いのです. そして, それを数学の言葉で実現するための入り口が Heyting 代数なのです.

完備 Heyting 代数は層の理論の定式化にも用いられ, 必然的に層と直観主義論理は密接な関係にあります.

このあたりの話を知りたい方には, 以下の書籍をお勧めします.

層・圏・トポス―現代的集合像を求めて

層・圏・トポス―現代的集合像を求めて

OD>直観主義的集合論 (紀伊國屋数学叢書 20)

OD>直観主義的集合論 (紀伊國屋数学叢書 20)

これらの書籍で用いられる圏の理論により詳しい書籍としては

Categories for the Working Mathematician (Graduate Texts in Mathematics)

Categories for the Working Mathematician (Graduate Texts in Mathematics)

和訳本もあります.

圏論の基礎

圏論の基礎

層の理論と論理学の関係については

Sheaves in Geometry and Logic: A First Introduction to Topos Theory (Universitext)

Sheaves in Geometry and Logic: A First Introduction to Topos Theory (Universitext)

補遺 : 古い束論の洋書などを参照する場合, Heyting 代数は "Brouwer lattices" という名称で紹介されています.