[FOM] sugared foundations

[Harvey Friedman]

Some of us have offline been discussing the best way to lay down
foundations of mathematics so that it fully reflects or at least
largely reflects the needs of actual mathematicians writing actual
papers. The main proposals for doing this amount to sugared ZFC or
perhaps sugared NBG or other related systems with plenty of sugar.

The foundations must be formally rigorous yet have a full range of
notational conventions with completely rigorous semantics that
conveniently support conventional mathematical activity.

I worked on this some years ago without finishing it, and some of the
ideas made its way into

A language for mathematical knowledge management
Steven Kieffer, Jeremy Avigad, Harvey Friedman

and see

http://www.andrew.cmu.edu/user/avigad/Papers/mkm/index.html

One question that immediately arises is whether one should enforce set
theory, or maybe class theory with sets and classes of sets, or maybe
superclass theory with sets, classes of sets, classes of classes of
sets, or more. Or is there a point in trying to use (a variant of)
NFU?

This issues is really at the fundamental ontological level. But there
are all kinds of notational issues as well. Like taking natural
numbers as primitive, and using function variables, etc. Also the use
of some elemental lambda notation in order to rigorous and streamline
the horrible notation from calculus and analysis used for integration
and partial differentiation, etc.

Harvey Friedman