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

71–80 of 88 posts

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#71

Post by Chinjut »

AnimalMuppet wrote: post #59
Chinjut wrote: post #55

Earlier quoted context omitted.

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

Sets of things are somewhat different from transfinitely iterated sets of sets of sets of sets, though… (I'll call these ZF-sets).

Discrete sets of atomic objects are in fact (special) weak omega-groupoids and aren't ZF-sets. (In a ZF-set, every element of a set is itself a set, which is not true of, say, {red, green, blue}, unless we impose some completely artificial and obfuscating coding). You could just as well say that when we were counting the elements of sets thousands of years ago, we were doing the first rung of building up weak omega-groupoids, rather than the first rung of building up ZF-sets.

The name "weak omega-groupoids" makes them sound more intimidating as a concept than they actually are. They're just certain kinds of shapes. A bunch of dots (like a discrete set) is a weak omega-groupoid. A circle is a weak omega-groupoid. Spheres and donuts are weak omega-groupoids.

That said, I don't assert that weak omega-groupoids are any more intrinsically a foundational concept than ZF-sets; rather, I just note that ZF-sets aren't particularly elementary, either.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#72

Post by Chinjut »

Kutta wrote: post #63
AnimalMuppet wrote: post #60

Earlier quoted context omitted.

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.

I concur.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#73

Post by AnimalMuppet »

Kutta wrote: post #63
AnimalMuppet wrote: post #60

Earlier quoted context omitted.

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.

So when you said, "at the lowest level it's a collection of typing and computation rules which one can apply successively to do proofs and constructions", That was what Chinjut meant by "Homotopy Type Theory axiomatizes weak omega groupoids; it gives you formal rules you can manipulate to reason about weak omega groupoids"? That is, those lowest-level rules don't assume weak omega groupoids; they turn out to define weak omega groupoids?

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#74

Post by [deleted] »

pron wrote: post #66
Kutta wrote: post #62

Earlier quoted context omitted.

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, w…

[deleted]

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#75

Post by Chinjut »

pron wrote: post #66
Kutta wrote: post #62

Earlier quoted context omitted.

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, w…

I think it's worth distinguishing "constructive vs. non-constructive" and "ZF style vs. type theory" as different axes, which I think are getting conflated a bit here; you can have type theory style formal systems that embody non-constructive/non-computational principles, and you can have ZF style systems limited only to constructive reasoning (in the sense of Heyting-style intuitionistic logic, say).

Having distinguished these axes, for what it's worth, I don't think ZF-style theories of the cumulative hierarchy of transfinitely iterated sets of sets of sets…, and everything else as encoded into this by hook or by crook, have any advantage over type theory in teaching mathematical foundations, and indeed have some notable drawbacks.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#76

Post by pron »

eastWestMath wrote: post #70
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…

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?

Oh, I picked it up from Church's original 1936 paper. Those were direct quotes. Did you actually read Church's An Unsolvable Problem of Elementary Number Theory and Turing's On Computable Numbers? If so, could you point out Church's rigorous definition of computation?

BTW, while the lambda calculus does indeed precede Turing's work, its recognition as a universal expression of what is calculable happened at exactly the same time. But regardless, Church does not define the notion of computation, while Turing does.

But you don't have to take my word for it. You can find such rubbish by Gandi (who called Turing's work a "paradigm of philosophical analysis"), Davis, Gödel and many others: Gödel offered enthusiastic praise when he wrote that Turing offered "the precise and unquestionably adequate definition of the general concept of formal system" (Floyd, https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf)

The belief that Church defined computation rigorously when he solved the Entschidungsproblem using the lambda calculus rather than just made an imprecise conjecture is a common mistake and historical revisionism. If anyone came close to defining computation before Turing, that would have been Brouwer.

Also, I don't know if Turing worked on lambda calculus before he wrote On Computable Numbers. After completing the manuscript, he saw Church's new paper and incorporated it in an appendix. Do you have any reference for that?

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#77

Post by eastWestMath »

pron wrote: post #76
eastWestMath wrote: post #70

Earlier quoted context omitted.

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?

Oh, I picked it up from Church's original 1936 paper. Those were direct quotes. Did you actually read Church's An Unsolvable Problem of Elementary Number Theory and Turing's On Computable Numbers ? If so, could you point out Church's rigorous definition of computation? BTW, while the lambda calculus does indeed precede Turing's work, its recognition as a universal expression of what is calculable happened at exactly…

>The belief that Church defined computation rigorously when he solved the Entschidungsproblem using the lambda calculus rather than just made an imprecise conjecture is a common mistake and historical revisionism.

Ok I'm out, you do you man.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#78

Post by nuncanada »

Pete_D wrote: post #40
nuncanada wrote: post #37

Earlier quoted context omitted.

Precisely. Any attempts of even discussion about Higher Order theories on that list ends up with Harvey stating something that can be translated to those without the technical expertise as "Every higher order theory is a first order theory in disguise". Which is true but besides the point. Just look at Peano's axiomatization of the Natural Numbers and perceive how intuitively bad it is at abstracting what Natural Num…

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.

A simple answer would be: the Natural Numbers can be axiomatized infinitely many different isomorphic ways in First Order Theories. Which one is the "right" one? None and according to FOM wisdom you shouldn't care. In Higher Order Theories there is a very straightforward and natural way to define the Natural Numbers. Could you create other isomorphic axiomatizions? Yes but they certainly wouldn't be as pleasant and straightforward...

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#79

Post by nuncanada »

pron wrote: post #66
Kutta wrote: post #62

Earlier quoted context omitted.

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, w…

I must the only crazy guy that thinks Boltzmann and Weierstrass got the wrong axiomatization and Real Number Set is an oxymoron? They are completely physically unrealizable.

Every number that is not computable in the the Real Set is also not possible to be written down, don't have an algorithm for it, we can't even talk about or name any of them. All we can talk about is this uncountable part of the Real Set as a Set but never about one of the numbers itself.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#80

Post by pron »

eastWestMath wrote: post #77
pron wrote: post #76

Earlier quoted context omitted.

Oh, I picked it up from Church's original 1936 paper. Those were direct quotes. Did you actually read Church's An Unsolvable Problem of Elementary Number Theory and Turing's On Computable Numbers ? If so, could you point out Church's rigorous definition of computation? BTW, while the lambda calculus does indeed precede Turing's work, its recognition as a universal expression of what is calculable happened at exactly…

>The belief that Church defined computation rigorously when he solved the Entschidungsproblem using the lambda calculus rather than just made an imprecise conjecture is a common mistake and historical revisionism. Ok I'm out, you do you man.

You're free to believe what you want, or you can go read the abundant material, starting with Church's paper. If you find a thorough treatment of the concept of computation, you can write a paper about it. Church himself explicitly writes that he's unable to give a precise definition. Church was the first (scooping Turing by a few months) to claim that a certain formalism is what we now call Turing complete, i.e., universal with respect to the "vague intuitive notion" of the algorithm, but he was unable to provide a satisfactory justification for his claim (he made a circular argument and then gave up, writing the sentence I quoted above).

Turing, on the other hand, gives a fundamental treatment of what computation is, independent of any particular formalism (in his review of Turing's paper, Church described it as explaining how to construct "arbitrary" computing systems, and Gödel said, in the quote I've given, that Turing was able to give a general, universal, treatment of what a formal system is).

While I can't argue with your claim that Turing had worked with lambda calculus prior to writing On Computable Numbers when he was 24, I have seen no mention of this, but would be happy to see a reference.

Post reply on HN