日記
今日も数学(集合論)をしようと思ってはいたものの、論理学に傾倒した結果いつもより全然していない。それにもかかわらず今日はいつもより進んだ。このことから同じようなことをただただし続けるというのもあまりよくはないのかもしれないと結論付けた
さてその論理学に関して、数学には証明論という証明を数学的に解釈するという学問がある。集合論を進めるにあたって、証明を既知の言語(日本語、英語、中国語、エスペラント...)で書くと不都合が生じるという事に気付いた。数学の証明とは論理の遷移であり、例えば式を解くという行為も左辺と右辺が等しいことを示すという証明題であると解釈した際には式変形を証明とみなすことができるが、この式を解く際もA=B=C...と式が論理的に変化する。このように一つの流れしかない証明は式を連ねるだけでいいのだが、例えば式に①、②、...の番号を振るような証明の際は複数の流れをまとめる必要がある。これは数式含めて書くと煩雑になりがちなためにあまり好きではなかったが、証明論にて用いられる手法を用いることでまとめることができ、さらには機械的に処理することもできる。いやはや今日も数学(集合論)をしようと思ってはいたものの、論理学に傾倒した結果いつもより全然していない。それにもかかわらず今日はいつもより進んだ。このことから同じようなことをただただし続けるというのもあまりよくはないのかもしれないと結論付けた
さてその論理学に関して、数学には証明論という証明を数学的に解釈するという学問がある。集合論を進めるにあたって、証明を既知の言語(日本語、英語、中国語、エスペラント...)で書くと不都合が生じるという事に気付いた。数学の証明というのは論理の遷移であり、例えば式を解くという行為も左辺と右辺が等しいことを示すという証明題であると解釈した際には式変形を証明とみなすことができるが、この式を解く際もA=B=C...と式が論理的に変化する。このように一つの流れしかない証明は式を連ねるだけでいいのだが、例えば式に①、②、...の番号を振るような証明の際は複数の流れをまとめる必要がある。これは数式含めて書くと煩雑になりがちなためにあまり好きではなかったが、証明論にて用いられる手法を用いることでこれらの異なった証明法を形式的に統一することができ、さらには機械的に処理することもできる。なかなかどうしてこれは素晴らしいものではないだろうか...
とばかり思っていたのだが、実際のところは余分にスペースは使うわ、機械的に処理すると言っても結局のところ人間が証明するわでわざわざ採用するメリットが低いようにも感じた
