I think the negation of the lemma needs to contain a disjunction as follows (since for the negation every tuple must be either (true,false) or (false,true)):

$\begin{align}(s\wedge \neg f(\ulcorner s \urcorner)) \vee (\neg s\wedge f(\ulcorner s \urcorner)) \end{align}$

Let's now look at A: $\begin{align}s\wedge \neg f(\ulcorner s \urcorner)\end{align}$. It must hold true for every sentence s. — 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.)

Something I don't get, though I don't know enough to decide if this is actually an error in the proof or a limitation of understanding, is that the proof doesn't seem to require that $f$ is computable, just that it has a boolean image. The conditional "if f is computable and maps to T F then ~ f is computable and maps to T F" only uses that f has a boolean image. Where have you used the assumption that f is computable?

In Godel's incompleteness theorem f is taken to be ~Prov('s'), the negative of the 'provability predicate'.
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.

I think the negation of the lemma needs to contain a disjunction as follows (since for the negation every tuple must be either (true,false) or (false,true)): — Andrew M

Agreed. Fixed. Thanks for the correction.

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.) — Andrew M

Yes, I think that you are right. The fix is more complex, though. Still working on it.

Where have you used the assumption that f is computable? — fdrake

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

It is easy to show via the construction of Prov('s') that s -> Prov('s') when s is a theorem. — sime

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

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.) — Andrew M

Agreed. I have applied a fix to the proof for this problem. Do you think it works?

Do you think it works? — alcontali

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.

Trying to square this with the wikipedia version, I'm struggling with,

for every computable function f that takes a number as an argument and returns false or true, — alcontali

Shouldn't it be more like,

there exists some computable function f with the special property that it takes the godel number of any 'gappy' sentence and returns the godel number of the same sentence eating itself,

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

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. — Andrew M

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?

But that still leaves disjunct B that could be true. So you would also need to show a case where B fails. — 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.

returns the godel number of the same sentence eating itself

The version in wikipedia indeed revolves around self-reference. When you look at the lemma's statement:

$s \leftrightarrow f(\ulcorner s \urcorner)$

Then, it does not necessarily say anything self-referential. What it literally says, is:

• any arbitrary logic sentence s can be true or false
• $f(\ulcorner s \urcorner)$ can be true or false, for any arbitrary f
• In those circumstances, there is at least one s for which the tuple (s,$f(\ulcorner s \urcorner)$) is (true,true) or (false,false)

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:

$s \leftrightarrow f(s)$

No need to use $\ulcorner s \urcorner$, because the conversion function $\ulcorner \urcorner$ 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:

$\begin{bmatrix}(sentence,property:f) & false & true \\ false & \textbf{(false,false)} & (false,true) \\ true & (true,false) & \textbf{(true,true)} \end{bmatrix}$

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.

Is your f really Γ, the "graph" predicate assumed available to "represent" (presumably like the way points on a 2d coordinate graph represent a relation of ordered pairs) any computable function and therefore f? — bongo fury

The proposition that there exists a Γ for which Γ(x,y=f(x)) -> true and Γ(x,y$\ne$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.

this somewhat bewildering and disorienting critique of wikipedia and everyone else — bongo fury

James R Meyer writes:

Because the Gödel numbering function is a function in the meta-language to the system T, there cannot be any such relation δ in the system T that contains the information of the definition of the Gödel numbering function and which can unambiguously reference formulas of its own formal system T.

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.

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? — alcontali

I think so.

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. — alcontali

Yes and renaming ¬f to g makes that visually clear:

$\begin{align}(s\wedge g(\ulcorner s \urcorner)) \vee (\neg s\wedge \neg g(\ulcorner s \urcorner)) \end{align}$

I think that the main issue left now, is to come up with a succinct way of phrasing this principle. — alcontali

Yes, in effect, with the negated lemma you have $s \leftrightarrow g(\ulcorner s \urcorner)$ for all logic sentences s.

The proposition that there exists a Γ for which Γ(x,y=f(x)) -> true and Γ(x,y≠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. — alcontali

I don't see how you are addressing anything like the same claim, e.g.,

• Any symbol system that can prove all arithmetic proves at least one liar sentence.

Your target seems to be something like,

• Any syntactically determined boolean valuation function (your f) on all sentences in a system must, for at least one of those sentences, return the value which is the (actual? semantically determined?) value of the sentence.

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,

Then, the diagonal lemma says that:

∀f ∈ F:N→{false,true} ∃s,t ∈ S: s ↔ f(⌜s⌝) ∧ ¬t ↔ f(⌜t⌝) — 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.

I don't see how you are addressing anything like the same claim, e.g.,
Any symbol system that can prove all arithmetic proves at least one liar sentence. — bongo fury

[/quote]

That is not a requirement for the diagonal lemma. The statement of the lemma says:

Let T be a first-order theory in the language of arithmetic and capable of representing all computable functions. Let F be a formula in the language with one free variable, then: There is a sentence ψ such that ψ ↔ F(°#(ψ)) is provable in T.

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.

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? — 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.

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? — bongo fury

I have finally received an answer for the issue that you have raised. The function that you describe, looks like this:

$f(\ulcorner s\urcorner) = \neg s$

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:

Toward a Big Surprise.Tarski’s Theorem is equivalent with the Semantic Diagonal Lemma. — Saeed Salehi

Saeed mentions three (surprisingly) short diagonal-free proofs for Tarski's Undefinability:

• Robinson (1963) on page 16
• Kotlarski (1998) on page 17
• Sereny (2004) on page 18

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!