Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

On Godel theorem

  1. Oct 4, 2007 #1

    Demystifier

    User Avatar
    Science Advisor

    The essence of the 1. Godel theorem can be reduced to the fact that one can always find a self-referring sentence. It is intuitively clear that such sentences lead to problems, which, indeed, is the source of the Godel theorem. Can someone explain to me why it is not possible to construct a relatively general logical system that does NOT contain self-referring sentences? I would appreciate an intuitive, rather than a rigorous explanation, as I am not a mathematician (but a theorethycal physicist).

    If that question has already been answered, please provide me a link.
     
  2. jcsd
  3. Oct 4, 2007 #2

    Integral

    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    Read GEB,Godle Esher Bach by Douglas Hofstadter
     
  4. Oct 4, 2007 #3

    Demystifier

    User Avatar
    Science Advisor

    This book does not seem available to me. Is there something readable on-line? E.g., a summary of this book?
     
  5. Oct 4, 2007 #4

    HallsofIvy

    User Avatar
    Staff Emeritus
    Science Advisor

    That was the whole point of Goedel's proof. He constructed his self-referential sentences by using only the natural numbers: any logical system that includes the natural numbers MUST include those self-referential sentences. Of course it is always possible to construct "toy" systems, not rich enough to include natural numbers, that does not contain self-referential statements.
     
  6. Oct 4, 2007 #5

    Demystifier

    User Avatar
    Science Advisor

    Can you provide a simple (intuitive) explanation of that fact? WHY any logical system that includes natural numbers MUST include self-referential sentences? (I know it is related to the Cantor diagonalization, but I still do not fully understand it.)

    Or let me reformulate the question a little bit. Given a logical system that does include self-referential sentences, why is it not possible to make a consistent truncation of this system, by removing all such "pathological" sentences? Intuitively it seems (to me) rather simple to make such a truncation, so why exactly my intuition fails?
     
  7. Oct 4, 2007 #6
    Essentially, anything that a computer can do can be expressed in terms of simple arithmetic. And checking the validity of proofs in a logical system is something that can be done with a computer. You may be interested in my web page on this subject: http://www.tachyos.org/godel.html
     
  8. Oct 4, 2007 #7

    Hurkyl

    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    It's not clear to me what "truncation" could possibly mean in this context.

    If you mean discarding axioms -- then sure, you can keep discarding axioms until your theory is no longer self-referential. But the resulting theory is still incomplete; you started with a theory that didn't have enough provable statements, and after discarding axioms, you are left with even fewer provable statements!
     
    Last edited: Oct 4, 2007
  9. Oct 4, 2007 #8

    Hurkyl

    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    I suppose it's instructive to know examples of complete theories.

    My favorite is the theory of real closed fields, which is equivalent to Tarski's axiomization of Euclidean geometry. This theory is a complete theory!
     
  10. Oct 5, 2007 #9

    Demystifier

    User Avatar
    Science Advisor

    I mean, adding one additional axiom that says: "Self-referring sentences are not considered meaningful, so they are to be removed/ignored whenewer they appear."
    Can something like this be done in a logically consistent way?
     
  11. Oct 5, 2007 #10

    Demystifier

    User Avatar
    Science Advisor

    Is it also consistent?
    If yes, it means that the Godel theorem does not refer to theories like that. Then my question is: What is the crucial ingredient required for the Godel theorem but missing in this theory?
     
  12. Oct 5, 2007 #11

    daniel_i_l

    User Avatar
    Gold Member

    I just finished GEB and here's the general idea:
    Let's say you have some complete formal system that talks about the natural numbers (TNT = typographic number thoery), this means that every property of a number can be expressed as a theorm in TNT.
    Now for example, "0=0" would be a TNT. But we can give each character in the system a unique 3 digit number. Let's say that the number of the character '0' is 100, the number for the '=' character is 111. So the number for "0=0" is 100111100. But the fact that 100111100 is a TNT number is a property of the number which can also be expressed in TNT (since TNT is complete). Now the trick is to find a theorm in TNT whose number talks about itself. To do this we introduce two concepts:
    1)TNT proof pairs: a and a' form a proof pair if a is a number which translated back into TNT prooves the theorm that you get in TNT if you translate a'. Now, we can say that a is a theorm in TNT by saying: "there exists an a so that TNT-PROOF-PAIR(a,a')"

    2)Arithmoqining: This means that given a TNT theorm with a free variable (such as "there exists a so that a=0) and put the number of the theorm into the free variable. (if the number of 'a' is 222 then the arithmoqinization of a=0 is 222111100=0 which is false. We now we define the function ARITHMOQUINE(a,a') which means that if you arithmoquine the number of a you get a')

    Now, lets make the following TNT theorm called 'u':
    "there doesn't exist two number a,a' so that TNT-PROOF-PAIR(a,a') and ARITHMOQUINE(a'',a')"
    But if we arithmoquine this theorm we get (by inserting the number of u into the free variable a'' in u):
    "there doesn't exist two number a,a' so that TNT-PROOF-PAIR(a,a') and ARITHMOQUINE(the number of u,a')"
    Which means:
    The number you get when you arithmoquine u doesn't translat into a theorm in TNT (since it has no tnt proof pair). But the theorm we just wrote down has a number which you get by arithmoquining u, so the theorm says "I'm not a theorm"!

    I probably explained that dreadfully, so feel free to ask tons of questions about this!
    Daniel
     
  13. Oct 5, 2007 #12

    Demystifier

    User Avatar
    Science Advisor

    Thank you for the link, which is quite instructive. I believe now I have a better intuitive understanding what is going on. The crucial thing is the sentence
    unprovable(y) = ¬Ex(proves(x,y))
    In words, an x that proves y does not exist. It is quite intuitive (recall that I am a physicist, mathematicians may not consider it so intuitive) that you cannot allways prove that something does NOT exist. Namely, to prove that something does not exist, in principle you must check an infinite number of possibilities, which is impossible. (In some cases you are lucky to find a trick that proves that something does not exist without explicitly checking all separate possibilities, but there is no guarantee that such a trick always exists.) So, in essence, the Godel theorem states that for some entities you cannot prove that they do not exist. This, indeed, seems very intuitive to me and easy to accept even without a rigorous proof.

    But then my question is the following: Is it possible to build an axiomatic system that does not contain one of the words "no" or "exist"? If it is, then, in my reading, you can avoid the Godel theorem. For example, it seems meaningful to consider a system that contains only positive claims, that is, does not contain the word "no". Similarly, it seems meaningful to consider a purely constructive system, in which the word "exist" is not needed, because this word expresses that something may exist even if you cannot explicitly find it.

    I suppose that it is possible to build such an axiomatic system. But then I am confused with the claim that the "Godel theorem is valid for ANY system that contains natural numbers." Why natural numbers imply the existence of the words "no" and "exist"? Have I misunderstood something?
     
  14. Oct 5, 2007 #13

    HallsofIvy

    User Avatar
    Staff Emeritus
    Science Advisor

    How can you possibly have an axiomatic system in which things DON'T exist? And certainly if you have any axiomatic system you have the notion of "true" or "false" which is what is meant by "yes" and "no".
     
  15. Oct 5, 2007 #14

    Demystifier

    User Avatar
    Science Advisor

    I guess I have a different understanding of the word "axiomatic system". For example, a single function f(n), say
    f(n)=n+1
    is an "axiomatic system" for me. It certainly does not contain the words such as "true" and "false". I call this the axiomatic system, because the function above represents an axiom specifying the rule of attributing f(n) to a given n. Now you will say that I have also need to define what are n, so if I say that they are natural numbers, you will say that I need to specify the axioms of natural numbers, such as Peano axioms. Indeed, from
    http://en.wikipedia.org/wiki/Peano_axioms
    I see that these axioms do contain the words "no" and "exist" (see Axiom 7).
    But now my idea is to replace the Peano axioms with something different, which perhaps leads to an inequivalent definition on natural numbers, but still correctly performs the function above. Namely, I can build a machine in which the input is a sequence of dots, say
    .......
    and the output is the same with one dot more, namely
    ........
    Thus, ALL "theorems" of this system is the following set of claims
    f(0)=1
    f(1)=2
    f(2)=3
    etc, or in a different notation
    f()=.
    f(.)=..
    f(..)=...
    etc.
    Is there something wrong with it? Is something missing?
     
    Last edited: Oct 5, 2007
  16. Oct 5, 2007 #15
    If you look at the system on http://www.tachyos.org/godel/proof.html and ask 'what can I get rid of' - well if you want to get rid of 'exists' [itex]\exists[/itex], then you need to get rid of [itex]\forall[/itex] as well, which means getting rid of Ax4, Ax5, Ind and Gen. Then you have no way to talk about variables, so the integer axioms I1-I8 don't make much sense. Thus you're left with the propositional axioms Ax1-Ax3, that is the propostional calculus. This is decidable - it is essentially the same as boolean algebra.

    However, you don't need to go that far to avoid Gödel's theorem, you just need to get rid of multiplication. Then you are left with Presburger Arithmetic which is decidable.

    The thing is that if you do any of these things then you will lose the ability to talk about most things of interest, for instance there would be no way you could express Fermat's last theorem: 'There do not exist integers a>0,b>0,c>0,n>2 such that a^n+b^n=c^n'
     
  17. Oct 5, 2007 #16

    Hurkyl

    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    I think I should mention something about internal versus external --

    Modern logic is very carefully structured so that you can't literally attain self-reference. (You very quickly run into things like the Liar's paradox) The 'self-reference' here occurs by passing between internal and external statements.

    What you normally think of as a logical statement is an external statement. In the theory of integer arithmetic, the only internal objects are numbers.

    The major trick in Godel's proof is to develop formal logic purely out of integer arithmetic; he elaborates a way to treat certain numbers as internal statements, or even as internal proofs. He also provides a way to translate back and forth between external statements P and their corresponding internal statements [itex]\bar{P}[/itex].

    He then shows how to use integer arithmetic to construct the function

    IsAProof(P, X)

    which is true if and only if X is an internal proof of P. From this, it's easy to construct the "IsProvable(P)" function.


    Now, if we had an external proof X of P, then we could translate it into an internal proof [itex]\bar{X}[/itex] of the internal statement [itex]\bar{P}[/itex], and thus [itex]IsProvable(\bar{P})[/itex] is true. So, conversely, if [itex]IsProvable(\bar{P})[/itex] is false, then P must not have a proof!


    Incidentally, the converse is not true: it is possible for [itex]\bar{P}[/itex] to have an internal proof, but for P to be unprovable externally.


    You might be interested in Universal Algebra.

    A universal algebra consists only of functions and equational identities. But this is enough to define groups, rings, and vector spaces. But it has severe limitations too -- for example, you cannot define fields with universal algebra!

    (But the logic still contains words like "not" and "exist" -- you're just not allowed to use them in your axioms)


    Horn clauses are a similar sort of thing, but with wider applicability.
     
  18. Oct 5, 2007 #17

    Hurkyl

    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    Being able to identify the class of integers.

    From the set R of real numbers (or within any other real closed field), it is impossible to identify the set N of natural numbers using only arithmetic operations. Therefore, it is impossible to use the theory of real closed fields (or equivalently, it is impossible to use Tarski's version of Euclidean geometry) to talk about number-theoretic statements.

    To put it differently... it's too easy to solve equations over the reals; real arithmetic cannot be used to capture the complexity of integer arithmetic.
     
  19. Oct 5, 2007 #18

    -Job-

    User Avatar
    Science Advisor

    You would use proofs by contradiction or induction even. By Godel's incompleteness not all statements can be proved from a set of axioms, but unless they fall under that category these types of proofs are very elligible.
    That's one way how lower bounds are proven in algorithm complexity analysis, for example.
     
  20. Oct 6, 2007 #19
    This was the whole point of Principia Mathematica by Alfred Whitehead and Bertrand Russell. They went to great pains to make sure NO "level" could talk about other "levels" and therefore self-reference is impossible. That was the objective.

    The problem was that Godel proved that for any system that was powerful enough for arithmetic (a few logical axioms, addition, multiplication, exponentiation, successor, subsistution, about all), the Godel sentence which is self referencing is constructible.

    That is exactly right! You would avoid the Godel sentence/theorems, but you would not have a system capable of arithmetic. Sentential Logic is reducible to 'not', 'or', and atomic letters. That's all. Godel's theorem does not apply. You can prove its consistency and completeness. When you add quantifiers, meaning 'all' or 'at least one' (existential), it gets more complicated. When you have all the things that PA has, you obviously get to Godel's theorem.

    Systems stronger than PA can prove the consistency of PA, but there is no point because that system's consistency is suspect. Bob may say that Frank is telling the truth, but if you aren't confident that Bob is telling the truth, then what's the point?

    I don't know about that truncation technique. I don't know what it means to "remove" sentences. They are constructible in the language, so you need to modify your axioms. If you do that, you make a system stronger than PA which may not have a PA-Godel sentence, but will have its very own.

    Self-reference is necessarily possible when you get to the strength of PA and above. You throw out exponentiation, you're fine. Throw out quantification, fine too. I don't know every way, but I remember that the Godel sentence uses basically everything PA has.
     
  21. Oct 7, 2007 #20
    You don't need to define exponentiation in your system, addition and multiplication are enough. The thing is that although multiplication is repeated addition and exponentiation is repeated multiplication, repetition is not defined within the system. What Gödel saw was that once you had multiplication as well as addition, then there was a trick to simulate repetition, and so give access to any computable function.
     
Know someone interested in this topic? Share this thread via Reddit, Google+, Twitter, or Facebook

Have something to add?



Similar Discussions: On Godel theorem
Loading...