Scribble at 2024-04-24 10:16:02 Last modified: unmodified
Lean is a large project, but one need only trust its kernel to ensure that accepted proofs are correct. If a tactic were to output an incorrect proof term, then the kernel would have the opportunity to find this mistake before the proof were to be accepted.
theorem prover を使っている以上は、上に引用した（PDF の論文から）ところが大きなポイントになるはずで、いまごろクワインの NF を取り上げてるなんてのは新鮮な感じがするので興味をそそられるけれど、Lean について検証してみるかどうかと言われたら、あんまり興味ないんだよなぁ。
ていうか、分析哲学だろうと科学哲学だろうと、NF というか初等レベルの集合論を教科書で取り上げる事例すら殆どないわけで（まぁ海外でもそうだけど）、確かに誰かが言ったように、分析哲学でロジックを使った議論が多かったのは、単なる歴史的な偶然にすぎないというのは、確かにそうなんだろうと思う。昨今の「分析なになに」みたいな本にしても、書店で眺めてみた限りでは形式的なアプローチなんて殆どないし、それどころか概念分析としてすら厳密さに欠ける、殆ど社会学か英米文学のエッセイみたいなものを「分析哲学」と称してるわけだからね。