7 ms·

I just recently stumbled upon the "univalent foundations" approach to mathematics, i.e. homotopy type theory (HoTT), and holy schnikes this is a deep rabbit hol

I just recently stumbled upon the "univalent foundations" approach to mathematics, i.e. homotopy type theory (HoTT), and holy schnikes this is a deep rabbit hole to fall into. It would appear that category theory and set theory can both be represented in HoTT. I think the world is not going to reap the true benefits of computers for scientific progress until we systematize formal knowledge within a single shared syntactical universe. Open science means nothing if it has become so siloed and complex that results are largely unverified and frequently unverifiable.

weatherlight 6y ago
All formal systems have their limitations as far as what is provable. Example:, for any statement A unprovable in a particular formal system F , there are, trivially, other formal systems in which A is provable (take A as an axiom). On the other hand, there is the extremely powerful standard axiom system of Zermelo-Fraenkel set theory (denoted as ZF, or, with the axiom of choice, ZFC), which is more than sufficient for the derivation of all ordinary mathematics. Now there are, by Gödel’s first theorem, arithmetical truths that are not provable even in ZFC. Proving them would thus require a formal system that incorporates methods going beyond ZFC. There is thus a sense in which such truths are not provable using today’s “ordinary” mathematical methods and axioms, nor can they be proved in a way that mathematicians would today regard as unproblematic and conclusive.
- guerrilla 6y ago
  This is well known. Type theories also do not assume the law of excluded middle. What's your point and it's relevance to the comment?
- jkhdigital 6y ago
  The issue is not one of “power”—one can make almost any formal system sufficiently “powerful” by adding a few axioms that get you over the rough spots in your proofs. The problem is that the modern world increasingly relies on mathematics, in nearly all aspects of life, to make consequential decisions about how to interpret data and act on it. The challenge is not one of power, but of fidelity—using a mathematical structure that is a suitable abstraction for the real world situation. Use the wrong abstraction, and you end up with paradoxes like the incompleteness theorems. I believe a goal of univalent foundations is to make the abstract structure that one is working with absolutely explicit, evidenced by the (almost) total absence of axioms from the system. If you want to work in ZFC, you can add those axioms yourself.
beaconstudios 6y ago
Isn't that a similar idea to the Hilbert program, which failed due to godel's incompleteness theorem?
- Twisol 6y ago
  Hilbert's program was about whether every statement could be proved ab nihilo either true or false. The question remains: given a proof, can we verify it? Arguably, any proof conceived by a human mind should be verifiable in principle. So the Incompleteness Theorem doesn't really apply, either formally or morally. A more interesting argument could be made on the basis of Rice's Theorem: for a Turing-complete language, the only non-trivial properties provable about a program are fundamentally syntactic. (Type systems can be seen as a way of elaborating your syntax to capture finer-grained details of your semantics). Here we have a richer and nearer-to-hand collection of programs whose properties are inaccessible -- take, for instance, whether the 3n+1 algorithm halts on all inputs. Again, though, if we have a proof of some property, we still ought to be able to verify it.
  - tshaddox 6y ago
    Isn’t verifying a proof equivalent to determining whether a certain computer program halts?
    - Twisol 6y ago
      No, but it would be equivalent to verifying that a given computer program halts on a specified N steps. This is the same distinction between (among other things) P and NP problems. For any problem in P, given an instance of the problem I can produce a solution in polynomial time. For any problem in NP, given an instance of the problem and a candidate solution, I can determine whether the solution is valid in polynomial time. Determining whether a certain computer program halts would be equivalent to producing a proof, not verifying an existing one. Verifying a proof is, in principle, only a matter of making sure that each step of the proof is valid. Coming up with the right steps is a creative endeavor. Certainly, coming up with the right set of allowable steps is a creative endeavor, and proving that your system is expressive enough for interesting proofs is a creative endeavor. But once given a proof, verifying that it legally applies legal steeps is a purely mechanical endeavor.
chobytes 6y ago
This kind of foundational (ZFC,CT,HTT) stuff is pretty niche in mathematics. Set theory, though touted as the foundation of math, isn't really used to its full extremes (HOD, etc) by anyone but set theorists. Its more like... A common datatype? And while CT could also be a foundation, as far as im aware its only practical uses as a tool are found in commutative algebra. I think the truth is that most math is pretty simple to describe and doesn't require a grand framework to formalize.
- Twisol 6y ago
  > I think the truth is that most math is pretty simple to describe and doesn't require a grand framework to formalize. I agree -- most fields of math are happy to establish their own axioms, and leave the reducibility of those axioms to some "foundations" as an exercise -- an important one, but not one that necessarily furthers the field itself. However, Voevodsky's stated aim for his Univalent Foundations project was not to formalize everything under a grand theory of everything. He got the bejeebus scared out of him when one of his results was very, very subtly wrong, in a way that was difficult for mathematicians to verify for years, even given a reasonable inkling of a counterexample. So he sought to improve the state of the art in proof verification. You might argue, it's better to produce a verification tool for one field of mathematics than all of them at once. But you'll have a hard time finding any significantly complex theorem that doesn't draw insight from multiple places. (Arguably, that's why they're significantly complex in the first place). And all fields of mathematics have some basic elements in common. So, I'd argue, you're unlikely to do a good job for any but the most narrow domains of mathematics without seeking some level of generality. Any "foundation of mathematics" can be used for this purpose, and plenty of theorem provers have been built on each (Twelf, PVS, Agda). The draw of category theory is that it seems to capture at a fundamental level many of the basic conceptual elements we see across mathematics. (Homomorphisms are so universal it's not even funny.) It seems reasonable to pick something that starts us closer to where we want to be; the difficulties we encounter are more likely to be fundamental problems and not issues of encoding.
  - chobytes 6y ago
    Im not opposed to the use of proof assistant software for difficult theorems. And if one foundation or another is more applicable to that software, then thats fine. Its more the narrative of the grand unification of mathematics thats spun around 'foundational theories' that irks me. In reality its just various emulation schemes. Rephrasing other mathematicians work and claiming fundamental status, while not producing many novel theorems... just strikes me as very distasteful.
joe_the_user 6y ago
It's not really a matter of what formal system is most powerful. It's a matter of what formal system can represent ordinary math in the simplest and clearest fashion. I think this what proponents of category theory argue. Basically, category theory lets one take many standard mathematical theorems and generalize them widely - ie, lot of standard math theories can be seen as theories about categories and when you see them that way, the generality of a category means the theorem applies broadly.
- rsj_hn 6y ago
  I know category theory is popular in CS-land but over in math land it falls squarely in the "general nonsense" bucket for most working mathematicians. E.g. most mathematicians learn the definitions of categories and the Yoneda Lemma perhaps as a chapter in some other text -- say a text on more modern algebraic geometry -- and that's about it. The thing to understand is that mathematicians have jobs to do like everyone else -- they are not philosophers sitting in contemplation, but eager beavers trying to answer specific questions and solve open problems. So they are interested in picking up the tools that will help them solve unsolved problems more than picking up the tools that will help repackage the research of others. And the main feature of category theory is its ability to repackage the discoveries of others, rather than necessarily driving new research. That's not to say that occasionally category theory can't be useful, but just not that many people are going to be working in those research fields where they find anything beyond the chapter's worth of Yoneda lemma plus some of the diagram formalism to be useful, and everyone's time and attention span is limited to what will help them make discoveries in their field. Rarely is the answer to the question of how to solve some problem in differential geometry, pdes, number theory, symplectic geometry, combinatorics etc, -- "more category theory". The same is true for formal logic. Most people learn the incompleteness theorems and maybe even some things on computability, but they do not use formal logic to advance their research agenda, even though in theory proofs can be encoded in formal systems and so in some sense, these formal systems are a unifying framework to view mathematical proofs. On the other hand, there have been some spectacular breakthroughs with physics/string theory, so a lot of people were trying to brush up on that. But here, too, progress is quite difficult, and most people aren't going to go out of their way to invest too much time in it beyond a summer school or so.
keithalewis 6y ago
An interesting thing happened when category theory was used to model sets. It turned out set membership was problematic. When wearing your category theory glasses "parameterized elements" (subobject classifier) were the natural thing. Think tangent planes to a sphere instead of points on a sphere.

weatherlight 6y ago

All formal systems have their limitations as far as what is provable. Example:, for any statement A unprovable in a particular formal system F , there are, trivially, other formal systems in which A is provable (take A as an axiom). On the other hand, there is the extremely powerful standard axiom system of Zermelo-Fraenkel set theory (denoted as ZF, or, with the axiom of choice, ZFC), which is more than sufficient for the derivation of all ordinary mathematics. Now there are, by Gödel’s first theorem, arithmetical truths that are not provable even in ZFC. Proving them would thus require a formal system that incorporates methods going beyond ZFC. There is thus a sense in which such truths are not provable using today’s “ordinary” mathematical methods and axioms, nor can they be proved in a way that mathematicians would today regard as unproblematic and conclusive.

guerrilla 6y ago
This is well known. Type theories also do not assume the law of excluded middle. What's your point and it's relevance to the comment?
jkhdigital 6y ago
The issue is not one of “power”—one can make almost any formal system sufficiently “powerful” by adding a few axioms that get you over the rough spots in your proofs. The problem is that the modern world increasingly relies on mathematics, in nearly all aspects of life, to make consequential decisions about how to interpret data and act on it. The challenge is not one of power, but of fidelity—using a mathematical structure that is a suitable abstraction for the real world situation. Use the wrong abstraction, and you end up with paradoxes like the incompleteness theorems. I believe a goal of univalent foundations is to make the abstract structure that one is working with absolutely explicit, evidenced by the (almost) total absence of axioms from the system. If you want to work in ZFC, you can add those axioms yourself.

beaconstudios 6y ago

Isn't that a similar idea to the Hilbert program, which failed due to godel's incompleteness theorem?

Twisol 6y ago
Hilbert's program was about whether every statement could be proved ab nihilo either true or false. The question remains: given a proof, can we verify it? Arguably, any proof conceived by a human mind should be verifiable in principle. So the Incompleteness Theorem doesn't really apply, either formally or morally. A more interesting argument could be made on the basis of Rice's Theorem: for a Turing-complete language, the only non-trivial properties provable about a program are fundamentally syntactic. (Type systems can be seen as a way of elaborating your syntax to capture finer-grained details of your semantics). Here we have a richer and nearer-to-hand collection of programs whose properties are inaccessible -- take, for instance, whether the 3n+1 algorithm halts on all inputs. Again, though, if we have a proof of some property, we still ought to be able to verify it.
- tshaddox 6y ago
  Isn’t verifying a proof equivalent to determining whether a certain computer program halts?
  - Twisol 6y ago
    No, but it would be equivalent to verifying that a given computer program halts on a specified N steps. This is the same distinction between (among other things) P and NP problems. For any problem in P, given an instance of the problem I can produce a solution in polynomial time. For any problem in NP, given an instance of the problem and a candidate solution, I can determine whether the solution is valid in polynomial time. Determining whether a certain computer program halts would be equivalent to producing a proof, not verifying an existing one. Verifying a proof is, in principle, only a matter of making sure that each step of the proof is valid. Coming up with the right steps is a creative endeavor. Certainly, coming up with the right set of allowable steps is a creative endeavor, and proving that your system is expressive enough for interesting proofs is a creative endeavor. But once given a proof, verifying that it legally applies legal steeps is a purely mechanical endeavor.

chobytes 6y ago

This kind of foundational (ZFC,CT,HTT) stuff is pretty niche in mathematics. Set theory, though touted as the foundation of math, isn't really used to its full extremes (HOD, etc) by anyone but set theorists. Its more like... A common datatype? And while CT could also be a foundation, as far as im aware its only practical uses as a tool are found in commutative algebra. I think the truth is that most math is pretty simple to describe and doesn't require a grand framework to formalize.

Twisol 6y ago
> I think the truth is that most math is pretty simple to describe and doesn't require a grand framework to formalize. I agree -- most fields of math are happy to establish their own axioms, and leave the reducibility of those axioms to some "foundations" as an exercise -- an important one, but not one that necessarily furthers the field itself. However, Voevodsky's stated aim for his Univalent Foundations project was not to formalize everything under a grand theory of everything. He got the bejeebus scared out of him when one of his results was very, very subtly wrong, in a way that was difficult for mathematicians to verify for years, even given a reasonable inkling of a counterexample. So he sought to improve the state of the art in proof verification. You might argue, it's better to produce a verification tool for one field of mathematics than all of them at once. But you'll have a hard time finding any significantly complex theorem that doesn't draw insight from multiple places. (Arguably, that's why they're significantly complex in the first place). And all fields of mathematics have some basic elements in common. So, I'd argue, you're unlikely to do a good job for any but the most narrow domains of mathematics without seeking some level of generality. Any "foundation of mathematics" can be used for this purpose, and plenty of theorem provers have been built on each (Twelf, PVS, Agda). The draw of category theory is that it seems to capture at a fundamental level many of the basic conceptual elements we see across mathematics. (Homomorphisms are so universal it's not even funny.) It seems reasonable to pick something that starts us closer to where we want to be; the difficulties we encounter are more likely to be fundamental problems and not issues of encoding.
- chobytes 6y ago
  Im not opposed to the use of proof assistant software for difficult theorems. And if one foundation or another is more applicable to that software, then thats fine. Its more the narrative of the grand unification of mathematics thats spun around 'foundational theories' that irks me. In reality its just various emulation schemes. Rephrasing other mathematicians work and claiming fundamental status, while not producing many novel theorems... just strikes me as very distasteful.

joe_the_user 6y ago

It's not really a matter of what formal system is most powerful. It's a matter of what formal system can represent ordinary math in the simplest and clearest fashion. I think this what proponents of category theory argue. Basically, category theory lets one take many standard mathematical theorems and generalize them widely - ie, lot of standard math theories can be seen as theories about categories and when you see them that way, the generality of a category means the theorem applies broadly.

rsj_hn 6y ago
I know category theory is popular in CS-land but over in math land it falls squarely in the "general nonsense" bucket for most working mathematicians. E.g. most mathematicians learn the definitions of categories and the Yoneda Lemma perhaps as a chapter in some other text -- say a text on more modern algebraic geometry -- and that's about it. The thing to understand is that mathematicians have jobs to do like everyone else -- they are not philosophers sitting in contemplation, but eager beavers trying to answer specific questions and solve open problems. So they are interested in picking up the tools that will help them solve unsolved problems more than picking up the tools that will help repackage the research of others. And the main feature of category theory is its ability to repackage the discoveries of others, rather than necessarily driving new research. That's not to say that occasionally category theory can't be useful, but just not that many people are going to be working in those research fields where they find anything beyond the chapter's worth of Yoneda lemma plus some of the diagram formalism to be useful, and everyone's time and attention span is limited to what will help them make discoveries in their field. Rarely is the answer to the question of how to solve some problem in differential geometry, pdes, number theory, symplectic geometry, combinatorics etc, -- "more category theory". The same is true for formal logic. Most people learn the incompleteness theorems and maybe even some things on computability, but they do not use formal logic to advance their research agenda, even though in theory proofs can be encoded in formal systems and so in some sense, these formal systems are a unifying framework to view mathematical proofs. On the other hand, there have been some spectacular breakthroughs with physics/string theory, so a lot of people were trying to brush up on that. But here, too, progress is quite difficult, and most people aren't going to go out of their way to invest too much time in it beyond a summer school or so.

keithalewis 6y ago

An interesting thing happened when category theory was used to model sets. It turned out set membership was problematic. When wearing your category theory glasses "parameterized elements" (subobject classifier) were the natural thing. Think tangent planes to a sphere instead of points on a sphere.