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
<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
<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
<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
<https://owlofminerva.net/files/fom_2018.pdf#page=12>
Kind regards,
Ken Kubota
____________________________________________________
Ken Kubota
doi.org/10.4444/100 <https://doi.org/10.4444/100>
> Am 09.03.2020 um 01:25 schrieb Martin Escardo <[email protected]>:
>
> 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
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/5A4889D8-3BD8-49E3-AFEE-ED1CEF457C2B%40kenkubota.de.
