[FOM] Improving Set Theory

[Victor Makarov]

On Jan 11, 2020, 1:26 AM Arnold Neumaier wrote:
>All meaning (and hence all understanding) is eliminated when
>reducing mathematics to pure ZFC. Moreover, since the same
>mathematical concepts can be (and are in practice) encoded
>in ZFC in multiple (set theoretically inequivalent) ways,
>math encoded in ZFC is different depending on who does it.

>Are your real numbers Dedekind cuts of rationals or infinite
>decimal fractions or equivalence classes of Cauchy sequences,
>or....? It doesn't matter at all for the mathematics, and
>shouldn't matter for the foundations.

For the mathematician the real numbers are the elements of
the unique(up to an isomorphism) complete ordered
 field (R , + , · , <): see, for example,
en.wikipedia.org/wiki/Construction_of_the_real_numbers

Dedekind cuts is just a model of the theory of
complete ordered fields.

Jean Dieudonne (one of the creators of modern mathematics)
stated in his book "A Panorama of Pure Mathematics",p.215,
that any mathematical theory is an extension of Zermelo-
Fraenkel (ZF) set theory.

So the theory of real numbers is the extension of ZF by adding
to ZF the constants R , + , · , <  and the corresponding axioms.

>Indeed, most proof assistants used to encode advanced
>mathematics in fully formalized terms are not based on ZFC,
>and are incompatible with each other.

Recently John Harrison (the author of one of the best proof
assistants HOL Light, based on a type theory) gave a talk
"Let’s make set theory great again!"
http://aitp-conference.org/2018/slides/JH.pdf

where he criticized "not based on ZFC" approaches.

Victor Makarov
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200111/e1e3c6b2/attachment-0001.html>