Godel's incompleteness; result of implication?

[friend]

I'm not an expert in mathematical logic by far. But I understand that Godel's incompleteness theorem states that there can be some statements in an arithmatical system that are true but cannot be proven by that system.

But that sounds like an implication. For part of the definition of an implication is that a true conclusion can proceed from a false premise. In other words a true statement can proceed from a false premise, or no true premise... or a true statement without something to prove it is true.

So it sounds like Godel's proof might start out with things being equivalent, but there might be implication introduced somewhere so that the conclusion (about a true statement) might also precede without something to prove it, as well as might procede from something that does prove it. That would only prove that Godel intoduced implication in his proof, right?

 

[CRGreathouse]

I don't understand. Could you rephrase, or maybe give an example of what kind of implication you mean?

 

[sylas]

I'm not an expert in mathematical logic by far. But I understand that Godel's incompleteness theorem states that there can be some statements in an arithmatical system that are true but cannot be proven by that system.

Yes; any formal system expressive enough to represent arithmetic is either incomplete or inconsistent.

Incomplete means that there are statements S where the system cannot prove either S or (not S).

Inconsistent means that there are statements S where the system can prove both S and (not S).

But that sounds like an implication. For part of the definition of an implication is that a true conclusion can proceed from a false premise. In other words a true statement can proceed from a false premise, or no true premise... or a true statement without something to prove it is true.

I don't know what you mean. Godel's theorem is pretty sophisticated. Note that you CAN can provide complete and consistent formal systems for simpler models.

Specifically, consider formal statements involving multiplication and addition of real numbers. There IS a formally complete and consistent logical system for such statements.

But there is no complete and consistent logical system for statements involving multiplication and addition of integers.

So Godel's theorem is not just something weird about "implication".

So it sounds like Godel's proof might start out with things being equivalent, but there might be implication introduced somewhere so that the conclusion (about a true statement) might also precede without something to prove it, as well as might procede from something that does prove it. That would only prove that Godel intoduced implication in his proof, right?

Certainly not.

Cheers -- sylas

 

[Phrak]

I'm not an expert in mathematical logic by far. But I understand that Godel's incompleteness theorem states that there can be some statements in an arithmatical system that are true but cannot be proven by that system.

Not quite. This is where you got thrown-off. Some statements cannot be proven nor disproven (in a sufficiently complex system such as algebra, but that can be constructed within the system syntax). This means that they are neither true nor false.

The axioms of the system are insufficient to provide an answer. As the telling goes, one is now free to decide on an additional axiom that will decide the proposition. The new axiom can support the undecidable proposition or deny it.

With the added axiom, the system of axioms is somewhat more complex than the original. Are there now additional propositions that have no truth value as provided by the expanded axiom set?

 

[Preno]

Not quite. This is where you got thrown-off. Some statements cannot be proven nor disproven (in a sufficiently complex system such as algebra, but that can be constructed within the system syntax). This means that they are neither true nor false.

Not really, you may be conflating truth and formal provability within a particular system of first-order logic. The Godel sentence is true because of the way it is constructed.

eta: unless, of course, you view PA as a game of symbols rather than at attempt at axiomatizing natural numbers - in which case you may be right, but then Godel's theorem becomes an uninteresting combinatorial result with no philosophical/metamathematical implications whatsoever.

 

[HallsofIvy]

It is trivially true that "true" statements can follow from "false" premises. That was well known long before Godel.

 

[friend]

It is trivially true that "true" statements can follow from "false" premises. That was well known long before Godel.

Yes, a statement can be true irrespective of whatever anything else might say (true or false). Here we have a proposition (P) constructed with the symbols of a system (S). And P can be true regardless of what S says. This is the situation also if S implies P, right?

 

[sylas]

Yes, a statement can be true irrespective of whatever anything else might say (true or false). Here we have a proposition (P) constructed with the symbols of a system (S). And P can be true regardless of what S says. This is the situation also if S implies P, right?

That doesn't make any sense. If S is a "system", then you can't say S implies P. You can say S proves P, but that is a different statement entirely.

It looks to me that you don't actually know anything about how Godel's theorem is actually proved. If so, you'd do a lot better to learn a bit more about the theorem.

There's a really lovely little book by logician Raymond Smullyan, called "Forever Undecided", which gives a discussion of an equivalent of the Godel theorems for a simple propostional local of belief. Smullyan is great for learning about logic and having fun while doing it.

 

[friend]

That doesn't make any sense. If S is a "system", then you can't say S implies P. You can say S proves P, but that is a different statement entirely.

I thought the word "proves" was just another say of saying "implies". What is implied that isn't proved? And what is proved that is not implied?

 

[sylas]

I thought the word "proves" was just another say of saying "implies". What is implied that isn't proved? And what is proved that is not implied?

Informally, yes, they can be used in similar ways.

But you are speaking here specifically of formal logic, where there are very precise meanings for things.

In formal logic, "implies" is propositional connective, just like "and" and "or". If P and Q are propositions, then "P implies Q" is also a proposition. Here are truth tables for and, or and implies:

$$\begin{array}{*{3}{c|ccc}} \wedge & T & F & \hspace{2em} & \vee & T & F & \hspace{2em} & \Rightarrow & T & F & \hspace{2em} \\ \cline{1-3} \cline{5-7} \cline{9-11} T & T & F && T & T & T && T & T & F \\ F & F & F && F & T & F && F & T & T \end{array}$$​

Proves, however, is a "meta-logical" relation, between a proof system, or a set of axioms, and a proposition. It is often written as follows:

$$S \vdash P$$​

This is not a "proposition" with a truth value, but a definite statement, that P can be proved from the system S.

 

[Phrak]

Not really, you may be conflating truth and formal provability within a particular system of first-order logic. The Godel sentence is true because of the way it is constructed.

eta: unless, of course, you view PA as a game of symbols rather than at attempt at axiomatizing natural numbers - in which case you may be right, but then Godel's theorem becomes an uninteresting combinatorial result with no philosophical/metamathematical implications whatsoever.

It took me a while to understand what you meant. The addendum helped.
The game of symbols is the manner in which Godel constructed his proofs.

I have one slime text on Godel's Theorem, "Godel's Proof", Nagel and Newman, that states:

"Godel showed that Principia, or any other system within which arithmetic can be developed , is essentially incomplete. In other words, given any consistent set of arithmetical axioms, there are true arithmetical statements that cannot be derived from the set."

But this is wildly dependent on what one thinks and believes is true. It's an informal statement by the authors about adherence to absolute truths (with the T capitalized) that have not been revieled by the original set of axioms.

If 'true' is taken to mean logical truth value then something taken as an absolute truth effectively imposes additional constraints to the original set of axioms. That is, it adds axioms. One could have chosen to add an alternative axiom, consistent with the rest, yet incompatible with the first choice. I believe that 'truth' in a non absolute sense is what Godel intended, that the authors seem to have missed.

 

[sylas]

It took me a while to understand what you meant. The addendum helped.

I have one slime text on Goedels Theorem, "Godel's Proof", Nagel and Newman, that states:

"Godel showed that Principia, or any other system within which arithmetic can be developed , is essencially incomplete. In other words, given any consistent set of arithmetical axioms, there are true arithmetical statements that cannot be derived from the set."

But this is wildly dependent on what one thinks and believes is true. It's an informal statement by the authors about adherence to absolute truths (with the T capitalized).

If we take 'true' to mean logical truth value then we have imposed additional constraints--more axioms to the formal set, to obtain it. I believe this is the sense which Godel intended, that the authors seem to have missed.

A more precise sense of what Godel proved is that for any logical system sufficiently expressive to represent arithmetic, one of the following two cases must hold:

• Every sentence is provable in the system. That is, the system is inconsistent.
• There are some sentences, where the system cannot prove the sentence OR prove its negation. That is, the system is incomplete.

The authors don't need to be assuming any absolute truth. In logic, "truth" is defined with respect to a model. You don't need an absolute model or an absolute truth. The incompleteness of a formal system means that for ANY model, there are statements true in that model which the system cannot prove.

Cheers -- sylas

 

[Phrak]

A more precise sense of what Godel proved is that for any logical system sufficiently expressive to represent arithmetic, one of the following two cases must hold:

• Every sentence is provable in the system. That is, the system is inconsistent.
• There are some sentences, where the system cannot prove the sentence OR prove its negation. That is, the system is incomplete.

The authors don't need to be assuming any absolute truth. In logic, "truth" is defined with respect to a model. You don't need an absolute model or an absolute truth. The incompleteness of a formal system means that for ANY model, there are statements true in that model which the system cannot prove.

Cheers -- sylas

As I have been saying, you first presume your model to hold absolutes for which your system must comform or it is incomplete.

 

[sylas]

As I have been saying, you first presume your model to hold absolutes for which your system must comform or it is incomplete.

And I responded to what you are saying because it is incorrect. I think you have misunderstood how this works.

A system is incomplete not with respect to a single model, but with respect to ALL models, because there are sentences for which it can neither prove the sentence nor its negation. It is wrong to think you first presume a particular model. You don't.

Incompleteness of a system is property of a system itself, independent of models.

Cheers -- sylas

 

[Preno]

It took me a while to understand what you meant. The addendum helped.
The game of symbols is the manner in which Godel constructed his proofs.

I have one slime text on Godel's Theorem, "Godel's Proof", Nagel and Newman, that states:

"Godel showed that Principia, or any other system within which arithmetic can be developed , is essentially incomplete. In other words, given any consistent set of arithmetical axioms, there are true arithmetical statements that cannot be derived from the set."

But this is wildly dependent on what one thinks and believes is true. It's an informal statement by the authors about adherence to absolute truths (with the T capitalized) that have not been revieled by the original set of axioms.

How is it wildly dependent on what one thinks and believes to be true? The only thing it depends on is the consistency of PA. Assuming that, the statement is true because of how it is constructed: G is true iff it is unprovable in PA, and if PA is consistent, then it indeed is unprovable and therefore true.

eta: if you want to know how I know that PA is consistent - since I know the axioms are all true, formal inferences preserve truth and a statement and its negation cannot simultaneously be true, it follows that we cannot prove both a statement and its negation from PA. (Also, if you wish to identify truth with provability in PA or some stronger system, you don't really have the option of doubting the consistency of PA, anyway.)

And of course a lot of other things that don't follow from PA are true. For example, the fact that the integers are well-ordered.

If 'true' is taken to mean logical truth value then something taken as an absolute truth effectively imposes additional constraints to the original set of axioms. That is, it adds axioms. One could have chosen to add an alternative axiom, consistent with the rest, yet incompatible with the first choice.

Yes, since Godel's sentence is undecidable, the theory remains consistent whether you add G or ~G as an axiom. That doesn't necessarily mean much, though. PA remains consistent even if you add a constant c and axioms c>1,c>2,c>3,... Consistency isn't everything, if you want the axioms to be true, you also need to demand omega-consistency. PA+~Con(PA) is consistent, but not omega-consistent, and therefore not true (where Con(PA) is the undecidable arithmetic statement coding the fact that PA is consistent).

I believe that 'truth' in a non absolute sense is what Godel intended, that the authors seem to have missed.

Godel was a well-known Platonist, he certainly did believe in absolute mathematical truth.

 

[friend]

I have one slime text on Godel's Theorem, "Godel's Proof", Nagel and Newman, that states:

"Godel showed that Principia, or any other system within which arithmetic can be developed , is essentially incomplete. In other words, given any consistent set of arithmetical axioms, there are true arithmetical statements that cannot be derived from the set."

It would seem the inherent truth of arithmaical statements is imposed from outside that system. We recognize the truth of those statements intuitively. But those statements in and of themselves do not equate to True or False. I mean whoever seen something like (2+3=5)=True, or (2+3=6)=False? We simply intuit the truth of 2+3=5. So when the logical truth values of True and False are not even part of the formal language of the system in question, like arithmatic, then it is trivially obvious that the system can't prove any statement True or False. What?

 

[sylas]

It would seem the inherent truth of arithmaical statements is imposed from outside that system. We recognize the truth of those statements intuitively. But those statements in and of themselves do not equate to True or False. I mean whoever seen something like (2+3=5)=True, or (2+3=6)=False? We simply intuit the truth of 2+3=5.

No, we don't. These are theorems of the formal system, which must be provable. The actual way of writing meta statements in logic is more like this. To say 2+3=5 is "true" in a model M, we write:

$${\cal M} \models 2+3=5$$​

If the model is implicit in context, then you can just write:

$$\models 2+3=5$$​

This is pretty much what you think of as "(2+3=5)=TRUE", except that that there is a clear difference between the formal language of arithmetic, and the formal meta-language for expressing whether sentences of arithmetic are true, or provable.

To say 2+3=5 is "provable" in a system S, we write:

$${\cal S} \vdash 2+3=5$$​

Note that there's a clear difference between "true" and "provable", which is important when you are looking at properties of formal system, like completeness or consistency.

So when the logical truth values of True and False are not even part of the formal language of the system in question, like arithmatic, then it is trivially obvious that the system can't prove any statement True or False. What?

You seem to be making assertions about logic without actually knowing any formal logic. You are mixing up models and axioms and sentences of the logic and statements about the logic, and don't even seem to be aware that you are doing it.

There's no point worry about Godel until you do a bit more basic introductory formal logic.

Formal systems do prove things just fine.

Cheers -- sylas

 

[friend]

There's no point worry about Godel until you do a bit more basic introductory formal logic.

Yes, at some point I might have to educate myself in these intricacies. At present I know propositional calculus and predicate logic. I wish I had more time to continue my studies. Where do you suggest I learn the rest?

The actual way of writing meta statements in logic is more like this. To say 2+3=5 is "true" in a model M, we write:

$${\cal M} \models 2+3=5$$​

, except that that there is a clear difference between the formal language of arithmetic, and the formal meta-language for expressing whether sentences of arithmetic are true, or provable.

I understand Russel and Whitehead tried to prove that math was complete by showing how it could be derived from propositional logic. Is that right? I understand their derivation went through the first order predicate logic of set theory. But to even recognize the truth that an element belongs to a set is imposed and not derived, right?

I think in order to prove that arithmetic statements are true, one would have to derive math statements from propositional logic, since propositional logic is the algebra of true and false. Otherwise, the truth of the math statements are merely recognized intuitively by the reader and not derived by algebraic manipulation of the system's axioms. And if the truth of statements is not derived from the axioms of the formal system, then of course the truth of statements is not connected to its provability.

Did Russel and Whitehead actually succeed in deriving math from propositional logic?

 

[CRGreathouse]

I understand Russel and Whitehead tried to prove that math was complete by showing how it could be derived from propositional logic. Is that right?

You need a lot more than propositional logic: you need predicate calculus and set theory. Have a look at Metamath for some examples of derivation of mathematics from the axioms themselves.

 

[sylas]

Did Russel and Whitehead actually succeed in deriving math from propositional logic?

As has been pointed out, they needed a lot more than propositional logic. They did show that formal logic could be used effectively as a basis for mathematics.

Godel showed that the formal systems of Principia could not be complete and consistent.

 

[friend]

I'll borrow Torkel's statement of the theorem:

First Incompleteness therem (Gödel-Rosser). Any consistent formal system S within which a certain amount of elementary arithmetic can be carried out is incomplete with regard to statements of elementary arithmetic: there are such statements which can neither be proved, nor disproved in S.​

You know, in all my discussions about Godel's theorem, I've never seen an example of a statement which is well formed and true, but not provable by that system. That would certainly help. I guess the trouble is as soon as you find one, it is immediately added as one of the axioms of a larger system. But that only argues for the definition of axioms to be such that each axiom is so fundamental it cannot be proven by the others. But's that's inherently obvious.

 

[CRGreathouse]

You know, in all my discussions about Godel's theorem, I've never seen an example of a statement which is well formed and true, but not provable by that system. That would certainly help.

Goodstein's theorem is the usual example. Kirby & Paris showed that this is not provable in Peano arithmetic.

Harrington & Paris' version of Ramsey's theorem is another (earlier) example.

 

[Hurkyl]

You are plainly speaking here of the first incompleteness theorem. I'll borrow Torkel's statement of the theorem:

First Incompleteness therem (Gödel-Rosser). Any consistent formal system S within which a certain amount of elementary arithmetic can be carried out is incomplete with regard to statements of elementary arithmetic: there are such statements which can neither be proved, nor disproved in S.​

I hate to say it -- but you left out the hypothesis that S be axiomizable by a Turing-recognizable set.

 

[sylas]

I hate to say it -- but you left out the hypothesis that S be axiomizable by a Turing-recognizable set.

Torkel's treatment specifies this explicitly as part of the definition of "formal system".

 

[Hurkyl]

Torkel's treatment specifies this explicitly as part of the definition of "formal system".

Ok good; I figured that might be the case, but wanted to make sure you weren't omitting something.

 

[diolu]

You know, in all my discussions about Godel's theorem, I've never seen an example of a statement which is well formed and true, but not provable by that system. That would certainly help. I guess the trouble is as soon as you find one, it is immediately added as one of the axioms of a larger system. But that only argues for the definition of axioms to be such that each axiom is so fundamental it cannot be proven by the others. But's that's inherently obvious.

Some other people have already shown theorems not provable in Peano arithmetic. For any "formal system" S; consider the assertion C(S) : "S is free of paradox". Proofs can be coded by finite sequences of symbols and the correctness of a proof can be checked by a Turing like machine. If S is strong enough to develop elementary arithmetic C(S) can be formalized in S. A paradox is a contradiction in the theory: i.e. the ability to proof a theorem and its contrary (and in this case we can show that the system can proof everything). Sure that if you consider a formal system S; you "believe" that S is free of paradox; so you believe that C(S) is true but it can be shown that C(S) is non provable in S (by Goedel). Of course since you have no proof you cannot be sure that C(S) is true. This has the consequence that if you want a formal system S in which you can develop all of mathematics; you cannot have a "convincing" proof P that S is consistent (because P would be reproducible in S; in contradiction with Goedel). The usual system that mathematician take to develop mathematics is ZFC (Zermelo Fraenkel set theory with the axiom of choice). Mathematicians "believe" it is consistent but it is exaggerate that they "know" it is consistent. The consistency of ZFC can be proved in stronger systems; say ZFC*; but it does not really help because if you consider ZFC* then you would be interested in the consistency of ZFC*; not ZFC alone and the problem appears again.