Explaining Godel's Theorem: Intuitive Explanation w/o Math

[Demystifier]

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.

 

[Integral]

Read GEB,Godle Esher Bach by Douglas Hofstadter

 

[Demystifier]

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

 

[HallsofIvy]

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.

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.

 

[Demystifier]

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.

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?

 

[chronon]

Can you provide a simple (intuitive) explanation of that fact? WHY any logical system that includes natural numbers MUST include self-referential sentences?

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

 

[Hurkyl]

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?

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!

 

[Hurkyl]

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!

 

[Demystifier]

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

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?

 

[Demystifier]

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!

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?

 

[daniel_i_l]

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 theory), 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, let's 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

 

[Demystifier]

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

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?

 

[HallsofIvy]

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.

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".

 

[Demystifier]

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".

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?

 

[chronon]

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' $\exists$, then you need to get rid of $\forall$ 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'

 

[Hurkyl]

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 $\bar{P}$.

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 $\bar{X}$ of the internal statement $\bar{P}$, and thus $IsProvable(\bar{P})$ is true. So, conversely, if $IsProvable(\bar{P})$ is false, then P must not have a proof!


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

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.

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.

 

[Hurkyl]

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?

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.

 

[-Job-]

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.)

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.

 

[codec9]

Can someone explain to me why it is not possible to construct a relatively general logical system that does NOT contain self-referring sentences?

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.

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.

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.

 

[chronon]

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.

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.

 

[codec9]

You need exponentiation for the Proof function.

 

[chronon]

You need exponentiation for the Proof function.

But you can define exponentiation in terms of addition and multiplication as follows:

$y=x^n$ is equivalent to
$\exists v(y=\beta(v,n)\wedge\beta(v,0)=1\wedge(1\leq i\leq n\Rightarrow \beta(v,i)=\beta(v,i-1)))$

where $\beta$ is the Gödel beta function as described in http://math.yonsei.ac.kr/bkim/goedel.pdf

 

[codec9]

Oh, we weren't really disagreeing. Sorry. I never learned about beta in PA, but in Turing Machines and Abacuses one can work out exp in terms of addition and multiplication, and further multiplication in terms of addition. In PA, assuming beta works exp is not explicitly needed, but in Turing and Ab., neither exp nor multiplication is. I know these three get to the same power (and limitation), so I am not sure why the discrepancy is not a problem.

 

[Hurkyl]

in Turing Machines and Abacuses one can work out ... multiplication in terms of addition.

Actually, you can't -- you are capable of computing individual products, but you cannot work out the theory of multiplication.

The language $\mathrm{Th}(\mathbb{N}, +)$ of true statements about integer addition is a decidable language, whereas $\mathrm{Th}(\mathbb{N}, +, \times)$ is not.

If you prefer the logical perspective, Presburger arithmetic is a theory of integer addition that is complete.

 

[codec9]

I don't know what you mean by theory of multiplication. I realized, though, that it does not matter where the different systems start but what they are capable of.

Off the top of my head you can multiply x and y by copying y to the left then adding the left y to the right x times. You delete x from right to left so that you can check if x is done by going to the right of the left y and seeing if you get the 2nd zero where a x stroke should be. It is multiplication in terms of addition because you are adding y to y x times. If this is what you mean by computing individual products, what would make it a 'theory' of multiplication?

 

[Owen Holden]

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.

Wrong. Self-referring statements are not always a problem. See: Quine, New Foundations,
Quine Mathematical Logic.

V=df {x:x=x}.
ie. (V e V) is not a problem for Quine.

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).

Russell's theory of types does exactly that.

That there are undecidable propositions within a logic that can deal with elementary arithmetic is obvious. The axioms of such a logic are not decidable.

 

[Big Red Dog]

Formal System w/o self-references

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.

Well, basically whenever you want to have a formal system which is interesting/useful, you *must* have some kind of self reference.

For instance, it's hard to demonstrate anything on Integers if you don't allow yourself to use recurrence (i.e. for a given property P, if P(n) --> P(n+1) and P(0) then P is true for all N).

Similarly, not allowing recurrence in the realm of computer languages would amount to forbidding any means to "loop" ... Hard to define something as simple as factorial or even a sort function...

 

[Big Red Dog]

Truncating or Adding axioms

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!

Well, not always. Presburger arithmetic (roughly "our" arithmetic but without the multiplication ) is complete (for any statement A, either A or NOT A is a theorem), consistent (you can never derive both A and NOT A) and decidable (a computer can prove in finite time if A is a theorem or not)

That's funny because usually people are tempted to ADD axioms. For instance upon discovery of an undecidable assertion, one can choose to have it as an additional axiom. But Gödel showed that you would end up with the same problem: you could build a different yet still undecidable assertion.

 

[Big Red Dog]

Consistent, Complete and Decidable "usual" arithmetic

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?

Actually you have a good point. You can decide for instance that "your" arithmetic is defined only on say the first million of integers. In which case you don't need any problematic axiom, and you can demonstrate or invalidate just any property by going over each number one at a time...

After all, most computers nowadays don't implement "Big Integer" and nobody seems to care ...

You could also define some notion of Real, by stipulating say that between 0 and 1 you have One million + 1 element: you would call this number Aleph1 since it's not an Integer :)

 

[Hurkyl]

Well, not always. Presburger arithmetic (roughly "our" arithmetic but without the multiplication ) is complete (for any statement A, either A or NOT A is a theorem), consistent (you can never derive both A and NOT A) and decidable (a computer can prove in finite time if A is a theorem or not)

It's a rather easy to prove that you cannot make an incomplete theory complete by removing axioms. If you have a subset of the axioms, then you only have a subset of the theorems.

The completeness of Presburger arithmetic comes from its restricted language. All of the undecidable propositions of number theory involve multiplication. Presburger does not explicitly have a multiplication operator and is incapable of constructing one. It achieves completeness not by removing axioms, but by reducing the number of statements in its language.

That's funny because usually people are tempted to ADD axioms. For instance upon discovery of an undecidable assertion, one can choose to have it as an additional axiom. But Gödel showed that you would end up with the same problem: you could build a different yet still undecidable assertion.

Not quite correct; you can add enough axioms to build a complete theory (i.e. all statements are provable). The problem is that you cannot do it in a recursively enumerable way.

 

[Big Red Dog]

It's a rather easy to prove that you cannot make an incomplete theory complete by removing axioms. If you have a subset of the axioms, then you only have a subset of the theorems.

"Complete" does not mean that you can demonstrate "everything" just that every sentence S either S or NOT S is a theorem.

The completeness of Presburger arithmetic comes from its restricted language. All of the undecidable propositions of number theory involve multiplication. Presburger does not explicitly have a multiplication operator and is incapable of constructing one. It achieves completeness not by removing axioms, but by reducing the number of statements in its language.

Let's see:

The 5 axioms of Presburger:

1. p7: No number has 0 as a successor
2. p8: Successor is injective: Sx=Sy --> x= y
3. x + 0 = X ;;
4. x + Sy = S(x + Y) ;; addition
5. p9: Induction

Apprentely Presburger is a subset of Peano ... Note: p7,p8, p9 refers to the Numbering of Peano axioms in http://en.wikipedia.org/wiki/Peano_arithmetic#The_axioms

Not quite correct; you can add enough axioms to build a complete theory (i.e. all statements are provable). The problem is that you cannot do it in a recursively enumerable way.

You're absolutely right. But since I cannot do it r.e. what would be the point? :)

 

[Hurkyl]

"Complete" does not mean that you can demonstrate "everything" just that every sentence S either S or NOT S is a theorem.

If a given theory contains neither S nor (not S), then the same is true of all of its subtheories.

In terms of generators... if neither S nor (not S) are provable from a given set of axioms, then the same is true for any subset of that set.

Let's see:

The 5 axioms of Presburger:

1. p7: No number has 0 as a successor
2. p8: Successor is injective: Sx=Sy --> x= y
3. x + 0 = X ;;
4. x + Sy = S(x + Y) ;; addition
5. p9: Induction

Apprentely Presburger is a subset of Peano ... Note: p7,p8, p9 refers to the Numbering of Peano axioms in http://en.wikipedia.org/wiki/Peano_arithmetic#The_axioms

You linked to a formalization of second-order Peano arithmetic. Not only does that yield an expanded language (you have propositional variables), but it introduces additional rules of deduction, so it's not even the same logic.

There is an explicit first-order formalization of Peano arithmetic later in that link (here).


IMHO, the situation can be most cleanly stated in terms of computability: for any model N of the natural numbers, the relevant theorems are that Th(N, +) -- the set of statements about + that are true in N -- is turing decidable. However, Th(N, +, *) is not turing decidable.

You're absolutely right. But since I cannot do it r.e. what would be the point? :)

If we're going to make true statements, we cannot neglect the cases we don't like.

Furthermore, recursive enumerability is not always relevant, and things can be more easily presented without imposing that restriction. For example, the simplest way I've ever seen to set up nonstandard analysis is to formulate the first-order theory starts as follows:

Let V be the superstructure built upon R. ($V = \bigcup_{i \in \mathbf{N}} \mathcal{P}^i (\mathbf{R})$)

Define a language L whose constant symbols include every element of V, and with the single binary relation symbol $\in$. (There is an obvious way to define an interpretation of L in V)

Define a first-order theory for L whose statements are precisely those that hold in V.

 

[Big Red Dog]

If a given theory contains neither S nor (not S), then the same is true of all of its subtheories.

In terms of generators... if neither S nor (not S) are provable from a given set of axioms, then the same is true for any subset of that set.

Ok, I made a fool of myself, I didn't realize that in Press. Arithm. all the pieces were actually moving (downsized): less theorems, restricted language, different model.

IMHO, the situation can be most cleanly stated in terms of computability: for any model N of the natural numbers, the relevant theorems are that Th(N, +) -- the set of statements about + that are true in N -- is turing decidable. However, Th(N, +, *) is not turing decidable.

Yep, much better/more clear since it refers to the model.

If we're going to make true statements, we cannot neglect the cases we don't like.

Well, it's more important for people to remember that just adding a theorem found undecidable is not going to solve the issue rather than to know about a technicality? (I know, I know ... :) )

Furthermore, recursive enumerability is not always relevant, and things can be more easily presented without imposing that restriction. For example, the simplest way I've ever seen to set up nonstandard analysis is to formulate the first-order theory starts as follows:

Let V be the superstructure built upon R. ($V = \bigcup_{i \in \mathbf{N}} \mathcal{P}^i (\mathbf{R})$)

Define a language L whose constant symbols include every element of V, and with the single binary relation symbol $\in$. (There is an obvious way to define an interpretation of L in V)

Define a first-order theory for L whose statements are precisely those that hold in V.

Showing off on both accounts of HTML and mathemathical wizardry, huh? :)

Actually now that you're mentioning it, non-standard analysis is a great way to demonstrate that Gödel's incompleteness theorems might have had a much lesser impact on the world than one could have thought: physicians were heavily using infinitesimal calculus before Robinson, so who cares if something is not properly defined/axiomatized/demonstrable? ;)

 

[gel]

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).

The following is the argument that I thought of when first thinking about Godel's incompleteness theorem, and it was enough to convince me that it can't be avoided in any way. It's similar to the proof of the Halting problem.
Suppose I have a computer program that takes a computer program as an input (say, as a plain text file) and returns one of the following
i) "Input program terminates."
ii) "Input program never terminates."
iii) Or, the main program itself never terminates.

Also suppose that the output is always correct. i.e. If (i) is output and you run the program in the text file then it will indeed terminate, and if (ii) is output then the program in the text file will never terminate.

Then, by the standard method of proof of the Halting problem, it is possible to construct a program which never terminates, but when fed as an input into the main program above will lead to situation (iii).

Suppose that we have a system of logic in which it is possible to state whether or not a program terminates, and which is consistent so that it never says that a terminating program doesn't terminate or vice-versa. You could then write a program that takes in the given text file and simply checks all possible proofs that the input program terminates or not. By the argument above you could feed in a program that causes (iii), so that you know it never terminates but which cannot be proven under the logic system.

So, my conclusion is that any system of logic which is rich enough to be able to make the statement "program P terminates/does not terminate", is consistent, and whose proofs could be enumerated & checked by computer must be incomplete and, furthermore, contains statements that you know are true but cannot be proven within the logic system.

I think Godels proof works because statements of this form "program P terminates" can be converted into statements about the natural numbers.

 

[epenguin]

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.

That was just what I meant to ask about! I had read in a Scientific American article, almost as an aside, that arithmetic can be proved consistent as long as you don’t have multiplication (and its inverse, division) in it.

BTW That would mean it can prove its own consistency within its own axioms. OK?
That is also true of projective geometry OK?
? Does that mean you could have a finite machine that can prove any theorem within these systems in a finite time or have I confused issues? If not, why doesn’t someone make such a machine?


Anyway the problem I always had about multiplication is I could never see why it is said to be a separate fundamental operation like an axiom.
Multiplying n by m is just adding n to itself m-1 times! As far as I can see you could specify an algorithm involving just the notions that are in the numbers, succession etc., and addition - define multiplication within those axioms etc.. So if you can assume addition by my reasoning you would have the whole of arithmetic.

But if I have missed something about multiplication, why is raising to a power, n^m being just multiplying n by itself m-1 times completely by the same form of definition as multiplication above, not also a fundamental independent operation or axiom?