[Agda] Why dependent type theory?

[Martin Escardo]

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,
> 
> I largely agree with you (at least in terms of my practice as an Agda
> user; users of other proof assistants should look to their own
> consciences regarding well-known and less-well-known sources of
> potential inconsistency in (implementations of) their favourite
> foundations), but I had a mind a separation even at the level you allude
> to:
> 
> -- that mathematicians are not/need not be bound by the
> restrictions/stipulations of a given foundational system; rather that
> they develop appropriate language/meta-language for their own eventual
> mathematical needs, and that such processes are very much historically
> bound, and subject to the dynamics of paradigm change in terms of the
> (greater) explanatory power of the paradigm within which they work; the
> example of Grothendieck developing a raft of categorical techniques in
> order to be able to successfully carry out his research programme in
> algebraic geometry being only one of the most familiar/famous/notorious;
> Kevin's and others' use of lean in the formalisation of perfectoid
> spaces suggest another such case, where the tool(s), and in particular
> their expressivity wrt the concepts being studied, made them more
> immediately ready-at-hand than any mere reduction to set theory (even if
> that were a possibility-in-principle with ZFC/TG implementations in
> Isabelle, Mizar or Egal);
> 
> -- that concern for (consistency of such) foundations has, historically
> at least, typically lagged behind the mathematical developments; though
> against that, one might say that the Grothendieck school were precisely
> concerned with developing such foundations, hand-in-hand with the
> dazzling mathematics they carried out therein (an example of a much
> longer gap between the mathematical development, and putting it on
> satisfactory foundations might lie in the history of distributions from
> Heaviside to Schwartz; or the foundations of geometry after the
> discovery of non-Euclidean geometries...); the contemporary frenzy of
> activity on a number of fronts in higher-dimensional (categorical)
> algebra via homotopy type theory suggests a similar interplay between
> the development of 'mathematics-of' and 'foundations-for'.
> 
> The Kolmogorov paper (as well as, for example, Lawvere's insistence on
> (a) 'logic' as somehow a conceptual secondary notion to the categorical
> structure which supports it, and indeed Brouwer's conception of logic as
> part of mathematics (and not the other way round, which perhaps seems
> strange to those who see the field of proof assistants as somehow the
> triumph of the logicist/formalist programme)) suggests that the logic of
> mathematical 'problems' (and their solutions) emerges from the domain of
> such problems. (What K points out as a "remarkable fact" is that such
> logic turns out to be (Heyting's formalisation of) Brouwer's
> intuitionistic logic, and such congruence would repeat itself 40 years
> later with the internal logic of toposes. )
> 
> It almost seems (to me at least), that the development and use of proof
> assistants has refocused our attention on the possibility that the
> 'Grundlagenstreit' was not a single historical moment, with a
> right/wrong outcome, but part of the dynamics of mathematical
> development: to each age its mathematics, and to each such mathematics,
> not only its freedom, but also its appropriate foundations. But that's
> not to say that we can, or should, be blas'e about such things. I'm
> sorry if my earlier post suggested otherwise.
> 
> James.
> 

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