Discussion: Gödelâs Fixed Point Lemma)
From the forum: Sam's Essays
This thread was started by: revoltair.
Discussion start time: 2010-12-29 11:52:57.
From the forum: Sam's Essays
This thread was started by: revoltair.
Discussion start time: 2010-12-29 11:52:57.
This article contains at least one elementary error that renders the entire proof invalid.
In the proof, a formula β(x) is defined as the formula: ∀y ( δ(x,y) → ψ(y) ). The rest of the proof assumes that β(x) is a formula of the formal system.
But there cannot be such a formula β(x).
The reason is simple. The function ψ(y) is defined as any formula in the formal system, where y is some number, so that the function is effectively the inverse of the Gödel numbering function. And as is the case for the Gödel numbering function, the function ψ(y) is a function that is defined in a language that is a meta-language to the formal language, and there cannot be a formula of the formal system that gives that function. And certainly the purported proof of the fixed point lemma does not provide any logical reason to support such an assertion.
And since the function β(x) is defined in terms of the function ψ(y), there is no logical reason to support the supposition that there can be such a formula of the formal system that is the function β(x).
In summary, this is not so much a proof as an assemblage of various assumptions which are unsupported by any logical basis.
Hi Revoltair,
When we say "Suppose ψ(x) is any formula in the language L, then ...", then ψ has not been nailed down at all, but the following statements are understood to hold for whatever specific ψ you want.
It's similar to when we say: "Suppose A is any real number, then by definition of -A, A-A=0." Surely you wouldn't argue that this is an incorrect deduction because A was defined as "any real number".
If you want a more concrete instance of the fixed point lemma, then assume the language has a truth predicate and replace ψ(x) throughout by not(T(x)), then the lemma will concretely build (depending on your model of computation and godel numbering) a formula φ such that basic arithmetic proves φ↔not(T(#φ)), i.e., φ says "φ is false", the liar's paradox.
It's just that the construction isn't restricted to just this one common choice of ψ(x). It works for any choice of ψ(x).
When we say "Suppose ψ(x) is any formula in the language L, then ...", then ψ has not been nailed down at all, but the following statements are understood to hold for whatever specific ψ you want.
It's similar to when we say: "Suppose A is any real number, then by definition of -A, A-A=0." Surely you wouldn't argue that this is an incorrect deduction because A was defined as "any real number".
If you want a more concrete instance of the fixed point lemma, then assume the language has a truth predicate and replace ψ(x) throughout by not(T(x)), then the lemma will concretely build (depending on your model of computation and godel numbering) a formula φ such that basic arithmetic proves φ↔not(T(#φ)), i.e., φ says "φ is false", the liar's paradox.
It's just that the construction isn't restricted to just this one common choice of ψ(x). It works for any choice of ψ(x).
You say, ‘ψ has not been nailed down at all’. While all the details of it have not been given, certain aspects of it have been precisely defined, in particular, the fact that it gives the inverse of the Gödel numbering function. That alone guarantees there is no formula of the formal system that gives that function.
When you say that: ‘the following statements are understood to hold for whatever specific ψ you want’, that is simply an assumption unless you provide a logical basis for that assertion - which you haven’t.
The remark "Suppose A is any real number, then by definition of -A, A-A=0." is utterly irrelevant. For a language system that includes real numbers. what you are really giving is the proposition “∀A, A-A = 0”, which is simply a statement of that language system, and is perfectly legitimate. It has nothing to do with assertions that involve a formal language AND a meta-language.
You then go on to say, ‘If you want a more concrete instance of the fixed point lemma, then assume the language has a truth predicate’. Why on earth would I want to assume such an absurd notion? I don’t know of anyone who thinks that any language can define the truth of its own statements in its own language. Certainly most people accept Tarski's conclusion that a language can't do that.
And the comment ‘isn't restricted to just this one common choice of ψ(x). It works for any choice of ψ(x).’ has no logical basis. As I have pointed out, all such ψ(x) have the common definition that they are the inverse of the Gödel numbering function. So the other details don't affect that.
As I said originally, there is no escaping the fact that what you have isn’t a proof, but is simply a series of unfounded assumptions.
When you say that: ‘the following statements are understood to hold for whatever specific ψ you want’, that is simply an assumption unless you provide a logical basis for that assertion - which you haven’t.
The remark "Suppose A is any real number, then by definition of -A, A-A=0." is utterly irrelevant. For a language system that includes real numbers. what you are really giving is the proposition “∀A, A-A = 0”, which is simply a statement of that language system, and is perfectly legitimate. It has nothing to do with assertions that involve a formal language AND a meta-language.
You then go on to say, ‘If you want a more concrete instance of the fixed point lemma, then assume the language has a truth predicate’. Why on earth would I want to assume such an absurd notion? I don’t know of anyone who thinks that any language can define the truth of its own statements in its own language. Certainly most people accept Tarski's conclusion that a language can't do that.
And the comment ‘isn't restricted to just this one common choice of ψ(x). It works for any choice of ψ(x).’ has no logical basis. As I have pointed out, all such ψ(x) have the common definition that they are the inverse of the Gödel numbering function. So the other details don't affect that.
As I said originally, there is no escaping the fact that what you have isn’t a proof, but is simply a series of unfounded assumptions.
What is this "inverse of the Gödel numbering function" business you keep talking about?
The fixed point theorem says that if ψ(x) is any formula with the one free variable x, in a sufficiently strong language, then there is a formula φ, in the same language, such that basic arithmetic proves φ↔not(T(#φ)).
The formula ψ(x) has not been "defined", and nothing has been assumed about it.
"You then go on to say, ‘If you want a more concrete instance of the fixed point lemma, then assume the language has a truth predicate’. Why on earth would I want to assume such an absurd notion? I don’t know of anyone who thinks that any language can define the truth of its own statements in its own language. Certainly most people accept Tarski's conclusion that a language can't do that."
When someone says "assume the language has a truth predicate", that means assume the language includes an unary predicate (T). Tarski and others have shown that there cannot be a model where the interpretation of T has certain properties. But of course the symbol can be added. And you can even get some truth properties for it, just not as many as you might like-- see Friedman & Sheard's paper "An axiomatic approach to self-referential truth" for a pretty exhaustive classification of what properties the predicate can and cannot have.
The fixed point theorem says that if ψ(x) is any formula with the one free variable x, in a sufficiently strong language, then there is a formula φ, in the same language, such that basic arithmetic proves φ↔not(T(#φ)).
The formula ψ(x) has not been "defined", and nothing has been assumed about it.
"You then go on to say, ‘If you want a more concrete instance of the fixed point lemma, then assume the language has a truth predicate’. Why on earth would I want to assume such an absurd notion? I don’t know of anyone who thinks that any language can define the truth of its own statements in its own language. Certainly most people accept Tarski's conclusion that a language can't do that."
When someone says "assume the language has a truth predicate", that means assume the language includes an unary predicate (T). Tarski and others have shown that there cannot be a model where the interpretation of T has certain properties. But of course the symbol can be added. And you can even get some truth properties for it, just not as many as you might like-- see Friedman & Sheard's paper "An axiomatic approach to self-referential truth" for a pretty exhaustive classification of what properties the predicate can and cannot have.