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

21–30 of 88 posts

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#21

Post by JumpCrisscross »

rntz wrote: post #10
JumpCrisscross wrote: post #3

> Given any class of mutually exclusive classes, of which none is null, there is at least one class which has exactly one term in common with each of the given classes... If anyone else's train of thought got wrecked by the proposition of mutually-exclusive classes sharing terms, here you go: http://www.encyclopedia.com/people/science-and-technology/ma... .

The "there is at least one class which.." doesn't mean "there is at least one class in that class of mutually exclusive classes which..."; it means "there exists at least one class at all which...". This is one way of phrasing the axiom of choice (although Russell uses "class" instead of "set"; in modern-day usage, we distinguish classes from sets, and AC applies to sets only).

It made sense once I mentally substituted "there exists at least one class" for "there is at least one class".

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#22

Post by wfn »

golergka wrote: post #15
jesuslop wrote: post #6

If you want to hear of Friedman in real debate there is great discussion in the foundations of mathematics mailing list archives that are public. There there is real lively yet high-standards scholar figth of first rate experts from all viewpoints. I liked for instance the 'myth of second order logic' theme initiated by S. Simpson. It seems to me that the article is wrong when it says that the spheres recompounded bi…

> I liked for instance the 'myth of second order logic' theme initiated by S. Simpson. Can you link to the thread? The archives seem gigantic

Possibly http://www.personal.psu.edu/t20/fom/postings/9903/msg00069.h... (and Simpson's replies downthread, e.g. http://www.personal.psu.edu/t20/fom/postings/9903/msg00151.h...)

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#24

Post by d3ckard »

logicallee wrote: post #7
d3ckard wrote: post #4

It's especially interesting given that P vs NP is suspected to be unprovable in ZFC. Waiting for further development!

I'm curious why you say "P vs NP is suspected to be unprovable in ZFC". What would make mathematicians suspect that (if you know)? I mean ZFC is not a toy system, it is obviously used in complex and deep ways to prove or resolve long-standing questions in ways that build on tons of deep results that themselves took tons of research. (By the way for anyone else reading, just so you don't get the wrong idea: ZFC is act…

I do not feel competent to say exactly why is it so. The information is available on Wikipedia, probably based on Scott Aaronson survey mentioned in other comment.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#25

Post by logicallee »

rocqua wrote: post #17
logicallee wrote: post #7

Earlier quoted context omitted.

I'm curious why you say "P vs NP is suspected to be unprovable in ZFC". What would make mathematicians suspect that (if you know)? I mean ZFC is not a toy system, it is obviously used in complex and deep ways to prove or resolve long-standing questions in ways that build on tons of deep results that themselves took tons of research. (By the way for anyone else reading, just so you don't get the wrong idea: ZFC is act…

> ZFC is actually the standard set of axioms mathematicians work with every day I'd dispute that mathematicians work with ZFC every day. Most pure but not foundational mathematics basically works with intuitionist set theory. By keeping the size and nesting of sets small enough, we never need to worry about ZFC. Zorn's lemma comes up occasionally, but that is all.

Wikipedia says "Today ZFC is the standard form of axiomatic set theory and as such is the most common foundation of mathematics."

What my parenthetical comment that you quoted meant to say (for anyone that was not familiar with it) is thaz ZFC is not some joke, or obscure set of axioms or something irrelevant. Without this remark I thought my comment read that way.

I hope you will agree that ZFC is simply "standard math" - even if its axioms are not referenced explicitly by many working mathematicians.

If this statement requires further refinement let me know. Obviously I'm not a mathematician!

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#26

Post by sanduu »

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…

Do you use a pay~pal ? because if you do you can include an extra 300 a week to your earnings only working on the internet for 5 hours per day, check this site... http://bit.ly/2atnA1a

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#27

Post by Chinjut »

jesuslop wrote: post #6

If you want to hear of Friedman in real debate there is great discussion in the foundations of mathematics mailing list archives that are public. There there is real lively yet high-standards scholar figth of first rate experts from all viewpoints. I liked for instance the 'myth of second order logic' theme initiated by S. Simpson. It seems to me that the article is wrong when it says that the spheres recompounded bi…

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

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#28

Post by rocqua »

logicallee wrote: post #25
rocqua wrote: post #17

Earlier quoted context omitted.

> ZFC is actually the standard set of axioms mathematicians work with every day I'd dispute that mathematicians work with ZFC every day. Most pure but not foundational mathematics basically works with intuitionist set theory. By keeping the size and nesting of sets small enough, we never need to worry about ZFC. Zorn's lemma comes up occasionally, but that is all.

Wikipedia says "Today ZFC is the standard form of axiomatic set theory and as such is the most common foundation of mathematics." What my parenthetical comment that you quoted meant to say (for anyone that was not familiar with it) is thaz ZFC is not some joke, or obscure set of axioms or something irrelevant. Without this remark I thought my comment read that way. I hope you will agree that ZFC is simply "standard m…

Certainly, ZFC is not a pathological constructed example. When a mathematician looks for a foundational set of axioms, ZFC is THE standard choice. It is, and has been, for the last ~90 years at least.

My point was that foundational mathematics is rarely touched upon by a lot of normal pure mathematics (say number theory, field extension, graph theory).

Interestingly, I believe a lot of people actually dislike the axiom of choice. They find it to be way to 'complex' when compared to the other axioms. It is a lot like euler's 5-th axiom (2 straight lines with the same direction are equidistant everywhere). Interestingly in that case, removing the axiom led to spherical and hyperbolic geometry.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#29

Post by benibela »

rocqua wrote: post #28
logicallee wrote: post #25

Earlier quoted context omitted.

Wikipedia says "Today ZFC is the standard form of axiomatic set theory and as such is the most common foundation of mathematics." What my parenthetical comment that you quoted meant to say (for anyone that was not familiar with it) is thaz ZFC is not some joke, or obscure set of axioms or something irrelevant. Without this remark I thought my comment read that way. I hope you will agree that ZFC is simply "standard m…

Certainly, ZFC is not a pathological constructed example. When a mathematician looks for a foundational set of axioms, ZFC is THE standard choice. It is, and has been, for the last ~90 years at least. My point was that foundational mathematics is rarely touched upon by a lot of normal pure mathematics (say number theory, field extension, graph theory). Interestingly, I believe a lot of people actually dislike the axi…

You could say the mathematicians work as much with ZFC as programmers work with assembly

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#30

Post by pron »

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…

> a lot of ordinary mathematics that is outside of ZFC

A lot of ordinary math? I think there's one if not two exaggerations in there.

> My opinion is still that ZFC itself is unnatural as a foundation for mathematics, precisely because we have to do so much encoding to get anything useful out of it.

One of the things Friedman likes to emphasize about the foundation of math is that there is very little you actually need to do with it. A good foundation is one that you don't even need to know is there. Most mathematicians don't work in any formalism, so a foundation doesn't need to be useful. It's not as if anyone actually needs to do all those tedious set encodings.

Except that many of those who call for new foundations are really interested in mechanical proof checkers, and those do have to be useful. In order to make these arguments less religious, I think it would be worthwhile to adopt Turing's mathematical philosophy, which called for adopting mathematical foundations on an ad-hoc basis (or even no foundation at all). In other words, choose whatever foundation (if any) for the task at hand. This would make it easier to argue that, say, type theory is a more convenient core for proof checkers.

> This is not a direction that Friedman considers worthwhile, because he thinks that first-order logic and ZFC are inevitable.

That's not how I read him. He thinks that FOL and ZFC are good enough, and as foundations don't matter in practice (a good foundation is one you can ignore; I think that's a quote by him), it would take some achievement to justify seriously considering alternatives. He even says what it would take: easier teaching and/or easier proofs. So far no alternative foundation has been able to improve either one.

Post reply on HN