[Agda] Type Theory vs. Set Theory – Re: [Coq-Club] Why dependent type theory?

[Ken Kubota]

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 <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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200309/6c96bcbd/attachment.html>