Alternative proof for the Carnap-Gödel diagonal lemma
The canonical proof for the Carnap-Gödel diagonal lemma is considered "unreadable". The lemma itself is considered quite understandable.
Say that [math]\Bbb{F}[/math] is the class of computable functions.
Say that [math]\Bbb{S}[/math] is the class of logic sentences in an arbitrary first-order theory T.
Say that [math]\ulcorner s \urcorner[/math] is the Gödel encoding of an arbitrary logic sentence [math]s[/math].
Then, the diagonal lemma says that:
[math]\forall f \in \Bbb{F}: \Bbb{N} \rightarrow \{false,true\} \exists s \in \Bbb{S}: s \leftrightarrow f(\ulcorner s \urcorner)[/math]
It means that for every computable function f that takes a number as an argument and returns false or true, there exists a logic sentence s for which both s and [math]f(\ulcorner s \urcorner)[/math] are either true or else false. In other words, it asserts the existence of a tuple (s,[math]f(\ulcorner s \urcorner)[/math]) which is (true,true) or (false,false).
It amounts to asserting that there exists a logic sentence s, for which:
(s [math]\wedge[/math] [math]f(\ulcorner s \urcorner)[/math]) [math]\vee[/math] ([math]\neg[/math]s [math]\wedge[/math] [math]\neg[/math][math]f(\ulcorner s \urcorner)[/math])
By contradiction, the negation of this lemma is that for each computable function f, and for all possible logic sentences s, the following would hold true:
(s [math]\wedge[/math] [math]\neg[/math][math]f(\ulcorner s \urcorner)[/math]) [math]\vee[/math] ([math]\neg[/math]s [math]\wedge[/math] [math]f(\ulcorner s \urcorner)[/math])
In that case, the only tuples (s,[math]f(\ulcorner s \urcorner)[/math]) that can exist, are (true,false) and (false,true).
Let expression A be the first alternative, i.e. (true,false): s [math]\wedge[/math] [math]\neg[/math][math]f(\ulcorner s \urcorner)[/math].
Let B be the second alternative, i.e. (false,true): [math]\neg[/math]s [math]\wedge[/math] [math]f(\ulcorner s \urcorner)[/math].
Let's now look at A: s [math]\wedge[/math] [math]\neg[/math][math]f(\ulcorner s \urcorner)[/math]. It must hold true for every true sentence s. So, it must also hold true for sentence [math]\neg[/math]s1 with s1 a false sentence. So, for [math]\neg[/math]s1, expression A becomes:
[math]\neg[/math]s1 [math]\wedge[/math] [math]\neg[/math][math]f(\ulcorner \neg s1 \urcorner)[/math]
If f is a computable function, then so is [math]\neg[/math]f. Let's rename [math]\neg[/math]f to g. The above then becomes:
[math]\neg[/math]s1 [math]\wedge[/math] [math]g(\ulcorner \neg s1 \urcorner)[/math]
Now, let's rename [math]\neg[/math]s1 to v. The above then becomes:
v [math]\wedge[/math] [math]g(\ulcorner v \urcorner)[/math]
We see that (v,[math]g(\ulcorner v \urcorner)[/math]) is (true,true). This is in contradiction with the negation of the lemma, which insists that the tuple must be (false,true) or (true,false). Hence, the negation of the lemma is not possible, which is proof by contradiction for the lemma itself.
Can someone verify my alternative proof by contradiction for flaws, or just comment on it? I would be most grateful!
Note:
This is meant to be a complete proof for the Carnap-Gödel diagonal lemma.
Note:
This proof is actually not complete because it ultimately depends on using a diagonal-free proof for Tarski's Undefinability Theorem (which is the hard part).
Say that [math]\Bbb{F}[/math] is the class of computable functions.
Say that [math]\Bbb{S}[/math] is the class of logic sentences in an arbitrary first-order theory T.
Say that [math]\ulcorner s \urcorner[/math] is the Gödel encoding of an arbitrary logic sentence [math]s[/math].
Then, the diagonal lemma says that:
[math]\forall f \in \Bbb{F}: \Bbb{N} \rightarrow \{false,true\} \exists s \in \Bbb{S}: s \leftrightarrow f(\ulcorner s \urcorner)[/math]
It means that for every computable function f that takes a number as an argument and returns false or true, there exists a logic sentence s for which both s and [math]f(\ulcorner s \urcorner)[/math] are either true or else false. In other words, it asserts the existence of a tuple (s,[math]f(\ulcorner s \urcorner)[/math]) which is (true,true) or (false,false).
It amounts to asserting that there exists a logic sentence s, for which:
(s [math]\wedge[/math] [math]f(\ulcorner s \urcorner)[/math]) [math]\vee[/math] ([math]\neg[/math]s [math]\wedge[/math] [math]\neg[/math][math]f(\ulcorner s \urcorner)[/math])
By contradiction, the negation of this lemma is that for each computable function f, and for all possible logic sentences s, the following would hold true:
(s [math]\wedge[/math] [math]\neg[/math][math]f(\ulcorner s \urcorner)[/math]) [math]\vee[/math] ([math]\neg[/math]s [math]\wedge[/math] [math]f(\ulcorner s \urcorner)[/math])
In that case, the only tuples (s,[math]f(\ulcorner s \urcorner)[/math]) that can exist, are (true,false) and (false,true).
Let expression A be the first alternative, i.e. (true,false): s [math]\wedge[/math] [math]\neg[/math][math]f(\ulcorner s \urcorner)[/math].
Let B be the second alternative, i.e. (false,true): [math]\neg[/math]s [math]\wedge[/math] [math]f(\ulcorner s \urcorner)[/math].
Let's now look at A: s [math]\wedge[/math] [math]\neg[/math][math]f(\ulcorner s \urcorner)[/math]. It must hold true for every true sentence s. So, it must also hold true for sentence [math]\neg[/math]s1 with s1 a false sentence. So, for [math]\neg[/math]s1, expression A becomes:
[math]\neg[/math]s1 [math]\wedge[/math] [math]\neg[/math][math]f(\ulcorner \neg s1 \urcorner)[/math]
If f is a computable function, then so is [math]\neg[/math]f. Let's rename [math]\neg[/math]f to g. The above then becomes:
[math]\neg[/math]s1 [math]\wedge[/math] [math]g(\ulcorner \neg s1 \urcorner)[/math]
Now, let's rename [math]\neg[/math]s1 to v. The above then becomes:
v [math]\wedge[/math] [math]g(\ulcorner v \urcorner)[/math]
We see that (v,[math]g(\ulcorner v \urcorner)[/math]) is (true,true). This is in contradiction with the negation of the lemma, which insists that the tuple must be (false,true) or (true,false). Hence, the negation of the lemma is not possible, which is proof by contradiction for the lemma itself.
Can someone verify my alternative proof by contradiction for flaws, or just comment on it? I would be most grateful!
Note:
This is meant to be a complete proof for the Carnap-Gödel diagonal lemma.
Note:
This proof is actually not complete because it ultimately depends on using a diagonal-free proof for Tarski's Undefinability Theorem (which is the hard part).
Comments (17)
[math]\begin{align}(s\wedge \neg f(\ulcorner s \urcorner)) \vee (\neg s\wedge f(\ulcorner s \urcorner)) \end{align}[/math]
Quoting alcontali
Shouldn't this be that it must hold true for every true sentence s? The conjunction is simply false when s is false. (Whereas B handles the case where s is false.)
It is easy to show via the construction of Prov('s') that s -> Prov('s') when s is a theorem. However it cannot be shown, assuming consistency, that s -> ~Prov('s') when s isn't a theorem. Prov is only a computable partial function, therefore a proof of the lemma by way of contradiction cannot be obtained.
Agreed. Fixed. Thanks for the correction.
Yes, I think that you are right. The fix is more complex, though. Still working on it.
I didn't.
By the way, the original proof does not seem to use the condition either.
I just kept the condition around, because the original proof does, and the lemma is phrased like that.
As far as I am concerned, the function only needs to map natural numbers to booleans -- I agree with your view -- but I also have no clue as to why Carnap insists that the function must be computable.
The condition may be used very implicitly in one of the steps in the proof. I was hoping that someone else would be able to point out why the condition is needed (I somehow suspect that it actually is).
A first remark to make is that Carnap's lemma does not need Gödel's first (syntactic) incompleteness theorem (G1SI). It is the other way around. So, in the context of the lemma's proof, we should not mention G1SI theorem, because that would make things circular.
A second remark is that Gödel's semantic completeness theorem proves that Prov('s') -> s. So, if s is provable in T then s is true in all M; with M any model of T.
The other way around is not true.
The sentence s could be true in M, but not provable in T. This could be the case, for example, when T has more than one model (T is not categorical). In that case, s could be true in M1 but false in M2. In that situation, s will not be provable in T.
Hence, we can assert:
Prov('s') -> s
However, we cannot assert:
s -> Prov('s')
The fact that there exist true statements in M that are not provable in T, is exactly what G1SI theorem proves (with T being, for example, first-order PA).
Agreed. I have applied a fix to the proof for this problem. Do you think it works?
Still thinking about it, but a couple more things. When you consider A, I think you can omit the s1 discussion and just note that A is an instance of the diagonal lemma that is (true,true) for function ~f. So, per the negated lemma, A can't be true.
But that still leaves disjunct B that could be true. So you would also need to show a case where B fails.
Quoting alcontali
Shouldn't it be more like,
... and then, continuing, state the existence of some suitable (gappy) sentence capable of consequent paradox?
Is your f really ?, the "graph" predicate assumed available to "represent" (presumably like the way points on a 2d coordinate graph represent a relation as a set of ordered pairs of numerals) any computable function and therefore f?
From which assumption, we get the desired result that, roughly speaking, (logical) ? of the gappy sentence is provably equivalent to (computable) f of the same sentence? Or, in my terms here, that the result of pushing the sentence through the (logical) u-bend is provably equivalent to the result of pushing it through the (computable) v-bend?
I appreciate the answer is probably no on all counts, because your approach is not wikipedia's. I've tried to widen my sources, but so far am only as far as (haha) this somewhat bewildering and disorienting critique of wikipedia but also everyone else. :fear:
Yes, agreed. That is what I wanted to say. I was still looking for a succinct way to put it. This is indeed what it is about. What you just wrote, is indeed the gist of it. I wonder if the proof can just be phrased like that? Would it still be considered a proof?
Quoting Andrew M
Yes. This issue actually got introduced by your previous remark, which turned the conjunction into a disjunction. So, now there is a need to handle case B too.
Concerning the expression in B, instead of being true for all true sentences, it will be true for all false sentences. So, B is then an instance of the diagonal lemma that is (false,false) for function ~f.
The whole point of the proof is that the practice of requiring that a sentence stays off the diagonal for f will always force the sentence onto the diagonal for ~f. This is the case for both true and false sentences.
I think that the main issue left now, is to come up with a succinct way of phrasing this principle.
The version in wikipedia indeed revolves around self-reference. When you look at the lemma's statement:
[math]s \leftrightarrow f(\ulcorner s \urcorner)[/math]
Then, it does not necessarily say anything self-referential. What it literally says, is:
It is not clear to me, what exactly would be self-referential about any of this.
Furthermore, there is another issue. Every digital representation of sentence s is always a natural number. This is generally true: every representation of language is a sequence of natural numbers and therefore again, one big natural number. In that sense, can sentence s even be anything else than a natural number? So, where does the need come from to encode sentence s as a Gödel number? The (digital) sentence s is already a Gödel number.
Therefore, I do not see the need to encode s again as a Gödel number, since it can only be represented by a Gödel number. For example, in this page, any sentence s is represented as a stream of utf8 characters, which is an entirely legitimate Gödel encoding. Hence, as far as I am concerned, the lemma can actually be simplified to:
[math]s \leftrightarrow f(s)[/math]
No need to use [math]\ulcorner s \urcorner[/math], because the conversion function [math]\ulcorner \urcorner[/math] is redundant.
Maybe it was not clear in 1931, before computers existed, that a text representation is always isomorophic with a unique natural number (unique up to an isomorphism under encoding translation, of course). So, I understand that Gödel created his own utf8-style encoding. Nowadays, however, it looks quite redundant to do that.
What else than a natural number can text be? I simply cannot imagine any other representation of text that is not isomorphic to a natural number. In other words, s is already an element of N, the natural numbers. It can be represented in decimal, hexadecimal, binary, or in alphabetic text, but it is in fact always the same thing. In my opinion, there simply is no text that is not a natural number.
I also have a different interpretation for the name of the theorem itself, i.e. "diagonal" lemma. I consider the "diagonal" aspect to be very similar to the one in Cantor's diagonal argument. It is simply again a diagonal in a table:
[math] \begin{bmatrix}(sentence,property:f) & false & true \\ false & \textbf{(false,false)} & (false,true) \\ true & (true,false) & \textbf{(true,true)} \end{bmatrix} [/math]
The "diagonal" lemma simply says that for every property/function f, there exists a sentence on the diagonal, i.e. (true,true) or (false,false). So, there must be sentence that is true and for which the property is true, i.e. (true,true), or a sentence that is false and for which the property is false, i.e. (false,false).
That is how I understand the term "diagonal". I really don't see the need for self-reference here.
Quoting bongo fury
The proposition that there exists a ? for which ?(x,y=f(x)) -> true and ?(x,y[math]\ne[/math]f(x)) -> false, is tautological for any (computable) function f. But then again, this proposition is needed just for the original proof, and not for this one.
Quoting bongo fury
James R Meyer writes:
My opinion is that any sentence or text is always in Gödel numbering. For example, this entire page is necessarily in Gödel numbering (utf8).
The confusion is caused by non-digital representations of text. They give the impression that text could be represented in something else than in something isomorphic with natural numbers (e.g. ink on paper), but that is not true. If someone manages to show me text that is not isomorphic with a natural number, I will of course change my mind, but first I need to see something like that. Up till now, I never have. In fact, I do not think that it even exists.
Therefore, I believe that the practice of Gödel numbering utf8 text again (which is already Gödel numbered), is simply redundant.
Hence, I fundamentally disagree with Meyer's criticism.
I think so.
Quoting alcontali
Yes and renaming ¬f to g makes that visually clear:
[math]\begin{align}(s\wedge g(\ulcorner s \urcorner)) \vee (\neg s\wedge \neg g(\ulcorner s \urcorner)) \end{align}[/math]
Quoting alcontali
Yes, in effect, with the negated lemma you have [math]s \leftrightarrow g(\ulcorner s \urcorner)[/math] for all logic sentences s.
I don't see how you are addressing anything like the same claim, e.g.,
Your target seems to be something like,
Quite apart from how this claim might or might not correspond to the first, I can't see it going through. Why shouldn't we assume that at least one valuation (call it f and even interpret it as the predicate "is false") creates a complete set of mis-matches (true-false and false-true) of s to f(s) while its opposite (~f = g) makes a complete set of matches?
I guess you were really hoping to show that any (syntactically determined) valuation must create at least one match and one mis-match, but forgot to make sure they were shown to arise from the same valuation? You really want to claim,
Quoting alcontali
?
Perhaps it does? But your proposed short-cut no longer works. When you negate the claim you no longer make the implausible demand to exclude the possibility of v ? g(?v?) for some (other) f or g.
[/quote]
That is not a requirement for the diagonal lemma. The statement of the lemma says:
The liar sentence is handled in a downstream theorem that makes use of the diagonal lemma, i.e. Tarski's undefinability theorem.
We should not mix downstream theories with the lemma itself, which only says what it says, and nothing more.
Quoting bongo fury
Yes, agreed with this remark. (I still need to rework the argument for that problem.)
I think you would be clearer by referring only to the syntactical notion of derivability, since the diagonal lemma does not refer to truth, and neither does it assume the law of excluded middle. Any derivation of the lemma that did appeal to LOM would not be constructively acceptable, invalidating any consequent formula that appealed to the lemma which would include Godel's and Tarski's theorems, which are in fact constructively accepted.
The diagonal lemma only states that for every well-formed formula f(x) of one free variable, there exists a sentence s, such that the derivation of s implies the derivation of f('s') and vice versa, and that this fact is itself derivable.
Earlier, I was referring to the syntactical fact that when you wrote
?f?F:N?{false,true}?s?S:s?f(?s?)
'f' isn't assumed to be a provably total predicate function. For example, when the lemma is applied to derive Godel's incompleteness theorem f refers to ~prov('s'), and whilst the disjunction "~prov('s') or prov('s')" might be derivable for any 's' via an appeal to LOM, axiomatic arithmetic cannot consistently decide which part of the disjunction is the case. Therefore any derivation of the diagonal lemma that appeals to such a hypothetical function isn't a permissible derivation of of Peano arithmetic.
I have finally received an answer for the issue that you have raised. The function that you describe, looks like this:
[math]f(\ulcorner s\urcorner) = \neg s[/math]
I asked the question on the computer science stack exchange:
Diagonal lemma and the negation function
It is indeed possible to define it, but it is not computable, because of Tarski's Undefinability Theorem (TUT).
Consequently, my proof ultimately depends on an underlying proof for TUT. That is in fact a real problem, because TUT is usually made to depend on the diagonal lemma, creating some kind circular situation.
The only possible salvation in this situation is to use a diagonal-free proof for TUT, which also exists.
In fact, that is exactly what Saeed Salehi pointed out in the Russian workshop, "Diagonal-Free Proofs of the Diagonal Lemma", University of Tabriz & IPM WORMSHOP 2017, Moscow.
Saeed writes in page 3:
Saeed mentions three (surprisingly) short diagonal-free proofs for Tarski's Undefinability:
Deriving the diagonal lemma from any diagonal-free proof for TUT is in fact considered trivial.
Therefore, the core of my proof does not particularly do much, over and beyond the diagonal-free proof on which it rests.
Hence, my own proof is not wrong, but it is unfortunately not the essence of the matter. The hard part is proving the diagonal lemma for the one, single case (equivalent to TUT) that you pointed out!
Thanks again, for pointing out the issue!