<story><title>Kurt Gödel and the Mechanization of Mathematics</title><url>https://www.the-tls.co.uk/articles/kurt-godel-incompleteness-theorems/</url></story><parent_chain></parent_chain><comment><author>libraryofbabel</author><text>One of the most interesting things about Gödel&amp;#x27;s Incompleteness theorem must surely be how _little_ effect it has had on the day to day practice of mathematical research. It&amp;#x27;s one of the most profound mathematical results in the last 100 years, and yet outside foundational fields like axiomatic set theory (Cohen&amp;#x27;s work on the Continuum Hypothesis comes to mind) it&amp;#x27;s quite possible to completely ignore the existence of undecideable statements. Gödel&amp;#x27;s work had a deep impact on mathematicians&amp;#x27; _philosophical_ views of what they do, but that didn&amp;#x27;t carry down into the actual day to day business of proving theorems.&lt;p&gt;Isn&amp;#x27;t that strange? Wouldn&amp;#x27;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&amp;#x27;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&amp;#x27;s last theorem 30 years ago). If we did find a first-rank conjecture in number theory or some other area that&amp;#x27;s undecidable in ZFC (or whatever system) then we would at last be stepping through the door that Gödel opened for us.</text></comment>
<story><title>Kurt Gödel and the Mechanization of Mathematics</title><url>https://www.the-tls.co.uk/articles/kurt-godel-incompleteness-theorems/</url></story><parent_chain></parent_chain><comment><author>rocqua</author><text>&amp;gt; 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.&lt;p&gt;As far as I know, that last clause was never a claim made by Godel. Specifically the claim that these propositions are &lt;i&gt;nevertheless true&lt;/i&gt;. 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.&lt;p&gt;Indeed, (again AFAIK) godel&amp;#x27;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 &amp;#x27;nevertheless true&amp;#x27; actually hides a lot of complexity.
Because there are philosophical positions in which these independent propositions are neither true not false.&lt;p&gt;And really, this is why we call them independent. The truthiness of these propositions is not determined by their axiom systems. It&amp;#x27;s a rather big philosophical stance to say that the &amp;#x27;truth&amp;#x27; 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.</text></comment>