$\newcommand{\defeq}{\mathrel{\mathop:}=}$

## 2009/02/22

### Type-theoretical checking and philosophy of mathematics

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.

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.

--

Labels:

XOO2/22/2009 3:29 pm 說：

MacLane 那本預設太多背景了, 不過是很好的嘗試 ... XD

Josh Ko2/23/2009 12:05 am 說：