23 ms·
Gödel’s first incompleteness theorem – an interactive tutorial
- oehtXRwMkIs 4y ago"mike-drop" should be "mic-drop"
- deleted 4y ago[deleted]
- fsckboy 4y agoI don't object grammar fascism, and I see the visual beauty of "mic-drop", but mike as a shortened form of microphone is well-established. "The talk show guest was miked up and ready to go on stage." kind of like bicycle and bike
- pvg 4y agomike as a shortened form of microphone is well-established. mike is, sometimes, but 'mike drop' for 'mic drop', not so much. But for even more pedantry, that would be spelling rather than grammar pedantry.
- fsckboy 4y agowell if we are delving into pedantry, natural language is spoken; we learn our native language as pre-literate children and we already have our vocabulary stored in our brains with phonetic features way before we learn to read and write. Orthography is thus but a facsimile of our language. We exchange and learn new words primarily by hearing them, and I'll bet "drop the mike" was first uttered out loud by a comedian/entertainer type, and to say that it even had a spelling is an unjustified leap.
- pvg 4y agoI don't think any of these are true (that this particular argument constitutes or delves into pedantry, what 'natural language' is, etc) but we've probably extracted what pedantifun was to be had already.
- deleted 4y ago[deleted]
- miga 4y agoThe assumption of this theorem is that we may encode any problem that is unbounded and infinite. What if we limit ourselves to *bounded* and *computable* functions only? See draft presented at many top logic conferences yet: https://arxiv.org/abs/2106.13309 https://arxiv.org/abs/2106.13309 Since the observable universe is bounded, and we are most interested in computable, why not to focus on maths that is most relevant to our universe instead of infinitary alternate?
- krunck 4y agoThe section header "Theorem mining — better than crypto?" makes me wonder: instead of POW based cryptocurrencies, could we use POT(Proof of Theorem)? Machines could grind away looking for theorems. It's still a POW method, but it provides some potentially useful output.
- Euphorbium 4y agoYou have to know in advance about how long it will take to mine the next block. Is it possible to do it here? Probably not.
- miga 4y agoMost useful proof-of-work yet... However, it is somewhat hard to mathematically define all criteria used to recognize *useful* theorem. There may be many propositions that are true, but cause no excitement among mathematicians.
- dvt 4y agoThis wouldn't work because all theorems are trivially extensible. Either by adding extra theorems via conjunction, e.g. my new theorem C = previously-mined theorems {A} ∪ {B}; or by adding garbage to the end, e.g my new theorem C = {A} ∪ {...arbitrary nonsense that cancels out}, e.g. (+ 0 + 0 + 0), or (- 1 + 1 - 1 + 1), or vastly more complex formulations. Logic isn't the study of merely finding out what's true, but what's true and interesting.
- hashmush 4y agoProof of... proof?
- zaik 4y agoIt's only useful if the theorems proven are interesting. Maybe there could be a cryptocurrency for mathematicians where you post theorem statements and put money in them. First one to find a proof gets whatever money was in the theorem.
- remram 4y agoThe way blockchain works is that you generate a problem based on the contents of the block. If the proof you find is in no way related to a block it cannot be a cryptocurrency. You could make a system to reward people for finding proofs, but it would be more of a Bounty system or a Leaderboard than a cryptocurrency. Indeed people do put up prizes for those kind of things today.
- timcavel 4y ago
- philip-b 4y agoI think there's either a mistake or a very very large omission here. It starts here: >This is looking better! We have an amazing function, is_statement_true, that can tell us whether anything is true or false, given enough time! >Read it through, and try to prove to yourself that is_collatz_true really does eventually return the truth of the Collatz conjecture. Namely, I think the author confuses Lean theorems and metatheory theorems, where when I say metatheory, I mean the language and the system we use to talk about lean, about Godel's incompleteness theorem, and everything else - basically, the English-math language in which the chapter is written. Hence, it's wrong to say that is_statement_true can tell us whether any statement is true - it can merely tell us which of the two options it is: the statement is a theorem of Lean or its negation is a theorem of Lean. Same for is_collatz_true - sure, it must tell us what Lean thinks about the Collatz conjecture but doesn't tell us anything about the truth or falsity of the Collatz conjecture. And finally, in the very end of Chapter 2, this problem arises as well. The chapter says that if Lean is sound and complete, then we can define a function which, for any Turing machine, returns one of two options: Lean thinks it halts, or Lean thinks it doesn't halt. But we haven't proved that what Lean thinks about that had anything to do with whether it actually halts or not.
- auggierose 4y agoHe skips connecting it with model theory by choosing statements where it is clear what they mean (collatz conjecture, halting problem). I think that's OK.
- puffoflogic 4y agoIt's not clear to me that model theory has much to say about Lean; do you have any resources on this? plato.stanford.edu does hedge that while modern model theory focuses on first-order logic, there's a broader sense of model theory which can be used to study even natural languages. But if you try to study type theory as natural language statements you aren't going to get much out of it. Going about it that way, the models you'll come up with are going to be of the form "doing some formal symbol manipulation X has certain formal symbol results Y" which will be neither illuminating nor useful. I did find an abstract[0] which claims that model theory has historical roots in type theory but I'm doubtful I have any way to access it. [0] https://www.cambridge.org/core/journals/bulletin-of-symbolic-logic/article/abs/logic-in-the-1930s-type-theory-and-model-theory/05C644923AF4F0415ECEFB5F535F1B2A https://www.cambridge.org/core/journals/bulletin-of-symbolic...
- IngoBlechschmid 4y agoBy Gödel incompleteness, the fundamental axioms of mathematics actually don't quite pin down the world of mathematics the way we would perhaps like them to do. As a consequence (also a result by Gödel), there are actually many worlds of mathematics, each spelling out the basic notions of mathematics in slightly different ways. I tried to survey this multiverse philosophy here: https://iblech.gitlab.io/bb/multiverse.html https://iblech.gitlab.io/bb/multiverse.html
- LudwigNagasena 4y agoWhat are “the fundamental axioms of mathematics”?
- IngoBlechschmid 4y agoI am sorry, I was being sloppy there. There are several systems of axioms we can use to base mathematics on. A common such is ZFC, Zermaelo–Fraenkel set theory with the axiom of choice. Among its axioms are assertions like "there is a set which is empty", "there is an infinite set" and "if A and B, then in particular A". Another is Martin-Löf type theory in one of its flavors, perhaps homotopy type theory.
- raydiatian 4y agoI think you can explain incompleteness without forcing readers to learn a prooflang
- kuwoze 4y agoreturning null for false and the string itself for true, lol,
- gregfjohnson 4y agoIs the essential similarity of the key trick in Godel's incompleteness theorem and the Y combinator well known? I finally "got" the incompleteness theorem when that relationship dawned on me. As a cute entry point, consider the standard lambda term with no normal form, "(lambda x. (x x)) (lambda x. (x x))". Now consider the Godel formula "Substitute(F, n)", which takes a number F, the Godel number of a formula with a single free variable, and another number n. It simplifies to a number M which is the Godel number of the formula F with n replacing all instances of its free variable. One might interpret F as function-like, in the sense that for any number n, F [free_var := n] simplifies to some other number m. So now consider "Substitute(F, F)", which is suggestive of "(x x)" in lambda notation. Let M be the Godel number of this formula, which has one free variable. Finally, use an analogy to the above self-referential lambda term to create the formula G, defined as "Substitute(M, M)". To what number does this arithmetic formula with no free variables simplify? The delightful answer is that it simplifies to its own Godel number! Just as it is a short step from the above simple self-referential lambda term to the Y combinator, so it is a short step from the above fact to the standard Godel formula for which neither it nor its negation has a proof.
- auggierose 4y ago> Will the string "(n : nat) : 0 + n = n" appear in this list? No, because the given alphabet does not contain the space character ...
- jamesfisher 4y agoThank you for your precise eyes! Fixed!
- evnp 4y agoSimilar nit, when you ask "Will theorems() discover `theorem halting_problem (n) : ¬ computable_pred (λ c, ..." I don't believe it will since `const alphabet` does not contain λ or ¬. Apart from my very slight indignance after answering that one incorrectly, loved the article! :)
- auggierose 4y agoGreat tutorial, by the way! There is another typo in one of the javascript functions, where you should write "return t;" instead of "return thm;"
- martincmartin 4y agoYes, this is in the definition of theorems().
- dvt 4y agoCool page, though the Halting Problem brings with it a lot of stuff, so using it to prove Godel's first incompleteness theorem is (imo) a bit like cheating. I've proven it before using diagonalization on my blog (but also using concepts like computability for free). At the end of the day, using these ideas, you get the Curry–Howard correspondence for free (which, again, is a bit like cheating). > Gödel’s original proof was slightly stronger Technically speaking, a lot stronger. Proving Godel's first incompleteness theorem (don't even get me started on the second) from first principles is actually much more involved; and certainly more difficult to make it intelligible for non-logicians.
- whimsicalism 4y agoIf you've managed to prove the halting problem, then I don't think it is cheating to use it on an easier result. This is how it was taught when I learned CS theory in uni [0] [0]: https://introtcs.org/public/lec_09_godel.html https://introtcs.org/public/lec_09_godel.html
- ianai 4y agoFurther, there just isn’t “cheating” in a proof. Being able to do a demonstration yet another way just illuminates the phenomena all the better. You might know something if you know one way to do it. You have a much better understanding if you have two ways. Three and your understanding is probably pretty solid. Etc Edit of to if, damn autocorrect
- Grothendank 4y agoIMO It's cool to invoke the lean halting theorem, since the author proves the informal version of the halting theorem in the previous lesson. See: https://tigyog.app/d/fr9uub3hqgab/r/the-halting-problem https://tigyog.app/d/fr9uub3hqgab/r/the-halting-problem
- fithisux 4y agoWhere is your blog?
- 4y ago
- deleted 4y ago[deleted]
- tybug 4y ago> But the same reasoning can be applied to any formal system F, with fairly minimal assumptions: Strictly speaking, F has to be satisfiable/consistent as well. {P, ~P} is a trivially recursively enumerable, complete theory which contains Q.
- dvt 4y agoYou get this for free in (2). You couldn't "reason about programs" if F were inconsistent, nor would the halting problem make any sense in an inconsistent system.
- tybug 4y agoI would argue "reasoning about programs" formally means "can prove P Q R ..." (with appropriate choices for P Q R) and doesn't implicitly carry an assumption of consistency. But, fair enough.
- dvt 4y agoYou make a good point, and on the other hand you're right that "reasoning about programs" is not a term of art, so who knows what it means. Given how Lean is used in the article, I took it as basically being some kind of Turing-complete language (lambda-calculus or some variant or what-not).
- adamnemecek 4y agoI’ve always thought that the completeness theorem was more interesting. Also I really like approaching this from Lawvere’s fixed point theorem. https://ncatlab.org/nlab/show/Lawvere's+fixed+point+theorem https://ncatlab.org/nlab/show/Lawvere's+fixed+point+theorem I have been thinking about some of this stuff https://github.com/adamnemecek/adjoint https://github.com/adamnemecek/adjoint Join the discord https://discord.gg/mr9TAhpyBW https://discord.gg/mr9TAhpyBW
- aljgz 4y agoA math prof had a brilliant blog and one of the subjects he covered was Gödel's incomepleteness theorems. I really loved his style (and his wife's illustrations). Too bad he stopped posting. https://infinityplusonemath.wordpress.com/2017/07/22/kurt-godels-story/ https://infinityplusonemath.wordpress.com/2017/07/22/kurt-go... https://infinityplusonemath.wordpress.com/2017/08/04/godels-incompleteness-theorems/ https://infinityplusonemath.wordpress.com/2017/08/04/godels-... https://infinityplusonemath.wordpress.com/2017/09/04/how-godel-proved-maths-inherent-limitations/ https://infinityplusonemath.wordpress.com/2017/09/04/how-god...
- V__ 4y agoI love the fact that it's interactive. Wish more articles were written that way. It was also relatively easy for me to follow up till "Consistency": > But what if theorems() contains both coll_conj and ¬coll_conj? Is that possible? > ... > But in general, a formal system can have both S and ¬S as theorems. Is there an intuitive explanation for this?
- tybug 4y agoFormal systems need not be consistent; if a formal system assumes both P and ~P as axioms, you can derive S and ~S (for any S) by explosion.
- V__ 4y agoIs the problem that you can't proof consistency? Because if it's consistent then shouldn't either P or ~P be true or the axiom doesn't exist?
- koyanisqatsi 4y agoIt is possible to prove consistency but to do so requires using a more powerful system of axioms which in turn might be inconsistent. What Goedel showed is that in any system that can encode arithmetic (and consequently some notion of computation, e.g. lambda calculus) can not be complete if it is consistent.
- V__ 4y agoAh, thank you, that makes more sense. Maybe a weird follow-up question: Is it possible (or does it make sense) to find a proof in an inconsistent system and to try to "transform" it into a consistent one?
- koyanisqatsi 4y agoYes, paraconsistent logic could be considered an instance of such a system: https://en.wikipedia.org/wiki/Paraconsistent_logic https://en.wikipedia.org/wiki/Paraconsistent_logic.
- perryizgr8 4y ago> So, even though 1+1=3 is surely false, we could prove it in Lean like so: “Let’s assume that ¬(1+1=3). But this leads to a contradiction: coll_conj and ¬coll_conj. We can therefore deduce that our assumption must be false, so 1+1=3.” I was following along with the logic, but got completely lost here. Can anyone explain how does the assumption "1 plus 1 is equal to three is false" lead to a contradiction? What is the contradiction here exactly?
- caiquelira 4y agoIt doesn't lead to a contradiction, the contradiction was already there. If you have a contradiction on your system you can prove everything: 1- Assume ¬X 2- Point out the contradiction 3- Therefore X is true
- aristofun 4y agoHow and why does a specific contradiction "coll_conj and ¬coll_conj" apply to all possible conjectures?
- plus 4y agoIf your system of logic contains a contradiction, then it can be said that any statement in that system "leads to" a contradiction. Thus "proof by contradiction" can prove any statement in that system.
- miga 4y agoTrying to find a formal system that encodes unbounded infinitary mathematical objects including most of maths, but yet to require that all statements are decidable within a finite number of steps... Is it contradiction in the proof, or rather a contradiction in assumptions? More on logic that permits all that *Bounded* Turing Machine does: https://arxiv.org/abs/2106.13309 https://arxiv.org/abs/2106.13309
- aristofun 4y ago> then it can be said that any statement in that system "leads to" a contradiction Why exactly it "leads to"? I don't get it. Why system can't have a contradiciton for one set of inputs, and not have it for others?
- koyanisqatsi 4y agoOne way to think of incompleteness/halting is that the future is not computable. Meaning that to see the result of some symbolic/computational process you have to actually run the program and there is no shortcut to making a prediction one way or the other if we want to know for certain what the result would actually be. There is something called abstract interpretation that can tell you what the result of some computation will be but by necessity it can only be an approximation because it must halt in some finite amount of time. Type systems are a good example of abstract interpretation because type systems assign a logical/mathematical semantics to code and allow one to determine in a finite amount of time whether some code is logically coherent according to the rules of the type system. The larger philosophical implication of all this is that symbolic/computational models of reality are always approximations. Whatever one can know for certain has either already happened and is in the past or there is some symbolic model/approximation which must necessarily have some degree of uncertainty and error. The tutorial itself is pretty cool. Props to the author for putting it together.
- oulipo 4y agoWell the correct statement would be "to know the result of ANY computational process, in some cases you would have to run it". For instance, there are many "simple programs" for which you can give the results by way of formal methods without running them. The incompleteness theorem says that there will exist one program for which you can't.
- occamrazor 4y agoIt says something more than that. There are necessarily infinitely many programs like that.
- fspeech 4y agoEven if you can predict halting (which for the large class of decidable problems you can) you still have to run the computation to see the results. To me it's more about the expressiveness of languages.
- MrsPeaches 4y agoNever come across TigYog. Seems pretty cool: https://tigyog.app/ https://tigyog.app/
- james-bcn 4y agoYes. There must be a Javascript framework for creating this type of interactive training. Does anyone know of one?
- jamesfisher 4y agoHi! TigYog.app actually started out as an attempt at building something like a JS framework for this. But it's evolved into a platform. Here are some reasons why ... - The "gradually revealed content" flow tends to require full control over the page. See by contrast https://quantum.country/ https://quantum.country/ which uses https://withorbit.com/ https://withorbit.com/, which is more like a framework. For that reason, it's quite restricted in what it can do in terms of flow control. - Tracking progress - you can just save answers client-side, but I wanted something that would allow users to sign on their mobile and continue from wherever they were on the desktop, etc. This also enables flashcard-style spaced repetition emails (future feature) - Saving answers while being able to edit the page requires that you have stable identifiers for all questions and buttons. The WYSIWYG does that for you. - I wanted it to feel like blogging, or traditional writing, rather than coding. All that said - I'm thinking about ways to open up TigYog for more like framework-style creation. Email me if you're interested!
- chaosite 4y agoUsing the halting problem here shows the consequences of the incompleteness theorem pretty well, but I don't think it explains it. This is basically hiding the self-references behind the halting problem black box. I really like this video for explaining it, I find it very funny and approachable: https://www.youtube.com/watch?v=WylL1m4K6Bk https://www.youtube.com/watch?v=WylL1m4K6Bk
- chatterhead 4y agoOne is the only number. Zero isn't one. n cannot equal anything other than n; adding anything else is what's creating the inconsistency and incompleteness. n must equal n. But, if that's true - which it is - the game is over and math is just a game of never ending bifurcations.
- dwringer 4y agoRather Borgesian I think.
- alexmolas 4y agoI know this proof is not as rigorous as some mathematicians would like, but it helped me a lot to understand a concept that I've failed to understand all my life, at least at an intuitive level. So thank you very much for sharing!