「集合\(A\)が有限集合であるとは、ある自然数\(n\)に対し、\(A\)と\(\{0,1,\dotsc,n-1\}\)の間に全単射が存在することである。一方、有限集合ではない集合は無限集合である。」
「存在量化子\(\exists\)の有限回の除去は通常の論理でできるので、選択公理が力を発揮するのはもっぱら無限集合が相手の時である。」
……本当にそうだろうか？
「集合は有限集合か無限集合のどちらかだ」という考え方は排中律的であり、構成的数学では考え直す必要がある。
この記事では、「無限」ではないが「有限」とも言えない集合について考えたい。有限集合の定義は最初に書いたものとする。無限集合のちゃんとした定義はしない。
続きを読む構成的数学に基づいて解析学を展開し、プログラミングでそれを実装するようなコンテンツを作れないかなあと去年ぐらいから考えています。
構成的数学と一口に言っても、選択公理をどのくらい認めるかによっていくつか流儀があります。Bishopの構成的数学は従属選択公理 (dependent choice) を認めていますが、人によっては可算選択公理 (countable choice) すら使いたくないかもしれません。
Bishop流の構成的数学では、古典数学とそう変わらない実数論が展開されています。これは可算選択公理が使える、という点が大きそうです。
それでは、可算選択公理を仮定しない構成的数学だと実数の概念がどうなるか気になるのが人情だと思います。
続きを読む最近、某所で「数学とプログラムはどちらが易しいか」という話題が出ました。その場ではあまり上手い返しができなかったので、ブログ記事の題材にして供養します。
もちろん、この質問の答えは人によって違うでしょうし、人によって違うからこそ質問として意味があると言えるでしょう。この記事に書くのは私の見方、私の意見です。
短い答えが欲しい人向けに2択で答えておくと「私にとってはプログラムの方が易しい」となりますが、以下に長い答えを書きます。
続きを読む背理法による証明の例として、よく「\(\sqrt{2}\)が無理数であること」が挙がる。大まかな流れは以下の通りだ：
「\(\sqrt{2}\)が有理数だったと仮定し、\(\sqrt{2}=p/q\)（\(p\), \(q\)は互いに素）とおく。すると\(2q^2=p^2\)で、左辺が偶数なので右辺も偶数、よって\(p\)は\(p=2p’\)と書ける。すると\(q^2=2p’^2\)が得られて、\(q\)も偶数ということになる。これは『\(p\)と\(q\)は互いに素』という仮定に反する。よって、\(\sqrt{2}\)は有理数ではない（無理数である）。」
さて、数学の一部の流儀では使用する論理を制限することがある。構成的数学というのがその例で、大まかには「排中律を使わないような数学」つまり「直観主義論理に基づいた数学」が構成的数学になる（Brouwerの「直観主義」とは違うので注意されたい。あと、構成的数学の中でも選択公理をどの程度認めるかでバリエーションがあるようだ）。「\(\sqrt{2}\)が無理数である」という上記の証明は、構成的数学では受け入れられるのだろうか？
続きを読む前に「週刊 代数的実数を作る」という一連の記事を書きました。
あれの続きじゃないですが、また計算機代数周りの記事を書きたいなあと最近思っています。
せっかく書くなら、今度は構成的数学の視点を取り入れたいです。
続きを読む