$1/0=0$ にはいろんな人が到達していたようです。Patrick Suppes は1957 年に『Introduction to Logic』という書籍を著しています。彼はこの中で，ロジカルに詰めると $1/0=0$ が出てくることを臭わす記述をしながら，そこで止めています。Proof asistant の…

定理証明支援システムと呼ばれるソフトウェアがあります。呼び方はいろいろあって，証明支援系とか証明支援言語などとも呼ばれています。西側では簡単に Proof assistant と呼ばれていて，これが一番わかりやすいかもしれません。 中身は命題を記述できる言…