数学基礎論・数理論理学　その11

>>40
直観主義ブラウワーと形式主義ヒルベルトの論争があったように、
直観主義は本来は形式化に反対するものなので、
その論理の部分とか非論理的公理とかいうのはおかしいと言えばおかしいのだけど、
現代的視点で形式化した場合に、と断りを付けておくけど：

有名どころは、

扇定理(Fan Theorem) と
連続選択公理(実数の選択関数で連続なものが取れる)

かな。これだけでブラウワーの数学が形式化できるのか、
もっと公理が必要なのかはよく知らない。