夏休みの自由研究：公理的関数論1 - ひかりちゃんの悲観的絵日記

やりたいこと

関数の体系を公理的に特徴づけ，関数の特別な場合として集合を定義したいです．
- 関数論の公理系ATFをつくります．

注意

特に先行研究とかは見ていません．
数学の素人が何の経験も無しでやるので，全然興味深くない体系ができたり，全然関数の特徴づけになっていなかったり，途中で矛盾したりするかもしれません．
これは私の夏休みの自由研究であり，とりあえず恐れずにやってみるの精神で行われています．

ATFの言語

通常の等号付1階述語論理に2座述語と3座述語を加えたもの．
- $Dxf$ は「 $x$ は $f$ の定義域に属する」と読みます．
- $Vfxy$ は「 $f(x)=y$ 」と読みます．

ATFの公理1

定義域の公理

「 $f(x)=y$ なる $y$ が存在するならば， $x$ は $f$ の定義域に属する」

$\forall f \forall x (\exists y Vfxy \rightarrow Dxf)$

空関数の公理

「ある関数が存在して，いかなる関数もその関数の定義域に属さない」

$\exists f \forall x \lnot Dxf$

外延性の公理

「定義域が同一であり，あらゆるところで値が一致するふたつの関数は同一の関数である」

$\forall f \forall g ( (\forall x (Dxf \leftrightarrow Dxg) \land \forall x \forall y ( Vfxy \leftrightarrow Vgxy)) \rightarrow f = g)$

単値性の公理

「 $f(x)=y$ かつ $f(x)=z$ ならば $y=z$ である」

$\forall x \forall y \forall z ( Vfxy \land Vfxz \rightarrow y = z )$

公理1のZFによるモデル

宇宙は $\{ \varnothing \}$ ．
$x$ の解釈として振られる集合を $x^\prime$ と書くことにします．
$Dxf$ は「 $\langle x^\prime, y \rangle \in f^\prime$ なる集合 $y$ が存在する」と解釈します．
$Vfxy$ は「 $\langle x^\prime, y^\prime \rangle \in f^\prime$ 」と解釈します．

　定義域と単値性に関しては，前件に $Vfxy$ とあり，ここで $f$ は $\varnothing$ と解釈されるので，常に偽．よって条件文全体は真となります．外延性に関しては，後件の $f = g$ が $f$ も $g$ も $\varnothing$ としてしか解釈されないので常に真．よって条件文全体は真となります．空関数に関しては， $f$ が $\varnothing$ として解釈されるとき $Dxf$ の解釈は「～なる順序対が $\varnothing$ に属するような $y$ が存在する」という形になっており， $\varnothing$ には何も属さないので，常に偽．よって空関数も存在します．どうやら公理1はZFと相対的に無矛盾らしいです．

　なお，上記のようなモデルが存在するので，公理1は「ただひとつの関数しか存在しない」という主張と両立してしまいます．そうならないためには，色々な関数の存在を要請する公理を追加していく必要があります．とりあえず合成関数とか部分関数とかでしょうか．でも集合論で言う対とか和集合みたいなやつがないと大きな対象は作れなそうですよね．「こういう公理追加したら？」というオススメがあったら教えてください！

公理1からの帰結

　公理1から空関数に関する定理を導きます．

定理

空関数はひとつしかない．

　証明． $f$ と $g$ が空関数だとして，外延性公理によって両者が同一であることを示します．まず $Dxf \leftrightarrow Dxg$ という条件ですが，これは $f$ と $g$ が空関数であるため，双条件文の両辺が常に偽になるので成り立ちます．次に $Vfxy \leftrightarrow Vgxy$ ですが，たとえば左辺を仮定すると定義域の公理から $Dxf$ が導かれ，これは $f$ が空関数であることに反します．よって左辺は常に偽で，同様に右辺も常に偽なので，双条件文が成り立ちます．したがって，外延性公理から $f=g$ です．

　以上の議論から，空関数の存在と唯一性が保証されたので，今後空関数を $\varnothing$ で表します．

定理

任意の $x$ ， $y$ に対して， $\lnot V\varnothing xy$

　これは上の証明でも出てきた，「 $V\varnothing xy$ を仮定すると $Dx \varnothing$ となり矛盾」という話と同じですが， $\varnothing$ の「値域」が空だということを強調しています．

振り返り

　とりあえず「関数ってこんな感じかな～」と適当に公理を並べただけでです．空関数に関しては集合論とのアナロジーで，これがいけてるのかは分かりません．今のところ関数らしい関数が存在していないので単値性からの帰結は調べていません．原始述語もこれでいいのか感はありますね．4つの公理の独立性も調べていません．これは自由工作なので段々改良していければと思っています．皆様のアドバイスお待ちしています！

追記

　Twitterで「定義域の公理の逆を入れると外延性の公理は簡略化できる」とのご指摘をいただきました．つまり，

定義域の公理（改訂版）

「 $f(x)=y$ なる $y$ が存在するのは， $x$ が $f$ の定義域に属するときであり，かつそのときに限る」

$\forall f \forall x (\exists y Vfxy \leftrightarrow Dxf)$

となります．定義域に属する $x$ に対して関数によって値が振られていないということはないので，この逆を入れない理由はないですね（この逆を入れることは部分関数を認めないことだともお教えいただきました）．

　ここで，外延性の公理における $\forall x \forall y ( Vfxy \leftrightarrow Vgxy)$ を仮定し， $Dxf$ とすると，定義域の公理の「右から左」から $\exists y Vfxy$ がいえて，仮定から $\exists y Vgxy$ で（量化に関する議論を少し飛ばしてます），定義域の公理の「左から右」から $Dxg$ が出ます．同様に $Dxg$ から例の仮定のもとで $Dxf$ を導けるので，外延性の公理は