The Coq mailing list

[Ken Kubota <mail AT kenkubota.de>]

There are two problems with this quote in favor of set theory.

1. The axioms of set theory are historically contingent, i.e., they only cover the mathematics practiced at a given time.

For example, ZFC doesn’t cover large cardinals. An additional axiom is necessary.

One can easily generalize this argument by establishing new mathematical fields not covered by a given set of axioms.

As mentioned earlier:

I would consider type theory superior to set theory as type theory is a systematic approach, whereas the axioms of set theory are historically contingent.

https://groups.google.com/d/msg/lean-user/_A82awhFlcM/4odQJX3rCgAJ

2. It should be possible to derive all of mathematics from type theory (in particular, from a dependent type variant of Andrews' Q0).

This claim is not only stronger as is covers all (!) of mathematics possibly expressible (instead of only "the whole of known [!] mathematics").

Q0 was specifically designed in this spirit ("to derive practically the whole of [...] mathematics from a single source"), what Andrews calls "expressiveness".

The claim that a further developed variant of Q0 would be identical with (all of) mathematics was made earlier here:

https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/7fCLcrftCQAJ

See also this contribution:

Type Theory vs. Set Theory (HOL, Isabelle/HOL, Q0, and R0 vs. ZFC)

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-June/msg00000.html

In short:

While type theory is a systematic approach, set theory was an auxiliary solution useful for practical needs at that time.

Jean van Heijenoort had expressed this very precisely:

9. Jean van Heijenoort on the development of type theory and set theory: “In spite of the great advances that set theory was making, the very notion of set remained vague. The situation became critical after the appearance of the Burali-Forti paradox and intolerable after that of the Russell paradox, the latter involving the bare notions of set and element. One response to the challenge was Russell’s theory of types [...]. Another, coming at almost the same time, was Zermelo’s axiomatization of set theory. The two responses are extremely different; the former is a far-reaching theory of great significance for logic and even ontology, while the latter is an immediate answer to the pressing needs of the working mathematician.” [Heijenoort, 1967c, p. 199] 

https://owlofminerva.net/files/fom_2018.pdf#page=12

Kind regards,

Ken Kubota

____________________________________________________

Ken Kubota

doi.org/10.4444/100

Am 09.03.2020 um 01:25 schrieb Martin Escardo <m.escardo AT cs.bham.ac.uk>:

James,

This resonates a bit with what Bourbaki wrote in "Introduction to the
Theory of Sets",
http://sites.mathdoc.fr/archives-bourbaki/feuilleter.php?chap=2_REDAC_E1:

"... nowadays it is known to be possible, logically speaking, to derive
practically the whole of known mathematics from a single source, the
Theory of Sets. ... By so doing we do not claim to legislate for all
time. It may happen at some future date that mathematicians will agree
to use modes of reasoning which cannot be formalized in the language
described here; according to some, the recent evolution of axiomatic
homology theory would be a sign that this date is not so far. It would
then be necessary, if not to change the language completely, at least to
enlarge its rules of syntax. But this is for the future to decide."

(I learned this quote from Thierry Coquand.)

Martin

On 08/03/2020 13:35, James McKinna wrote:

Martin, on Fri, 06 Mar 2020, you wrote:

In other words, choose your proof assistant as a function of what you
want to talk about *and* how you want to talk about it. Martin

On 06/03/2020 21:05, Martin Escardo wrote:

The troubling aspect of proof assistants is that they not only
implement proof checking (and definition checking, construction
checking etc.) but that also that each of them proposes a new
foundation of mathematics.

Which is sometimes not precisely specified, as it is the case of e.g.
Agda. (Which is why I, as an Agda user, I confine myself to a
well-understood subset of Agda corresponding to a (particular)
well-understood type theory.

For mathematically minded users of proof assistants, like myself,
this is a problem. We are not interested in formal proofs per se. We
are interested in what we are talking about, with rigorously stated
assumptions about our universe of discourse.

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe