Harvey Friedman bringing incompleteness and infinity out of quarantine • Hacker News Board

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#41

Post by catnaroek » Thu, Feb 23, 2017, 6:36 PM UTC

pron wrote: post #30

fmap wrote: post #8

There is a lot of ordinary mathematics that is outside of ZFC, which Friedman is well aware of but the writer of this article may not be. Grothendieck was not interested in abstract set theory when he introduced what are now called "Grothendieck Universes". He merely wanted to do algebraic geometry at a high level of abstraction. Similarly, Conway was apparently a bit dismayed when the formalization of his simple ide…

> a lot of ordinary mathematics that is outside of ZFC A lot of ordinary math? I think there's one if not two exaggerations in there. > My opinion is still that ZFC itself is unnatural as a foundation for mathematics, precisely because we have to do so much encoding to get anything useful out of it. One of the things Friedman likes to emphasize about the foundation of math is that there is very little you actually ne…

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

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#42

Post by pron » Thu, Feb 23, 2017, 7:02 PM UTC

catnaroek wrote: post #41

pron wrote: post #30

Earlier quoted context omitted.

> 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 ne…

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…

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

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#43

Post by lgandersen » Thu, Feb 23, 2017, 7:13 PM UTC

fmap wrote: post #8

There is a lot of ordinary mathematics that is outside of ZFC, which Friedman is well aware of but the writer of this article may not be. Grothendieck was not interested in abstract set theory when he introduced what are now called "Grothendieck Universes". He merely wanted to do algebraic geometry at a high level of abstraction. Similarly, Conway was apparently a bit dismayed when the formalization of his simple ide…

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

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#44

Post by pron » Thu, Feb 23, 2017, 8:06 PM UTC

eastWestMath wrote: post #35

pron wrote: post #30

Earlier quoted context omitted.

> 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 ne…

>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 m…

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

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#45

Post by Kutta » Thu, Feb 23, 2017, 8:16 PM UTC

Pete_D wrote: post #40

nuncanada wrote: post #37

Earlier quoted context omitted.

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

At the risk of asking a naïve question, why do you think the Peano axioms are ugly? As a mostly-lay mathematician I always thought they were quite elegant.

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.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#46

Post by catnaroek » Thu, Feb 23, 2017, 8:18 PM UTC

pron wrote: post #42

catnaroek wrote: post #41

Earlier quoted context omitted.

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…

> 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 quant…

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.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#47

Post by pron » Thu, Feb 23, 2017, 8:28 PM UTC

catnaroek wrote: post #46

pron wrote: post #42

Earlier quoted context omitted.

> 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 quant…

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…

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

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#48

Post by catnaroek » Thu, Feb 23, 2017, 8:40 PM UTC

pron wrote: post #47

catnaroek wrote: post #46

Earlier quoted context omitted.

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…

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

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

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#49

Post by jesuslop » Thu, Feb 23, 2017, 8:58 PM UTC

catnaroek wrote: post #36

jesuslop wrote: post #32

Earlier quoted context omitted.

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

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.

yep I should have made the distinciton cartesian product and pair of elements, thanks.

Re: Harvey Friedman bringing incompleteness and infinity out of quarantine

#50

Post by AnimalMuppet » Thu, Feb 23, 2017, 9:26 PM UTC

Kutta wrote: post #45

Pete_D wrote: post #40

Earlier quoted context omitted.

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 cor…

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