Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Harvey Friedman bringing incompleteness and infinity out of quarantine

nautil.us

Post reply on HN
Print view View original

51–60 of 88 posts

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#51

Post by AnimalMuppet »

catnaroek wrote: post #46
pron wrote: post #42

Earlier quoted context omitted.

> If anything, if we want to take computation more seriously, we should adopt a foundation that accounts for non-terminating computation natively... Of course, ZFC is even worse in this regard. I really don't understand this line of argument, regardless of the conclusion. Does the application of math to physics suggest that we should adopt a logical foundation of mathematics that does not allow expressing speed quant…

With all due respect to physicists and their work, physics doesn't belong in the foundation of mathematics. If our understanding of physics changed drastically tomorrow (an admittedly very improbable event), all mathematics not directly related to physics should remain unaffected. On the other hand, computation does belong in the foundations: constructing and verifying proofs (even informal ones) is computing, and it…

> constructing and verifying proofs (even informal ones) is computing

I'd like to see your proof for that assertion...

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#52

Post by pron »

catnaroek wrote: post #48
pron wrote: post #47

Earlier quoted context omitted.

But the definition of computation is physical. The Church-Turing thesis is a physical hypothesis. It is conceivable that a new physical discovery will contradict the Church-Turing thesis, and with it the definition of what is computable (and in particular how we construct and verify proofs, which is but a small part of computation).

> But the definition of computation is physical. A lot of mathematics is inspired by physical considerations, but mathematical concepts are themselves not physical. In particular, computation is just having state transitions, not necessarily in a physical system. (Just like recursion is any form of self-reference in any definition, not necessarily procedure definitions.) > The Church-Turing thesis is a physical hypot…

> A lot of mathematics is inspired by physical considerations, but mathematical concepts are themselves not physical.

I'm not sure I understand your point. It is true that any computation can be modeled mathematically, but so can any other physical process. Also, computation does not require a specific physical implementation and is an abstract concept, but so what? Gödel, Turing and von Neumann were very well aware that computation is a physical/philosophical concept described mathematically, not a purely mathematical one.

> Then let's not mention it, and stick to what can be dealt with mathematically.

But the definition of what is computable and what isn't depends on the Church-Turing thesis.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#53

Post by AnimalMuppet »

orbifold wrote: post #18

I think homotopy type theory has a better shot at providing a good foundation for math as opposed to some revision of set theory.

I don't understand HoTT. But every time I try to learn a bit about it, I go to the Wikipedia article (hey, everybody's got to start somewhere). And something always bugs me:

They're trying to build a foundation for all of mathematics. But their starting point requires weak omega groupoids. But weak omega groupoids are not exactly a fundamental object; you kind of need a foundation of something else before you ever get anywhere near weak omega groupoids. Their foundation, then, seems to me to be inevitably recursive.

Now, I get that the people involved in this are much smarter than me, and know far more mathematics. So, if you can, ELI5: Why isn't HoTT a recursive house of cards?

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#54

Post by Kutta »

AnimalMuppet wrote: post #50
Kutta wrote: post #45

Earlier quoted context omitted.

My perspective is that classical axiomatic theories have a far weaker philosophical grounding than constructive type theories. In type theory every definable natural number is a program which evaluates to a concrete finite numeral. You can't get more grounded than that. Of course, there is still a large variety of standard and nonstandard models of type theory as well, but the computational interpretation already cor…

> So, Peano arithmetic is just too loose and fuzzy for my taste. It's full of things which aren't numbers... OK. > In type theory every definable natural number is a program which evaluates to a concrete finite numeral. To me, that sounds like type theory is also full of things that are not numbers , namely computations. ("Evaluates to a natural number" != "is a number".)

Evaluation is always implicitly used in any sort of mathematical formalism. "2 + 2" is a program which evaluates to "4". Type theory just makes the computation arising from substituting definitions rigorous. Not letting "2 + 2" be equal to "4" by definition would be weird and inconvenient.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#55

Post by Chinjut »

AnimalMuppet wrote: post #53
orbifold wrote: post #18

I think homotopy type theory has a better shot at providing a good foundation for math as opposed to some revision of set theory.

I don't understand HoTT. But every time I try to learn a bit about it, I go to the Wikipedia article (hey, everybody's got to start somewhere). And something always bugs me: They're trying to build a foundation for all of mathematics. But their starting point requires weak omega groupoids. But weak omega groupoids are not exactly a fundamental object; you kind of need a foundation of something else before you ever ge…

Homotopy Type Theory axiomatizes weak omega groupoids; it gives you formal rules you can manipulate to reason about weak omega groupoids. This is exactly the same way, say, ZFC axiomatizes sets of sets of sets… "You're allowed to shuffle symbols in these ways, and the results of doing so we shall call theorems".

There's not an intrinsic sense in which sets are "foundational objects" and groupoids aren't; yes, you can encode groupoids as set structures with certain properties, but in just the same way, you can encode sets as groupoid structures with certain properties. Or, for example, you can encode points and lines using coordinates and Dedekind cuts of rational numbers or what have you, but you can also do Euclidean geometry without first developing some theory of real number arithmetic in that fashion, just directly axiomatizing the relevant properties of points and lines.

Any formal system gives you some basic rules to work with; as long as you can communicate and understand the rules, you're good to go. You don't need any other prerequisites.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#56

Post by pron »

Kutta wrote: post #45
Pete_D wrote: post #40

Earlier quoted context omitted.

At the risk of asking a naïve question, why do you think the Peano axioms are ugly? As a mostly-lay mathematician I always thought they were quite elegant.

My perspective is that classical axiomatic theories have a far weaker philosophical grounding than constructive type theories. In type theory every definable natural number is a program which evaluates to a concrete finite numeral. You can't get more grounded than that. Of course, there is still a large variety of standard and nonstandard models of type theory as well, but the computational interpretation already cor…

You are making a philosophical choice that was heavily debated in the early 20th century, namely, you contend that a mathematical foundation is truly foundational (perhaps even unique), and that math is built on top of one. Another alternative (favored by Turing[1]) is that any mathematical foundation is just like any other calculus, only one that deals with the lower-levels of mathematics.

Also, by picking computation as the "true" foundation, you are being a bit arbitrary. On the one hand, you can get more grounded. Computability was justified on physical arguments, and Turing and others recognized that computability is only a rough approximation of feasibility, which was given a more precise treatment much later. So if you want to base the foundations of math on the physical -- which is what you're doing if you're basing them on Turing computability -- then you can go a lot further down towards "grounded". On the other hand, there is really no reason to limit math at the computable. Brouwer thought there was, but Turing didn't. If non-constructive math yields results that are useful, compatible with constructive math and is easier to work with in some cases, what justification is there to reject it other than by taking a view that is both fundamentalist (in the sense I described) and somewhat arbitrary? After all, constructive math is a very different math, and if classical math rests on shaky foundations, how is it so useful in practice, and how come it agrees with constructive math on everything that is physically observable?

[1]: https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#57

Post by AnimalMuppet »

Kutta wrote: post #54
AnimalMuppet wrote: post #50

Earlier quoted context omitted.

> So, Peano arithmetic is just too loose and fuzzy for my taste. It's full of things which aren't numbers... OK. > In type theory every definable natural number is a program which evaluates to a concrete finite numeral. To me, that sounds like type theory is also full of things that are not numbers , namely computations. ("Evaluates to a natural number" != "is a number".)

Evaluation is always implicitly used in any sort of mathematical formalism. "2 + 2" is a program which evaluates to "4". Type theory just makes the computation arising from substituting definitions rigorous. Not letting "2 + 2" be equal to "4" by definition would be weird and inconvenient.

I get that evaluation is always implicit (or at least implicitly assumed to happen). My quarrel is with "evaluation == program == computation", and even more with the reverse: "a number == computation that would produce the number, therefore number == computation".

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#58

Post by Kutta »

AnimalMuppet wrote: post #53
orbifold wrote: post #18

I think homotopy type theory has a better shot at providing a good foundation for math as opposed to some revision of set theory.

I don't understand HoTT. But every time I try to learn a bit about it, I go to the Wikipedia article (hey, everybody's got to start somewhere). And something always bugs me: They're trying to build a foundation for all of mathematics. But their starting point requires weak omega groupoids. But weak omega groupoids are not exactly a fundamental object; you kind of need a foundation of something else before you ever ge…

HoTT doesn't build on any notion of omega groupoids; at the lowest level it's a collection of typing and computation rules which one can apply successively to do proofs and constructions. The resulting constructions can be interpreted as talking about properties of spaces. The rules themselves are very stripped-down and abstract when viewed in a homotopical light, like "every path can be retracted to an endpoint" or "the interval has two points and a path between them". Originally the basic rule for reasoning about paths ("path induction") was intended to allow construction of equality proofs between elements of types. Later people discovered that equalities can be interpreted as paths in spaces (and equalities of equalities as homotopies and so on).

Remarkably, the four typing rules of equality suffice to generate all homotopical reasoning in classic HoTT. However, they aren't enough to prove univalence as a theorem, or at least no one knows how to do it. If we switch to cubical type theory, we get considerably more structure which allows us to prove univalence. But cubical type theory is also "synthetic" and builds up notions of spaces from ground-up.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#59

Post by AnimalMuppet »

Chinjut wrote: post #55
AnimalMuppet wrote: post #53

Earlier quoted context omitted.

I don't understand HoTT. But every time I try to learn a bit about it, I go to the Wikipedia article (hey, everybody's got to start somewhere). And something always bugs me: They're trying to build a foundation for all of mathematics. But their starting point requires weak omega groupoids. But weak omega groupoids are not exactly a fundamental object; you kind of need a foundation of something else before you ever ge…

Homotopy Type Theory axiomatizes weak omega groupoids; it gives you formal rules you can manipulate to reason about weak omega groupoids. This is exactly the same way, say, ZFC axiomatizes sets of sets of sets… "You're allowed to shuffle symbols in these ways, and the results of doing so we shall call theorems". There's not an intrinsic sense in which sets are "foundational objects" and groupoids aren't; yes, you can…

Well, it's pretty easy to say that math started with the counting numbers. It's not much more of a reach to say that when we were counting some collection of things, we were counting the elements of a set. So saying that sets are the foundation of mathematics is, historically, quite natural.

Weak omega groupoids? Not so much.

[Edit: Excellent ELI5, though. Thanks.]

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#60

Post by AnimalMuppet »

Kutta wrote: post #58
AnimalMuppet wrote: post #53

Earlier quoted context omitted.

I don't understand HoTT. But every time I try to learn a bit about it, I go to the Wikipedia article (hey, everybody's got to start somewhere). And something always bugs me: They're trying to build a foundation for all of mathematics. But their starting point requires weak omega groupoids. But weak omega groupoids are not exactly a fundamental object; you kind of need a foundation of something else before you ever ge…

HoTT doesn't build on any notion of omega groupoids; at the lowest level it's a collection of typing and computation rules which one can apply successively to do proofs and constructions. The resulting constructions can be interpreted as talking about properties of spaces. The rules themselves are very stripped-down and abstract when viewed in a homotopical light, like "every path can be retracted to an endpoint" or…

Thanks to you (and Chinjut) for the replies. I don't know how to correlate your reply to Chinjut's, though (or vice versa). Could either of you take a stab at it? Are you saying the same thing in different ways? Or are you actually disagreeing?
Post reply on HN