Kurt Gödel and the Mechanization of Mathematics

https://www.the-tls.co.uk/articles/kurt-godel-incompleteness-theorems/

by vo2maxer • 7 years ago

155 132 7 years ago

the-tls.co.uk

are there any practical impacts (direct or indirect) of these results?

zozbot2343• 7 years ago

Not really. Gödel's theorem only proved that the specific kind of "mechanization of mathematics" that's implied by Hilbert's program as originally devised is impossible. The wiki has a nice section on varieties of Hilbert's program after Gödel https://en.wikipedia.org/wiki/Hilbert%27s_program#Hilbert%27... , citing (Zach, 2006) https://arxiv.org/abs/math/0508572

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.

mikorym• 7 years ago

Yes. Because of Gödel, von Neumann and others stopped trying to build machines that can prove anything.

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

mar77i• 7 years ago

For one practical example, Gödel's incompleteness is directly related to decidability problems in CS. there's this glorious liar paradox machine discussed by Computerphile [0].

[0] https://www.youtube.com/watch?v=macM_MtS_w4

chewxy• 7 years ago

There is one - a particular viewpoint on the Incompleteness Theorems imply that you cannot in general tell if a program encoded on a UTM will halt or not.

archi42• 7 years ago

You want to ask Hilbert ;-) Yes, there are. You/we can not programmatically derive all mathematical truths from ZFC ("the basic math axioms"). E.g. we recently had the Collatz Conjecture here on HN [1], and I strongly suspect that it can be neither proven nor falsified. Also, if one could solve the Halting Problem that would be quite useful.

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

[1] https://news.ycombinator.com/item?id=21780068

zozbot2343• 7 years ago

Specifically, "mathematical truths" here meams statements that, while logically independent from ZFC, are not independent from e.g. ZFC plus Con(ZFC). Or Con(Con(ZFC)), or Con(for any n, Con^n(ZFC)), or even more elaborate varieties. AIUI, part of what Recursion theory does is characterize these "true" consistency statements. The field is closely related to, e.g. halting oracles in TCS.

Yajirobe2• 7 years ago

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.

yters6• 7 years ago

The computer theory version of Godel's result is the halting problem, and that is applicable all over the place, in the same way that physical conservation laws imply a large variety of invention are impossible.

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.

pure-awesome2• 7 years ago

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.

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!

nohat• 7 years ago

You argue that because it is impossible for an algorithm to do some tasks perfectly, and humans can do "quite a decent job at these tasks," thus human minds are doing something beyond computation. Firstly this just doesn't logically follow. Perfection is completely different from "okay." Secondly it's far from clear that humans do any better than machines on many of these tasks, which would imply the opposite according to your argument.

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.

chithanh• 7 years ago

The computer theory version of Godel's result is the halting problem

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.

pron7• 7 years ago

formalism: the idea that mathematics can be reconstructed in a content-free manner, or more strongly put, that mathematics itself is nothing but “a formal game of symbols”.

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

neel_k3• 7 years ago

Brouwer was absolutely not a finitist! Indeed, he completely rejected the idea that you could use formal logic to bound what mathematics could talk about.

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.

pron7• 7 years ago

Hey Neel! Brouwer was a finitist in the sense that he did not accept infinitist axioms. His epistemology indeed was one of "mathematicians become able to assert mathematical truths as they engage in the process of constructing mathematical objects," but the justification was empiricism. I.e., his concept of establishing truth was by empirical, and therefore finitist. Here he is in "On the significance of the excluded middle in mathematics", 1923 (in Heijenoort):

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

dwohnitmok2• 7 years ago

Hilbertian formalism is only one particular brand of formalism.

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

pron7• 7 years ago

Frege started Logicism, so I don't think he would say that mathematical sentences lack content. Where are you getting this?

alimw• 7 years ago

Note that if a system is inconsistent then everything is provable, thus if a system is consistent there must be a proposition which cannot be proved.

¬ ∀ (P Q : Prop), (P → Q) → (¬P → ¬Q)

rocqua• 7 years ago

The First Incompleteness Theorem tells us that assuming PA is consistent, one can formulate propositions that cannot be proved (nor disproved) on the basis of PA, but which are nevertheless true.

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.

xamuel3• 7 years ago

There is an objective definition of truth in any particular model. For any particular model M of, say, Peano arithmetic, there is an objective, unambiguous, perfectly well-defined notion of truth in that model (of course, the definition of truth cannot itself be formalized within the model).

strbean3• 7 years ago

There is an objective definition of truth in any particular model.

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

pfortuny• 7 years ago

What Gödel does is the following: he constructs a sequence of symbols which is not decidable (i.e. there is no “proof” of it or of its negation).

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.

S_O_M_M_S• 7 years ago

Question for you. The first part...how does he ‘construct a sequence of symbols which is not decidable’ to begin with?

alentist2• 7 years ago

It's a rather big philosophical stance to say that the 'truth' of these propositions can be determined outside of the axiomatic systems.

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.

im3w1l• 7 years ago

I'm not 100% sure this perspective works, but could one take the position that this is because of a disconnect between model and reality?

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?

morelisp3• 7 years ago

Philosophical arguments aside, Gödel himself was absolutely, even evangelically, a mathematical realist. He believed any meaningful statement about mathematics had an objective truth value, axiomatic systems be damned.

https://plato.stanford.edu/entries/goedel/#GodRea

chrisshroba2• 7 years ago

What would be a good starting point to learn more about the topics described in this article? I felt like I understood the gist, but a lot of things went over my head.

munificent• 7 years ago

Douglas Hofstadter's "Gödel, Escher Bach" does a very slow gradual walk through Gödel's incompleteness theorem. If you can get into his writing style, it's a good way to really "get" the points.

chrisshroba2• 7 years ago

Thanks for the recommendation! I actually just picked it up off a friend's bookshelf yesterday and it's next on my list of books to read.

I appreciate your response!

mathgenius• 7 years ago

Chaitin's "meta math" is also a good read. Less arduous than G.E.B.

ProfHewitt27• 7 years ago

Chaitin made the very good point that inferential undecidability (incompleteness) is too important a result to depend on the triviality of the existence of the proposition I'mUnprovable. Fortunately, inferential undecidability of strongly-typed theories can be proved without using the nonexistent I'mUnprovable.

libraryofbabel3• 7 years ago

One of the most interesting things about Gödel's Incompleteness theorem must surely be how _little_ effect it has had on the day to day practice of mathematical research. It's one of the most profound mathematical results in the last 100 years, and yet outside foundational fields like axiomatic set theory (Cohen's work on the Continuum Hypothesis comes to mind) it's quite possible to completely ignore the existence of undecideable statements. Gödel's work had a deep impact on mathematicians' _philosophical_ views of what they do, but that didn't carry down into the actual day to day business of proving theorems.

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.

cscurmudgeon3• 7 years ago

https://en.m.wikipedia.org/wiki/Goodstein%27s_theorem

Not provable in Peano Arithmetic.

https://en.m.wikipedia.org/wiki/Continuum_hypothesis

Not provable in ZFC.

There are a few more.

ProfHewitt27• 7 years ago

Goodstein's theorem is easily provable in the [Dedekind 1888] theory of the Natural Numbers.

Cohen's incompleteness results do not hold for a theory of sets that axiomatizes sets up to a unique isomorphism. See the following:

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3457802

6gvONxR4sf7o• 7 years ago

I don't think it's too surprising. Mathematicians aren't in the business of searching around for all true theorems. They work on problems of interest. It seems much more likely that you fail to progress for all the usual reasons (it's hard) rather than because it's undecidable.

It's like the halting problem. It doesn't prevent programmers from automating stuff and reasoning about programs.

libraryofbabel3• 7 years ago

Yes and no. The analogy with the halting problem is a good one, and I completely agree that mathematicians are guided by what's interesting, not just by enumerating propositions. But they also advance many conjectures that are considered interesting open propositions to prove or disprove. Very very few of these interesting conjectures have turned out to be undecidable (the Continuum Hypothesis being, again, a notable special exception). And I guess that's my point: it's a curious fact that undecidability and "interestingness" don't seem to intersect very much, as far as we can tell. I don't think that's something that self-evidently had to be the case, but it's where we are after close on 100 years of living with what Gödel showed us.

Iv• 7 years ago

(total novice question here) Isn't it that because you can approach these mathematical questions from a variety of axiomatic systems?

kasmura• 7 years ago

I am not much of an expert either, but as I understand it Zermelo-Frankel set theory is the most common foundation of mathematics and it is stronger than Peano arithmetic so I think Gödel's results hold in general.

yters6• 7 years ago

Just like the conservation of energy has little effect on day to day practice of physics, besides blocking off an entire unbounded fruitless field of research into free energy.

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.

cjfd• 7 years ago

Actually, conservation of energy has enormous effect on the day-to-day practice of physics.....

currymj2• 7 years ago

AI has a ton of impossibility results. the "no free lunch theorems" are probably the best known. people now actively think in terms of designing assumptions, priors, or inductive biases to make their systems work better on the data they actually care about, because there's typically no solution that is always superior without tradeoffs.

https://en.wikipedia.org/wiki/No_free_lunch_in_search_and_op...

ProfHewitt27• 7 years ago

With respect to Intelligent Systems, there are two important theoretical results.

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:

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3428114

empath75• 7 years ago

it's quite possible to completely ignore the existence of undecideable statements.

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.

libraryofbabel3• 7 years ago

there are whole classes of problems that are no longer being worked on because they're impossible to solve.

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?

morelisp3• 7 years ago

One of the most interesting things about Gödel's Incompleteness theorem must surely be how _little_ effect it has had on the day to day practice of mathematical research.

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!

ProfHewitt27• 7 years ago

It is quite easy to prove consistent the theory ZFC and even a much powerful theory of the ordinals. See the following:

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3457802

haecceity• 7 years ago

Just like problem of induction didn't stop scientists from doing science?

currymj2• 7 years ago

i have noticed that to get day-to-day mathematical work done of any kind, you basically have to at least pretend to be a mathematical Platonist. the mathematical objects are things "out there" to be discovered or manipulated. everybody seems to do this, whatever their professed philosophical views on math.

whatshisface• 7 years ago

The undecidability of the halting problem is directly related to the existence of undecidable statements, and several important problems are uncomputable. (The word problem for groups, for example.)

ProfHewitt27• 7 years ago

Actually, because of the nonexistence of Gödel’s proposition I'mUnprovable in strongly-typed theories, the computational undecidability of the halting problem can be used to prove inferential undecidability (incompleteness).

deepnet• 7 years ago

I would counter that Gödel's Incompleteness theorem has had the greatest effect on the practice of mathematics by inventing digital computing which has revoltionised mathematics - all as a side effect of Turing and Church's proofs of Gödel's theorem.

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.

DantesKite• 7 years ago

Stephen Wolfram has an interesting article about Gödel and the implications of his work for the 21st century.

https://writings.stephenwolfram.com/2006/05/kurt-godels-100t...

lisper• 7 years ago

It's possible that P=NP? is undecidable.

noname120• 7 years ago

Yes! And 4 out of the 79 theorists from this survey[1] think that it is.

[1] https://www.cs.umd.edu/~gasarch/papers/poll.pdf#page=3

8bitsrule• 7 years ago

I don't think Heisenberg's 'uncertainty principle' has had much impact on day-to-day physics either. But the idea of built-in limitations may have helped to make the humiliation of mere probabilities more palatable. As did the idea that the observer is part of the equation.

"What we observe is not nature itself, but nature exposed to our method of questioning ."

ProfHewitt27• 7 years ago

Physical indeterminacy is extremely important in modern day many-core computation because of essential reliance on arbiters with physical indeterminacy. The following for an axiomatization:

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3459566

lioeters• 7 years ago

Along these lines, a book I've seen recommended here:

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.

ProfHewitt27• 7 years ago

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. Consequently, some other way had to be devised to prove inferential incompleteness without using Gödel’s proposition I'mUnprovable. A complication is that theorems of strongly-typed theories of the natural numbers and computation are not computationally enumerable because there are uncountable instances of the induction axiom in each theory. However, proof checking is computationally decidable :-) The complication can be overcome using special cases of induction axioms to prove inferential incompleteness of the theories. See the following:

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3418003

swayvil• 7 years ago

One way of describing the Incompleteness Theorems (1931) of the Austrian logician Kurt Gödel is to say that he proved, in the form of a mathematical theorem, that the possibility of a fully automated mathematics can never be realized.

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.

bjornsing9• 7 years ago

I always get a feeling articles like the OP (and there seem to be many) are pushing some kind of mysticism instead of clearly explaining...

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?

fipso_act7• 7 years ago

Sure. Most mathematicians think it's true that ZFC is consistent; but that can't be proved in ZFC.

mic drop/Halmos block

ProfHewitt27• 7 years ago

However, the consistency of ZFC can be proved in strongly-typed higher-order theories that subsume ZFC.

bjornsing9• 7 years ago

Most mathematicians probably think the Riemann conjecture is true, but that wasn’t what I meant. I should probably have said “consider proven”.

ProfHewitt27• 7 years ago

Mathematicians consider that there are "true" propositions of the form procedure P on input x does not halt but the propositions are not provable in ZFC.

bjornsing9• 7 years ago

Sure, such statements exist. But would a mathematician consider one of them true without a proof of some sort?

(Nope.)

neonate• 7 years ago

http://archive.md/iyvzm

darkmighty• 7 years ago

One way of describing the Incompleteness Theorems (1931) of the Austrian logician Kurt Gödel is to say that he proved, in the form of a mathematical theorem, that the possibility of a fully automated mathematics can never be realized

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.

calf• 7 years ago

Yeah I was confused by that and maybe the article could have clarified this in relation to the Church-Turing thesis.

manifestsilence• 7 years ago

Yeah, that's a lot of Hofstadter's thesis in Godel, Escher, Bach. In his long, rambling way, he eventually gets into the subtle differences between the different formulations of the Church-Turing thesis and argues that all consciousness is the same kind of epiphenomenon as a computer and thus subject to the same rules.

aey• 7 years ago

It’s an open question if it is decidable to show that P=NP problem is decidable :). We may live in a universe where undecidable problems exist and it may not ever be possible no show that they are undecidable. Which imho is kind of beautiful. Even if we live in a simulation it is so incomprehensible that it might as well be God to us.

Kurt Gödel and the Mechanization of Mathematics

Related Stories