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

[Ken Kubota]

Hi Thorsten,

> Am 10.03.2020 um 12:10 schrieb Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk>:
> 
>  
> 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>
>  
> I don’t agree with this description. As set theory, type theory is an evolving system. For example a while ago we were using intensional type theory with uniqueness of identity proofs and now we have a much more extensional type theory with univalence and without uip. And also the question isn’t just wether we “can derive” all Mathematics but can we structure mathematical constructions in a reasonable way. Otherwise we are left with the usual argument that all programs can be written in machine language.


It seems that the traditions of type theory we represent are very different, so a reasonable answer should reflect the underlying basic design decisions.
In the examples you mention intensional type theory, the univalence axiom, and the desire to "structure mathematical constructions in a reasonable way".

My concept of type theory is in the tradition of Russell, Church, and Andrews – in particular Andrews' Q0, which is an elegant reformulation of Church's type theory (1940, see: https://owlofminerva.net/sep-q0 <https://owlofminerva.net/sep-q0>).
The purpose of the types in this concept of type theory is mainly to preserve the dependencies such that (negative) self-reference causing paradoxes/antinomies is avoided, as discussed here: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-June/msg00048.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-June/msg00048.html>

This means that types are the result of simple operations such as lambda abstraction and lambda application (cf. wff constructions (b) and (c) at [Andrews 2002 (ISBN 1-4020-0763-9), p. 211]).

Moreover, using Andrews' concept of "expressiveness" (also intuitively used by Church before), all mathematical concepts can be reduced – naturally (not like in machine language) – to a few basic notions: 
Q0 basically has a single variable binder (lambda), two primitive symbols and two primitive types, and a single rule of inference.
R0 has only little more (some features required for type variables, type abstraction, and dependent types).
Both are Hilbert-style systems (operating at the object language level only).

The notion of type theory you refer to seems to intend more than just preventing (negative) self-reference.
The univalence axiom, and the desire to „structure mathematical constructions in a reasonable way“ are motivated by philosophical or metamathematical considerations.
These motivations have their legitimation, but shouldn’t be part of the formal language.

For this reason I already object to the Pi type (as implemented in Lean), or dependent function type, which I consider a metamathematical notion: https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ <https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ>
I believe that type abstraction is fully sufficient to express what the Pi type is supposed to express.

How is type abstraction implemented in Lean, and where can I find the group definition?

Concerning constructivism (intuitionism) and intensionality, these are philosophical debates with little relevance for mathematics nowadays.
I fully agree to Kevin Buzzard’s argument that "within mathematics departments, the prevailing view is that Hilbert won the argument 100 years ago and we have not looked back since, despite what constructivists want us to believe." – https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/ <https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/>

Kind regards,

Ken Kubota

____________________________________________________


Ken Kubota
doi.org/10.4444/100 <https://doi.org/10.4444/100>

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