Type-theoretical checking and philosophy of mathematics

下午到圖書館借 Saunders Mac Lane 的《Categories for the Working Mathematicians》，想說如果只是要看前面一點的話或許有機會看懂 XD。在附近瞄到一本《Twenty-Five Years of Constructive Type Theory》，裡面收錄 15 篇論文，包括一些大頭如 Per Martin-Löf 和 N.G. de Bruijn 的文章。其中 de Bruijn 的文章標題是〈Type-theoretical checking and philosophy of mathematics〉，就「machine-checked proofs 和數學活動的相互影響」發表一些看法，讀起來挺有趣的，摘錄兩段於下。第一段對 truth-value semantics 發了一點牢騷：

So natural deduction is by no means a new idea. On the contrary, it follows the way people reasoned before it was tried to explain logic by means of an algebra of truth values. Such Boolean logic is the metatheory of classical reasoning. It does not show what that reasoning is. It is silly that education in elementary logic so often takes truth values as the point of departure.

The idea that truth values are the basis of logic may have been one of the reasons why Brouwer's rejection of the law of the excluded middle was so little understood in his time. If one starts from Boolean logic instead of from natural deduction it is impossible to understand what that rejection means.

第二段對於 mathematical platonism 提出生動的比喻：

A historian writes about things that happened in the past, a journalist writes about what is happening today, but a novelist gets everything from his or her imagination. The first two write non-fiction, the novelist writes fiction, but all use the same language; there are no separate languages for fiction and non-fiction.

Mathematics seems to talk about things, but do these really exist? We seem to have no way to find out, and, worse, we have no way to express what we mean by existence. It is called mathematical platonism to consider the mathematician as a journalist, and anti-platonism to consider him or her as a novelist.

--
這種文章已經可以當作我的休閒讀物了 XD。