Journal InTime

_ Brouwerの不動点定理と直観主義論理

Conceptual Mathematicsと並行して記号論理入門を読んでいるのだが、たまたまConceptual Mathematicsの方でBrouwerの不動点定理を取り上げた章を読んでいる時に、記号論理入門の方でBrouwerの名前が出て来て面白かった。

記号論理入門によると、Brouwerは「数学において排中律を無制限に用いるのは正当でない」と主張したそうで、古典論理から排中律を除いた論理体系を直観主義論理と呼ぶそうなのだが、Conceptual MathematicsのSession 10の§4の演習では背理法を使う必要があって、このケースでは排中律(を前提とする背理法)を使ってよいのかなと疑問に思った。

ところが、改めて前の§を読み返すと、p.125に以下のような記述があった。

We need to use another principle of logic, that not (not A) implies A, to reach `every f has a fixed point.' Brouwer himself seriously questioned this rule of logic; and we will later see that there are examples of useful categories in whose `internal' logic this rule does not hold.

[Conceptual Mathematicsより引用]

日本語に翻訳すると、以下のような意味だと思う。

「すべてのfは不動点をもつ」を導くためには、論理のもう一つの原理である「not (not A) ならば A」を使う必要があります。Brouwer自身はこの論理規則に対して深刻な疑問を呈していました。後に見るように、いくつかの有用な圏の例においては、その「内部の」論理ではこの規則が成り立ちません。

読み流していたけど、Brouwerの直観主義を踏まえて敢えてこういう構成になっているんだな、とちょっと感動した。 ちなみに「not (not A) ならば A」（¬¬A→A）は、排中律「A or not A」（A∨¬A）と同値である（記号論理入門 p.57）。

追記: 後で読み返したらここはBrouwerの証明をなぞっているだけで、別にこの本独自の構成というわけではないようだ。独自なのは、§5で二つの公理を導入することで、位相空間と連続写像の詳細を説明せずに、Brouwerの定理を一般化した定理［topological spaceだけでなくsmooth space（ってなんじゃらほい）などにおいても成り立つ］を導いているところのようだが、消化しきれていないので後でもう一度読む。