13 ms·

Kurt Gödel and the Mechanization of Mathematics

155 points by vo2maxer 7y ago

pron 7y 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_k 7y 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.
  - pron 7y 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 https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf).
- dwohnitmok 7y 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).
  - pron 7y ago
    Frege started Logicism, so I don't think he would say that mathematical sentences lack content. Where are you getting this?
    - dwohnitmok 7y ago
      Frege was certainly arguing against formalism; he was the one responsible for taking its defenders to task. 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
dajohnson89 7y ago
are there any practical impacts (direct or indirect) of these results?
- archi42 7y 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 https://news.ycombinator.com/item?id=21780068
  - zozbot234 7y 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.
    - ProfHewitt 7y ago
      True propositions of sets are those that hold in the up to unique isomorphism model of the theory Ordinals defined here: https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3457802 https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3457802
  - Yajirobe 7y 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.
alimw 7y 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 7y 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.
- xamuel 7y 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).
  - strbean 7y 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.
chrisshroba 7y 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 7y 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.
  - chrisshroba 7y 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 7y ago
  Chaitin's "meta math" is also a good read. Less arduous than G.E.B.
  - ProfHewitt 7y 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.
libraryofbabel 7y 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.
- cscurmudgeon 7y ago
  https://en.m.wikipedia.org/wiki/Goodstein%27s_theorem https://en.m.wikipedia.org/wiki/Goodstein%27s_theorem Not provable in Peano Arithmetic. https://en.m.wikipedia.org/wiki/Continuum_hypothesis https://en.m.wikipedia.org/wiki/Continuum_hypothesis Not provable in ZFC. There are a few more.
  - ProfHewitt 7y 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 https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3457802
    - cscurmudgeon 7y ago
      But the thing is you are just trading off computability. Aren't you? > The theory Ordinals is algorithmically inexhaustible
bjornsing 7y 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_act 7y ago
  Sure. Most mathematicians think it's true that ZFC is consistent; but that can't be proved in ZFC. mic drop/Halmos block
  - ProfHewitt 7y ago
    However, the consistency of ZFC can be proved in strongly-typed higher-order theories that subsume ZFC.
    - fipso_act 7y ago
      why are you telling me this
      - ProfHewitt 7y ago
        Mistake is often made that ZFC is the be-all and end-all ultimate foundation of mathematics. Unfortunately, 1st-order ZFC (often referred to as just "ZFC") is a very weak theory. For example, if O is the type of the ordinals, then O Boolean // type of all functions from ordinals into type Boolean cannot be represented in ZFC because it does not exist in the cumulative hierarchy of sets.
        fipso_act 7y ago
        No, I mean, why me, specifically? Did I accidentally say something to give the impression I find your odd rantings interesting? Because if I did, please let me know so I can correct the misunderstanding.
lioeters 7y 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.
- ProfHewitt 7y 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 https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3418003
swayvil 7y 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.
neonate 7y ago
http://archive.md/iyvzm http://archive.md/iyvzm
darkmighty 7y 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 7y ago
  Yeah I was confused by that and maybe the article could have clarified this in relation to the Church-Turing thesis.
- manifestsilence 7y 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 7y 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.

155 points by vo2maxer 7y ago

pron 7y 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_k 7y 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.
- pron 7y 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 https://mdetlefsen.nd.edu/assets/201037/jf.turing.pdf).
dwohnitmok 7y 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).
- pron 7y ago
  Frege started Logicism, so I don't think he would say that mathematical sentences lack content. Where are you getting this?
  - dwohnitmok 7y ago
    Frege was certainly arguing against formalism; he was the one responsible for taking its defenders to task. 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

dajohnson89 7y ago

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

archi42 7y 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 https://news.ycombinator.com/item?id=21780068
- zozbot234 7y 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.
  - ProfHewitt 7y ago
    True propositions of sets are those that hold in the up to unique isomorphism model of the theory Ordinals defined here: https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3457802 https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3457802
- Yajirobe 7y 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.

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

xamuel 7y 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).
- strbean 7y 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.

chrisshroba 7y 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 7y 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.
- chrisshroba 7y 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 7y ago
Chaitin's "meta math" is also a good read. Less arduous than G.E.B.
- ProfHewitt 7y 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.

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

cscurmudgeon 7y ago
https://en.m.wikipedia.org/wiki/Goodstein%27s_theorem https://en.m.wikipedia.org/wiki/Goodstein%27s_theorem Not provable in Peano Arithmetic. https://en.m.wikipedia.org/wiki/Continuum_hypothesis https://en.m.wikipedia.org/wiki/Continuum_hypothesis Not provable in ZFC. There are a few more.
- ProfHewitt 7y 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 https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3457802
  - cscurmudgeon 7y ago
    But the thing is you are just trading off computability. Aren't you? > The theory Ordinals is algorithmically inexhaustible

bjornsing 7y 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_act 7y ago
Sure. Most mathematicians think it's true that ZFC is consistent; but that can't be proved in ZFC. mic drop/Halmos block
- ProfHewitt 7y ago
  However, the consistency of ZFC can be proved in strongly-typed higher-order theories that subsume ZFC.
  - fipso_act 7y ago
    why are you telling me this
    - ProfHewitt 7y ago
      Mistake is often made that ZFC is the be-all and end-all ultimate foundation of mathematics. Unfortunately, 1st-order ZFC (often referred to as just "ZFC") is a very weak theory. For example, if O is the type of the ordinals, then O Boolean // type of all functions from ordinals into type Boolean cannot be represented in ZFC because it does not exist in the cumulative hierarchy of sets.
      - fipso_act 7y ago
        No, I mean, why me, specifically? Did I accidentally say something to give the impression I find your odd rantings interesting? Because if I did, please let me know so I can correct the misunderstanding.

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

ProfHewitt 7y 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 https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3418003

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

neonate 7y ago

http://archive.md/iyvzm http://archive.md/iyvzm

darkmighty 7y 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 7y ago
Yeah I was confused by that and maybe the article could have clarified this in relation to the Church-Turing thesis.
manifestsilence 7y 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 7y 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.