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

61–70 of 88 posts

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#61

Post by [deleted] »

jesuslop wrote: post #32
Chinjut wrote: post #27

Earlier quoted context omitted.

I find Harvey Friedman has made the FOM mailing list completely unreadable. AND incredibly hostile to anyone with any sympathy to category theory, type theory, or the like. See https://plus.google.com/+CodyRoux/posts/6TiKLxjSCnu (not by me, but expressing many of the same thoughts I've had; I particularly agree with many of the comments made by John Baez).

That's true that categories are not going to find any special love there and that's sad. Much of the foundational tradition has been made in Set Theoretic language and its value cannot be ignored (think say on Gödel on CH), but it's sad that there is such community divide forbidding any osmosis. Categorical thinking leads to natural costless abstractions with practical unifying power and transversal applicability, an…

[deleted]

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#62

Post by Kutta »

pron wrote: post #56
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…

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 computati…

I'm fine with classical reasoning and uncomputability, and I acknowledge the intuition for classical truth (it got popular for a reason). But pretty much all the useful classical math can be performed all the same in type theory without significant change, therefore the presence of "useful math" is not an argument for or against type theory and classical foundations. Rather, the main thing is that type theory is just better for formalizing things, and while type theory can conveniently embed classical reasoning and talk about various levels of constructivity, classical foundations is not convenient for constructive reasoning. Math with justification in ZFC is useful in practice, but ZFC itself is mostly not. I would like to see eventually many or event most things formalized, and for that we need fundamentals for more than justification.

On the more philosophical side, "philosophers should care about computational complexity", certainly, but it's not like one cannot have gradation in philosophical appeal. Also, it definitely helps to have computation at hand if we want to talk about feasible computation.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#63

Post by Kutta »

AnimalMuppet wrote: post #60
Kutta wrote: post #58

Earlier quoted context omitted.

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?

The same thing as far as I see.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#64

Post by eastWestMath »

pron wrote: post #47
catnaroek wrote: post #46

Earlier quoted context omitted.

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…

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).

Computation is an entirely abstract thing. Nowhere does the definition of Turing machines or the lambda calculus makes any reference to actual physical things.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#65

Post by pron »

eastWestMath wrote: post #64
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).

Computation is an entirely abstract thing. Nowhere does the definition of Turing machines or the lambda calculus makes any reference to actual physical things.

Church doesn't really define computation[1], and Turing most certainly bases his entire definition (the first ever definition of computation) on multiple references to physical things (finite "states of mind", limits of what can be read or manipulated at any one time etc.). Brouwer also bases intuitionism on the physical, when he appeals to the limited capability of a finite (idealized) mind. Computation carried out with an infinitely fast (in terms of physical time) and/or infinitely large computer is not Turing computation.

[1]: He conjectures that LC coincides with what he calls a "a vague intuitive notion" of an algorithm, and when he tries to make a rigorous argument he finds that he needs to rely on circularity, and writes this: "if this [circular] interpretation or some similar one is not allowed, it is difficult to see how the notion of an algorithm can be given any exact meaning at all."

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#66

Post by pron »

Kutta wrote: post #62
pron wrote: post #56

Earlier quoted context omitted.

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 computati…

I'm fine with classical reasoning and uncomputability, and I acknowledge the intuition for classical truth (it got popular for a reason). But pretty much all the useful classical math can be performed all the same in type theory without significant change, therefore the presence of "useful math" is not an argument for or against type theory and classical foundations. Rather, the main thing is that type theory is just…

> therefore the presence of "useful math" is not an argument for or against type theory and classical foundations

I wasn't making an argument against type theory (although constructive analysis is quite different from classical analysis) but an argument against a weak argument against classical math. Useful math is very much an argument in favor of a foundation. In fact, it was the winning argument in favor of ZFC, when it was thought that intuitionism would mean radically changing analysis.

> Rather, the main thing is that type theory is just better for formalizing things

In mechanical proof checkers? Then say that type theory is a more convenient small core for a mechanical proof checker. But you're arguing for constructive math, and constructive math is significantly less convenient for proving many things (and constructivists openly acknowledge that).

> ZFC itself is mostly not.

Useful for what? Mathematical foundations are not used when doing math unless you're doing formal math. ZFC seems a lot more useful that type theory when, say, teaching mathematical foundations (which, to reiterate, don't really mean the actual foundations of math).

> I would like to see eventually many or event most things formalized, and for that we need fundamentals for more than justification.

OK, formalizing mathematics is a 100 year old dream and a noble one, but one that may not be shared today by most mathematicians today. Your argument would be clearer and less religious if you said: I want to formalize math mechanically, and currently type theory seems more convenient for that particular task than ZFC.

> but it's not like one cannot have gradation in philosophical appeal

Sure, but I don't understand the aesthetic gradation. Does a mathematical foundation become more appealing to you the more closely it constrains math to the physical? Why? Would a mathematical foundation that doesn't allow expressing speed quantities greater than the speed of light be appealing to you?

I would understand if you said you're an intuitionist, but the intuitionists really did have a problem explaining the effectiveness of classical math (which is simply invalid to them). Classical analysis coincides with constructive analysis on all physically observable propositions and is still easier to work with (at least currently).

> Also, it definitely helps to have computation at hand if we want to talk about feasible computation.

There is absolutely nothing wrong, missing, or inconvenient with how classical math models computation. Type theory or any other constructive math has no advantage there. It certainly doesn't make talking about feasible computation easier.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#67

Post by fmap »

pron wrote: post #65
eastWestMath wrote: post #64

Earlier quoted context omitted.

Computation is an entirely abstract thing. Nowhere does the definition of Turing machines or the lambda calculus makes any reference to actual physical things.

Church doesn't really define computation[1], and Turing most certainly bases his entire definition (the first ever definition of computation) on multiple references to physical things (finite "states of mind", limits of what can be read or manipulated at any one time etc.). Brouwer also bases intuitionism on the physical, when he appeals to the limited capability of a finite (idealized) mind. Computation carried out…

Can you link to some of the references you cite? That seems like an interesting read.

As for computability being a physical notion, I can't speak to the motivation of Church and his students, but I do know that there are characterizations of total computable functions in domain theory which make no mention of physics. The intuition about computable functions is that they are precisely the functions whose output for any given input depends only on a finite part of the input. The really interesting thing about the Church Turing thesis is that there are so many different models of computation that capture precisely this idea (the surprising part is that these very simple models are expressive enough to cover all computable functions).

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#68

Post by fmap »

lgandersen wrote: post #43
fmap wrote: post #8

There is a lot of ordinary mathematics that is outside of ZFC, which Friedman is well aware of but the writer of this article may not be. Grothendieck was not interested in abstract set theory when he introduced what are now called "Grothendieck Universes". He merely wanted to do algebraic geometry at a high level of abstraction. Similarly, Conway was apparently a bit dismayed when the formalization of his simple ide…

> To some extend this can be encoded in set theory, but only with ridiculously large (Mahlo) cardinals. I don't see why the size of Mahlo cardinals is ridiculous. Considering all the strongly inaccessible cardinals that have been discovered, Mahlo cardinals is rather weak. Also, the definition of a Grothendieck universe strongly resembles the definition of a strongly inaccessible cardinal, imho. That they are equival…

What do you mean exactly? Grothendieck universes correspond to the some inaccessible cardinals, but the axiom that every set is contained in a Grothendieck universe (which is stronger than just saying that there are omega-many inaccessible cardinals of increasing size) is itself weaker than the existence of a single Mahlo cardinal...

And (afaik) you need a Mahlo cardinal for every type theoretic universe that is closed under induction-recursion. My point is that induction-recursion is a very intuitive notion from a computational perspective, yet its encoding in set theory is anything but intuitive...

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#69

Post by pron »

fmap wrote: post #67
pron wrote: post #65

Earlier quoted context omitted.

Church doesn't really define computation[1], and Turing most certainly bases his entire definition (the first ever definition of computation) on multiple references to physical things (finite "states of mind", limits of what can be read or manipulated at any one time etc.). Brouwer also bases intuitionism on the physical, when he appeals to the limited capability of a finite (idealized) mind. Computation carried out…

Can you link to some of the references you cite? That seems like an interesting read. As for computability being a physical notion, I can't speak to the motivation of Church and his students, but I do know that there are characterizations of total computable functions in domain theory which make no mention of physics. The intuition about computable functions is that they are precisely the functions whose output for a…

> Can you link to some of the references you cite? That seems like an interesting read.

Sure.

It's best to start with Jean van Heijenoort's seminal From Frege to Gödel A Source Book in Mathematical Logic, 1879-1931[1]. It includes the original texts by Hilbert, Brouwer and many others, but the text I personally found most interesting was Hermann Weyl's, which I quoted here[2] nearly in full (in the parent comment I quoted some relevant passages from Brouwer and Hilbert; in fact, it was as part of that Reddit discussion that I found the references and learned what little I know of the philosophy of mathematics).

I've also found Juliet's Floyd's discussion of Turing's (and Wittgenstein's) mathematical philosophy[3] fascinating. She pinpoints how and why Turing viewed the philosophy of mathematics the way he did, how that view led him to the discovery of computation, and why people like Gödel and others found that to be such a profound philosophical breakthrough.

The Stanford Encyclopedia of Philosophy's entry on the philosophy of mathematics gives a good overview[4].

> The intuition about computable functions is that they are precisely the functions whose output for any given input depends only on a finite part of the input.

Once you know what computation is, you can define it in many ways. But why would that definition coincide with what we call computation? You can define foo to be such functions, but why are you calling them computable? And, BTW, even the very definition of finite possibly (I'm not sure about this point) requires reliance on the physical due to the multiple models of FOL and the problems with SOL.

> The really interesting thing about the Church Turing thesis is that there are so many different models of computation that capture precisely this idea

It is absolutely trivial to come up with a super-Turing mathematical model (e.g. just use reals, as in "pick the supremum of this bounded set of reals", or use a Turing machine with an infinite number of heads). All those other models are somehow based on capturing an intuitive notion of the human thought process, which is completely physical, and therefore, it is not surprising that they coincide. Turing was just the first who was able to give the notion a precise mathematical meaning. If you go back to the inception of those ideas, from Brouwer's intuitionism, Hilbert's formalism and even to the far older notion of the algorithm, you see that they're all tied to the capabilities of a physical human mind.

It's true that not all of those ideas actually mention physics because not all thinkers necessarily believed the mind to be completely physical, but they're all based on the idea of a limited mind, which I think we can safely call physical.

[1]: http://www.hup.harvard.edu/catalog.php?isbn=9780674324497

[2]: https://www.reddit.com/r/programming/comments/5k1v04/is_math...

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

[4]: https://plato.stanford.edu/entries/philosophy-mathematics/

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#70

Post by eastWestMath »

pron wrote: post #65
eastWestMath wrote: post #64

Earlier quoted context omitted.

Computation is an entirely abstract thing. Nowhere does the definition of Turing machines or the lambda calculus makes any reference to actual physical things.

Church doesn't really define computation[1], and Turing most certainly bases his entire definition (the first ever definition of computation) on multiple references to physical things (finite "states of mind", limits of what can be read or manipulated at any one time etc.). Brouwer also bases intuitionism on the physical, when he appeals to the limited capability of a finite (idealized) mind. Computation carried out…

The lambda calculus preceded Turing machines, in fact Turing worked on the lambda calculus before he published his work on Turing machines. Where on Earth did you pick up this rubbish?
Post reply on HN