Kurt Gödel Research Center

2013 seminar talk: Mathematics as open-ended human activities

Talk held by Masahiko Sato (Kyoto University, Japan) at the KGRC seminar on 2013-10-24.

Abstract

In this talk, I will explain how I view mathematics as open-ended human activities. I have gradually developed this view through my experience of designing and implementing a proof assistant which I call NF (Natural Framework).

NF is based on a theory of classes, which is rigorously describable in an informal metalanguage but is never completely formalizable since it is an open-ended theory. I will sketch the outline of the theory and the philosophy behind it.

NF has the following characteristics.

(1) NF is implemented on top of a simple programming language called Ez.

(2) Ez is implemented on top of its minimal sublanguage.

(3) Ez supports definitions and constructions of new finitary mathematical objects from scratch.

(4) Ez objects are either mutable or rigid (i.e., immutable).

(5) The background theory of NF/Ez is finitary, but in this finitary framework one can design and define any conceivable formal systems.

(6) Because of (3) above, NF/Ez is open-ended and extendable by the users.

I will also compare NF with other proof assistants and will argue that open-endedness of the system is essential to assist developing mathematics as open-ended human activities.