THE LATE (hi twerp) Raymond Smullyan's trick (below explained by THE LATE ;) Tom Etter) demonstrates the essential triviality of Godel incompleteness. It's a lot more interesting to investigate the essential non-triviality of directed cyclic graphs of NOR gates.
Godel’s Theorem in a Nutshell(1) By Tom Etter Boundary Institute October, 2001 How did you learn what you know about English grammar? Probably by hearing your teacher talk about it in English, or by reading about it in English, or both. English, like all modern languages, can describe its own grammar. Godel’s theorem is a very surprising discovery about such languages. What it says is that they all contain certain propositions about their own grammar whose truth is perfectly obvious to anyone who understands them, but which their self-described rules of grammar cannot formally disclose. This theorem is easily converted into a theorem about numbers; in fact, that’s the form in which Godel discovered it. What it says in this form is that that there are certain obvious-to-us facts about numbers that can’t be proved from the usual axioms for arithmetic. It’s not that these axioms are too weak; on the contrary they are too strong, so strong that they give us the power to encode the grammar of the language of arithmetic in arithmetic itself. Adding the unprovable true statements as new axioms doesn’t help, it just makes other obviously true statements unprovable. The essence of Godel’s theorem is not about numbers, however, but about language, and the limits imposed by logic alone on the ability of language to describe itself. Just what is a proof? Philosophers and mathematicians argued about this for thousands of years. For a starter, a proof is a sequence of statements leading from a premise to a conclusion. But how do we know that the steps in such a sequence are valid? This question was finally answered once and for all at the turn of the twentieth century when logicians discovered certain simple and universal rules for valid steps in a proof that refer only to the outward form of these steps. These rules are implicit in the grammar of all of the languages we speak; what modern logic has done is to make them explicit and devise several very efficient vocabularies for stating them. The details can be found in any logic book, so I’ll say no more here. English refers to its own expressions in a number of ways. The most straightforward way is to name them by putting them in quotation marks. Once letters and words have names, we can talk about various ways of combining them. For instance, we can talk about the result of writing ‘ dog’ after ‘hot’, which is of course ‘hot dog’. Another very useful thing we can do is make up new short words for long expressions that we want to use often. Let’s do this right now: we’ll write ‘x + y’ in place of the expression ‘the result of writing y after x’. Thus ‘hot dog’ is ‘hot’ + ‘ dog’. This brings up another trick, which is to add letters like ‘x’ and ‘y’ to our temporary vocabulary as new pronouns to add to the list ‘it’, ‘this’ and ‘that’. Finally, and this is important in our present enterprise, we need to find an efficient way to talk about expressions that contain quotation marks. We can’t just enclose them in quotation marks, since that would lead to ambiguities. The same problem arises in computer programming, where it is solved by referring to the quotation mark as the character having the ASCII number 34, abbreviated Chr(34). We’ll borrow this solution. Thus Chr(34) + ‘dog’ + Chr(34) will refer to the five letter expression consisting of ‘dog’ in quotation marks. With these new rules in mind, we are finally off to the races. Let A be some statement that we are assuming. This can be a list of self-evident axioms, or a hypothesis assumed for the sake of investigating where it leads, whatever. Let x be any expression. We’ll now define a certain property of x relative to A that we’ll call the Godel property, abbreviated Godel(x,A), defined by the statement x + ‘(‘ + Chr(34) + x + Chr(34) + ‘, A)’ is unprovable from A. Now since provability from A means that there is a sequence of expressions of a well-defined kind leading from A to x, this property Godel(x, A) of x is perfectly well- defined; either there is such a sequence or there isn’t. This will be the case whatever x may be. Let us then take x to be the expression ‘Godel’. Godel(x, A) then asserts that Godel(‘Godel’, A). Unpacking this expression according to the above definition involves substituting the word ‘Godel’ in quotes for ‘x’ in it, which yields: ‘Godel’ + ‘(‘ + Chr(34) + ‘Godel’ + Chr(34) + ‘, A)’ is unprovable from A. Before reading any further, please get out a pencil and paper. Now look at the above line and carefully write down the expression that the above line says is unprovable from A. Be very literal in following these three simple rules: if you see something in quotes, write down what’s inside the quotes; if you see the name ‘Chr(34)’ of the quotation mark character, write down a quotation mark, it you see a plus, keep writing. What do you get? Let’s call what you get the Godel statement. OK, then, so what does it mean to say that Godel(‘Godel’,A)? It means that what you have just asserted is itself unprovable from A. That is, it asserts that no chain of valid steps will lead from A to this self-referential assertion that we are calling the Godel statement. Suppose, for instance, that A is the statement ‘The Giants will win the pennant.’ The Godel statement is then clearly unprovable from A, since you can’t deduce statements about grammar from statements about baseball. Since the Godel statement asserts of itself that it is unprovable, it is true. No surprise there. Suppose, however, that A is a statement of what constitutes a valid proof. That is, given any expression E that begins in a premise P and ends in a conclusion C, from we can conclude from A whether E is a valid proof or not. More than that, we can prove our conclusion, i.e. we can construct a proof that begins with A and, if E is provable, ends with ‘C is provable from P’, or if E is not provable, ends with ‘C is not provable from P’. Knowing what a proof is, we know what a theorem is, namely a statement that comes at the end of a proof. If, given certain axioms and infinite patience, we want to know whether T is a theorem, we can simply keep testing expressions for proof-hood; if we find a proof, T is a theorem, if we keep trying for all eternity and never find a proof, it is not. This, in principle, would work for any expression T, so, given a set of axioms, being a theorem is a well-defined property on the class of all expressions. Suppose we take A as our axiom set. Then our theorems will be true statements about provability. Since A defines what we mean by provability, it seems obvious that all true statements about provability must be among these theorems. After all, A says what provability is; what possible basis could there be for deciding the truth or falsehood of a statement other than whether or not it is derivable from A? But let’s now consider the Godel statement. Is it provable? Is there a chain of valid steps leading from A to Godel(‘Godel’,A)? If there were, then Godel(‘Godel’,A) would be a theorem and hence what it says would be true. But what does it say? That it itself is not provable! This proves that the Godel statement is unprovable. But we clearly see that it is true. Clearly, then, there is a basis for deciding the truth of statements about provability other than their being derivable from how provability is defined. That basis is the human understanding. This is Godel’s theorem in a nutshell. Coda. Since the Godel statement is obviously true, why don’t we simply add it to A as another axiom? This, in fact, works just fine, making Godel(‘Godel’,A) both provable and true. But it also enlarges the axioms for provability into a new set B, which creates a new unprovable true statement Godel(‘Godel’,B). As remarked before, the problem is that not that our axioms for logical grammar are too weak, but that they are too strong. New axioms can indefinitely expand the domain within which logical grammar is complete, but they can never end its incompleteness. 1. The basic trick used here for self-reference was discovered by Raymond Smullyan. On Sat, Nov 13, 2021 at 8:55 AM James Bowery <[email protected]> wrote: > > "head up its ass" is a cute aphorism for the ancient concept of Maya but doesn't really reflect the rigorous reformulation that Godel owes us. > > On Sat, Nov 13, 2021 at 7:10 AM Quan Tesla <[email protected]> wrote: >> >> Godel might muse that even a system with its head up its ass cannot know itself to completion. >> >> On Sat, Nov 13, 2021 at 8:43 AM James Bowery <[email protected]> wrote: >>> >>> What would Godel say about a NOT gate with its input connected to its output? >>> >>> On Fri, Nov 12, 2021 at 9:28 PM Quan Tesla <[email protected]> wrote: >>>> >>>> Gödel's incompleteness theorum still wins this argument. However, what really happens in unseen space remains fraught with possibility. The question remains: how exactly is this relevant to AGI? >>>> >>>> In transition, energy is always "lost" to externalities. Excellent design would limit such losses to not impact negatively on internal functionality. E.g., Losses can be recycled for reuse, and so on. It all depends on the relevance of the dynamical boundary that was either set, or which emerged. >>>> >>>> Even so, the "lossy" argument should be finite. As a system, its boundaries of argument should also be maintained. This remains true for all systems, even systems of systems. As such, it's more a function of a design decision, than an incomplete argument. >>>> >>>> On 12 Nov 2021 20:41, "James Bowery" <[email protected]> wrote: >>>>> >>>>> >>>>> >>>>> On Fri, Nov 12, 2021 at 6:27 AM John Rose <[email protected]> wrote: >>>>>> >>>>>> ... >>>>>> >>>>>> While these examples may sound edgy, often these incompleteness's are where there is much to be learned. Exploring may help some understandings especially, as James pointed out, that “AIXI = AIT⊗SDT = Algorithmic Information Theory ⊗ Sequential Decision Theory". >>>>> >>>>> >>>>> AIXI reduced the parameter count of an AGI with unlimited computation but limited information. Before you jump all over the fact that it is necessary to limit the computation, we still need to talk about the remaining open parameters in AIXI. In AIT the open parameter is: "Which Turing Machine?" In SDT the open parameter is "Which Utility Function?" >>>>> >>>>> To answer "Which Turing Machine?" I've intuited an approach that Matt reduced to a pretty restrictive descriptive space of NOR DCGs. This reduces what might be thought of as the descriptive space of Turing Machines to what Matt formalized. It doesn't get rid of _all_ of the unknowns in that space, but it is far more rigorous than the descriptive space of all UTMs. There is a _lot_ of work to be done with this approach and advances will, IMNSHO, have immediate and profound application in logic design. >>>>> >>>>> To answer "Which Utility Function?" we must become a lot more philosophically serious than has heretofore been the case in all the brouhaha about "friendly AI". >>>>> >>>>> Hutter's paper "A Complete Theory of Everything (will be subjective)" is his (still incomplete) approach to addressing what you refer to as "these incompleteness's". >>>>> >>>>> Now, having said all that: Yes, the measurement level of abstraction does get into the economics of computation resources and, yes, it would be nice to find approaches that obviate all of the above "incompletenesses", but you must do better than to redefine the words "lossy" and "lossless" compression as that merely hobbles an existing approach to these incompletenesses while at the same time threatening to hobble their practical applications by confusing the meanings of words. >> >> Artificial General Intelligence List / AGI / see discussions + participants + delivery options Permalink ------------------------------------------ Artificial General Intelligence List: AGI Permalink: https://agi.topicbox.com/groups/agi/T5ff6237e11d945fb-M649278c503335d1ca532f903 Delivery options: https://agi.topicbox.com/groups/agi/subscription
