Harvey Friedman bringing incompleteness and infinity out of quarantine
nautil.us
nautil.us
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...
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.
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.
But I think it's naive to pretend that there's no fight over aesthetics here, which is why I mentioned Turing, as I see a return to logicistic (as in logicism) arguments (which view mathematical foundations as truly fundamental) in new form, while Turing's philosophy manages to, according to Wittgenstein, avoid "needless dogmatism and dispute". I strongly encourage anyone interested in the subject to read Juliet Floyd's fascinating paper on Turing's mathematical philosophy: https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf
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...
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 quantities greater than the speed of light? This notion may not be as far-fetched as it may seem, because the sole justification for defining problems that take an infinite number of steps to compute as "non-computable" in the first place was physical, as was Brouwer's justification for intuitionistic mathematics. Moreover, Turing quickly realized that computability (or its converse, non-termination) are crude approximations for feasibility (or tractability), that was more fully developed later. And we could continue this argument further to any degree, so why stop at computability?
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 hypothesis.
Then let's not mention it, and stick to what can be dealt with mathematically.
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.
[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."
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).
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/
I also strongly recommend the excellent 1988 paper by Robin Gandy, The Confluence of Ideas in 1936, published in The Universal Turing Machine A Half-Century Survey (ed. Rolf Herken), 1995[1] (pp. 51-102).
Gandy gives a full historical background of who knew what in 1936, what the general state of knowledge was at the time, and the reception of both Church's and Turing's papers.
[1]: https://www.amazon.com/Universal-Turing-Machine-Half-Century...
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?
Ok I'm out, you do you man.
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.
I'd like to see your proof for that assertion...
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 corresponds very closely to intuitions about intended (standard) models.
In contrast, the lack of clear computational meaning in classical theories makes it necessary find philosophical justifications, which in turn usually refer to other theories without clear computational meaning. Of course, we can compile classical proofs to programs as well through a variety of transformations, but they tend to be sort of unsatisfying, for example we may get functions with empty domains that we can't actually call, instead of programs evaluating to numerals.
So, Peano arithmetic is just too loose and fuzzy for my taste. It's full of things which aren't numbers, rather statements referring to things which have properties which we think numbers should have. And then we can choose between sticking to first-order logic and leaving non-standard models in, or switching to second-order induction which lets us prove more statements at the cost of completeness and leaning more on ambient set theory.
Simpson seems to be critical of second-order logic because it's set theory in disguise; but to me that kind of dispute is moot because I find any sort of classical logic unsuitable for mathematical foundations.
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".)
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?
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.
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.
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.
When mathematicians, not logicians, learn logic, it should be made to combine with what they actually do. Type theory is not quite there yet, and is still rather inaccessible and arcane, although that may change.
Turing was interested in making type theory approachable to mathematician, and came up with a gradual path to adoption in his 1944 unpublished manuscript The Reform of Mathematical Notation and Phraseology. He writes:
> It has long been recognised that mathematics and logic are virtually the same and that they may be expected to merge imperceptibly into one another. Actually this merging process has not gone at all far, and mathematics has profited very little from researches in symbolic logic. The chief reasons for this seem to be a lack of liaison between the logician and the mathematician-in-the-street. Symbolic logic is a very alarming mouthful for most mathematicians, and the logicians are not very much interested in making it more palatable. It seems however that symbolic logic has a number of small lessons for the mathematician which may be taught without it being necessary for him to learn very much of symbolic logic.
> In particular it seems that symbolic logic will help the mathematicians to improve their notation and phraseology, which are at present exceedingly unsystematic, and constitute a definite handicap both to the would-be-learner and to the writer who is unable to express ideas because the necessary notation for expressing them is not widely known.
> ... It would not be advisable to let the reform take the form of a cast-iron logical system into which all the mathematics of the future are to be expressed. No democratic mathematical community would stand for such an idea, nor would it be desirable. Instead one must put forward a number of definite small suggestions for improvement, each backed up by good argument and examples. It should be possible for each suggestion to be adopted singly. Under these circumstances one may hope that some of the suggestions will be adopted in one quarter or another, and that the use of all will spread.
In the preface to the manuscript, published in Collected Works of A.M. Turing, Volume 4: Mathematical Logic, 2001, Robin Gandy writes:
> Perhaps the most striking thing about this paper is its modesty. Turing was first and foremost a mathematician. He believed that the chief purpose of mathematical logic and the study of the foundations of mathematics was to help mathematicians to understand what they were doing, and could do. In pursuit of this goal, mathematical logicians must perforce construct and manipulate complex formal systems. But they have a duty to explain to mathematicians, in as non-technical way as possible, what they have accomplished. ... Turing disliked those high priests of logic who sought... to blind the mathematician-in-the-street with arcane formalisms.
It is my impression (and I'm not even a mathematician-in-the-street but a programmer-in-the-street) that type theory hasn't yet emerged out of the "high priest" stage.
This is orthogonal to the distinction between type theory-style frameworks and everything-is-a-set ZF-style frameworks, as I was noting before. Whether "all subsets of a finite set are finite" or not can be true or false just as well in ZF-style systems as in type theory systems (taking "finite" to mean "having cardinality equal to a natural number", this is basically just the question of whether we are using classical or intuitionistic logic; you can have classical type theories, and you can have intuitionistic ZF-style theories). As I said, let's not conflate the type theory vs. ZF-style axis with the constructive vs. non-constructive axis.
As for what non-logician mathematicians use in practice, almost everything they do could be done in Zermelo set theory simpliciter (making use only of sets of rank less than omega * 2). I doubt the majority of non-logician mathematicians could even reliably correctly list all the axioms of ZFC. Sure, they've been trained ritualistically to say ZFC is what they're using, but they really aren't using ZFC in particular, any more than any other formal system into which their work could be just as well translated (the formal system of higher-order logic corresponding to Boolean topoi with natural numbers and choice, say).
Frankly, type theory is a lot closer to what "actual" (i.e., non-logician) mathematicians actually do than ZF; actual mathematicians don't spend a lot of time talking or thinking about transfinitely iterated sets of sets of sets…. Actual mathematical practice does come implicitly with types; integers are one type of thing, and functions from reals to natural numbers are another type of thing, and sets of complex numbers paired with Booleans are a third type of thing, and one would never ask whether 7 was an element of 3 or the squaring function on integers was an element of the complex number 3 + 5i, etc.
Framing mathematical ontology in terms of types is not some esoteric practice far removed from the mathematician/programmer in the street. If you've ever written a program in C/C++ or Java, you've worked with types.
Finally, your Turing quotes aren't about type theory in particular, but symbolic logic in general. They apply equally so to ZFC or any other such formal system.
I agree, but that's not my argument.
> Frankly, type theory is a lot closer to what "actual" (i.e., non-logician) mathematicians actually do than ZF
I've seen this claim made many times, and it's quite iffy. Mathematicians may think of types, but those types are not really much closer to type-theoretical formal types than to formal sets.
> and one would never ask whether 7 was an element of 3 or the squaring function on integers was an element of the complex number 3 + 5i, etc.
This is a misrepresentation of formal set theory in practice. No one investigates those anyway, and in proof assistants based on ZFC they are unprovable. I.e. 3 ∈ 7 has some truth value like any proposition but not one that could be determined in the theory, and it is nonsensical. In other words, 3 ∈ 7 has the same meaning as 1/0 in practical formalizations of set theory (like proof assistants): they are both equal to some value, but that value cannot be determined.
> Framing mathematical ontology in terms of types is not some esoteric practice far removed from the mathematician/programmer in the street.
Right, but there are plenty of annoying details. Even with simple questions such as what 1/0 means: if it's well typed you need to introduce partial functions which are not a familiar or simple concept; if it isn't, you need to introduce dependent types, with their own world of pain. The annoying details of type theory don't get in the way until you get to large sets.
See Leslie Lamport's discussion on the use of types in math[1].
In any event, I think TT should take some more time to mature and become canonized.
> Finally, your Turing quotes aren't about type theory in particular, but symbolic logic in general. They apply equally so to ZFC or any other such formal system.
Yes, but the paper talks about gradually introducing mathematicians to "naive" type theory (Turing wrote a couple of papers about making type theory practical). But my point is about his approach: logicians must make their formal systems approachable. Set theory (at least the part that concerns most ordinary math) is very approachable. Type theory isn't yet.
[1]: Types Are Not Harmless, 1995 research.microsoft.com/en-us/um/people/lamport/tla/types.ps.Z
I meant set theory there, not type theory.
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.
There are numerous philosophical justifications for non-constructive math, but the pragmatic one is that it is -- as far as we know -- consistent, and coincides with constructive math in all physically realizable instances. Hilbert, for example, said that math has "real propositions" (with physically observable consequences), as well as formalistic propositions, which we can accept as they agree with the real propositions in all instances.
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.
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...
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.
Can you link to the thread? The archives seem gigantic
If I recall correctly, categorical thinking doesn't emphasize elements of objects much, but in certain categories (perhaps pretoposes? I forget), morphisms from the terminal object to X can be considered the “global elements” of X.
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.
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.
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...)
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?
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.
Weak omega groupoids? Not so much.
[Edit: Excellent ELI5, though. Thanks.]
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.
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.
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.
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....
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.
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.
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!
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.