How is Gödel's incompleteness theorem interpreted in intuitionistic logic? - Philosophy Stack Exchange most recent 30 from philosophy.stackexchange.com 2019-08-22T13:55:35Z https://philosophy.stackexchange.com/feeds/question/7194 http://www.creativecommons.org/licenses/by-sa/3.0/rdf https://philosophy.stackexchange.com/q/7194 28 How is Gödel's incompleteness theorem interpreted in intuitionistic logic? Mozibur Ullah https://philosophy.stackexchange.com/users/933 2013-06-07T16:30:20Z 2016-09-16T23:37:50Z <p>Classically, one sets up an axiomatic system with a formal deduction system &amp; an interpretation in a model. Generally it is <em>sound</em>, that is: a formally deduced theorem is also true when interpreted in the model. The reverse is called completeness, if a sentence in the model is true then it is also formally deducible. This is the statement of <a href="http://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem">Godels completeness Theorem</a>.</p> <p>Confusingly <a href="http://en.wikipedia.org/wiki/G%F6del%27s_incompleteness_theorems#First_incompleteness_theorem">Gödel Incompleteness Theorem</a> refers to the notion of decidability (this is distinct to the notion of decidability in computation theory aka Turing machines and the like) - a statement being decidable when we are able to determine (decide) that it has either a proof or a disproof. If all statements in the language are decidable we call it complete. The theorem says that axiomatic systems containing PA is incomplete - that is there are always statements which we cannot find a proof or a disproof. </p> <p>Now, what happens if the formal deduction system is not classical but intuitionistic? <a href="http://en.wikipedia.org/wiki/Intuitionistic_logic">Intuitionistic logic</a> is many-valued but rather than modelling truth one models constructability/provability, which instead of using set theory semantics uses Kripke semantics. Now:</p> <ol> <li><p>Is it still <em>sound</em>? That is: a formally deduced theorem is also constructible?</p></li> <li><p>Is it <em>incomplete</em>? There is a constructible sentence that is not formally deducible?</p></li> <li><p>Does it have undecidable statements? </p></li> </ol> https://philosophy.stackexchange.com/questions/7194/how-is-g%c3%b6dels-incompleteness-theorem-interpreted-in-intuitionistic-logic/7195#7195 15 Answer by Dennis for How is Gödel's incompleteness theorem interpreted in intuitionistic logic? Dennis https://philosophy.stackexchange.com/users/2297 2013-06-07T19:23:29Z 2013-06-07T21:17:08Z <p>The common axiom systems for intuitionistic logic are both <em>sound</em> and <em>complete</em>. It is interpretable as an S4 <a href="http://en.wikipedia.org/wiki/Modal_logic">modal logic</a> or as a weakening of <a href="http://en.wikipedia.org/wiki/Classical_logic">classical logic</a> (essentially you just drop the <a href="http://en.wikipedia.org/wiki/Law_of_excluded_middle">law of excluded middle</a> and <a href="http://en.wikipedia.org/wiki/Double_negative_elimination">double negation elimination</a> and then tweak the quantifier rules).</p> <p>Since it is both sound and <em>complete</em> it is <em>not</em> incomplete. The fact that they treat "truth" as something like "provability" does not bear on the situation.</p> <p>Now, is intuitionistic logic incomplete? No, but neither is classical <a href="http://en.wikipedia.org/wiki/First-order_logic">first order logic</a> and incompleteness tends to come with <em>stronger</em> logical systems than FOL, not weaker ones.</p> <p>The question I imagine you have in mind (though I apologize for presuming to be able to read your thoughts) is whether intuitionistic/constructive <em>mathematics</em> is susceptible to incompleteness. The answer here is yes. Gödel gave the proofs in a constructively/intuitionistically acceptable manner (i.e., using only inferences they endorse) and so the result would hold for intuitionistic number theory.</p> <p>It is worth noting that you don't need an arithmetic as strong as PA to fall prey to incompleteness. All that is required is a number theory which is recursively axiomatizable.</p> <p><a href="http://en.wikipedia.org/wiki/Robinson_arithmetic">Robinson arithmetic (Q)</a> is a theory much weaker than PA (I believe it is PA without induction) but incompleteness still arises. It might be (can't remember exactly) the weakest system still prey to the incompleteness theorems. It was actually designed to be such a weak system--- a system which can represent all and only recursive number-theoretic functions.</p> <p><a href="http://www.logika.umk.pl/llp/06/fp.pdf">Here</a> is an interesting article I found on the topic--- looks like a good read. <a href="http://courses.umass.edu/phil513-klement/ln4.pdf">These lecture notes</a> (again from Kevin Klement) do quite a good job of walking through Gödel's theorems if you want that. Otherwise the <a href="http://plato.stanford.edu/entries/logic-intuitionistic/">SEP entry</a> @commando linked to should be helpful as well.</p> https://philosophy.stackexchange.com/questions/7194/how-is-g%c3%b6dels-incompleteness-theorem-interpreted-in-intuitionistic-logic/8825#8825 6 Answer by Mauro ALLEGRANZA for How is Gödel's incompleteness theorem interpreted in intuitionistic logic? Mauro ALLEGRANZA https://philosophy.stackexchange.com/users/4752 2013-11-28T16:06:36Z 2016-09-15T22:46:09Z <p>The two notions (completeness and incompleteness) are not opposites but very much connected (not only by Godel's name in the name of the two theorems).</p> <p>Do take into account that Godel's Completeness Th of First-Order Logic is :<br> if a sentence is <strong>true in all the models</strong> of the axioms (i.e. it is a logical consequence of the axioms) then it is also formally deducible (in FOL) by the axioms. </p> <p>Godel's Incompleteness Th is relative to formal systems containing "a certain amount" of arithmetic (for example : Robinson Arithmetic, that is weaker than Peano's) and says that we can find in an effective way a statement expressible in those formal systems that is "true" in the intended model (i.e. the model with domain the standard numbers and operation the standard addition and multiplication) but not deducible from the axioms.</p> <p>This does not contradict the Completeness Th : the aforesaid statement is true in the standard model but is <strong>NOT</strong> true in some other "strange" model (there are many): this is the reason it is not deducible from the said axioms.</p> <p>The arithmetical statement constructed by Godel in his proof is quite "strange", but starting from a result of Paris &amp; Harrington (1977) has been possible, in mathematical logic, to find statements that are true (in the standard model) but not provable in Peano arithmetic and are more "natural". This was the first "natural" example of a true statement about the integers that could be stated in the language of arithmetic, but not proved in Peano Arithmetic.</p> https://philosophy.stackexchange.com/questions/7194/how-is-g%c3%b6dels-incompleteness-theorem-interpreted-in-intuitionistic-logic/26859#26859 0 Answer by Nikos M. for How is Gödel's incompleteness theorem interpreted in intuitionistic logic? Nikos M. https://philosophy.stackexchange.com/users/14508 2015-09-02T22:33:51Z 2015-09-02T22:33:51Z <p>reproduced from <a href="https://math.stackexchange.com/a/1418923/139391">https://math.stackexchange.com/a/1418923/139391</a></p> <p><strong>NOTE1</strong> Intuitionistic logic is <strong>NOT</strong> many-valued! (and in fact Goedel's name is again related to investigations in this direction)</p> <blockquote> <p>Are the Godel's incompleteness theorems valid for both classical and intuitionistic logic?</p> </blockquote> <p>In a sense YES.</p> <p><strong>BUT</strong></p> <ol> <li><p>Goedel's incompleteness theorem(s) apply first to <em>classical logic</em></p></li> <li><p>Goedel's incompleteness theorem and its proof is <em>constructive</em> but <em>not intuitionisticaly constructive</em> (<a href="http://www.research.ibm.com/people/h/hirzel/papers/canon00-goedel.pdf" rel="nofollow noreferrer">Goedel's paper</a>)</p></li> </ol> <p>Why?</p> <p>Goedel himself stated in his paper that the above procedure is "<em>constructively non-objectionable</em>", however </p> <p>a) Goedel's reference to contructivism (intuitionism), is rather formal than actual (more detailed below)</p> <p>b) variations of LEM (law of excluded middle) are used throughout Godel's proof</p> <p>c) combined with the use of a diagonalisation procedure</p> <p>(see also <a href="http://www.jamesrmeyer.com/ffgit/intuitionism.html" rel="nofollow noreferrer"><em>Gödel’s Proof and Intuitionism</em></a> for another analysis)</p> <blockquote> <p>Does this apply the same to intuitionistic logic?</p> </blockquote> <p>In a sense YES.</p> <p><strong>BUT</strong></p> <ol> <li>Goedel's <strong>negative translation</strong> of <em>classical logic</em> into <em>intuitionistic logic</em> is only formal (<a href="http://www.csl.sri.com/papers/cade92-ns/cade92-ns.ps" rel="nofollow noreferrer">Goedel's paper</a>)</li> </ol> <p>Why?</p> <p>a) negative translation of classical logic to intuitionistic logic <strong>is not intuitionism</strong>, rather a <em>formal analogy</em>, because the semantics of what constitutes a construction, a proof, implication and of course the definition/construction of new entities based only on previously constructed entities is totally different, being <em>classical than intuitionistic</em> (and same holds for the original incompleteness proof, where these conditions are neither formalised nor met) (see also <a href="http://homepages.inf.ed.ac.uk/jmckinna/kolmogorov-1932.pdf" rel="nofollow noreferrer">Kolmogorov's Interpretation of Intuitionistic Logic as Problems</a>)</p> <p>b) intuitionism has, in a sense, already embedded the incompletenmess theorems as it accepts statetements which can neither be proved nor refuted (at a certain given time)</p> <p>c) Brouwer himself foresaw Goedel's results by a decade at least (note: Goedel himself had attended Brouwer's lectures on the foundations of mathematics)</p> <p>Quoting from <a href="http://www.cs.cornell.edu/Info/People/artemov/spinoza.ps" rel="nofollow noreferrer">Artemov's Understanding Constructive Sematics (Spinoza Lecture)</a></p> <p><a href="https://i.stack.imgur.com/HFzuK.png" rel="nofollow noreferrer"><img src="https://i.stack.imgur.com/HFzuK.png" alt="enter image description here"></a></p> <p>And also from <a href="http://www.math.nsc.ru/conference/malmeet/13/Artemov.pdf" rel="nofollow noreferrer">here</a></p> <blockquote> <p><strong>Intuitionistic vs. Classical Perspective</strong></p> <p><strong>Intuitionists</strong> normally base their formal systems on intuition of constructive, e.g., <strong>BHK-style</strong> informal semantics, rather then on classical foundations...</p> <p><strong>Classical mathematicians</strong> (such as Gödel, Kolmogorov, Kleene, Novikov, and others) seek a rigorous</p> <p><strong>classical definition of the constructive semantics.</strong></p> </blockquote> <p>In the light of the above Goedel's incompleteness results <strong>do indeed hold for intuitionistic logic in a formal way (with classical semantics) but not for intuitionism</strong> (which in any case does not need any incompleteness result as they are already embedded in the practice and semantics)</p>