Harvey Friedman bringing incompleteness and infinity out of quarantine

http://nautil.us/issue/45/power/this-man-is-about-to-blow-up-mathematics

by dnetesn • 9 years ago

141 81 9 years ago

His recent posts on equivalence theory: http://www.cs.nyu.edu/pipermail/fom/2017-February/020299.htm... http://www.cs.nyu.edu/pipermail/fom/2017-February/020300.htm... http://www.cs.nyu.edu/pipermail/fom/2017-February/020301.htm...

They still don't strike me as particularly natural or simple, particularly when compared to my favorite example of incompleteness, the surreal numbers. The surreal numbers are defined via transfinite induction and can grow as large as whatever cardinal you choose, and there are good reasons to pick large cardinals (closure under various operations), with the associated complications.

“The idea that there’s absolute solidity, a right and wrong, in mathematics—that mathematics has no real conceptual philosophical issues that have to be dealt with … I’m interested in completely blowing that up.”

First-order logic is sound and complete; it's only second-order and higher logic that supports Godel's incompleteness theorem. Since most math is done in first-order logic (plain ZF, not even C; I think this is what the 85% figure in the article is referring to) I'm pretty sure this is not going to happen.

cousin_it2• 9 years ago

ZF is subject to the incompleteness theorems, it can't prove Con(ZF). Even much simpler systems, like Peano arithmetic, are subject to them.

Mathnerd3143• 9 years ago

It's consistent/complete in first-order logic, because Con(ZF) is a higher-order statement and thus can't even be formulated.

First-order logic has a lot of nice properties, e.g. "if a result is finitary in the sense that it can be phrased as a first-order statement in Peano Arithmetic, and it can be proven using the axiom of choice (or more precisely in ZFC set theory), then it can also be proven without the axiom of choice (i.e. in ZF set theory)." (c.f. https://terrytao.wordpress.com/2013/12/07/ultraproducts-as-a...)

JumpCrisscross2• 9 years ago

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

Mathnerd3143• 9 years ago

Yeah. Typically you don't even use Choice though, instead it's Zorn's Lemma: https://en.wikipedia.org/wiki/Zorn's_lemma. Zorn's Lemma has interesting weakenings, like https://en.wikipedia.org/wiki/Boolean_prime_ideal_theorem (they all amount to statements about particular types of ultrafilters: https://terrytao.wordpress.com/2007/06/25/ultrafilters-nonst...).

rntz• 9 years ago

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

JumpCrisscross2• 9 years ago

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

d3ckard2• 9 years ago

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

IngoBlechschmid• 9 years ago

I hugely enjoyed a survey article by Scott Aaronson on P ≟ NP. Section 3.1 contains a discussion on the possibility of the question being independent from ZFC. (He doesn't believe this possibility to be likely.)

http://www.scottaaronson.com/papers/pnp.pdf

logicallee2• 9 years ago

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 actually the standard set of axioms mathematicians work with every day. It's the normal way to do math.)

What would make someone suspect this one is impossible to prove/decide under ZFC? (Or what would make someone think it is independent under ZFC?)

"A lot of people have tried to prove it" doesn't seem a convincing argument. (Consider advances toward the twin prime conjecture, or the now-proven Fermat's last theorem, etc.) There must be something more that makes you say that.

Thank you for any answer.

rocqua2• 9 years ago

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.

d3ckard2• 9 years ago

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.

jesuslop4• 9 years ago

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 bigger are a problem of large cardinal axioms. I think it derives from Choice, the C in ZFC instead.

golergka• 9 years ago

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

wfn• 9 years ago

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

jesuslop4• 9 years ago

I made this version for me of the relevant posts, too big for pastebin, hope permissions are ok: https://app.box.com/s/l36rfge3stx6go34or6l64m2eexijd26 Some initial posts are warmup.

Chinjut7• 9 years ago

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

jesuslop4• 9 years ago

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, and while that's not a FOM, it's an indicative that there may be something there. Also by comparison, as user fmap said, there is much coding in Set Theory. Just look at an ordered pair. In set theory it is the Kuratowski pair, and that a violent encoding. It a hack. We're not nearer to answer what they really are by that. Categorically they are a limit, which perhaps it's also not metaphysical chant, but we can feel it however less hacky.

fmap3• 9 years ago

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 idea of "surreal numbers" required deeply unnatural encodings in ZFC...

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. And whenever you iterate "large" encodings you leave the universe of "ordinary ZFC". Conway suggested - and this is realized in modern type theory - that we should instead allow arbitrary "free" constructions, such as his surreal numbers, to extend the basic universe of mathematics. To some extend this can be encoded in set theory, but only with ridiculously large (Mahlo) cardinals.

This is not a direction that Friedman considers worthwhile, because he thinks that first-order logic and ZFC are inevitable. It's a shame that so many people on the FOM mailing list share the same view. There are good reasons why you don't find a lot of category theorists on that list anymore...

auggierose• 9 years ago

You can combine ZFC and simple type theory to give you something in which you can comfortably do surreal numbers. This is done by embedding ZFC as a simple type. For example, here this is done for Partizan Games (which contain the surreal numbers): http://link.springer.com/chapter/10.1007/11921240_19

pron17• 9 years ago

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.

hyperpape• 9 years ago

Algebraic geometry seems entirely like ordinary math, in the funny sense where it doesn't mean "elementary" but "the kind of thing mathematicians who don't intrinsically care about foundations like to do".

eastWestMath4• 9 years ago

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.

I think you're misrepresenting the category theorists, they're usually the ones arguing for choosing whatever foundation is convenient for a given domain. A lot of the time, this is a type theoretic foundation because a lot of modern mathematics is about pretending you have function types when you don't actually have function types in your category (such as differential geometry) or that all you care about is a "core" set of operations and the rest of the framework you're working in simply gets in the way (such as Hilbert spaces vs. compact closed dagger categories in categorical quantum mechanics). And if you know already knew dependent type theory then synthetic homotopy theory is easier than classical homotopy theory, some proofs in homotopy theory can take several lectures to present and even then it will still be pretty hard to see why they hold.

It's just weird to see people thing the category theorists are the one being impractical compared to the set theorists like Friedman. I can't think of a categorical logician who doesn't have an active line of research outside of logic; usually in topology, computability, quantum mechanics, or algebraic geometry. They're not just logicians but active researchers in computer science, physics and mathematics, logic is a powerful tool and should be applied in these fields.

catnaroek4• 9 years ago

If anything, if we want to take computation more seriously, we should adopt a foundation that accounts for non-terminating computation natively. One defect of MLTT is that, when you add non-terminating computation to it, the mathematical structures you can describe in it get horribly deformed. So MLTT users tend to limit themselves to a world where computation can't be expressed unless you have established beforehand that it will halt. What a sorry state of affairs! (Of course, ZFC is even worse in this regard, at least in MLTT you have a more or less direct relationship between programming and proving.)

Fortunately, I think the solution already exists, although the details might yet have to be polished: take Paul Blain Levy's “call by push value” (which distinguishes between values and computations), and make the dependent type formers (sigma and pi) range over values and only values...

nuncanada4• 9 years ago

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 Numbers are. He constructs an "ugly" object that is isomorphic to Natural Numbers, but doesn't correspond to what Mathematicians intuitively believe the Natural Numbers to be. With a Second Order theory you can just axiomatize the Natural Number in a pretty straightforward way that correspond to Mathematician's intuition about the Set...

Pete_D• 9 years ago

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.

lgandersen• 9 years ago

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 equivalent are (relatively) straightforward.

Harvey Friedmans work on provable equivalences between large cardinals way larger than Mahlo cardinals and theorems about objects in the domain of the rationals further substantiates this. Very fascinating.

fmap3• 9 years ago

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

lmm• 9 years ago

Showing it’s not provable, on the other hand, is more difficult. He did this with a proof by contradiction: He began with the assumption that he could prove his theorem in ZFC, and then constructed from it a system of objects in which ZFC holds. Which means that if his theorem holds true, then ZFC is consistent—and, transitively, that ZFC has proven its own consistency. But by Gödel’s incompleteness theorem, that cannot possibly be the case. And so, the theorem cannot be proven in ZFC. He’s working to extend the theory to other types of symmetries, other definitions of “maximal,” and other types of objects.

So he encoded some statements about ZFC into these statements about sets of rationals. Wasn't Gödel was able to do better already, encoding statements about ZFC into basic arithmetic/number theory? I guess I just don't understand what the big breakthrough is supposed to be, even though I'm interested in alternate axiom systems (e.g. the whole homotopy type theory / univalent foundations business). Is the idea that he's come up with some new natural statements about symmetries of sets that turn out to demonstrate incompleteness? That would be an innovation, but the above description makes it sounds like it's more about finding symmetry statements that correspond to ZFC.

arketyp• 9 years ago

How does this relate to automata theory and Wolfram's principle of computational equivalence (spare me any lectures about his self-promotion) and the conjecture that universal Turing machines are virtually ubiquitous and arise from the simplest of rules?

orbifold• 9 years ago

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

AnimalMuppet7• 9 years ago

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?

Chinjut7• 9 years ago

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.

Kutta5• 9 years ago

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.

ibgib• 9 years ago

Interesting article. I can relate to his dictionary investigations when I was confronted with being taught about "circular definitions". I couldn't get around (no pun intended) the fact that all definitions were circular.

This is what has led me to developing ibGib, which as I stated here elsewhere (https://news.ycombinator.com/item?id=13632500) that ibGib is heavily influenced by Goedel in that it uses a SHA-256 hash of an immutable datum to effectively be the Goedelian number of that datum. So there are four fields: ib, gib, data, rel8ns. The gib is the hash of the other three fields, which allows for integrity of the data, as well as allowing it to be content addressable since the ib^gib is the address. So it's a monotonically increasing data store that focuses on the process of defining.

So instead of "proofs" that imply an ontological/objective "truth", ibGib focuses on "the meta proof" that is the prov-ing process by assigning any "proving mechanism" a number (just as it assigns anything a number). This way, you are approaching paradoxes and the like as a process of economics and evolution of proving systems. This is like the "proof" that contains the peer review process that is doing the proving.

Harvey Friedman bringing incompleteness and infinity out of quarantine

Related Stories