DavidCooper wrote:
It is wrong nonetheless. The error comes from taking "this statement is true" to be true and then using that same incorrect handling of infinite recursion elsewhere.
That sentence has nothing to do with what 'Gödel's theorem' states;
Gödel's Incompleteness theorems (plural) aren't about infinite recursion at all. You seem to be confusing them with
von Neumann's Catastrophe of Infinite Regress, except that that isn't about mathematics in any way, being more of an informal statement about the physical sciences (it is about the limits of certainty, specifically about how precisely we can measure the accuracy and precision of physical measurement devices when the devices we are measuring them with are themselves physical devices).
Or perhaps you are thinking of
Turing's proof that the
Halting Problem is undecidable, which does involve an infinite loop (though not quite the one you are discussing). More on this, and how it relates to Gödel's theorems, later.
Gödel's theorems are actually about the limits of how much we can
formalize and
mechanize the process of mathematical logic, which was of considerable interest to axiomatic formalists such as David Hilbert, who was the leading logician of the 1920s - Gödel was trying to show that the
Hilbert program (a project to formalize all of mathematics in terms of predicate logic) was feasible, but ended up showing that it wasn't. It is also why most logicians these days have dropped the idea of axiomatic formalism, at least in the strictest form.
What Gödel's Incompleteness Theorems state (giving it in very general, non-mathematical terms) is that, for a given formal symbolic logic system
P capable of expressing
Peano arithmetic (or some other equivalent formulation of basic arithmetic) together with sets and functions (the so-called 'sufficient strength' clause, which is a bit more specific than what I am saying, but bear with me), entirely in terms of logical predicates (i.e., a series of logical propositions, and a set of rules for applying transformations on those propositions), there either exists a proposition
G which can be produced within system
P, while at the same time the proposition
¬G ('not
G') can also be produced within
P (i.e., a direct contradiction),
or else there must exist a true predicate
Q which cannot be proven within the rules of
P through purely formal means (i.e., transforming existing propositions according to a strict set of rules, without interpretation of what those rules mean). In other words, that any formal predicate logic system is either inconsistent (it allows a contradiction) or incomplete (it is incapable of proving some true propositions).
(The connection to
Russell's Paradox - which was about '
naïve set theory' (the earliest formulation of set theory; the paradox was meant to demonstrate that Cantor's original model of sets was flawed, and succeeded in that), not propositional logic, though it was used in the debate over the topic later - was that Bertrand Russell also tried to prove Hilbert's thesis, by trying to show that you could alter the rules of set theory to eliminate the paradox. His approach was basically the same one you are taking, of eliminating such contradictions by forbidding recursive sets. IIRC, one of Gödel's Theorems show that this approach always leads to incompleteness.)
The proof itself is often explained through an analogy to
Epimenides' Paradox (the assertion by a Cretan that "All Cretans always lie", or more generally, 'this statement is
false' - not, as you keep saying, 'this statement is true') because the proof shows that, in any logical calculus which is complete, you can construct a statement which is true if and only if the statement is simultaneously false (i.e., that any complete logical calculus is also inconsistent). However, it is not actually
about Epimenides' Paradox, it is simply similar to it in some ways.
A large part of the problem, and why the theorems were such a shock to logicians when they were published, came from the fact that logicians
were interpreting the meaning of the transformations, and that they kept letting bits and pieces of that interpretation slide into their work - that is to say, they kept cheating without realizing it. In
Gödel, Escher, Bach, AI researcher
Douglas Hofstadter compares this to how non-Euclidean geometry was a shock to mathematicians in the early 19th century - the problem wasn't that they were wrong about the geometry so much as that they were assuming properties of concepts such as 'point' and 'line' which did not actually come out of the mathematics, because the mathematics defined them in a more abstract way than a human being would naturally view them.
Hofstadter explains all of this pretty thoroughly in that work, but in a way that most people have difficulty following without a lot of careful reading, and the book is so dense and nuanced that few can get through the whole thing - it is to computer science what
Finnegan's Wake is to literary criticism. I can easily see how one could come away from it with an incomplete impression of what Gödel's theorems say (I certainly did the first dozen or so times I tried reading it).
As an aside, I'd like to point out that early in the book, Hofstadter includes the whole of Lewis Carroll's
"What the Tortoise said to Achilles", a dialogue about what mathematical proofs mean, if anything - which leads me to think that this is what you were thinking of when you misquoted Epimenides' Paradox as 'this statement is true', because Carroll used just such an infinite regress as a
reducto ad absurdum for mathematical formalism in general. It went something like this:
Quote:
"B implies A, so if B is true, A is true."
"Ah, but how do I know if this assertion that B implies A - let's call it 'C' - is itself true?"
"Well, OK, if I prove C is true, and B is true, will you accept that A is true?"
"Of course not! How do I know that the assertion that C is true - which I will call 'D' - is itself true?"
the dialogue trails off ad infinitum
This sounds a lot like what you think Gödel's theorems say, but it isn't really related except in very general ways.
Getting back on track... I don't have the mathematical background to explain this in greater depth, but the really important part is that Gödel's theorems are only relevant if you are trying to formalize a system of logic through a purely mechanical process. They have broad implications about formal systems in general, but little direct import on most other things. Whether they have any on AI is an open question, probably depending on whether AI can be built solely through formal logic - so far, that hasn't worked out, and I am not aware of anyone taking that approach these days (you don't seem to be going in quite that direction yourself, from the sounds of it, as you aren't basing your work on first-order logic in the usual sense).
In a nutshell, there's no need to be concerned with the proof itself regarding AI, because if 'Natural General Stupidity' is anything to go by, there's no reason to think an intelligent system must, or even can, be both logically complete and logically consistent.
(All this assumes that intelligence is a meaningful concept. I have my doubts about that
fnord. Certainly the idea of
measuring intelligence is pretty flawed, but then we're no longer talking about Hofstadter, we're now referencing
Stephen Jay Gould instead...)
Aside from the basic demonstration that there are limits to computability and decidability (not a small thing in and of itself), the part that is relevant to computer science - the
meta-circular encoding of logical assertions as numeric values - isn't particularly related to the theorems themselves, as (IIUC) other formulations of the proofs which don't rely on it had already been published before Gödel's death (in much the same way reformulations of the derivative as the limit of a function at a point had been developed during Newton's lifetime), but it became important in an unrelated way because Turing took the idea when creating the
Universal Turing Machine formalization, while in parallel to this,
Alonzo Church used it in constructing the
Lambda Calculus, as well as in his later proof that the UTM and LC were of equivalent expressive power as methods of computation.
Turing came up with the UTM while trying to solve the Halting Problem, which is the question of whether their exists an
a priori method for determining if any arbitrary algorithm would eventually go to completion for any given input. He started by showing that you could construct a very simple hypothetical device - a simple Turing Machine - which could compute a specific algorithm with a limited set of operations and a starting data set. He then used Gödel's idea of encoding functions as mathematical statements to show that he could 'build' a Turing Machine whose mathematical operation was "take as your starting data an encoded description of a simple Turing Machine and compute its algorithm" - in other words, a
Universal Turing Machine.
Taking this demonstration that at least
some algorithms could be encoded as mechanical operations, he then postulated that if one could construct a describable Turing Machine
H implementing an algorithm (in modern computer programming terms, a function or procedure) which took another Turing Machine's (e.g., function's) description and determine whether if would ever reached its end state for a given input, then
H would be a solution to the Halting Problem.
However, he then argued that if you constructed a Universal Turing Machine data set
T which took the UTM description for
H, another Turing Machine description
F, and a datset for
F, and computed the operation, 'if H(F(s)) halts in a finite time, repeat', and then applied
T(T), it would never halt, contradicting the test results, and thus showing that creating a general halting test function was undecidable. This also may be what you were confused about regarding the idea that Gödel's Theorems involve an infinite recursion.
Later still, Church and Turing worked together to prove that two other formal models of computation,
general recursive functions and
Post productions, were also of equivalent power to the Universal Turing Machine, which led them to the
Church-Turing Thesis, a conjecture that they all represented a limit of computational power itself - that is, that anything which could be formally computed, as opposed to guessed at or surmised, could be computed by any of those models, and nothing which can't be computed by them is not computable in finite time and finite memory by means of formal mathematics.
This is where the concept of '
Turing equivalence' comes from, as well as the related ideas of '
Turing Completeness' (which describes a programming language which is, in principle, capable of computing anything a UTM could; in practice, since all real-world computers have finite memories and computation speeds, they are actually equivalent to a
Linear Bounded Automaton, but that's usually handwaved as overly pedantic) and the '
Turing tarpit' (that a language could be theoretically Turing complete, but be entirely impractical for actual use - this is where a lot of the
esolangs such as
Thue,
Unlambda, and
Brainf**k get their humor, such as it is).
(
EDIT: Oops,
INTERCAL isn't a Turing Tarpit as such, since it isn't a
minimal Turing complete system. I replaced the reference with one to Thue instead, which
is considered a
Turing Tarpit class language.)
While it is probably an undecidable proposition itself, so far the Church-Turing Thesis has held, at least for any sequential system with finite resources (there are a few hypotheticals about algorithms which can be solved in finite time with an infinite number of parallel UTMs, but not a single UTM, such as the so-called
Parallel Infinite Reduce, but obviously they only serve as thought experiments).
Note that Turing-completeness is no big feat - things as disparate as Postscript markup, TeX markup, C++ templates, Game of Life,
Minecraft (since you can
create a working simulation of a register machine within the game world), the
Magic: The Gathering card game (no, seriously, it's
provably TC), and a number of
One-Instruction Set Computers (which we all heard far too much about from Geri last year) are all Turing Complete systems, being in principle capable of computing anything that can be computed. However, there are a number of things which you'd expect would be Turing complete which aren't, so it isn't entirely a trivial matter. Still, it is rare for there even to be any question of whether a programming language is or not; basically, if it can perform basic arithmetic, perform some sort of test of a variable's value (e.g.,
x == 1), and either a) an indefinite loop (i.e., a
while loop), b) a backwards conditional branch (i.e., an
IF ... THEN jumping to some point earlier in the code), or c) a guarded recursion, it is pretty much a certainty that it is Turing complete.
(That combination - which can be reduced to the instruction 'subtract and branch if negative' - was the first OISC demonstrated, proving that such a thing was theoretically possible; the operation is roughly parallel that of the notional read/write head of a Universal Turing Machine.)
So, yeah... that's a lot to unpack, I know.
Everything is deeply intertwingled fnord.