[FOM] sugared foundations

[martdowd at aol.com]

 FOM
My book
 "A Beginner's Guide to Modern Set Theory"
 https://www.researchgate.net/publication/
  337334150_A_Beginner's_Guide_to_Modern_Set_Theory
attacks the problem from the opposite direction,
introducing set theory to beginning students.

Chapters 1-6 and chapters 11-12 provide a treatment of set theory
for mathematicians only interested in its utility for general mathematics.
Chapters 7-8 and 14 provide a formal treatment of the real numbers.

I favor the "classical" treatment of proper classes, as predicates on $V$,
with less formal uses considered as "abbreviations".

Martin Dowd

 
-----Original Message-----
From: Harvey Friedman <hmflogic at gmail.com>
To: Foundations of Mathematics <fom at cs.nyu.edu>
Sent: Mon, Nov 18, 2019 7:48 am
Subject: [FOM] sugared foundations

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
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
https://cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20191118/1cba0415/attachment.html>