Harvey Friedman bringing incompleteness and infinity out of quarantine(nautil.us)
nautil.us
Harvey Friedman bringing incompleteness and infinity out of quarantine
http://nautil.us/issue/45/power/this-man-is-about-to-blow-up-mathematics
85 comments
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...
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.
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 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.
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.
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 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?
[1]: https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf
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?
[1]: https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf
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.
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.
> 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.
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.
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.
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.
I agree, except that when people say "set theory" today, referring to formal set theory, they mean ZF by default, whereas when they say "type theory" it's unclear which type theory they mean. This alone suggests that type theory (or theories, rather) may not be ready for pedagogical use just yet.
Not everyone who says "(formal) set theory" means ZF by default. After all, many mean ZFC; probably moreso than mean ZF simpliciter. And some mean ZFC + various large cardinal axioms. Others go the other way, intending only Zermelo set theory. Some others default to meaning IZF or CZF. Some would even push for Aczel's Anti-foundation Axiom as cleaner system instead. Even in a world of sets of sets of sets of sets…, "set theory" does not mean just one particular formal theory.
Right, ZFC. Almost all mathematicians accept the axiom of choice. The rest are minor nuances that most students won't even encounter and are only ever investigated by logicians. And even the difference between ZF with or without C only manifests with uncountable sets. This is not the case with type theory. AFAIK, the theories can differ on such questions like whether all subsets of a finite set are finite.
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.
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.
The difference between ZF with and without C doesn't only emerge with uncountable sets, in any significant sense; even, say, the question of whether every countable set of two-element sets has a choice function depends on Choice.
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.
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 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.
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.
It's not like this issue hasn't come up, you know. That was at the core of the controversy between Hilbert and Brouwer. But if you think that math must be constructive you must realize that the ramifications are significant and the resulting math is very different and has its own counter-intuitive results. For one, analysis becomes much harder (at least so far) and very different; for example, in intuitionistic math, every function on the reals is continuous. Some counter-intuitive results are that a countable set can have an uncountable subset; in fact, not all subsets of a finite set are even finite. Andrej Bauer wrote a nice, mostly readable introduction to constructive math, which you may find interesting: http://www.ams.org/journals/bull/0000-000-00/S0273-0979-2016...
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.
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.
[deleted]
> So, Peano arithmetic is just too loose and fuzzy for my taste. It's full of things which aren't numbers...
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".)
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".)
Evaluation is always implicitly used in any sort of mathematical formalism. "2 + 2" is a program which evaluates to "4". Type theory just makes the computation arising from substituting definitions rigorous. Not letting "2 + 2" be equal to "4" by definition would be weird and inconvenient.
I get that evaluation is always implicit (or at least implicitly assumed to happen). My quarrel is with "evaluation == program == computation", and even more with the reverse: "a number == computation that would produce the number, therefore number == computation".
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...
[deleted]
> 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.
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.
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...
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...
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
> 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.
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.
>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.
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.
I'm not trying to rule who is more reasonable (and frankly, I have no idea) and certainly not to misrepresent category theorists (whom I didn't mention), but just respond to fmap's statement that "ZFC itself is unnatural as a foundation for mathematics", which assumes that 1. a foundation is something is regularly used for anything, and 2. that it is something that is both fixed and essential for mathematics; in other words that the name "foundation", rather than signifying the study of math at the lowest levels, actually refers to something fundamental mathematics "rests on". Very little math is done on top of a formal foundation at all, and most of math does not even require a foundation. In fact, it is questionable whether any formal "foundations" are really foundational, or, as Wittgenstein called them, "just another calculus". If that is the case, it's meaningless to argue that ZFC isn't a natural foundation for mathematics, because in spite of the name, it may not really be a foundation at all; just another calculus that is called "foundational" because of its level of discourse, in which case the arguments against it can only be aesthetic or pragmatic. In order to be pragmatic, you need to say what for what uses the foundation is inadequate.
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
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
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".
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...
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...
> If anything, if we want to take computation more seriously, we should adopt a foundation that accounts for non-terminating computation natively... Of course, ZFC is even worse in this regard.
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?
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?
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 is the role of foundations to tell us how those computations can be carried out in a pleasant way. Any change in our understanding of computation should lead us to revise how we construct and verify proofs.
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."
[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."
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).
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).
P.S.
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...
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...
> 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/
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/
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?
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?
>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.
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.
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.
> But the definition of computation is physical.
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.
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.
> A lot of mathematics is inspired by physical considerations, but mathematical concepts are themselves not physical.
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.
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.
> constructing and verifying proofs (even informal ones) is computing
I'd like to see your proof for that assertion...
I'd like to see your proof for that assertion...
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.
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.
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, 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.
Categorically, what's a limit is an object of ordered pairs (assuming you define them negatively, by their projections), not individual ordered pairs, right?
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.
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.
yep I should have made the distinciton cartesian product and pair of elements, thanks.
[deleted]
> 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
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...)
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.
> 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.
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.
[deleted]
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.
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.
ZF is subject to the incompleteness theorems, it can't prove Con(ZF). Even much simpler systems, like Peano arithmetic, are subject to them.
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...)
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...)
Con(ZF) is a sentence in ZF.
I think homotopy type theory has a better shot at providing a good foundation for math as opposed to some revision of set theory.
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?
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?
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.
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.
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?
I concur.
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.
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.
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.]
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.
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.
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?
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.
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.
> 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....
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".
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...).
It's especially interesting given that P vs NP is suspected to be unprovable in ZFC. Waiting for further development!
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
http://www.scottaaronson.com/papers/pnp.pdf
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.
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.
> 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.
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!
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!
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.
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.
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.
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...