[HN Gopher] Godel's first incompleteness theorem - an interactiv...
___________________________________________________________________
Godel's first incompleteness theorem - an interactive tutorial
Author : jamesfisher
Score : 250 points
Date : 2022-10-17 17:00 UTC (5 hours ago)
(HTM) web link (tigyog.app)
(TXT) w3m dump (tigyog.app)
| chatterhead wrote:
| One 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 wrote:
| Rather Borgesian I think.
| krunck wrote:
| The 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.
| hashmush wrote:
| Proof of... proof?
| Euphorbium wrote:
| You 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 wrote:
| Most 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.
| zaik wrote:
| It'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 wrote:
| The 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.
| dvt wrote:
| This 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.
| [deleted]
| philip-b wrote:
| I 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 wrote:
| He 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.
| MatthiasPortzel wrote:
| > But we haven't proved that what Lean thinks about that had
| anything to do with whether it actually halts or not.
|
| Well I can tell you if it actually halts: it does. By the time
| of the heat-death of the universe, all computers will have
| stopped running, so the halting problem is quite solvable.
|
| But the halting problem, and the Collatz conjecture, and all
| mathematical truth, is fundamentally embedded inside of systems
| of formal logic. Godel's Incompleteness Theorem doesn't say
| anything about systems of truth outside of formal mathematical
| logic. So this result isn't relevant to Physics, for example.
|
| However, Godel's Theorem, and this proof, don't rely on any
| particular qualities of the formal system, other than the
| ability to enumerate proofs (and other things that we think of
| as inherit to logic). So this proof applies not just to Lean,
| but also to every method of proving things in math.
| tybug wrote:
| > 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 wrote:
| You 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 wrote:
| I 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 wrote:
| You 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).
| oehtXRwMkIs wrote:
| "mike-drop" should be "mic-drop"
| [deleted]
| [deleted]
| fsckboy wrote:
| I 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 wrote:
| _mike 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.
| MrsPeaches wrote:
| Never come across TigYog. Seems pretty cool: https://tigyog.app/
| adamnemecek wrote:
| I'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
|
| I have been thinking about some of this stuff
|
| https://github.com/adamnemecek/adjoint
|
| Join the discord https://discord.gg/mr9TAhpyBW
| perryizgr8 wrote:
| > 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?
| plus wrote:
| If 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 wrote:
| Trying 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
| caiquelira wrote:
| It 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
| aljgz wrote:
| A math prof had a brilliant blog and one of the subjects he
| covered was Godel'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-go...
|
| https://infinityplusonemath.wordpress.com/2017/08/04/godels-...
|
| https://infinityplusonemath.wordpress.com/2017/09/04/how-god...
| timcavel wrote:
| auggierose wrote:
| > Will the string "(n : nat) : 0 + n = n" appear in this list?
|
| No, because the given alphabet does not contain the space
| character ...
| jamesfisher wrote:
| Thank you for your precise eyes! Fixed!
| auggierose wrote:
| Great 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 wrote:
| Yes, this is in the definition of theorems().
| evnp wrote:
| Similar nit, when you ask "Will theorems() discover `theorem
| halting_problem (n) : ! computable_pred (l c, ..."
|
| I don't believe it will since `const alphabet` does not
| contain l or !. Apart from my very slight indignance after
| answering that one incorrectly, loved the article! :)
| chaosite wrote:
| Using 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
| koyanisqatsi wrote:
| One 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 wrote:
| Well 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 wrote:
| It says something more than that. There are necessarily
| infinitely many programs like that.
| fspeech wrote:
| Even 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.
| alexmolas wrote:
| I 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!
| V__ wrote:
| I 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 wrote:
| Formal 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__ wrote:
| Is 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 wrote:
| It 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__ wrote:
| Ah, 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 wrote:
| Yes, paraconsistent logic could be considered an instance
| of such a system:
| https://en.wikipedia.org/wiki/Paraconsistent_logic.
| dvt wrote:
| Cool 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).
|
| > Godel'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.
| lisper wrote:
| > the Halting Problem brings with it a lot of stuff
|
| Not really. The idea of a Turing Machine brings with it a lot
| of stuff, but nowadays Turing Machines are a dime a dozen, and
| the idea of a "program" is common place. So proving the non-
| computability of the halting problem is pretty easy [1]:
|
| Assume that there exists a program H that solves the halting
| problem, that is, H takes two input parameters, a program P and
| an input I and returns true if P halts when run on input I,
| false otherwise.
|
| Construct a program B that does the following: B accepts as
| input a program P and computes H(P,P), that is, it calls H as a
| subroutine to determine if program P halts when run on a copy
| of itself as the input. If the result from H is true then B
| enters an infinite loop, otherwise B halts (that is, B does the
| opposite of what P would do when run on a copy of itself).
|
| Now consider what happens if we run B on a copy of itself. B
| will halt iff H(B,B) is false. But H(B,B) is false iff B
| doesn't halt, which is a contradiction. Therefore, our
| assumption is false, and H is impossible. QED.
|
| ---
|
| [1] Taken from https://flownet.com/ron/chaitin.html
| dvt wrote:
| > nowadays Turing Machines are a dime a dozen, and the idea
| of a "program" is common place
|
| I think you may have misconstrued what I meant. From a
| metamathematical standpoint, leveraging the Halting Problem
| gives you a lot of stuff for free. Just the fact that we're
| assuming that a formal logic system and a programming
| language are isomorphic is actually a pretty huge deal and
| those developments span several generations of logicians.
|
| Specifically, Godel numbering really originally made this
| entire thing work. And that sausage was not very intuitively-
| made.
| lisper wrote:
| > leveraging the Halting Problem gives you a lot of stuff
| for free.
|
| Not exactly for free. You still have to prove the non-
| computability of the halting problem. But I get your
| meaning.
|
| > Just the fact that we're assuming that a formal logic
| system and a programming language are isomorphic is
| actually a pretty huge deal and those developments span
| several generations of logicians.
|
| Sure, but that is no different from any technological
| advance. Arabic numerals were a major breakthrough when
| they were first invented. Nowadays it is pretty safe to
| take them for granted in most cases.
|
| > Godel numbering really originally made this entire thing
| work.
|
| Sure, but that was only necessary because Godel didn't know
| about ASCII. Proving Godel's theorem using Godel numbers is
| kind of like writing a C compiler as a state table for a
| Turing Machine. You could do it, but no one in their right
| mind would except perhaps as an intellectual exercise.
|
| The history of how technological innovations came about is
| very different, and usually much more difficult, than the
| way one can re-invent those innovations with the benefit of
| hindsight.
| Tainnor wrote:
| Godel numbering is chosen because numbers are very easy
| to reason about and mathematicians like that things are
| provable from simple principles like arithmetic, and
| because for Godel's theorem to actually work on theories
| of arithmetic the encodings of formulas have to be
| numbers.
|
| Of course, you can choose some other encoding scheme -
| one that is easier for humans to read, such as the binary
| encoding of a nicely formatted string - but that's not as
| directly amenable to a rigorous mathematical proof. In
| particular, you technically have to prove that that
| encoding scheme doesn't lead to ambiguities, i.e. every
| string has (at most) a unique parsing. That may seem (and
| is) obvious, but technically does require a proof,
| something you can avoid when you just use Godel numbering
| via the fundamental theorem of arithmetic instead
|
| But Godel numbering is not really the bread and butter of
| the proof. The more technically relevant part about
| Godel's proofs that doesn't just readily follow from the
| halting problem is the fact that incompleteness of first-
| order theories has only very weak conditions - Robinson
| arithmetic is already sufficient.
|
| You have to prove that Robinson arithmetic is strong
| enough to express every primitive recursive function and
| that requires some mathematical tricks.
| lisper wrote:
| > because for Godel's theorem to actually work on
| theories of arithmetic the encodings of formulas have to
| be numbers
|
| ASCII codes are numbers.
|
| > but that's not as directly amenable to a rigorous
| mathematical proof
|
| Why not?
|
| > you technically have to prove that that encoding scheme
| doesn't lead to ambiguities,
|
| ASCII is unambiguous. In fact, the only difference
| between ASCII and Godel numbers is that ASCII encodes
| strings as powers of 256 whereas Godel numbers encode
| strings as powers of prime numbers.
|
| > i.e. every string has (at most) a unique parsing
|
| Huh? That makes no sense. Did you mean that every
| _number_ has a unique mapping to a string? Because ASCII
| certainly meets that requirement.
|
| > The more technically relevant part about Godel's proofs
| that doesn't just readily follow from the halting problem
| is the fact that incompleteness of first-order theories
| has only very weak conditions - Robinson arithmetic is
| already sufficient.
|
| Why does that matter? This seems to me like an
| interesting bit of trivia about Robinson arithmetic, but
| I don't see why this matters to the main point. Any
| system _less_ powerful than PA is trivially incomplete.
| lapcat wrote:
| > 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.
|
| I remember having to do it for my logic class final exam. I
| wouldn't remember exactly how to do it today though.
|
| The little click sounds on the linked page are unfortunate. I
| had to stop after like 20 seconds.
| Grothendank wrote:
| IMO 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
| whimsicalism wrote:
| If 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
| [deleted]
| miga wrote:
| The 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
|
| 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?
___________________________________________________________________
(page generated 2022-10-17 23:00 UTC)