= 27d567bc2d48d9f40e9ccc20ea370b15)
Cyan comments on The two meanings of mathematical terms - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (78)
I interpreted that to mean that Eliezer doubts that a model that requires infinite sets will correspond to reality, not that the mathematics are incorrect. The figurative use of the word "atheist" makes the statement ambiguous, but his use of the phrase "actually seen" indicates that his concern is with modeling reality, not the math per se.
That was my (charitable) interpretation too, until, to my dismay, Eliezer confirmed (at a meetup) that he had "leanings" in the direction of constructivism/intuitionism -- apparently not quite aware of the discredited status of such views in mathematics.
And indeed, when I asked Eliezer where he thinks the standard proof of infinite sets goes wrong, he pointed to the law of the excluded middle.
His idol E.T. Jaynes may be to blame, who in PTLS explicitly allied himself with Kronecker, Brouwer, and Poincaré as opposed to Cantor, Hilbert, and Bourbaki -- once again apparently not understanding the settled status of that debate on the side of Cantor et al. One is inclined to suspect this is where Eliezer picked such attitudes up.
Can you elaborate on constructivism, intuitionism, and their discrediting? And what that has to do with the law of the excluded middle? I thought constructivism and intuitionism were epistemological theories, and it isn't immediately obvious how they apply to mathematics. Does a constructivist mathematician not believe in proof by contradiction?
Also, I don't know what you mean by "the standard proof of infinite sets".
I think komponisto is a little confused about the discredited status of intuitionism, and you're a little confused about math vs epistemology. Here's a short sweet introduction to intuitionist math and when it's useful, much in the spirit of Eliezer's intuitive explanation of Bayes. Scroll down for the connection between intuitionism and infinitesimals - that's the most exciting bit.
PS: that whole blog is pretty awesome - I got turned on to it by the post "Seemingly impossible functional programs" which demonstrates e.g. how the problem of determining equality of two black-box functions from reals in [0, 1] to booleans turns out to be computationally decidable in finite time (complete with comparison algorithm in Haskell).
Not at all. Precious few are the mathematicians who take the views of Kronecker or Brouwer seriously today. I mean, sure, some historically knowledgeable mathematicians will gladly engage in bull sessions about the traditional "three views" in the philosophy of mathematics (Platonism, intuitionism, and formalism), during which they treat them as if on par with each other. But then they get up the next day and write papers that depend on the Axiom of Choice without batting an eye.
The philosophical parts of intuitionism are mostly useless, but it contains useful mathematical parts like Martin-Löf type theory used in e.g. the Coq proof assistant. Not sure if this is relevant to Eliezer's "leanings" which started the discussion, but still.
Right, but in this context I wouldn't label such "mathematical parts" as part of intuitionism per se. What I'm talking about here is a certain school of thought that holds that mainstream (infinitary, nonconstructive) mathematics is in some important sense erroneous. This is a belief that Eliezer has been hitherto unwilling to disclaim -- for no reason that I can fathom other than a sense of warm glow around E.T. Jaynes.
(Needless to say, Eliezer is welcome to set the record straight on this any time he wishes...)
I do not understand what the word "erroneous" is supposed to mean in this context.
For the sake of argument, I will go ahead and ask what sort of nonconstructive entities you think an AI needs to reason about, in order to function properly.
Some senses of "erroneous" that might be involved here include (this list is not necessarily intended to be exhaustive):
Mathematically incorrect -- i.e. the proofs contain actual logical inconsistencies. This was argued by some early skeptics (such as Kronecker) but is basically indefensible ever since the formulation of axiomatic set theory and results such as Gödel's on the consistency of the Axiom of Choice. Such a person would have to actually believe the ZF axioms are inconsistent, and I am aware of no plausible argument for this.
Making claims that are epistemologically indefensible, even if possibly true. E.g., maybe there does exist a well-ordering of the reals, but mere mortals are in no position to assert that such a thing exists. Again, axiomatic formalization should have meant the end of this as a plausible stance.
Irrelevant or uninteresing as an area of research because of a "lack of correspondence" with "reality" or "the physical world". In order to be consistent, a person subscribing to this view would have to repudiate the whole of pure mathematics as an enterprise. If, as is more common, the person is selectively criticizing certain parts of mathematics, then they are almost certainly suffering from map-territory confusion. Mathematics is not physics; the map is not the territory. It is not ordained or programmed into the universe that positive integers must refer specifically to numbers of elementary particles, or some such, any more than the symbolic conventions of your atlas are programmed into the Earth. Hence one cannot make a leap e.g. from the existence of a finite number of elementary particles to the theoretical adequacy of finitely many numbers. To do so would be to prematurely circumscribe the nature of mathematical models of the physical world. Any criticism of a particular area of mathematics as "unconnected to reality" necessarily has to be made from the standpoint of a particular model of reality. But part (perhaps a large part) of the point of doing pure mathematics (besides the fact that it's fun, of course), is to prepare for the necessity, encountered time and time again in the history of our species, of upgrading -- and thus changing --our very model. Not just the model itself but the ways in which mathematical ideas are used in the model. This has often happened in ways that (at least at the time) would have seemed very surprising.
Well, if the AI is doing mathematics, then it needs to reason about the very same entities that human mathematicians reason about.
Maybe that sounds like begging the question, because you could ask why humans themselves need to reason about those entities (which is kind of the whole point here). But in that case I'm not sure what you're getting at by switching from humans to AIs.
Do you perhaps mean to ask something like: "What kind of mathematical entities will be needed in order to formulate the most fundamental physical laws?"
Regarding your three bullet points above:
It's rude to start refuting an idea before you've finished defining it.
One of these things is not like the others. There's nothing wrong with giving us a history of constructive thinking, and providing us with reasons why outdated versions of the theory were found wanting. It's good style to use parallel construction to build rhetorical momentum. It is terribly dishonest to do both at the same time -- it creates the impression that the subjective reasons you give for dismissing point 3 have weight equal to the objective reasons history has given for dismissing points 1 and 2.
Your talk in point 3 about "map-territory confusion" is very strange. Mathematics is all in your head. It's all map, no territory. You seem to be claiming that constructivsts are outside of the mathematical mainstream because they want to bend theory in the direction of a preferred outcome. You then claim that this is outside of the bounds of acceptable mathematical thinking, So what's wrong with reasoning like this:
"Nobody really likes all of the consequences of the Axiom of Choice, but most people seem willing to put up with its bad behavior because some of the abstractions it enables -- like the Real Numbers -- are just so damn useful. I wonder how many of the useful properties of the Real Numbers I could capture by building up from (a possibly weakened version of) ZF set theory and a weakened version of the Axiom of Choice?"
Why do you think that the axiomatic formulation of ZFC "should have meant an end" to the stance that ZFC makes claims that are epistemologically indefensible? Just because I can formalize a statement does not make that statement true, even if it is consistent. Many people (including me and apparently Eliezer, though I would guess that my views are different from his) do not think that the axioms of ZFC are self-evident truths.
In general, I find the argument for Platonism/the validity of ZFC based on common acceptance to be problematic because I just don't think that most people think about these issues seriously. It is a consensus of convenience and inertia. Also, many mathematicians are not Platonists at all but rather formalists -- and constructivism is closer to formalism than Platonism is.
Aaaand this makes me curious. Eliezer, for the sake of argument, do you really think we'd do good by prohibiting the AI from using reductio ad absurdum?
Nope. I do believe in classical first-order logic, I'm just skeptical about infinite sets. I'd like to hear k's answer, though.
Oi, that's not right. The domain of these functions is not the set of reals in [0, 1] but the set of infinite sequences of bits; while there is a bijection between these two sets, it's not the obvious one of binary expansion, because in binary, 0.0111... and 0.1000... represent the same real number. There is no topology-preserving bijection between the two sets. Also, the functions have to be continuous; it's easy to come up with a function (e.g. equality to a certain sequence) for which the given functions don't work.
Of course, it happens that the usual way of handing "real numbers" in languages like Haskell actually handles things that are effectively the same as bit sequences, and that there's no way to write a total non-continuous function in a language like Haskell, making my point somewhat moot. So, carry on, then.
Your comment is basically correct. This paper deals with the representation issue somewhat. But I think those results are applicable to computation in general, and the choice of Haskell is irrelevant to the discussion. You're welcome to prove me wrong by exhibiting a representation of exact reals that allows decidable equality, in any programming language.
Yes, a constructivist mathematician does not believe in proof by contradiction.
Huh. Good to know.