Kurt Gödel and the Mechanization of Mathematics
the-tls.co.uk
the-tls.co.uk
Isn't that strange? Wouldn't you think that undecidable propositions would be scattered through mathematics and turn up at curious and interesting moments in different fields? But apparently that's not generally the case. The Goldbach conjecture (Knuth) and of course the Riemann Hypothesis have been mentioned as possible candidates (but you might have said the same thing about Fermat's last theorem 30 years ago). If we did find a first-rank conjecture in number theory or some other area that's undecidable in ZFC (or whatever system) then we would at last be stepping through the door that Gödel opened for us.
Not provable in Peano Arithmetic.
https://en.m.wikipedia.org/wiki/Continuum_hypothesis
Not provable in ZFC.
There are a few more.
Cohen's incompleteness results do not hold for a theory of sets that axiomatizes sets up to a unique isomorphism. See the following:
> The theory Ordinals is algorithmically inexhaustible
Proof checking in the theory Ordinals is algorithmically checkable although theorems are not computationally enumerable because instances of strongly-typed induction axiom are uncountable.
Cheers, Carl
The link below works for me in FireFox:
That URL produces a HTML page containing a link to "Delivery.cfm/SSRN_ID3488706_code2561841.pdf?abstractid=3457802&mirid=1" with text "Download This Paper", which I assume is supposed to be the direct link. However https://papers.ssrn.com/sol3/Delivery.cfm/SSRN_ID3488706_cod... 302 redirects back to https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3457802 .
It's like the halting problem. It doesn't prevent programmers from automating stuff and reasoning about programs.
In other words, impossibility results make it possible to have a practical discipline where people are focused on feasible approaches instead of spending all their time and money researching pie in the sky technologies that can never work. It's like when alchemy turned into chemistry and astrology turned into astronomy, because the fields became restricted to what is realistic.
Arguably the same still has to occur in other disciplines cough AI cough.
https://en.wikipedia.org/wiki/No_free_lunch_in_search_and_op...
According to [Shamir, et. al 2019] “given any two classes C1 and C2, along with any point x∈C1, and our goal is to find some nearby y which is inside C2. Our ability to do so suggests that all the classes defined by neural networks are intertwined in a fractal-like way so that any point in any class is simultaneously close to all the boundaries with all the other classes.” Their results suggests that gradient classifiers (aka "Deep Learning") could remain forever fragile in ways that cannot be remedied by larger training sets.
Also important are the results on Inference Robust Logic, e.g. speed bumps) in the following:
I used a human in the loop approach for comparison, and those models, while not as accurate, seem much more robust. I think humans are better at identifying the big picture patterns, whereas ML approaches will microoptimize their way to a fragile approximation of the big picture pattern.
Practically, besides likelihood of breakdown, this means these overfit ML models are very susceptible to hacking. I predict once ML becomes more commercially widespread, we'll see a big increase in ML hacking.
It's not being ignored, it's just that once you know about the theorem, there are whole classes of problems that are no longer being worked on because they're impossible to solve.
It's like once you know about relativity, you stop trying to learn about the properties of the aether.
Genuinely curious - what problems? (Outside special things in Axomatic Set Theory like the Continuum Hypothesis.) E.g. are there topologists not working on certain problems in Topology because they're know to be undecidable?
This seems like post-hoc reasoning. Imagine the state of mathematics if his theorems had not been true and ZFC (or some extension) had been proven complete and consistent. Mathematics could have been the first entire field of knowledge to automate itself out of a job!
Turing's proof of Godel's incompleteness devised the Turing machine as a metaphorical device to demonstrate incompleteness - this then led to the whole of computing.
And for Church's proof of Godel's incompleteness he devised the lambda calculus which founded functional programming, McCarthy's LISP, and the Y-combinator of algebraic recursion.
https://writings.stephenwolfram.com/2006/05/kurt-godels-100t...
"What we observe is not nature itself, but nature exposed to our method of questioning ."
As far as I know, that last clause was never a claim made by Godel. Specifically the claim that these propositions are nevertheless true. This follows quite simply from the assumption that either a proposition is true, or its negation is true (i.e. the law of the excluded middle). But I recall reading that Godel, in his proofs, went to great lengths to avoid the law of the excluded middle over infinite sets.
Indeed, (again AFAIK) godel's first incompleteness theory still holds in constructive mathematics (roughly where the law of the excluded middle cannot be used). As such, I think the addition that these propositions are 'nevertheless true' actually hides a lot of complexity. Because there are philosophical positions in which these independent propositions are neither true not false.
And really, this is why we call them independent. The truthiness of these propositions is not determined by their axiom systems. It's a rather big philosophical stance to say that the 'truth' of these propositions can be determined outside of the axiomatic systems. It seems to me like that claims there is an objective (as in, not dependent on an axiomatic system) definition of what is true.
"in any particular model" - this is exactly parent's point.
From Wikipedia, a restatement of the 1st incompleteness theorem:
> there are statements of the language of F which can neither be proved nor disproved in F
The truth of a proposition P, within F, means "P is an axiom of F, or can be proved in F".
Saying "there are statements of the language of F which can neither be proved nor disproved in F... but the statements are true nevertheless" is appealing to some 'objective notion' of truth that transcends F.
No, truth and proof are NOT the same thing. The system F needn't have any notion of truth. For example, Peano arithmetic has no notion of truth. Peano arithmetic has notions of zero, successor, addition, and multiplication--none of truth.
Almost all competent mathematicians would agree that there exist theorems in the language of PA which are neither provable nor disprovable in PA but which are nevertheless true. Here, "true" means "true in the standard model of PA", not "true according to PA"---the latter isn't even meaningful because there is no such thing as "truth according to PA".
Less contrived examples are:
2. Goodstein's Theorem https://en.wikipedia.org/wiki/Goodstein%27s_theorem
3. A theorem stating that every computable strategy is a winning strategy in the hydra game (see https://faculty.baruch.cuny.edu/lkirby/accessible_independen...)
4. The strengthened finite Ramsey theorem, see https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theor...
Then (and this is super important) he explains that IN THE STANDARD INTERPRETATION that sequence of symbols can be translated to “the sequence of symbols corresponding to the number XXXXX is a statement which has no proof” (and has to be true) and that very sequence corresponds to that number XXXXX.
But those two things (the construction and the interpretation) are totally separated, and goes to great lengths to keep them so.
I don’t think so. ZFC is either consistent or it isn’t. That is, a Turing machine enumerating all theorems of ZFC either produces 0=1 or it doesn’t. This is, however, independent of ZFC (if the latter is consistent) by the second incompleteness theorem. See https://mathoverflow.net/a/332266, in particular Nik Weaver’s comment:
> I think the strongest argument in favor of the definiteness of ℕ, and against the idea that PA, or any other axiomatization, is the be-all end-all, is the evident fact that we have an open-ended ability to go beyond any computable set of axioms, for instance by affirming their consistency. If you accept PA you should accept Con(PA), and the process doesn't stop there: you can then accept Con(PA + Con(PA)), and so on. This goes on to transfinite levels. If our understanding of ℕ really were fully captured by some particular set of axioms then we would not feel we had a right to strengthen those axioms in any special way; the fact that we do feel we have this right shows that our understanding is not captured by any particular set of axioms.
You look at some big list of symbols and say "this formula (model) corresponds to whether a Turing machine enumerating all theorems of ZFC produces 0=1 (reality)". But does it really?
This is a common misrepresentation of Hilbert's Formalism. It doesn't state that no mathematical sentence has content beyond its mere symbols, but that not every mathematical sentence has content beyond its mere symbols.
Formalism was meant as a compromise between the two dueling philosophies of mathematics of the time: Russel's Logicism, which essentially said that all of mathematics can be derived from some self-evident, obviously true, logical axioms, and Brouwer's Intuitionism, which essentially said that the truth of mathematics stems from empirical confirmation that breaks down when infinities are involved, and therefore some logical axioms cannot be taken to be true for infinites. Hilbert tried to accept Brouwer's finitist philosophical position without rejecting any useful axioms. Formalism, then, separates mathematical sentences into two kinds: "real" -- those dealing with finite quantities and can be tied to physical observation and prediction, and "ideal" -- those dealing with infinities. Instead of rejecting the latter, Formalism says that as long as they don't introduce inconsistencies that invalidate the former, one could view them -- the ideal sentences -- as having no content beyond symbols, i.e. as not referring to anything "real".
A better (but still not entirely accurate) description would be that Brouwer had an epistemic conception of mathematical truth: mathematicians become able to assert mathematical truths as they engage in the process of constructing mathematical objects. This is indeed a constructive process, but it isn't finitistic -- for Brouwer mathematical reasoning is open-ended rather than a closed set of rules.
So much like Goedel (who disagreed with Brouwer in many other respects), Brouwer was totally committed to the idea that mathematical statements actually mean things. And because they carry meaning, the mathematical process and the properties of the mathematical objects created by a mathematician take precedence over the rules of logic.
This is why Brouwer rejected classical logic -- not because of any finitistic reason, but because (for example) classical logic permits disassembling the continuum into its set of points. Since (for Brouwer) the point of a continuum is that it is continuous, it followed that any logical principles (such as classical logic plus set theory) that permitted you to break up the continuum were fallacious. This is why he spent a lot of time on his so called "strong counterexamples", such as his proof that intuitionistically all total functions on the reals are continuous.
Notice that the direction of reasoning here is exactly the opposite of what a finitist would accept: Brouwer used the properties of the continuum to justify various finitary logical rules, rather than the other way around. The continuum was real, and logic just a façon-de-parler.
I find this kind of thing really interesting because it illustrates that the pretheoretical idea of truth can be formalized in many different ways, and that the various formalizations are not all compatible with each other. We are used to informal ideas like space having many different mathematical realizations -- metric spaces, topological spaces, vector spaces, etc -- but it is a little disconcerting (and a lot fascinating) to realize that logic and truth exhibit the same plural nature.
> Within a specific finite "main system" we can always test (that is, either prove or reduce to absurdity) properties of systems, that is, test whether systems can be mapped, with prescribed correspondences between elements, into other systems; for the mapping determined by the property in question can in any case be performed in only a finite number of ways, and each of these can be undertaken by itself and pursued either to its conclusion or to a point of inhibition [here is his mention of induction that I provide below].
> ... On the basis of the testability just mentioned, there hold, for properties conceived within a specific finite main system, the principle of excluded middle
> ... It is a natural phenomenon, now, that numerous objects and mechanisms of the world of perception, considered in relation to extended complexes of facts and events, can be mastered if we think of them as (possibly partly unknown) finite discrete systems that for specific known parts are bound by specific laws of temporal concatenation. Hence the laws of theoretical logic, including the principle of excluded middle, are applicable to these objects and mechanisms in relation to the respective complexes of facts and events, even though here a complete empirical corroboration of the inferences drawn is usually materially excluded a priori and there cannot be any question of even a partial corroboration in the case of (juridical and other) inferences about the past.
Note his use of "testability", "natural phenomenon" and "empirical corroboration." So the source of truth is nature by way of empiricism, and that demands finitism. Even his reasoning about the continuum was finitist: no determination on order/separation can be made after examining a finite prefix of the decimal expansion of a real number (see ibid §2). If he were alive today, I have little doubt he would have been an ultra-finitist -- not any constructivist! -- because, as it turns out, there is no empirical justification (even in principle) to accept inifinite induction. The very arguments he uses to reject LEM must also reject unbounded induction: it is not verified by nature.
(Here's what he says on induction:
> Here the principle of mathematical induction often furnishes the means of carrying out such tests without individual consideration of every element involved in the mapping or of every possible way in which the mapping can be performed; consequently the test even for systems with a very large number of elements can at times be performed relatively rapidly.
After the discovery of computational complexity he would have had no choice but to be an ultra-finitist.)
As to the notion of truth, I completely agree, but here Alan Turing came up with a completely different perspective. Whereas both Brouwer and Russel were looking for Truth in mathematics (and Hilbert, too, although he was content to Truth in the contentual "real propositions" and the finitist rules of inferene), Turing rejected that notion altogether. To him, mathematics was a means whose intrinsic truth is irrelevant. It is valuable inasmuch as it is useful, not because it is true (see https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf).
Brouwer's analysis of the continuum depends heavily upon the notion of a "free choice sequence" (aka a lawless sequence). The idea is that a creating subject -- i.e., you or me -- is free to make an unbounded sequence of choices to produce a sequence. At any finite time, you can only have made a finite number of arbitrary choices, but if you wait long enough you can make any number of arbitrary choices. Because these choices are arbitrary, free choice sequences cannot be described as being generated by any finite rule.
This is a constructive process, if you imagine (for example) generating a lawless sequence by throwing dice or from the clicks of a Geiger counter. But it's not a finitist one, because there is no finite data from which a choice sequence can be computed. This let Brouwer retain the idea that a mathematician can only have considered a finite amount of information at any point, without having to make any identification of the real numbers with computable functions.
In terms of complexity, there's an interesting analogy between choice sequences and the question of whether randomization gives you extra power -- the Miller-Rabin primality test lends immense force to the intuition that RP is stronger than P, but we might be centuries from proving it.
Even if we set aside randomness, though, an ultra-finitist/complexity-aware-logic is something that basically every logician I've ever talked to has agreed should exist, except we basically don't know how to do it. It's something that pretty clearly demands more creative insight than technical grunt, and unfortunately imaginative leaps don't come on demand. :/
What is essential to his philosophy is that the only justification for the axioms can come from nature by way of empiricism, and is therefore finite. If you accept Russel's, Brouwer's and Hilbert's belief that mathematics contains Truth, and if you then accept Brouwer's belief that the only source of truth is nature by way of empiricism, you have no choice today but to reject both LEM and induction. It is perfectly fine to work in constructive mathematics, and, in the Turingian sense it is of value, but it is no longer justified by Brouwer's philosophy of mathematical truth. Brouwer would have had to reject today's constructive mathematics on the same grounds he rejected classical mathematics: its axioms are unjustified by nature and empirical observation, even in principle. In fact, I don't think there is any philosophy of mathematics that could distinguish between constructivism and classical mathematics on any reasonable philosophical grounds today.
I would say that Brouwer's philosophy is (with today's knowledge) constructivist and ultra-finitist. BTW, Brouwer was not opposed to formalism as much as he was to logicism, and he even tried to propose a way to reconcile the two ("Intuitionistic reflections on formalism", 1927).
This identification is precisely what choice sequences are used to rule out. If a sequence is genuinely arbitrary, then you cannot describe it up front with a finite amount of data and a finite rule for updating that data. Instead, you have to imagine a mathematician adding a new axiom at each time step about the next element of a choice sequence, and requiring that any constructions they do works uniformly regardless of what axioms may be chosen in the future.
In this picture, the total amount of axiomatic data is actually going up over time, and this is actually important for the results Brouwer proved. In particular, without the axioms for choice sequences, you cannot derive the strong counterexamples, because you need classically-false axioms to prove classically-false theorems (like the continuity of all real-valued functions).
But you don't need to rule them out -- Brouwer certainly didn't. He just wanted to rule out decidable sequences. It's the undecidability that's important to his result, not arbitrariness, and that's perfectly compatible with automata. He just didn't know about computational undecidability and thought that undecidability requires lawlessness, but it doesn't. In any event, he didn't think randomness violates finitism. That only finite systems can be the source of axioms has been a constant refrain of his. I see that according to Wikipedia's definition of Finitism, he would be a "classical finitist."
> In particular, without the axioms for choice sequences, you cannot derive the strong counterexamples, because you need classically-false axioms to prove classically-false theorems (like the continuity of all real-valued functions).
The continuity of all real-valued functions can be proven with just computable sequences because of undecidability; you just can't do it if computational undecidability hasn't been discovered yet. In fact, it doesn't even become quite "classically false", but can be "embedded" in classical mathematics by restricting the "all": all computable real functions are continuous is a classical theorem. AFAIK, all constructive theorems can be embedded in classical mathematics by restricting them to computable entities. Do you have an example of any result that relies on uncomputable sequences?
Undecidability is arbitrariness - to say that, for example, the axiom of choice is independent of ZF is the same thing as saying that there is a arbitrary choice[0] between ZF+C and ZF+!C. Similarly, the sequence[1] G(PA),G(PA+G(PA)),G(PA+G(PA)+G(PA+G(PA))),... requires (at least) one additional arbitrary bit per item.
0: not asserting anything about what makes that choice, though.
1: where G(X) is the Godel sentence, roughly "X cannot cannot prove G(X)"
The definition in the article is the one put forth by Frege, perhaps the man most responsible for launching the debate about formalism into the wider philosophical community.
It seems okay to me for an informal article to define formalism in the same way (certainly the game aspect of it is the thing that ties the various schools of formalism together).
But the formalism he presented and argued against (and the version held by its defenders of the day) is clearly the form described in the article and the discussions he sparked later all circled around the same.
Frege quotes Heine as
> Suppose I am not satisfied to have nothing but positive rational numbers. I do not answer the question, What is a number?, by defining number conceptually, say by introducing irrationals as limits whose existence is presupposed. I define from the standpoint of the pure formalist and call certain tangible signs numbers.
and Thomae
> The formal conception of arithmetic accepts more modest limitations than does the logical conception. It does not ask what numbers are and what they do, but rather what is demanded of them in arithmetic. For the formalist, arithmetic is a game with signs, which are called empty. That means they have no other content (in the calculating game) than they are assigned by their behavior with respect to certain rules of combination (rules of the game).
within the Grundgesetze der Arithmetik.
And indeed Frege defines the position he is arguing against as
> Arithmetic is concerned only with the rules governing the manipulation of the arithmetical signs, not, however, with the denotation of the signs
These are from Max Black's translation of the Grundgesetze der Arithmetik in his three part series "Frege Against the Formalists." These quotes are from part 1 in The Philosophical Review, Vol. 59, No. 1 (Jan., 1950), pp. 79-93
¬ ∀ (P Q : Prop), (P → Q) → (¬P → ¬Q)
Computability: Turing, Gödel, Church, and Beyond. B. Jack Copeland, Carl J. Posy, Oron Shagrir (2013) MIT Press
Description:
In the 1930s a series of seminal works published by Alan Turing, Kurt Gödel, Alonzo Church, and others established the theoretical basis for computability. This work, advancing precise characterizations of effective, algorithmic computability, was the culmination of intensive investigations into the foundations of mathematics. In the decades since, the theory of computability has moved to the center of discussions in philosophy, computer science, and cognitive science. In this volume, distinguished computer scientists, mathematicians, logicians, and philosophers consider the conceptual foundations of computability in light of our modern understanding. Some chapters focus on the pioneering work by Turing, Gödel, and Church, including the Church-Turing thesis and Gödel's response to Church's and Turing's proposals. Other chapters cover more recent technical developments, including computability over the reals, Gödel's influence on mathematical logic and on recursion theory and the impact of work by Turing and Emil Post on our theoretical understanding of online and interactive computing; and others relate computability and complexity to issues in the philosophy of mind, the philosophy of science, and the philosophy of mathematics.
What Gödel apparently missed (although it's hard to tell without going over his writings carefully), is that humans, by the same criterion, can't "solve" mathematical problems. This is essentially a re-statement of the halting problem (undecidability).
You can't expect to go to the best mathematician in the world (o.c. that's not a thing, but say for example Terry Tao), give him an arbitrary problem and expect the problem to be solved within a fixed time. Or even some arbitrary but finite time (even if he had infinite scratch paper). If he had an obligation to solve the problem (within an axiomatic basis), there could be problems that go unsolved. Any mathematician knows this -- there's no guarantee the Riemann hypothesis will be resolved -- it could be within a year, within a century, or never.
It's very attractive to think we have some kind of higher powers (that transcend ordinary matter, or computers, or w.e.), but we do not and mysticism is not necessary to explain our abilities.
Can anybody give an example of mathematics that mathematicians consider “true”, but which is not provable in ZFC?
If no such mathematics exist, then mathematics is essentially just a game of symbol manipulation, right?
mic drop/Halmos block
For example, if O is the type of the ordinals, then
O
Boolean // type of all functions from ordinals into type Boolean
Does it only mean that ZFC is consistent when subsumed within a strongly-typed higher order theory, or does it mean that ZFC by itself is consistent?
Which is a "stronger" theory than ZFC; but you can also prove ZFC consistent in a system consisting of ZFC plus the axiom that "ZFC is consistent"; or indeed, in weaker theories than ZFC, augmented with the axiom that "ZFC is consistent".
It does sound a bit like you want something out of formal systems that they just can't give you, which is "absolute" truth.
edited to add: It's also worth noting that very, very few mathematicians care about actually formalising proofs in a formal system - it's a niche area. The vast majority of mathematicians go on about their business without giving much thought to ZFC and its axioms at all.
Many can't even name them all. (I know this, because they are quite surprised when you tell them what some of the axioms are. Especially the Axiom of Infinity.) Lol, I probably can't either,I suspect I would miss a few if I did it off the top of my head.
I don’t think I want more from formal systems than they can offer. I definitely don’t think of truth as “absolute”.
I think it’s actually the opposite: I’m skeptical of the “absolute” and almost mystical truth that some mathematicians seem to ascribe to mathematics. Do you believe in it? :)
If so, why should I believe that? What’s the evidence?
The theory Ordinals has a convincing proof of consistency because the theory has a provably unique up to isomorphism model. Consequently, ZFC must also be consistent because it is a special case of the theory Ordinals.
(Nope.)
Which suggests the following solution : limit our endeavors to that part of mathematics that CAN be automatically proven (and drill down infinitely into details thereof). And stub off the rest with good-enough axioms (aka holy doctrine).
Crazytalk? Well it's basically how we as a culture handle pretty much everything, epistemologically (and ontologically) speaking.
It could be very efficient. It could be a dystopian nightmare.
I appreciate your response!
Of course from a slightly different POV there are plenty of practical implications, since e.g. unsolvability of the Halting problem can be viewed as a close variant of Gödel's results.
Of course, following the critiques and further revisions of Zermelo’s set theory by Fraenkel, Skolem, Hilbert and von Neumann, a young mathematician by the name of Kurt Gödel in 1930 published a paper which would effectively end von Neumann’s efforts in formalist set theory, and indeed Hilbert’s formalist program altogether, his theorem of incompleteness. von Neumann happened to be in the audience when Gödel first presented it [1]
[1] https://medium.com/cantors-paradise/the-unparalleled-genius-...
Thanks to Gödel we know that we might be not just stupid apes, but that some things are indeed undecidable (even if they must be true or false).
What does it mean 'even if they must be true or false'? What does truth and falsehood mean if you cannot in theory prove/disprove a proposition?
You are suggesting the existence of some sort of Platonic realm, where propositions have definite truth/falsehood values, while at the same time being inaccessible to us.
Yes, I know. I meant that their truth value is inaccessible. What I'm saying is that claiming 'some things are indeed undecidable (even if they must be true or false)' suggests the existence of a Platonic realm with an existing truth value.
If a proposition is undecidable, it makes no sense to talk about whether 'it actually is true/false', because truth/falsehood is attached to a proposition by virtue of proving/disproving the proposition.
The thing is, this isn't necessarily the case. "Proving/disproving" a proposition can only be done starting from a set of axioms that are independently thought of as "true". But if you think of, e.g. ZFC as true, you'll also think of Con(ZFC) as true, even though the statement of Con(ZFC) can't be proven from ZFC. Similarly for Con(Con(ZFC)) and many sorts of increasingly-complex "consistency" statements.
But Godel showed that there exist propositions for which neither can be proven.
⊢(Ψ or ~Ψ) (⊬Ψ) and (⊬~Ψ)This is a standard assumption by mathematicians.
For example, it is impossible in general to understand what an English sentence says, because that sentence may describe the operation of an arbitrary program, and understanding an arbitrary program is undecidable.
Another example, it is impossible to detect all variants of malicious programs, because that requires understanding what all programs do, which requires identifying whether an arbitrary program halts or not.
Yet another example, optimal machine learning is impossible, since that is based on Solomonoff induction, based on Kolmogorov complexity, which is uncomputable due to the halting problem.
And another off the top of my head, it is impossible to create a general program creating program, such that you give it a well defined specification and it spits out a program that meets the requirements, if the requirements are satisfiable, since that requires solving the halting problem.
Finally, humans, while not optimally satisfying all the above tasks, do quite a decent job at these tasks, which is surprising if humans themselves were some sort of algorithm. So, this strongly suggests the human mind is doing some operation beyond computation, which in turn would imply that human intelligence level AI is impossible in theory, and thus impossible in practice. Furthermore, if the human mind is indeed doing something uncomputable, this has technological implications that human in the loop computation approaches are inherently more powerful than computation alone, a vastly under researched concept, although arguably the secret to the success of most AI/ML/datamining companies these days, such as Google, Facebook, Amazon, and Palantir. And the software industry in general is proof of this concept that humans are program generating processes performing much better than the halting problem would lead one to expect if humans were indeed mere computation.
Anyways, a whole bunch of impossibility implications, which have the practical application of protecting your wallet from comp. sci. snake oil salesmen, and the intriguing possibility 'beyond computation' technology.
Whilst I agree with everything in your comment before this point, I don't agree with this.
There is a very big difference between almost achieving something and actually achieving it. For example, there exist algorithms which are able to determine whether a given program halts, for a large class of programs, or to give some probability that a program halts prior to some point, even if they are unable to solve the general halting problem. So you haven't really argued that humans are doing something computers can't do.
In addition, I take issue with your statement that humans "do quite a decent job at these tasks". On the face of it, I agree that yes, (when sufficiently motivated) (some) humans do indeed do a pretty good job of e.g. proving mathematical theorems and writing programs that halt when they should. Certainly better than the best computers we can build. But that "pretty good" is a _far_ cry from the optimality referenced in the theorems you've stated. And if you are using this "pretty good" to indicate that humans are better than any possible algorithm, that argument doesn't follow-through.
I think that human-level algorithms are in principle possible. They will have to incorporate a lot of probability and approximate results and the like, and likely will have something similar to "intuition" where the path from input to output is not clear, whether to human onlookers or to the algorithm itself (whatever that might mean). We already see hints of this today with our deep learning algorithms. Not to say that we are necessarily close to achieving this, or that we ever will, but on the other hand it might very well be just around the corner!
There is also a class of deciders that can decide for an infinitely large class, which cannot be decided computationally, yet is not complete. I'd say humans most likely fall in this class, since they far exceed anything we can do with the best algorithms we've dreamed up, yet also cannot solve everything.
Of course, you can always say there is a yet undiscovered algorithm to fill the gap between state of the art and human performance, but at some point that hypothesis is less well supported by the evidence than the uncomputable mind hypothesis, and I'd say we are well past that point.
If we track the capability of computation machines from binary adders through old-school chess AI, expert systems and robotics, to the neural networks playing Go, chess, Starcraft, DOTA, we see an ever expanding sphere of ability and influence - often exceeding what humans predicted was impossible for computers.
> Of course, you can always say there is a yet undiscovered algorithm to fill the gap between state of the art and human performance
This implies a kind of asymptotic approach towards human intelligence, that it's something we keep trying to approach but will never reach.
But beyond "filling the gap" I believe computers have the potential to shoot past us in ability. And if they do, I think it's going to be a pretty shocking experience, because I think the rate of increase in intelligence at that point is going to be bigger than we expect - there's no reason to believe the exact level of intelligence is a special border, objectively speaking.
To claim that the evidence so far supports the uncomputable mind hypothesis seems to me like if we had managed to build tiny motors which had been getting bigger and better each year, and then claiming that we would never be able to beat an elephant in strength because no motor up to that point had yet been able to do so. Yes, our metaphorical motors are still tiny, and yes, it takes other extra pieces of engineering beyond motors to actually push down a tree, and indeed it's possible we will perhaps never build a big enough machine. But to take each larger motor as somehow being evidence AGAINST us ever getting to that point is a strange viewpoint.
As it is, compare the amount of processing, space and energy humans have to expend to perform equivalent tasks to computers, and there is no comparison. Computers are extraordinary orders of magnitude inferior to human performance. The only reason there is the appearance of parity is because we are not looking at the back end of what it takes computers to accomplish these tasks.
It is like we flipped a coin to create the works of Shakespeare, and waited the many eons necessary for just the right sequence to occur. We then say a coin is just as capable as Shakespeare, but that's only because we've ignored how much effort it took to flip the coin vs how much effort it took Shakespeare.
So, I'm not arguing our motors will not become bigger. I'm arguing that as our motors become bigger, the returns are diminishing exponentially, much more rapidly than can get us to true human parity.
Your greater than mere computation mind can makes huge bucks solving any problem since it can see if a program halts. Lets factor out some large primes and crack RSA. Just make a program that would halt if the answer is less than a certain value, then do binary search. A bit tedious, but surely huge piles of money are motivating. I'd do it myself but my mind seems to be malfunctioning.
Basically this is just a silly claim which is a shame because the first half of your response was pretty good.
And you might be correct that a human in the loop approach could crack RSA better than algorithmic approach, I've given it a shot in the past. There was a slight correlation of better answers with human involvement. Not entirely unexpected since our method of generating RSA primes has to be computable in a tractable time frame, so there is probably some exploitable regularity in the generation scheme that a super computational process could assist in identifying.
I am not sure that I agree with this. Of course if you can solve the halting problem, then you can decide some propositions. Like you have two Turing machines, one that enumerates proofs and the other that enumerates counterexamples, and they stop after finding the first one. Prove that one or them halts and you have decided the proposition.
On the other hand, there are "highly undecidable" problems which you cannot solve even if you had an oracle for the halting problem.
Using Orders on propositions, the construction of Gödel’s proposition I'mUnprovable is blocked because the mapping Ψ↦⊬Ψ has no fixed point because ⊬Ψ has order one greater than the order of Ψ since Ψ is a propositional variable.