[HN Gopher] 1931: Kurt Godel shows limits of math, logic, comput...
___________________________________________________________________
1931: Kurt Godel shows limits of math, logic, computing, AI
Author : hardmaru
Score : 267 points
Date : 2021-06-17 07:20 UTC (15 hours ago)
(HTM) web link (people.idsia.ch)
(TXT) w3m dump (people.idsia.ch)
| warmfuzzykitten wrote:
| I don't understand how Godel showed limits of AI, or even
| addressed AI in its modern incarnation, which has little to do
| with logic. Perhaps some more knowledgeable reader can elucidate?
| YeGoblynQueenne wrote:
| Without getting too technical, if AI must run on a computer,
| and there are programs that computers cannot compute, then
| there are limits to what AI can compute, or in other words
| _think_ (because it 's an AI; so to think, it computes).
|
| As a very crude example of this kind of limitation, I'm sure
| I've read a hundred Sci-Fi stories where the humans defeat the
| AI by posing to it an unsolvable problem, usually a variation
| of the "liar's paradox", e.g. "this statement is false" (which
| btw is used by Godel in his proof). So a human traipses over to
| the superintelligent AI and blurts "I always lie". Then the AI
| spends an aeon processing the sentence and then blows up.
|
| Even worse, intelligence itself may turn out to be an
| uncomputable program that cannot be executed on a computer. In
| that case- no AI.
| acuozzo wrote:
| If your AI uses a classical computer, then everything it's
| doing is reducible to the Boolean algebra of its component
| logic gates.
|
| All of the training you've done on the GPU; all of the
| coordination done by the CPU; everything... it's all one
| (absurdly long) boolean expression.
|
| Like all algebraic structures, Boolean algebra is built from an
| initial set of axioms. Under Godel's incompleteness theorem, it
| is therefore true that if Boolean algebra isn't inherently
| broken (inconsistent), then we can craft questions that cannot
| be answered using Boolean algebra alone, but this is all your
| classical computer is capable of doing!
|
| Now, if you're training AI using an analog system or a non-
| classical computer such as a quantum computer, then this opens
| up a totally different discussion.
| mseepgood wrote:
| (1931) This is old news.
| littlecranky67 wrote:
| Veritasium recently released a very good video that explains
| Godels incompletenes theorem such that even I could understand
| it: https://www.youtube.com/watch?v=HeQX2HjkcNo
| sillysaurusx wrote:
| In traditional HN style, I will now thumb my nose at
| Vertasium's excellent video due to him skipping over _how_
| godel came up with the proof.
|
| He built up the whole damn video for that one moment, when he
| says "And godel went through all this trouble to come up with
| this card..." and flips over the card. But _how_ godel did it
| is at least as cool as the proof itself.
|
| I'm mostly being tongue in cheek with the Veritasium nose-
| thumbing. But if you saw it and want to understand it more
| deeply (and in my opinion more satisfyingly), I recommend "What
| Godel Discovered":
| https://news.ycombinator.com/item?id=25115746
|
| It explains Godel's proof using Clojure. Quite accurately, too.
|
| The thread is also hilarious. Shoutout to the MIT professor who
| took offense at someone linking to his wikipedia page:
| "Wikipedia is contentious and often potentially libelous." ...
| and then you check his wikipedia page, and it's a super
| positive article about all of his discoveries and life's work.
| espadrine wrote:
| > _Shoutout to the MIT professor who took offense at someone
| linking to his wikipedia page [...] and it 's a super
| positive article about all of his discoveries and life's
| work._
|
| Carl Hewitt is no doubt a famed and accomplished professor,
| but why does nobody point out that he is claiming that
| Godel's proof is incorrect[0]?
|
| I already heard of his conviction that _"The Church /Turing
| Thesis is that a nondeterministic Turing Machine can perform
| any computation. [...] [T]he Thesis is false because there
| are digital computations that cannot be performed by a
| nondeterministic Turing machine."_[1]. (Which, to be fair, is
| a strongly related argument to the one that Godel was wrong.)
|
| I don't personally know whether he is right, and his
| digression about millions of people risking death as a result
| does not inspire confidence, but in my understanding, neither
| statement is widely accepted.
|
| [0] https://news.ycombinator.com/item?id=25160970
|
| [1]
| https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3603021
| myWindoonn wrote:
| I don't want to be a professional Hewitt debunker, but his
| stance has been ripped to shreds; at this point, he is
| _wrong_ about Direct Logic refuting Godel and Turing, and
| his ActorScript can 't be implemented on real machines.
| alecst wrote:
| I don't know anything about Hewitt or his stance, but I
| don't feel like this adds a whole lot to the
| conversation. I mean I can tell that you're sure that
| he's wrong, but why should the strength of your belief
| convince me?
|
| It would be helpful if you added some links or some
| explanation, or just anything beyond what you've written
| there.
| kaba0 wrote:
| It's similar to claiming someone made a perpetuum mobile
| -- extraordinary claims going against basically every
| mathematician/computer scientist since Godel require
| extraordinary evidence. And the result is quasi always
| that the one claiming, looked over some small but crucial
| detail.
| ProfHewitt wrote:
| Veritasium, et. al. overlooked the crucial aspect that
|
| orders on propositions play in maintaining the
| consistency
|
| of foundations.
|
| Neglecting to include the order of a proposition in in
| its
|
| Godel number makes it possible to mistakenly conclude
| that
|
| the proposition _I 'mUnprovable_ exists as a fixed point
| of a
|
| recursive definition.
|
| See the following for details:
|
| https://papers.ssrn.com/abstract=3603021
| espadrine wrote:
| Isn't the order of a proposition included in its Godel
| number?
|
| Each proposition is assigned to an increasing prime
| power, and the increasing list of primes has total order,
| such that swapping propositions yields a distinct Godel
| number.
| ProfHewitt wrote:
| [Godel 1931] encoded the characters of a proposition in
| its
|
| Godel number but did not include the order of the
| proposition.
| espadrine wrote:
| Could you provide two statements with equal Godel numbers
| but distinct proposition orders, and a detail of how you
| compute the Godel numbers?
| ProfHewitt wrote:
| If two propositions have the same characters, then they
| have the same Godel numbers.
| espadrine wrote:
| Could you provide two statements with equal Godel numbers
| and the same characters in different orders, and a detail
| of how you compute the Godel numbers?
| deadbeef57 wrote:
| I know of several computer verified proofs of the
| incompleteness theorem. See entry 6 of
| https://www.cs.ru.nl/~freek/100/ for a small catalogue.
| How does this relate to your objection? Are there bugs in
| the verifiers? Or did people verify the wrong theorem
| statement?
| ProfHewitt wrote:
| Proofs forgot to include order of proposition in its
| Godel number.
| deadbeef57 wrote:
| So you say that the computer verified proofs of the
| incompleteness theorem of verifying the wrong theorem?
| Because there can't be bugs in a computer verified proof.
|
| (Of course there _can_ theoretically be bugs in a
| computer verified proof. If there are bugs in the
| verifier. But if 4 independent proof assistants verify a
| proof of a theorem, this is extremely unlikely.)
| [deleted]
| mcguire wrote:
| " _...his ActorScript can 't be implemented on real
| machines._"
|
| I think I understand why, but could you provide some more
| details?
| joelbluminator wrote:
| Maybe he should try writing it in Elixir instead of
| ActorScript?
| weatherlight wrote:
| Hewitt argues that erlang/elixir/beam isn't the actor
| model because of how Erlang processes receive/process
| messages
|
| more here: https://www.erlang-solutions.com/blog/lets-
| talkconcurrency-p... and here:
| https://codesync.global/media/almost-actors-comparing-
| pony-l...
| [deleted]
| ProfHewitt wrote:
| Of course, Erlang can be accurately modeled using the
| theory of Actors.
|
| See discussion in Related Work section of the following
| article:
|
| https://papers.ssrn.com/abstract=3603021
| alisonkisk wrote:
| What's wrong with ActorScript? Does it have some kind of
| infinite-size features?
|
| More interesting facts:
|
| His Twitter account has been relatively recently deleted
|
| https://mobile.twitter.com/drcarlhewitt/status/3972794314
| 824...
|
| And his PhD advisor was Seymour Papert.
| ProfHewitt wrote:
| Twitter account is @ProfCarlHewitt and blog is
|
| https://professorhewitt.blogspot.com/
|
| See following for a simple ActorScript program that
| cannot be
|
| implemented using a Nondeterministic Turing Machine:
|
| https://papers.ssrn.com/abstract=3603021
| ProfHewitt wrote:
| myWindoonn: Do you have anything of actual substance to
|
| contribute to the the discussion?
| saurik wrote:
| That wikipedia article is edit-locked and if you look at its
| history it is, in fact, hilarious.
| ProfHewitt wrote:
| A fundamental problem with Wikipedia is that it doesn't have
|
| proper accountability for material that it publishes.
|
| Furthermore, Wikipedia is heavily censored by an anonymous
| group.
|
| See [von Plato 2018] on how Godel deceived von Neumann in
|
| developing one of his fundamental proofs in [Godel 1931].
| gpderetta wrote:
| for those that haven't clicked through, the MIT professor is
| none other than Carl Hewitt of actor model fame.
|
| I should post the wiki link so that we can have the whole
| discussion again :)
| Workaccount2 wrote:
| >Carl Hewitt of actor model fame
|
| I'll admit that threw me for a loop for a second.
| rottc0dd wrote:
| There is a little great book called "Godel's proof" by Nagel
| and Newman[1]. And definitely requires some focus but readable
| nevertheless.
|
| [1] https://www.amazon.com/G%C3%B6dels-Proof-Ernest-
| Nagel/dp/081...
|
| Edit : removed a line
| alok-g wrote:
| A good book as such. However, whereas the authors claim that
| they outline the proof in chapter 6, that chapter fell short
| of it with key aspects of the proof missing. Overall, I was
| disappointed.
| [deleted]
| ruste wrote:
| I second this! I spent a few days of summer vacation in
| highschool slowly working my way through this and it was mind
| expanding.
| chriswarbo wrote:
| I knew Godel's (first) incompleteness theorem pretty well
| already, but I really enjoyed how much that video managed to
| get across without getting _too_ bogged down.
|
| One thing I'd like to see in a companion video would be an
| explanation of _why_ Turing machines represent computation.
| That video (like many others) skims over the why, and only
| talks about what they can /can't do after we've already decided
| to use them.
|
| Turing's 1936 "On Computable Numbers" paper gives a nice
| _philosophical_ justification for his model, which (from my
| reading) boils down to the following:
|
| - Mathematicians can do their work within a finite volume of
| space (their brain, or a room, or the whole Earth if we want to
| be conservative). Also, they could (in principle) do their work
| using only written communication, on standard pieces of paper,
| each of which also has a finite volume.
|
| - Finite volumes can only have finitely-many distinguishable
| states (having infinitely many states would require them to be
| infinitesimally similar, and hence indistinguishable from each
| other within a finite amount of time)
|
| - Hence we can label every distinguishable state of a brain
| with a number; and likewise for every distinguishable piece of
| paper (at least in principle)
|
| - Since these are both finite, any mathematician's behaviour
| could (in principle) be completely described by a table
| detailing how one state (brain + paper) leads to another
|
| - Given such a table, the actual content of the states (e.g.
| the wavefunctions of particular protons, the electrical
| potential of particular synapses, the placement of ink
| molecules, etc.) is irrelevant for the behaviour; only the
| transitions from one numbered state to another matter
|
| - Hence we could (in principle) build a machine with the same
| number of states as one of these tables, and the same
| transitions between the states, and it would exactly reproduce
| the behaviour of the mathematician
|
| This is the philosophical justification for _why_ a (Turing)
| machine can calculate anything a human can (in fact, the same
| argument shows that a Turing machine can reproduce the
| behaviour of _any_ physical system).
|
| However, this is still a rather hand-wavey "in principle"
| thought experiment about unimaginably huge numbers. Turing
| managed to take it further.
|
| For simplicity we assume all the papers are arranged in a
| sequential "tape", we'll call the distinguishable states of the
| papers "symbols" and those of the mathematician/machine
| "states":
|
| - One thing a mathematician can do is read a tape with one of
| these tables written on it, followed by a sequence of numbers
| representing the symbols of another tape, and _emulate_ what
| the described machine would do when given the described tape
| (i.e. they could keep track of the current state and tape
| position, and look up the transitions in the table, to see what
| would happen)
|
| - Since a mathematician can emulate any given table (in
| principle), so can a machine. This would be a "universal
| machine", able to emulate any other. (The video talks about
| such a machine, in the proof that the halting problem is
| undecidable)
|
| So the question becomes: how unfathomably complicated would
| such a universal machine have to be?
|
| - These transition tables and tapes can be very big, and may
| contain very large numbers, but we can _write them down_ using
| only a small alphabet of symbols, e.g. "start table", "new
| row", "the digit 7", etc.
|
| - Reading a sequence of such symbols, and emulating the
| described machine, can get tricky. Turing described a universal
| machine "U", but he did so in a rather indirect way, which also
| turned out to have some mistakes and glaring inefficiencies.
| Davies later worked through these and ended up with an explicit
| machine using only 147 states and 295 symbols.
|
| Hence we can use a machine with only a few hundred states to
| exactly reproduce the behaviour of _any_ mathematician (or any
| physical system), as long as it 's given an appropriate
| description (i.e. "software"). Later work has found universal
| Turing machines with only 4 states and 6 symbols.
|
| One reason Turing's _justification_ for his model is important,
| rather than just proposing the model and seeing what happens
| (like in the video), is that Alonzo Church had _already_
| proposed a model of computation (called Lambda Calculus), but
| didn 't have such a justification.
|
| Godel himself _dismissed_ Lambda Calculus, proposing his own
| system (General Recursive Functions) as a better alternative.
| When Church proved they were equivalent, Godel took that as
| reason to _dismiss his own system too_! Yet Turing 's argument
| _did_ convince Godel that a fundamental limit on computation
| had been found. Turing proved his machines are also equivalent
| to Lambda Calculus, and hence General Recursive Functions; so
| _all_ of these proposed models turned out to be 'correct', but
| it was only Turing who could explain _why_.
|
| Personally I consider this reduction of physical behaviour to
| transition tables and then to machines, to be the main reason
| to care about Turing machines. Proving the undecidability of
| the halting problem was also a great achievement of Turing's
| 1936 paper (as shown in that video), but that can also be
| explained (I would argue more easily) using other systems like
| Lambda Calculus.
|
| _Without_ Turing 's justification of his model, undecidability
| comes across as simply a flaw. Sure Turing machines may be
| (distantly) related to our laptops and phones, but if we found
| a _better_ model without this 'undecidability bug' we could
| make _better_ laptops and phones! Turing 's argument shows that
| _there is no better model_ (just equivalents, like Lambda
| Calculus).
| ProfHewitt wrote:
| There are very simple digital computations that cannot be
|
| performed by a Nondeterministic Turing Machine.
|
| See the following for an example:
|
| https://papers.ssrn.com/abstract=3603021
| tsimionescu wrote:
| That would be a major revolution to the foundations of
| computer science if it were true, disproving the Church-
| Turing thesis. It seems unlikely that such a fundamental,
| world-shattering result would be so obscure, so I am much
| more likely to believe it is false.
| ProfHewitt wrote:
| Do you have any reasoning to back up your belief?
| tsimionescu wrote:
| As I said, if someone had convincingly proved this, it
| would shake the field to its core. Since that didn't
| happen, they can't have convincingly proven this.
| ProfHewitt wrote:
| Scientific progress does occur!
|
| Recent advances are compatible with a long tradition with
|
| contributions by Euclid, Dedekind, Frege, Russell,
| Church, Turing, von Neumann, etc.
|
| The following article is in furtherance of the long
| tradition:
|
| https://papers.ssrn.com/abstract=3603021
| jjgreen wrote:
| That's 7 times you've linked to that paper in this
| discussion, going for some kind of record?
| kaba0 wrote:
| With all due respect, it would be very hard for me to
| believe so. For the simplest case, one can trivially create
| a Turing machine that simulates a CPU, so I'm not sure the
| digital computation holds any water.
| ProfHewitt wrote:
| Issue is that a Turing Machine cannot communicate with
| other Turing Machines in the middle of a computation.
| kaba0 wrote:
| Let me rephrase: an n-core CPU can be simulated on a
| Turing machine with eg. time sharing -- effectively being
| able to simulate the Actor model.
| ProfHewitt wrote:
| Turing Machine can only do cooperative multiprogramming
| and cannot do time-interrupted scheduling.
| kaba0 wrote:
| Well, not _time_ -interrupted but there absolutely is a
| way to schedule n steps of each core, isn't there?
| Similarly to how the universal Turing machine is
| constructed, or how the nondeterministic TM is made
| deterministic.
| ProfHewitt wrote:
| Nondeterministic Turing Machine has only _bounded
|
| nondeterminism_. That is, for a given input a
| Nondeterministic
|
| Turing Machine can only explore the number of
| alternatives
|
| bounded by its input. Actors do not have the limitation.
| kaba0 wrote:
| So unbounded nondeterminism is basically
| hypercomputation? Then I assume one can write a program
| for the theoretical Actor model that computes a function
| on every natural number, is that right? Or that it can
| solve the halting problem for Turing machines, since if
| it is stronger then it, the halting problem of TMs is no
| longer true for them (is replaced by their own halting
| problem).
| ProfHewitt wrote:
| An Actor _cannot decide the halting problem for program
|
| expressions_. See proof in the following:
|
| https://papers.ssrn.com/abstract=3603021
| tsimionescu wrote:
| Does this difference still hold if time were discrete? I
| may be out of my depth, but it seems intuitive that if
| time were discrete, you could enumerate all possible
| interleavings of actors' actions, and reproduce their
| behaviors in a Turing machine.
| [deleted]
| oscardssmith wrote:
| This is just false. A Turing machine can emulate multiple
| Turing machines that communicate with each other.
| ProfHewitt wrote:
| Turing machine can _simulate_ multiple Turing Machines
| but _cannot implement multiple Turing Machines
| communicating with each other_ because there is no means
| to communicate.
| oscardssmith wrote:
| But since Turing machines can emulate multiple Turing
| machines, any problem that can be completed by multiple
| machines communicating can be solved by 1 Turing machine.
| As such, the computational power is exactly the same.
| ProfHewitt wrote:
| As said elsewhere in this posting:
|
| Nondeterministic Turing Machine has only bounded
|
| nondeterminism. That is, for a given input a
| Nondeterministic
|
| Turing Machine can only explore the number of
| alternatives
|
| bounded by its input. Actors do not have the limitation.
| dahjkol wrote:
| Don't need to em every 10th word.
| 0x0203 wrote:
| I know I'm pretty inept when it comes to this subject, but
| can someone help me understand how the first three points of
| Turing's philosophical justification listed above can be
| true? For example, in computing the sequence of n values of
| an infinite series or the first n digits of pi, how can the
| claim be made that this can be done in a finite amount of
| space or with a finite number of states?
| mensetmanusman wrote:
| It might be because pi isn't infinite in practice. E.g. we
| could use all the available energy in the universe and only
| calculate up to a finite digit (ignoring the information
| storage issue!).
|
| Whether the abstract infinite pi 'exists' is up for
| metaphysical debate :)
| chriswarbo wrote:
| Here is pi, written as a number to infinite precision
| (from http://davidbau.com/archives/2010/03/14/python_pipy
| _spigot.h... ): def
| pi_decimal_digits(): q, r, t, j = 1, 180, 60, 2
| while True: u, y = 3*(3*j+1)*(3*j+2),
| (q*(27*j-12)+5*r)//(5*t) yield y
| q, r, t, j = 10*q*j*(2*j-1), 10*u*(q*(5*j-2)+r-y*t), t*u,
| j+1
|
| If you mean that pi can't be written as a number to
| infinite precision _using place-value notation_ (as
| opposed to a more useful notation like Python) then I
| agree that only a finite prefix can ever be observed.
| mensetmanusman wrote:
| Also, pi = C/d
|
| in geometry notation :)
| mcguire wrote:
| Note that the Python version of pi requires an unbounded
| amount of memory and, more importantly, an infinite
| amount of time to produce pi to infinite precision.
| chriswarbo wrote:
| > Note that the Python version of pi requires an
| unbounded amount of memory
|
| Really? I measure it as exactly 200 bytes (not counting
| the 4-space indentation that HackerNews requires, and not
| including a trailing newline)
|
| > and, more importantly, an infinite amount of time to
| produce pi to infinite precision
|
| I can see it right now, with infinite precision. If it's
| taking an infinite amount of time to show up I'd contact
| your ISP ;)
| chriswarbo wrote:
| We're allowed an unlimited amount of paper, but each
| _piece_ has a finite size, and hence each _piece_ is in one
| of only finitely-many distinguishable states. Turing called
| these piece-of-paper-states "symbols", and arranged the
| pieces of paper in a "tape" of unlimited length (a stack of
| sheets, or a library of books would also work; but moving
| between the pieces would be more complicated).
|
| In fact, we only ever need 2 symbols, e.g. 0 and 1. This is
| because any set of symbols can be replaced by a set of
| numbers, and those numbers can be written in binary (with a
| fixed width, to avoid needing 'spacers'). This can require
| a lot more machine states, since those states allow the
| machine to 'remember' the bits it's read so far (e.g. if
| we're using 8 bits at a time, then we need enough states to
| "remember" what the first 7 bits were as we're reading the
| 8th).
|
| For a calculation like pi, we can use the tape to (a) write
| down the digits (or bits) of pi, and (b) keep track of
| intermediate variables needed for the calculation. One
| simple approach to keeping track of intermediate variables
| is to store them in order on the tape, where each variable
| is a sequence of 1 symbols, separated by 0 symbols. For
| example a tape like: 111010010 represents four variables
| with values 3, 1, 0 and 1 (the number of 1s we see before
| we hit a 0). This actually corresponds to Peano arithmetic,
| if we use the symbols S and Z instead like SSSZSZZSZ.
|
| An algorithm which spits out digits of pi forever (e.g. htt
| p://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/sp..
| . ) could work by moving its 'variables' section further
| and further to the right, allowing the digits of pi to
| accumulate, e.g. Start ^
| Initialise variables and output/variables separator
| |VARIABLES Move variables to make space for
| next digit _|VARIABLES Calculate and
| write next digit 3|VARIABLES Move
| variables to make space for next digit 3_|VARIABLES
| Calculate and write next digit 31|VARIABLES
| and so on
| mcguire wrote:
| Turing's machine includes an "infinite" tape. The number of
| states, the state transitions, and the number of symbols
| are finite, but an unbounded number of symbols can be
| written, one to a cell, on the tape.
| mensetmanusman wrote:
| I've wondered recently whether the brain can be represented
| by a Turing machine if our computation mechanisms utilize
| something like back propagation through time via quantum
| effects.
|
| Maybe we will make progress in our understanding this
| millennia :)
| chriswarbo wrote:
| Quantum physics can be represented and calculated by Turing
| machines. There are many ways to do this, depending on
| preference: via symbolic algebra, via probabilistic
| inference, via random/pseudorandom numbers, via non-
| deterministic functions, etc.
|
| Note that quantum computers are no more powerful than
| Turing machines; although it's thought they might be
| _faster at certain tasks_. For example, we know how to
| factorise integers quickly using Shor 's algorithm on a
| quantum computer, but we don't yet know a _quick_ algorithm
| for factorising integers on a classical computers. We can
| still factorise integers on a classical computers: we can
| do it with a non-quantum algorithm, or we can even do it by
| emulating a quantum computer and using that emulator to run
| Shor 's algorithm (in this case the emulation is so slow
| that it exactly cancels out the speedup from Shor's
| algorithm).
|
| Backpropagation through time is also a pretty simple
| algorithm, which is already implemented on classical
| computers.
| wizzwizz4 wrote:
| > _Note that quantum computers are no more powerful than
| Turing machines;_
|
| But computers with self-consistent time travel _are_ more
| powerful. It 's perhaps physically possible to construct
| one of those, depending on whether we ever end up with a
| more-correct timeless theory of physics that makes
| different predictions to existing physics.
|
| > _Backpropagation through time is also a pretty simple
| algorithm, which is already implemented on classical
| computers._
|
| I read "backprop through time" as meaning that you have
| the result of the backprop at the beginning of the
| process - _that 's_ more powerful, if we're using
| continuous computation. (With discrete computation,
| you're right that it's no more powerful.)
| meroes wrote:
| > Quantum physics can be represented and calculated by
| Turing machines.
|
| 1) Where does the randomness of QM come in though? You
| need a random number generator alongside your Turing
| machine.
|
| We coud debate that one can never prove true randomness
| as it may always be due to some deeper determinism. But
| if we take the wavefunction of QM as complete, which Many
| Worlds does - the most compsci-like interpretation - then
| randomness is fundamental according to theory.
|
| I can have all the TM's I want, but I still need this
| extra component. Just like the human Turing machine could
| have all the pen and paper and math in the entire
| universe and beyond, a human can't produce a truly random
| number (or can we, then we get into a debate about true
| free will and whether free will can produce a "random"
| number).
|
| 2) Let's say we instead use quantum computation instead
| of classical. There are still physical systems we can't
| "compute", like the state of the entire observable
| universe, the state of the entire universe, or anything
| requiring information that has forever left our light
| cone. I know TM's and quantum versions of TM's are
| infinite, but they can't bypass the speed of light. So we
| need some softer version of saying all of physical
| reality is computable imo.
| chriswarbo wrote:
| > Where does the randomness of QM come in though?
|
| That's why I said it's up to your own preference.
|
| It's interesting that you mention a many-worlds approach,
| since that doesn't actually involve _any_ randomness.
| Rather than choosing a single result probabilistically,
| many-worlds keeps them all. This can be represented quite
| nicely with what I referred to above as
| 'nondeterministic functions', i.e. functions which may
| return multiple values (in some sense, those values are
| literally the "worlds"). This would look like a logic
| language a la Prolog, but wouldn't be restricted to
| depth-first traversal: it could run breadth-first (very
| slow), concurrently (nice in principle, but would swamp
| any finite machine with overheads), or iterative
| deepening (probably the nicest implementation IMHO).
| Haskell programmers would call this a "breadth-first list
| monad" (AKA LogicT, AKA Omega). Instead of "returning
| multiple values", we could also do a continuation-passing
| transform and invoke the continuation multiple times
| (concurrently).
|
| This would run exponentially slowly, but that's a whole
| separate issue ;)
|
| > We coud debate that one can never prove true randomness
| as it may always be due to some deeper determinism.
|
| We could get a Copenhagen-like approach by doing the same
| as above, but only returning one of the results, chosen
| "at random" according to the square of the wavefunction
| (plus some hand-wavey Copenhagen-craziness, like defining
| whether or not Wigner's Friend is an 'observer')
|
| When it comes to "randomness" my own approach is to
| mentally substitute the word "unpredictable", since it
| tends to be more enlightening. Turing machines can
| certainly produce results which are "unpredictable", in
| the sense that the only way to know what will happen is
| to run the program; in which case that's more like a
| (repeatable) _observation_ rather than a prediction. (BTW
| I also think that 's a nice resolution of the "free will"
| paradox: my behaviour may be predicted by observing what
| an exact copy of me does; but it was still "decided by
| me", since that copy essentially _is_ "me")
|
| In any case, the outcome of a Turing machine using some
| pseudorandom algorithm is indistinguishable from "quantum
| randomness". There is certainly a limit to the
| unpredictability of any pseudorandom events (given by its
| Kolmogorov Complexity, which is upper-bounded by the
| Turing machine's program), but on the other hand I think
| it's quite presumptuous to think "quantum randomness" has
| _infinite_ Kolmogorov Complexity.
|
| > There are still physical systems we can't "compute",
| like the state of the entire observable universe, the
| state of the entire universe, or anything requiring
| information that has forever left our light cone.
|
| That's a very different question, since it involves how
| we choose what to put on the tape, rather than what a
| Turing machine is capable of computing. It's like
| criticising a genie for being unable to grant a wish,
| when in fact it's we who can't think of what to ask for.
|
| Besides this, there _is_ a way for a Turing machine to
| compute the whole universe, _including_ what 's outside
| our visible lightcone: we simply run _every program_.
| That 's actually a pretty straightforward task (and
| _remarkably_ efficient), e.g. see the FAST algorithm in
| section 9 of
| https://people.idsia.ch/~juergen/fastestuniverse.pdf
|
| Note that if we run such a program, there is no way to
| know which of the outputs corresponds to our universe.
| However, our ignorance of where to look does _not_ imply
| that such a Turing machine has not computed it!
| mensetmanusman wrote:
| " Turing machines can certainly produce results which are
| "unpredictable", in the sense that the only way to know
| what will happen is to run the program."
|
| This doesn't seem true since all predictions are 'running
| the program'
| chriswarbo wrote:
| Not necessarily; lots of systems have 'shortcuts', e.g. I
| can predict the result of sin(1000000t) will be 0,
| without anything physical/virtual having to wiggle up and
| down a million times. Lots of systems can be described by
| equations involving a time variable 't', where we can set
| t = whenever we like, then solve the equation to get the
| predicted value.
|
| When a system is Turing-complete, equations like this
| will _inevitably_ involve some expression with t-1; and
| solving _that_ involves some expression with t-2; and so
| on back to the initial condition. Hence there 's no
| 'shortcut' (this is a consequence of Rice's theorem BTW,
| which itself is a consequence of the halting problem).
| meroes wrote:
| Where in there did Turing prove computation can "exactly
| reproduce the behavior to...(any physical system)"? Because
| we humans seem to be able to describe and write down the
| behavior of any physical system? I'm not sure that jump is
| airtight.
|
| I'm not sure we can say this part even though we might
| believe it to be true. I mean maybe now we can since we have
| no deeper theories than quantum field theories, and we can
| posit all of physical reality reduces to QFTs and GR and
| simulate all of QFT computationally either with quantum
| computers (in real time) or classical (not in real time +
| need a random number generator). But the we'd still have
| computational limits by which observables we can measure and
| how big of computations we can run (think size of computer
| limited by black hole density for one crude example -
| although I guess a blackhole could be used as a quantum
| computer. So then I'd say the speed of light is the other
| main limit, we've already lost the information to run certain
| calculations to the depths of space).
|
| And to focus back in on the random number generator
| requirement for classical to simulate quantum...nothing
| fundamentally random can be simulated classically in
| principle. Yet randomness is needed to describe the most
| basic layer of reality. I can't get true randomness from
| classical no matter what.
| chriswarbo wrote:
| > Where in there did Turing prove computation can "exactly
| reproduce the behavior to...(any physical system)"? Because
| we humans seem to be able to describe and write down the
| behavior of any physical system?
|
| Turing's scenario essentially applies to a person in a
| room, with an unlimited amount of paper (this could be a
| movable tape extending through the walls, to prevent the
| room filling up with paper!).
|
| However, the same argument works if we replace the person
| with any other physical system (e.g. some mechanical
| device, or some physics experiment), and replace the room
| with any finite region of space (e.g. the Milky Way
| galaxy).
|
| I don't remember Turing himself making this argument (let
| alone in his 1936 paper), but it's known as the "physical
| Church-Turing thesis" https://en.wikipedia.org/wiki/Church%
| E2%80%93Turing_thesis#V... (the Church-Turing thesis is the
| argument that all 'effective methods of calculation' can be
| carried out by a Turing machine)
|
| As for your points about quantum physics, etc. that's
| certainly true, and it's why the Church-Turing thesis isn't
| a theorem (and can't be, since we can never know if any
| particular model of reality is correct). However, it's
| certainly a valid _physical law_ , akin to nothing moving
| faster than light, etc. i.e. it's empirically true,
| theoretically sound, and we have no better explanation _for
| the moment_.
|
| Perhaps its origin in mathematics, where it is a second-
| class citizen compared to provable theorems, prevented the
| Church-Turing thesis getting the recognition it deserves,
| e.g from physicists.
| foxes wrote:
| Well I might add the quantum complexity-theory version of
| the Church-Turing thesis.
|
| I believe that quantum computation is a richer more
| powerful theory. In essence BQP is a superset of BPP in
| your link.
|
| I think this happens with all sorts of mathematical
| objects. Non commutative algebra is much richer than
| commutative algebra. There are also more interesting non
| commutative things than just deformations of classical
| objects. Its the classical commutative case that is the
| weird limit.
| chriswarbo wrote:
| Yeah, there are all sorts of layers we can add,
| especially regarding complexity (i.e. resource usage
| limits, rather than simple yes/no questions of
| decidability).
|
| It's interesting to consider P = NP as a physical law,
| although that's certainly more tenuous than the Church-
| Turing thesis, etc.
| Rioghasarig wrote:
| > This is the philosophical justification for why a (Turing)
| machine can calculate anything a human can (in fact, the same
| argument shows that a Turing machine can reproduce the
| behaviour of any physical system).
|
| I don't think this assertion follows. I don't think an
| argument like this can work without delving further into
| reasonable description of a "physical system".
|
| If you just just use the mathematics we employ to describe
| physical systems unreservedly it is possible to construct
| "physical systems" that exhibit non-computable behavior. For
| instance you can have computable and continuous initial
| conditions to the wave equation that produces a solution that
| is non-computable. See : https://en.wikipedia.org/wiki/Comput
| ability_in_Analysis_and_...
|
| I think it's important to emphasize that Turing stated his
| arguments in regards to "effective procedure" (which I see
| you mention in a different post). I don't think the
| substitution of "effective procedure" with "physical system"
| is justified.
| chriswarbo wrote:
| > For instance you can have computable and continuous
| initial conditions to the wave equation that produces a
| solution that is non-computable.
|
| Thanks, that's a really nice example which I hadn't come
| across before (or at least not spent too much time
| studying). I may have to refine the language I use in
| future; although a cursory look _seems_ to be compatible
| with my own understanding (my mental model is roughly: "if
| we found a halting oracle, we would have no way to tell for
| sure")
|
| > I think it's important to emphasize that Turing stated
| his arguments in regards to "effective procedure" (which I
| see you mention in a different post). I don't think the
| substitution of "effective procedure" with "physical
| system" is justified.
|
| Yes, Turing did not say as much (at least in his 1936
| paper). He was essentially abstracting over 'whatever it is
| that a person might be doing', in an incredibly general
| way. Others have since taken this idea and applied it more
| broadly.
|
| Another useful caveat is that Turing machines are framed as
| (partial) functions over the Natural numbers. It's quite a
| leap from there to a "physical system". An obvious example
| is that no matter how cleverly we program a Turing machine,
| it cannot wash the dishes; although can _simulate_ the
| washing of dishes to arbitrary precision, and it could wash
| dishes by controlling actuators _if_ we decided to attach
| some (but even that would run into problems of time
| constraints; e.g. if calculating the first instruction took
| so long that the water had evaporated).
| wizzwizz4 wrote:
| The problem with your assumption is that you're assuming
| there are a finite number of states. There might be an
| uncountably infinite number of states, for instance if
| the states were the reals between 0 and 1.
| lurquer wrote:
| Interesting post.
|
| Can you please flesh out the following? I don't quite follow
| it..
|
| > having infinitely many states would require them to be
| infinitesimally similar, and hence indistinguishable from
| each other within a finite amount of time
| chriswarbo wrote:
| Sure. Let's take a finite region, like a room. We don't
| want to get too bogged down in the details of human
| psychology, anatomy, etc. so we'll stick to something very
| low-level like particle physics (which, in principle, can
| describe a person in exact detail). One state of this
| region is that it's completely empty (maybe quantum effects
| rule that out, but we can still include it if we're being
| conservative ;) ). Another state could have, say, a single
| electron, at some position we'll call (0, 0, 0). Another
| could have a single electron at position (0, 0, 1). Another
| has an electron at (25, 5, 3) _and_ a proton at position
| (0, 0, 0). And so on.
|
| Let's consider the states which just contain a single
| electron, somewhere in the room (I'm not bothering with
| quantum effects, but we would do the same thing just in
| Hilbert space instead of 3D space). The region is finite,
| so the coordinates of this electron are bounded: if the
| boundaries are at, say, 0 and 100 in each axis, then
| putting the electron at position (101, 0, 0) would be the
| same state as the empty one we started with (since the
| electron is outside the region we care about, and there's
| nothing else).
|
| Now let's say we do some measurement of this electron's
| position, which is only accurate to whole number
| coordinates. That gives us 100^3 = 1,000,000
| _distinguishable_ states with a single electron. We might
| imagine all sorts of different states 'in between', but
| they can't affect that measurement due to its limited
| resolution.
|
| If we increase the resolution of our measurement by 10, we
| get 10^3 times as many distinguishable states; another
| factor of 10 gives 10^3 times as many states again; and so
| on. However, _regardless_ of how finely we can resolve the
| electron 's position, we can only distinguish between
| finitely-many states. Any differences finer than that limit
| are irrelevant to the measurement, and hence to any
| behaviour that depends on that measurement.
|
| If we _could_ resolve between infinitely-many positions for
| the electron, that would require distinguishing between
| states which are infinitesimally-close together, i.e. on an
| infinitely-fine grid; this would require distinguishing
| between two numbers whose decimals only differ after
| _infinitely many_ digits. This doesn 't seem like a
| reasonable capability.
|
| The same principle applies when we have two electrons in
| the room, or trillions, or any combination of electrons,
| protons, photons, etc. in any arrangement we like.
|
| A similar thing happens when we reach really large numbers
| too, e.g. trying to put as many particles in the region as
| we can: at some point the _relative_ difference between,
| say, a googolplex and five particles versus a googolplex
| and six particles becomes too small to distinguish. There
| will _eventually_ be a limit. (This is like the resolution
| problem, but instead of adding decimal places to the right
| of each number, we 're adding factors of 10 to their left)
|
| One way to get around this problem of limited resolution is
| to avoid an explicit 'measurement', and instead have the
| _region itself_ behave differently for different states. A
| good example is _chaotic_ behaviour, where tiny changes in
| an initial state will grow exponentially until those
| differences eventually become distinguishable. However, the
| infinitesimally-similar states described above will remain
| infinitesimally close for all finite lengths of time; in
| order to distinguish between them, we would need to wait an
| _infinite_ amount of time.
| beltsazar wrote:
| That Veritasium's video is great! I'd also recommend
| Computerphile's 3-part video series (~10 mins each) which tells
| the history of undecidability and the incompleteness theorem:
|
| https://www.youtube.com/watch?v=nsZsd5qtbo4
|
| https://www.youtube.com/watch?v=FK3kifY-geM
|
| https://www.youtube.com/watch?v=lLWnd6-vSGo
| skissane wrote:
| > Thus he identified fundamental limits of algorithmic theorem
| proving, computing, and any type of computation-based AI
|
| Fundamental limits presuming one has arbitrarily high (but
| finite) quantities of time and space with which the computations
| can be performed. Given in real world computation we will never
| have either, the fundamental limits of real-world computation are
| a lot less (even infinitely less) than those given by Godel's
| work.
|
| Also, demonstrations of the theoretical limits of computation
| (Godel, Turing, etc) often make the assumption that we only have
| finite (even if arbitrarily large) resources, and that true
| contradictions (dialetheias) are disallowed. If we give up either
| (or both) of those of two assumptions, we can compute beyond
| those limits. It may be objected that computations beyond those
| limits are not physically realisable; but, almost all
| computations within those limits are not physically realisable
| either, so how much significance does that objection actually
| have?
| Valmar wrote:
| It's a harsh, but true reality that with only have finite
| quantities of time and space, especially in real world
| computation. The assumption of finite resources is also a
| harsh, but true reality.
|
| There are many things that fundamentally defy any form of
| computation. Things which cannot create mathematical formulae
| to represent, nor create algorithms for.
|
| For a major example, we cannot translate the mental activities
| of conscious, aware living beings into any sort of computable
| form, as these activities are not algorithmic in nature. They
| aren't random, nor deterministic ~ rather, they are
| indeterministic, following no rigid patterns.
|
| Even the most complex, complicated computer program follows an
| algorithm, which is ultimately deterministic. Even if you throw
| in some random inputs at some parts, the algorithm still acts
| deterministically. Perhaps the only really indeterministic part
| in an algorithm's behaviour might be hardware level bugs and
| errata which interfere with the otherwise very predictable
| algorithm.
| amanaplanacanal wrote:
| > For a major example, we cannot translate the mental
| activities of conscious, aware living beings into any sort of
| computable form, as these activities are not algorithmic in
| nature. They aren't random, nor deterministic ~ rather, they
| are indeterministic, following no rigid patterns.
|
| How could you possibly know that? Following no _known_
| patterns, maybe.
| skissane wrote:
| Trivially, for any finite string (in a finite alphabet),
| there is a finite program (Turing machine, whatever) which
| outputs that string given empty input. Hence, "the mental
| activities of conscious, aware living beings" are trivially
| computable if there exists a finite string which describes
| them with perfect accuracy.
|
| Furthermore, there obviously are _some_ computable patterns
| in those activities, so the shortest possible computable
| program to generate that description will actually be
| shorter than the length of the description itself.
|
| One could respond that a string describing those mental
| activities, no matter how accurately, is a different thing
| from the mental activities themselves. I think that is
| indeed the correct response, but it has nothing to do with
| any questions of computability.
|
| (Another response would be to claim that those mental
| activities cannot be finitely described because they are
| actually infinite. Few however will want to claim that
| human minds are infinite.)
| onethought wrote:
| > Even the most complex, complicated computer program follows
| an algorithm, which is ultimately deterministic.
|
| Godel's work proved this statement false.
|
| To give an example, what if the algorithm is to generate the
| correct algorithm? What if the correct algorithm ends up
| being the original algorithm?
|
| That is not deterministic.
| Rioghasarig wrote:
| >> To give an example, what if the algorithm is to generate
| the correct algorithm?
|
| That's not a description of an algorithm. You've stated a
| "problem". An algorithm, by definition, is an actual
| deterministic procedure.
| skissane wrote:
| > That's not a description of an algorithm. You've stated
| a "problem".
|
| I wanted to say the same thing, but you managed to find
| the words I couldn't.
|
| > An algorithm, by definition, is an actual deterministic
| procedure
|
| That's not necessarily true. There are non-deterministic
| algorithms:
| https://en.wikipedia.org/wiki/Nondeterministic_algorithm
| skissane wrote:
| If a machine is deterministic, all programs for the machine
| must be deterministic. Godel's theorems don't contradict
| that. If you think they do, you've misunderstood them.
| [deleted]
| skissane wrote:
| I don't care about being downvoted, but I wish those doing so
| would reply to explain why.
| mlasson wrote:
| > almost all computations within those limits are not
| physically realisable either, so how much significance does
| that objection actually have?
|
| If some thing is _impossible_ with arbitrarily large finite
| resources, it is still impossible with "practically large"
| finite resources ! That's why Turing / Godel results really
| tell something fundamental about computing/proving; it tells
| everyone that they do not need to spend time solving an
| unsolvable problem on computers "as we know them".
|
| But if you prove that something is _possible_ in a your own
| magic computing framework, it remains practically useless until
| you implement it in the real world (an example of such a
| situation is the framework of "quantum computer" trying to
| solve prime factorization).
| skissane wrote:
| > That's why Turing / Godel results really tell something
| fundamental about computing/proving; it tells everyone that
| they do not need to spend time solving an unsolvable problem
| on computers "as we know them"
|
| Consider something like Turing's proof that the halting
| problem is undecidable - does that have practical relevance,
| even just in telling us that there is no point in trying to
| solve an unsolvable problem?
|
| That's the standard line but I doubt it. The thing is, the
| halting problem is practically irrelevant; what has practical
| relevance is the _bounded halting problem_. Practically, you
| don 't care about the difference between a program that never
| halts, and a program that halts after a googolplex steps, but
| that distinction is essential to the halting problem as
| defined. And, the practically relevant, bounded halting
| problem, is in fact decidable. Now, it is still intractable,
| because it is EXPTIME-complete, and we also know (per the
| time hierarchy theorem) that EXPTIME-complete problems are
| not in P.
|
| So Turing's proof doesn't actually tell us anything much
| useful about whether the halting problem is solvable in
| practice, whereas the proof that the bounded halting problem
| is EXPTIME-complete does. Suppose (counterpossibly) that the
| bounded halting problem was in P instead of EXPTIME-complete;
| then the halting problem might actually be tractable in
| practice, even though Turing's proof of the unbounded halting
| problem's undecidability would still hold.
| oscardssmith wrote:
| The problem with this is that proving an algorithm is in P
| is also undecidable.
| skissane wrote:
| How is that a problem with what I said?
|
| You are saying that the decision problem of "Is this
| algorithm A in P?" is undecidable for arbitrary
| algorithms A. We don't need a general solution to that
| decision problem to be able to prove that some particular
| algorithm is or isn't in P; just like how, we don't need
| a general solution to the halting problem to prove some
| particular program does or doesn't halt. The halting
| problem only means we can't have a computable procedure
| which will generate such a proof in every case.
|
| The fact that we've actually proven the bounded halting
| problem is not in P doesn't contradict this. The
| undecidability of determining whether _any_ arbitrary
| problem is or isn 't in P doesn't prevent us from having
| a proof that _some particular_ problem is or isn 't.
|
| And I said _counterpossibly_ that if the _bounded_
| halting problem were in P not EXPTIME-complete, then the
| halting problem might be _practically_ solvable even if
| Turing 's proof of the undecidability of the _unbounded_
| halting problem still held. In this counterpossible, we
| don 't need to be able to solve the decision problem of
| determining whether an algorithm is in P, all we need is
| a proof that this one particular algorithm is in P. The
| undecidability of the decision problem _in general_ tells
| us nothing about whether we could know its answer for
| individual cases.
| b3kart wrote:
| Schmidhuber has done a lot of important, fundamental work, at the
| time when none of it was "cool", but whenever I stumble upon his
| writing it always reads like a bad history book, where _when_ and
| _who_ are more important than _what_ or _why_. I get (and
| moderately support) his obsession with proper attribution, but I
| wish he first talked about ideas, and _then_ delved into the
| intricate historical details.
| truth_ wrote:
| If you want to learn thoroughly about Godel's Incompleteness
| Theorem, and all its implications, nothing is better than Godel,
| Escher, Bach: An Eternal Golden Braid by Hofstadter.
|
| This book is quite outdated in both approaches and ideas about
| computers, and computer-aided approaches to Artificial
| Intelligence, this book still has to offer a lot. It is one of
| the most impactful books I have read.
| alok-g wrote:
| Does it explain the proof itself in it's full glory? I had read
| "Godel's Proof" by Ernest Nagel et al [1] and it fell short.
|
| [1] https://www.amazon.com/Godels-Proof-Ernest-
| Nagel/dp/08147583...
| ruslan wrote:
| Fascinating book indeed. I read it when I was a student some
| twenty years ago, I had been astonished by simple and clever
| trick Godel used to prove his theorem - to digitize everything,
| then operate with just numbers.
| [deleted]
| scotty79 wrote:
| For me it just means that math is just like the code. If you
| start defining stuff and cross-calling it without special care
| you will end up in trouble in form of infite loop or recursion or
| in case of math, a paradox.
|
| From what I understand it is that you might reason about but not
| prove that statement "this statement is not provable" must be
| true but thus unprovable.
|
| Godel's result shows that if you are willing to assume axioms
| that let you do arithemetics, statement equivalent to this
| paradoxical one just crops up.
|
| For me it just means that you need to put additional restrictions
| of what you can do in math so that kind of statement is excluded
| from math.
|
| Same way that "set of all sets that are not their own elements"
| got excluded from consideration by more carefully defining what
| set theory is involved with.
| magneticnorth wrote:
| >> For me it just means that you need to put additional
| restrictions of what you can do in math so that kind of
| statement is excluded from math.
|
| The thing about Godel's proof is that he didn't just come up
| with one example of a "this statement is not provable"
| sentence; he proved that any sufficiently complex math system
| will have unprovable sentences (some true, some false, some
| you'll never be able to know). And "sufficently complex" is not
| all that complex! So if you want to be able to do calculus, or
| even most arithmetic, you can't just "put additional
| restrictions ... so that kind of statement is excluded from
| math."
| runT1ME wrote:
| I think it's important to point out that you can do calculus
| and arithmetic and only construct proofs that _are_ provable.
| The possibility of deriving unprovable but true statements in
| an axiomatic system doesn 't mean they're common or you can't
| prove all the satatements one has encountered thus far.
| Animats wrote:
| _He proved that any sufficiently complex math system will
| have unprovable sentences._
|
| That's mostly because "sufficiently complex" is defined by
| mathematicians, not computer scientists. In particular, it
| includes infinities, which do not exist in the physical
| universe. Godel's proof requires allowing unlimited depth
| recursion, which does not exist in the physical world.
|
| The halting problem is decidable for any deterministic system
| with finite memory. Either you halt, or you repeat a state.
| This covers most real-world computer programs.
|
| There's a useful subset of arithmetic and logic which is
| completely decidable. It contains integer addition,
| subtraction, multiplication by constants, and all the logic
| operators. This covers most subscript checking in programs,
| which is quite useful. You can probably add modular
| arithmetic with a fixed upper bound to that subset.
|
| Now, some systems may require very large amounts of work to
| prove, but that's different from being undecidable. "Very
| large" is not infinite. That heads us off into the theory of
| lower bounds, P = NP, and all that, where there are still
| many open questions.
|
| This knocks out many of the sillier claims about
| undecidability making something impossible in the real world.
| rssoconnor wrote:
| > The halting problem is decidable for any deterministic
| system with finite memory. Either you halt, or you repeat a
| state. This covers most real-world computer programs.
|
| Problem being that you cannot decide whether a system with
| such finite memory halts without using another different
| system that has even more memory. And if that larger system
| doesn't "real-world" exist, can you truly say that the
| halting problem is decidable?
| Animats wrote:
| You can determine if a program halts by running two
| copies in lockstep, one at half the speed of the other.
| If their states are ever the same after the first step,
| they're in an infinite loop.
|
| That was actually used in an early batch system for
| running student jobs in an interpreter. A successful
| student job ran for under a second; one in a loop ran for
| 30 seconds until it was killed for taking too long. So
| detecting simple loops, even with substantial extra
| overhead, was worth it.
| alok-g wrote:
| Exactly!
|
| For the same reason, when someone uses halting problem to
| 'explain' why their program freezes, they are wrong. They
| are wrong on multiple counts actually.
|
| For pure mathematics, this stuff is relevant. For all
| practical purposes, it is not (as far as infinite-precision
| analog memories are not involved).
| anon_tor_12345 wrote:
| >In particular, it includes infinities, which do not exist
| in the physical universe.
|
| Bold claim. As far as I know the centers of black holes are
| indeed non-removable singularities of (some) solutions to
| GR equations.
|
| What's funny is I had a debate with a cosmologist where I
| was on your side of the debate because he was a
| mathematical realist (and therefore forced to reconcile the
| same divergences with the "reality" of math).
| scotty79 wrote:
| Sure you can. Just ban the concept of provability from your
| math language (or some elements that lead to it). Same way
| like they banned weird kinds of sets and started talking
| about set families instead of sets of sets.
|
| If you declare that set being its own element is nonsensical
| statement you no longer have a paradox with set of sets that
| are not their own elements.
|
| Base assumption of math is that correctly constructed
| mathematical statement is not nonsensical. It must be true or
| false or not determined by current set of axioms. And I think
| that assumption of sensibility of any math statement leads to
| paradoxes.
| rssoconnor wrote:
| A set of elements that lead to the concept of
| provability[1] are: 0, 1, addition, multiplication,
| quotient, remainder and inequality.
|
| Quotient and remainder are definable implicitly in the
| language of number theory (the language of Peano
| Arithmetic). Sometimes inequality is explicitly defined,
| and sometimes it is implicitly defined using exists and
| addition.
|
| From these elements you can go on to define the Goedel beta
| function, which allows you to encode lists of numbers and
| extract the nth element from such an encoding. From there
| you can go on to define arbitrary primitive recursion (and
| even more). From there provability can be defined as a
| primitive recursive function.
|
| I'm not sure which element there you want to ban. Maybe you
| want to ban multiplication?
|
| [1]http://r6.ca/blog/20190223T161625Z.html
| magneticnorth wrote:
| In the case of set theory, you can exclude sets of sets and
| still have an extremely rich and deep mathematical theory
| of sets. (But it is definitely still incomplete - for
| example ZFC can't prove the continuum hypothesis, and if
| you take the continuum hypothesis or its negation as an
| axiom, there are still infinitely more unprovable
| statements in that mathematical theory)
|
| In the case of Godel's incompleteness theorem, excluding
| the amount of math you need to in order to avoid unprovable
| sentences leaves you with only very simple axiom systems.
| If your mathematics is complete enough to even do simple
| arithmetic (i.e. Peano arithmetic), then there are
| unprovable statements.
|
| It's not as easy a fix as Russell's set theory paradox,
| which is why it's an important and foundational aspect of
| nearly all mathematics even today.
| magneticnorth wrote:
| Perhaps a better explanation - it's similar to the halting
| problem in computer science. There are programs p where
| "Program p halts on input x" is unprovable (equivalently
| there is no computable way to determine which p,x halt),
| and the key is that we have no way of knowing which
| programs p and x this is true for, of the ones we don't yet
| have proofs/halt-prediction-programs about.
|
| You may want to argue that this can be "solved" by never
| letting programs take other programs as input, which isn't
| wrong, exactly, but you're left with not very much you can
| compute in that paradigm for computation.
| ProfHewitt wrote:
| Good point, scotty79!
|
| In fact the [Godel 1941] proposition _I 'mUnprovable_ does not
|
| exist in mathematical foundations.
| m4rtink wrote:
| As a sidenote, my alma mater, Faculty of Informatics in Brno,
| Czech Republic, has Goedel depicted on its insignia, as he was
| active in the city: https://www.em.muni.cz/udalosti/698-insignie-
| fakulty-informa...
| masswerk wrote:
| Fun fact, on the PDP-7, there was a rare case of completeness,
| where the instruction "-0" not only encodes itself, but also
| operationally loads itself.
|
| For details see: https://www.masswerk.at/nowgobang/2019/pdp7-by-
| law
| bonoboTP wrote:
| How can you leave out von Neumann from such a list?
|
| Also, I feel like Schmidhuber tends to be German-speaking-
| centric.
|
| And overall, acknowledging that this is his signature shtick and
| it's good to have a voice like this too, he does a lot of
| anachronistic reinterpretations of early discoveries in light of
| later results. It streamlines the story as if it was always
| headed towards the today, culling aspects that didn't pan out or
| magnifying aspects that were at the time more minor and not
| considered the central issue or angle.
| inigojonesguy wrote:
| Schonfinkel (1920)
| h8hawk wrote:
| I feel he is actively trying to dismiss Turing / Von neumann /
| church contributes and attributing them to Godel and etc.
| 317070 wrote:
| That is a bit his schtick. He himself feels like he has been
| the victim of an anglo-centered science history (one might
| debate about that), so he is retelling how the story could
| work if you put less focus the anglo-part.
|
| To me, it seems like a healthy coping mechanism.
| mefaso wrote:
| Von Neumann is also german-speaking by the way
| bonoboTP wrote:
| Spoke German among many other foreign languages, but his
| native language was Hungarian.
| weinzierl wrote:
| > _" How can you leave out von Neumann from such a list?"_
|
| When I read the title:
|
| _" 1931: Kurt Godel shows limits of math, logic, computing,
| AI"_
|
| my head automatically completed it with
|
| _" John von Neumann approves."_
|
| I always found it fascinating and a sign of von Neumann's
| greatness how quickly he not only understood the consequences
| of Godel's discovery but also that he immediately and publicly
| accepted them.
| ProfHewitt wrote:
| It is particularly ironic that Godel deceived von Neumann
|
| about having already developed an important proof for [Godel
| 1931].
|
| The deception was discovered years after both had died.
|
| See [von Plato 2018]
| osullivj wrote:
| I found it refreshing to read a non anglocentric view. Agree we
| must be alert for the fallacy of conceptual retrospection.
| kaba0 wrote:
| I mean, Godel was Austrian and von Neumann Hungarian who
| traveled/lived a lot in many German speaking countries, so I
| don't see the anglocentrism here.
| denton-scratch wrote:
| I have relied on Douglas Hofstadter and Roger Penrose for
| explanations of Godel's theorem. Hofstadter is easier - Godel
| Escher and Bach. Penrose's explanation is dryer, but more direct
| - The Emperor's New Mind.
|
| I understand the idea of Godel numbering; I understand Cantor's
| diagonal slash; but I struggle to assemble the components into a
| proof that convinces me. I think I just lack the cerebral
| capacity.
| alok-g wrote:
| Does either (claims to) explain the proof itself in it's full
| glory? I had read "Godel's Proof" by Ernest Nagel et al [1] and
| it fell short.
|
| [1] https://www.amazon.com/Godels-Proof-Ernest-
| Nagel/dp/08147583...
| pmmck wrote:
| For me the click came while finishing To Mock a Mockinbird by
| Raymond Smullyan.
|
| https://en.wikipedia.org/wiki/To_Mock_a_Mockingbird
|
| Smullyan "tricks" you into deriving the Godel Incompleteness
| Theorem from the BCKW combinator calculus.
| tovej wrote:
| Tangentially related: the book "Godel, Escher, Bach: an Eternal
| Golden Braid" by Douglas Hofstadter is a computer science classic
| that deals with incompleteness among other things (mostly self-
| references in formal systems) in a fun way.
| ProfHewitt wrote:
| Mathematical foundations are indeed incomplete, that is,
|
| there are true propositions, which are unprovable.
|
| However, [Godel 1931] _failed_ to prove incompleteness of
|
| foundations using the _nonexistent_ proposition
|
| _I 'mUnprovble_. The [Godel 1931] attempt to construct
|
| _I 'mUnprovable_ using fixed points fails because it violates
|
| restrictions on orders of propositions. The Godel number of a
|
| proposition left out its order.
|
| Furthermore, existence of _I 'mUnprovable_ would have the
|
| unfortunate consequence that foundations are inconsistent.
|
| It is worth noting that the proposition _I 'mUnprovable_ is of
|
| no practical importance in mathematical foundations.
|
| Consequently its nonexistence does not much matter.
|
| See the following for further explanation:
|
| https://papers.ssrn.com/abstract=3603021
| jkhdigital wrote:
| Nice to hear from you again, Carl. Your comments about
| inconsistent foundations brings to mind the _Univalent
| Foundations_ approach to mathematics--can you comment on how
| your research relates to univalent foundations and homotopy
| type theory?
| ProfHewitt wrote:
| Thanks jkhdigital!
|
| Of course, mathematical foundations _must not be
| inconsistent_.
|
| Homotopy type theory is an attempt address issues of
|
| equality in type theory.
| rssoconnor wrote:
| For the record, Godel proposition can be constructed[1] in the
| same manner that Quines[2] can be constructed. I myself have
| formalized[3] the first incompleteness theorem in the Coq proof
| assistant, and many others have as well in various proof
| assistants.
|
| You can find specific and concrete instance of a Godel
| proposition written by Stephen Lee at
| <http://tachyos.org/godel/Godel_statement.html>. It really is
| not that large of a proposition. I'm not sure how you can claim
| that proposition that I can see with my own eyes does not
| exist.
|
| [1] http://r6.ca/blog/20190223T161625Z.html
|
| [2] https://en.wikipedia.org/wiki/Quine_(computing)
|
| [3] https://github.com/coq-community/goedel
| ProfHewitt wrote:
| Godel proposition _I 'mUnprovable_ cannot be constructed in
|
| foundations because fixed-point construction violates orders
|
| on propositions. Existence of _I 'mUnprovable_ would render
|
| foundations inconsistent.
|
| See the following;
|
| https://papers.ssrn.com/abstract=3603021
| rssoconnor wrote:
| Since you allege the existence of I'mUnprovable
| propositions renders Peano Arithmetic (see
| <http://tachyos.org/godel/Godel_statement.html> cited
| above), Coq, HOL Light, Isabelle and every other proof
| assistant that has proven the incompleteness theorem
| inconsistent, I look forward to you facilitating the
| development of a formal contradiction in any one of these
| systems. In particular a proof of False in Coq[1] would
| greatly aid me in getting through some of my troublesome
| proofs.
|
| [1]http://r6.ca/blog/20061211T203500Z.html
| ProfHewitt wrote:
| Proposition _I 'mUnprovable_ must not exist in
| _foundational
|
| theories_. A proof of inconsistency for a foundational
| theory
|
| that has _I 'mUnprovable_ appeared here:
|
| https://papers.ssrn.com/abstract=3603021
| rssoconnor wrote:
| Very good. Then surely the paper proof can be translated
| into an inconsistency of Coq, Isabelle or HOL-light,
| since all of these proof assistants already prove the
| existance of such an "I'mUnprovable" proposition.
| truth_ wrote:
| I appeciate how Schmidhuber puts focus on non-US-centric history
| of Deep Learning and modern AI.
|
| He sometimes overdoes these. Even when something is not related
| to Deep Learning and modern AI. He tries to push very narrow and
| one-sided views without much room for nuance.
|
| For example- _" Turing used his (quite inefficient) model only to
| rephrase the results of Godel and Church on the limits of
| computability."_
|
| He is trying to say that Turing did nothing new, his work is a
| mere extension of Godel's (!), and he only accounted for
| practical computational reality. That is not true.
|
| He goes on further by saying, _" Later, however, the simplicity
| of these machines made them a convenient tool for theoretical
| studies of complexity."_ Like, Turing and Church's work was only
| good for that. I digress. I believe that Turing's work is more
| seminal and paved the way for modern general computers.
|
| Another bit here says _" The formal models of Godel (1931-34),
| Church (1935), Turing (1936), and Post (1936) were theoretical
| pen & paper constructs that cannot directly serve as a foundation
| for practical computers."_
|
| It is putting the works of Turing, Post, Church, and Godel all
| together. Like they are the same. I see the logic as they are all
| impractical, but they are different levels of impractical.
| Putting them all under one bracket like that makes no sense.
|
| I respect Schmidhuber a lot, but some of his behaviour is
| borderline childish which are more pronounced in his claims about
| AI history. You should be skeptical about what he says (and what
| anyone says).
|
| Despite all this, I did not know many things written in this
| article. I learned a lot and had fun reading it.
|
| I first read about Zuse in Isaacson's Innovators book. Did not
| know that he used a high-level language for a chess program.
| Fascinating. He is very underrated.
| maweki wrote:
| Both the discovery of Lambda Calculus and the Turing Machine as
| models of computation are quite important and immediately
| useful, I'd say. Though very formal, just a little bit of
| syntactic sugar and eye-squinting make for useful programming
| constructs and more or less direct lines to early as well as
| modern programming languages.
| ProfHewitt wrote:
| Development of Lambda Calculus [Church 1931] and Turing
|
| Machine [Turing 1936] were fundamental achievements. However,
|
| they are inadequate models of computation because there are
|
| digital computations they cannot implement.
|
| See the following for an example:
|
| https://papers.ssrn.com/abstract=3603021
| tsimionescu wrote:
| I've tried really hard to understand which part of that
| paper is an example of a computation that a Turing machine
| couldn't implement, and I have been completely unable to do
| so. I will say that the writing in the paper is in serious
| need of some basic copy editing - it is full of typos,
| repeated phrases and entire paragraphs (especially in the
| abstract).
| ProfHewitt wrote:
| What exactly are the typos?
|
| Which paragraph is repeated?
| kamray23 wrote:
| Only true for nondeterministic systems. Which all computers
| are as there is physical nondeterminism. However, it can
| (mostly) be ignored in any practical application of these
| theories, because the chances of you ending up in a
| nondeterministic computation at all are minute, never mind
| an unbounded one. And we are talking about practical
| applications here.
|
| Also, isn't that your own paper?
| ProfHewitt wrote:
| Many-core computer systems and networked computer systems
|
| depend crucially on indeterminacy in order to gain
|
| performance.
|
| See the following
|
| https://papers.ssrn.com/abstract=3459566
| wizzwizz4 wrote:
| Many-core and networked computer systems _fight_
| indeterminacy. My networking algorithms would be a lot
| simpler if I could guarantee that everything operated in
| lockstep; the fact that I have to discard lockstep to get
| performance is because lockstep is a high-cost
| abstraction over a high-entropy (so, basically non-
| deterministic) underlying reality, not because
| indeterminacy is somehow inherently better.
|
| It's a concession.
| ProfHewitt wrote:
| A concession to the physical world?
| 1024core wrote:
| US and EU researchers have been on parallel and competing
| tracks for a long time, ever since the days of Prolog and Lisp.
| slipframe wrote:
| De-emphasizing Turing as an instance of focusing on non-US-
| centric history? Turing was not American! Furthermore, Church
| _was_ American, but that quote is aggrandizing to Church while
| diminishing of Turing. I don 't think that quote is an example
| of what you claim.
| sn41 wrote:
| This is classic Schmidhubris, a mixture of truth and
| exaggeration.
|
| Turing's paper is a landmark, and includes even an equivalence
| proof of the power of the lambda calculus and his universal
| machine. In doing so, he came up with a fixed-point combinator,
| an applicative combinator, now called the Turing fixed point
| combinator [1]. Especially appropriate on a website run by the
| Y combinator.
|
| Turing's paper should run as a TV ad "But wait, there's
| more..." Many applications of topology (he argues why the
| alphabet should be finite, rather than simply saying that it is
| finite, by using the Bolzano-Weierstrass theorem, essentially),
| combinatorics, logic, functional programming - when FP was
| hardly a decade old and largely unknown outside Princeton - and
| all from an undergraduate course project report!
|
| [1] https://en.wikipedia.org/wiki/Fixed-
| point_combinator#Other_f...
| mudlus wrote:
| The author hasn't read any David Deutsch, I can tell.
| bo1024 wrote:
| Agree, the quote lumping the models of computation together is
| very misleading. Turing's machines are immediately obvious how
| to mechanize and automate, even with very old technology. That
| was the key difference. Then proving them equivalent to mu-
| recursive functions and lambda calculus showed that these
| models of computation actually deserved to be called such. It
| proved that they could be implemented on a machine with no
| human ingenuity or creativity required to carry out the steps,
| which is the heart of what it means to be computable.
| erichahn wrote:
| What most ppl don't notice is that Godels incompleteness theorems
| are themselves expressible only in a logic system capable of
| expressing Peano arithmetic. Now this means that they apply to
| themselves which means that we cannot know if they are made up
| from a axiomatic system that can prove anything.
| dandanua wrote:
| It's ok to use logic to prove theorems in logic. We also use
| thinking to deduce some facts about our thinking. Self-
| reference is not always paradoxical. In a higher-order logic
| some self-referential definitions are legitimate.
| erichahn wrote:
| Yes and then you can do self-referential statements again
| which leads you to the conclusion that Godels theorems are
| provable only in a system that cannot prove its own
| consistency.
| dandanua wrote:
| True, but it's not a logical paradox. The fact that a
| system can't prove its own consistency doesn't imply that
| this system is inconsistent. The fact that Godel's theorems
| are provable only in such systems also doesn't imply that
| they are wrong.
|
| From the common sense the whole situation looks
| paradoxical, indeed. To prove consistency of some theory we
| have to use some stronger theory, to prove consistency of
| that theory we need even stronger theory and so on.
|
| Perhaps, the best way to realize why there is no paradox is
| the following:
|
| Our memory is finite. As well as our thinking. But the
| total number of true facts about mathematics is infinite.
| By constructing theories we are trying to compress the
| infinite number of true facts into some finite form.
| Godel's theorem says it's impossible. And it looks quite
| natural from this perspective.
| kaba0 wrote:
| I'm not too knowledgeable on the topic, but Godel's proof uses
| a smaller logic system -- on which a meta-language can be used
| to prove consistency/completeness. It is precisely about not
| being able to prove these properties "from within".
| erichahn wrote:
| Which one? I don't think so tbh because his proof uses PA.
| kyberias wrote:
| It's very easy for you to check this from his 1931 article.
| erichahn wrote:
| If you figure this out correctly you can claim the third
| incompleteness theorem. (If I am right)
| bidirectional wrote:
| It's not Peano arithmetic, it is basically 'enough of'
| arithmetic for Goedel's methods to apply. Robinson arithmetic
| is weaker than PA but Goedel still applies. Goedel's argument
| is basically a meta-argument about _any_ mathematical system
| which is rich enough to describe useful mathematics, it does
| not rely on any particular axiomatisation, rather it applies to
| all axiomatisations with a few simple features.
| erichahn wrote:
| "it does not rely on any particular axiomatisation"
|
| -- OK, what does it rely on then?
| carnitine wrote:
| The axioms allowing one to express enough of arithmetic for
| Goedel's methods to apply. As the comment says.
| erichahn wrote:
| I think if Godels proof needs Q then that is OK.
|
| Q cannot prove its own consistency. Which means there is no
| way of telling that Godels theorems are proved in a theory
| that is inconsistent (where everything is true).
| rssoconnor wrote:
| While it is true that Goedel's theorem applies to weak
| systems such as Robinson Arithmetic (and any decidable
| extensions there of), The proof of Goedel's result itself
| requires at least some amount of induction.
|
| As a consequence the minimum system that Goedel's second
| incompleteness applies to is stronger than the minimum system
| that the first incompleteness theorem applies to.
| IngoBlechschmid wrote:
| This is not quite true, Godel's incompleteness theorems can
| luckily be formalized in extremely weak fragments of Peano
| arithmetic such as primitive recursive arithmetic (PRA) with
| its very limited induction principle. :-)
|
| The only position on the philosophy of mathematics I know which
| does not accept PRA is ultrafinitism.
| YeGoblynQueenne wrote:
| >> The machine was still considered impressive decades later when
| the AI pioneer Norbert Wiener played against it at the 1951 Paris
| conference,[AI51][BRO21] [BRU1-4] which is now often viewed as
| the first conference on AI--though the expression "AI" was coined
| only later in 1956 at another conference in Dartmouth by John
| McCarthy. In fact, in 1951, much of what's now called AI was
| still called Cybernetics, with a focus very much in line with
| modern AI based on deep neural networks.[DL1-2][DEC]
|
| Yeess, that's true. John McCarthy named "AI". And he wisely set
| the foundations of the field in the work of his thesis advisor,
| Alonzo Church, and the mathematicians of his generation, and the
| ones before, all the way back to Godel.
|
| That is to say, McCarthy set the foundations of AI in
| _mathematical logic_ , the branch of mathematics that began in
| antiquity by Aristotle, flourished in the Middle Ages, the
| Rennaissance and the Enlightenment with the works of Arab and
| Christian scholars, reached its peak with Leibniz and was finally
| exalted with the work of Frege, Russel, Whitehead, Hilbert,
| Tarski, Skolem, Herbrand, Godel himself, Church, Turing and
| others. The branch of mathematics that gave us digital computers,
| much like Jurgen Schmidhuber points out in his article. It is
| this work that is the only, well, logical, foundation of
| artificial intelligence. That suffices to explain why the earlier
| "cyerbnetics" branch of research fell through: because unlike
| McCarthy's AI, it was not grounded in solid theoretcial
| foundations that had already yielded such monumental results in
| mathematics and computer science.
|
| And it is the foundations of AI in logic that AI research must
| return to, eventually, because it makes no sense to throw out two
| thousand years of progress, just because an intellectual midget
| by the name of Sir James Lighthill wrote a report. It would be
| even worse to throw out such richess of knowledge in return for
| the ability to put bunny noses and ears on selfies with "neural
| networks".
| asimpletune wrote:
| Honest question, is the incompleteness theorem ever used for
| anything?
| ffhhj wrote:
| A strong AI would need a theory of incompleteness in order to
| save time when solving problems, and that's not as simple as
| saying "this program is taking more than a second to finish, I
| quit!". There must be some intuition to make the decision.
| ccity88 wrote:
| See Veritasium's video, he goes into depth about Godel's
| theorems:
|
| https://www.youtube.com/watch?v=HeQX2HjkcNo
___________________________________________________________________
(page generated 2021-06-17 23:01 UTC)