3 ms·

> It turns out most people don’t want to work in foundations, and want to think of 1 and 2 as non-sets Which is to say most mathematicians prefer type theory t

> It turns out most people don’t want to work in foundations, and want to think of 1 and 2 as non-sets Which is to say most mathematicians prefer type theory to set theory :). Perhaps we should stop saying "maths is usually done in ZFC", or that "ZFC is mainstream math". For one math is almost never formalized and second informal math is quite strongly typed (the basic object usually not a set but a structured set) where set theory is very untyped. At some point people (erm mathematicians) have to acknowledge that we computer sciency-math have brought far better foundations (being intuitionistic type theory) insofar that it has set theory as a subpart, but is much finer in what it can distinguish. It's newtonian mechanics vs general relativity. What set-foundationalists say is fine, but the frontier is elsewhere.

creata 5y ago
How is intuitionistic type theory a "better" foundation? As a simple example, where can I find a statement of Brouwer's fixpoint theorem in an intuitionistic type theory, and how is it better stated than its classical counterpart?
- lapinot 5y ago
  :) i don't know about that theorem, don't remember having seen. Now i'm reading stuff about Brouwer! Since it seems to be about topology so i'd guess homotopy type theory folks would have written something about it. edit: You seem to know some stuff apparently?
Tainnor 5y ago
> For one math is almost never formalized and second informal math is quite strongly typed [...] I think you're correct about the first part, but not about the second. It is incredibly common in mathematics to silently "convert" objects between different types or to ignore certain things that will trip you up once you try to encode things super formally. For example, "the function x^2" (instead of x->x^2), basically all the common notational shorthands in differential equations, where functions are treated as variables, silently identifying isomorphic objects and so on. Plus, very few working mathematicians actually use constructivism and are quite happy with the existence of, for example, the whole set of real numbers.
- lapinot 5y ago
  > It is incredibly common in mathematics to silently "convert" objects between different types. [..] silently identifying isomorphic objects Would you agree that correct instances of this pattern are exactly cases of considering objects only up to isomorphism? The problems of equality in constructive mathematics is a complicated one but things are starting to clear out, with constructive interpretations of this pattern (eg constructive models of univalence, implemented in cubical agda) people are starting to do wonders, like this superb grad thesis about finiteness [1]. The hard part is certainly the silentness of these identifications (which if i'm not mistaken is kind of the difference between extensional and intensional logics). But again i believe that they can be systematized contextually: one could for example declare in a preample which implicit isomorphisms they are going to use, which would then be disambiguated by type and decidably searched-for. > ignore certain things [..] basically all the common notational shorthands This is certainly a challenge for formalization, but my belief is that it can be done. Imho this is where the cross-pollination between "real-life programming" and constructive maths shows: contextual generalization (binding) of unbound variables (eg implicit polymorphism in ML-likes types, structure inference and coercions along structure refinements using typeclasses/search-like procedures and unification hints, ...). We definitely have to continue developing nice "surface languages" for generating proofs (compiling?) in the formal core (assembly?). > Plus, very few working mathematicians actually use constructivism and are quite happy with the existence of, for example, the whole set of real numbers. I'm not sure i understand your point: constructive models of real number exist (usually as equivalence classes of some kind, which a sufficiently sophisticated type theory will give you tools to work with). Constructive models doesn't mean we have a decidable normalization procedure tho. I skimmed through it but there is this recent talk at msp101 about real numbers in agda [2] and there is a chapter about it in the HoTT book. [1] https://doisinkidney.com/posts/2021-01-04-masters-thesis.html https://doisinkidney.com/posts/2021-01-04-masters-thesis.htm... [2] http://msp.cis.strath.ac.uk/101/slides/2021-06-10_bob.pdf http://msp.cis.strath.ac.uk/101/slides/2021-06-10_bob.pdf
- klodolph 5y ago
  “The function x^2” isn’t a silent conversion between objects of different types. It’s really exactly one thing: the function x->x^2. It's just shorthand. Also note that intuitionistic type theory is only one kind of type theory. There’s nothing about assuming the existence of real numbers that implies you are not using type theory. Intuitionistic type theory is useful because computer programs must construct their values… the Curry-Howard correspondence is between the types system in a computer program and statements in intuitionistic logic.

creata 5y ago

How is intuitionistic type theory a "better" foundation? As a simple example, where can I find a statement of Brouwer's fixpoint theorem in an intuitionistic type theory, and how is it better stated than its classical counterpart?

lapinot 5y ago
:) i don't know about that theorem, don't remember having seen. Now i'm reading stuff about Brouwer! Since it seems to be about topology so i'd guess homotopy type theory folks would have written something about it. edit: You seem to know some stuff apparently?

Tainnor 5y ago

> For one math is almost never formalized and second informal math is quite strongly typed [...] I think you're correct about the first part, but not about the second. It is incredibly common in mathematics to silently "convert" objects between different types or to ignore certain things that will trip you up once you try to encode things super formally. For example, "the function x^2" (instead of x->x^2), basically all the common notational shorthands in differential equations, where functions are treated as variables, silently identifying isomorphic objects and so on. Plus, very few working mathematicians actually use constructivism and are quite happy with the existence of, for example, the whole set of real numbers.

lapinot 5y ago
> It is incredibly common in mathematics to silently "convert" objects between different types. [..] silently identifying isomorphic objects Would you agree that correct instances of this pattern are exactly cases of considering objects only up to isomorphism? The problems of equality in constructive mathematics is a complicated one but things are starting to clear out, with constructive interpretations of this pattern (eg constructive models of univalence, implemented in cubical agda) people are starting to do wonders, like this superb grad thesis about finiteness [1]. The hard part is certainly the silentness of these identifications (which if i'm not mistaken is kind of the difference between extensional and intensional logics). But again i believe that they can be systematized contextually: one could for example declare in a preample which implicit isomorphisms they are going to use, which would then be disambiguated by type and decidably searched-for. > ignore certain things [..] basically all the common notational shorthands This is certainly a challenge for formalization, but my belief is that it can be done. Imho this is where the cross-pollination between "real-life programming" and constructive maths shows: contextual generalization (binding) of unbound variables (eg implicit polymorphism in ML-likes types, structure inference and coercions along structure refinements using typeclasses/search-like procedures and unification hints, ...). We definitely have to continue developing nice "surface languages" for generating proofs (compiling?) in the formal core (assembly?). > Plus, very few working mathematicians actually use constructivism and are quite happy with the existence of, for example, the whole set of real numbers. I'm not sure i understand your point: constructive models of real number exist (usually as equivalence classes of some kind, which a sufficiently sophisticated type theory will give you tools to work with). Constructive models doesn't mean we have a decidable normalization procedure tho. I skimmed through it but there is this recent talk at msp101 about real numbers in agda [2] and there is a chapter about it in the HoTT book. [1] https://doisinkidney.com/posts/2021-01-04-masters-thesis.html https://doisinkidney.com/posts/2021-01-04-masters-thesis.htm... [2] http://msp.cis.strath.ac.uk/101/slides/2021-06-10_bob.pdf http://msp.cis.strath.ac.uk/101/slides/2021-06-10_bob.pdf
klodolph 5y ago
“The function x^2” isn’t a silent conversion between objects of different types. It’s really exactly one thing: the function x->x^2. It's just shorthand. Also note that intuitionistic type theory is only one kind of type theory. There’s nothing about assuming the existence of real numbers that implies you are not using type theory. Intuitionistic type theory is useful because computer programs must construct their values… the Curry-Howard correspondence is between the types system in a computer program and statements in intuitionistic logic.