Talk:Diagonal lemma

notation

What does the double sided arrow mean? What are the differences between 'function', 'theorem', 'formula', and 'sentence'? 173.227.92.65 (talk) 18:33, 11 March 2015 (UTC)

unsure about proper LaTeX use

I made some of the equations into LaTeX form, but I'm unsure of how to format the quotes. I was taught to open and close quotes (in text mode) with ` and '. Unfortunately, the backquote character produces a rendering error. Instead, I used

T \vDash t = ''B''

which produces

$T\vDash t=''B''$

That aint' right, obviously. What's the right way to get quotes in an equation? Twinxor t 21:17, 8 April 2006 (UTC)

Actually, using ``B" (a double quote on the right) works in LaTeX, and it seems that's what most people do if they need quotes in an equation. Unfortunately, as you noticed, it doesn't work in MediaWiki. At this point, I would suggest asking on Wikipedia_talk:WikiProject_Mathematics, as that will attract the attention of some people very savvy in this kind of stuff. --C S (Talk) 08:17, 9 April 2006 (UTC)

Damn, where was all this expertise when I ran into excatly the same problem? :) I spent ages reading all the documentation and concluded that there is no clean way of doing real quotes in equations, if you can't escape out of math mode temporarily. Stevage 14:53, 7 May 2006 (UTC)

Now, $\ulcorner \phi \urcorner$ works (and also $\llcorner \phi \lrcorner$). (In older times, it did ot work on some Mediawiki systems). But now on Wikipedia, corner notations works, and that can be good solution for the problem. The scientific literature (on mathematical logic) uses this notation. see . Physis 16:32, 23 November 2006 (UTC)

Proposed new proof

Proof. Substitute the code number of A for x in A(x) and obtain the sentence A("A"). Let Diag(A) denote this sentence, called the diagonalization of A. Diag, the diagonal function, is representable in T because Diag can be proved computable and by assumption, all computable functions can be represented in T. Let D(x) denote the T representation of the diagonal function. Consider the sentence A(D(x)), which asserts that the diagonalization of x has property A. Now let B be the diagonalization of A(D(x)), so that B is the sentence A(D("A(D(x))")). Hence B has the form A(t), where t is the term D("A(D(x))"). Clearly,

(1) $T\vdash B\leftrightarrow A(t).$

But t denotes the diagonalization of A(D(x)), namely B. Also,

(2) $T\vDash t=\,''\!B''.$

because B is provable in T. Substituting (2) into (1) yields:

$T\vdash B\leftrightarrow A(''B'').$ QED.

This proof isn't so much "new" as "reworded". I want to give experts in the area an opportunity to twiddle this proof until they are satisfied. I have interchanged D(x) and Diag(x). The shorter notation should be used for the function that can be an argument of predicates.

Where can I find a proof that Diag is computable?202.36.179.65 23:54, 16 August 2006 (UTC)

The theory of recursive functions is very new to me, so I cannot present a direct proof in few time. But I would try to make an algorithm for D and diag in a (for me) more friendly algorithm scheme (e.g. in lambda calculus or combinatory logic), then I would try to see whether any corresppndence can be established between terminating functions in combinatory logic and total functions in recursive function theory. Unfortunately, I am new to these arithmetic-based algorithmical schemes! Good old combinatory logic is much easier to program with for me. It is so funny to represent trees, term trees with it, writing tree traversal algorithms etc. But maybe any other programming language will be good for this, I proposed combinatory logic and lambda calculus only because there are many materials available on the equivalence of expressive power of combinatory logic vs recursive function theory. But I do knot now any details yet on this for me new area. Physis 03:18, 24 November 2006 (UTC)

But maybe we can try a direct proof too: /Diagonal formula as a representation of a recursive function. Physis 12:17, 3 December 2006 (UTC)

Questions about proof

Why is B provable? The current proofs just assert this without explanation. Why is provability of B necessary to show $T\vDash t=\,''B''$? - 72.57.120.3 09:43, 7 September 2006 (UTC)

Representing function with formula

I am a newbie in this topic, thus, it was hard for me the use of diag as a function embedded in our object languge. No, not the quine was hard for me (I can write quines). What was hard for me is that our object language is an arithmetic-like language, thus, it has funtion symbols like 0, s, $+$, $\cdot$, but of course no diag. That diag can be represented, of course, but only through formula. This may seem making things overcomplicated, but for me, the correctness of the proof may be more verifyable.

My proposed proof can be read on subpage: /Proof with diagonal formula.

Sorry for mistakes and weak points, but I a newbye on these things. What I learnt is writing a quine interpreted in a combinatory logic programming language (which, in turn, has been implemented in Haskell), but I am not accustomed to pure mathematical logic.

Physis 13:46, 23 November 2006 (UTC)

Expert attention still needed?

I think I have cleaned up the page enough that the tag can be removed. So if you agree, please remove it. --Quux0r 10:07, 16 April 2007 (UTC)

Does the Lemma trivially result in the Liar's Paradox?

What happens if you take ψ to be the property of falsehood? Surely it implies there is a fixed point for θ in the statement θ<=>~θ. Does the lemma not apply to this special case, or is it instead proof by contradiction that the assumption "all computable functions can be represented in T" cannot actually be true?

Moon Oracle 21:14, 4 August 2007 (UTC)

I think what you've re-proved here is Tarski's undefinability theorem -- there is no ψ such that ψ holds of a code for θ just in case θ is false. --Trovatore 17:39, 5 August 2007 (UTC)

Author of Diagonalization and Self-Reference reference

I've added the author of said book in the references of the article. It seems that this book on Amazon is the one talked about. I don't know why it wasn't there before, since it's three clicks to find, but if there is a reason, why? and feel free to remove it again. Somejan (talk) 10:22, 24 June 2008 (UTC)

Question about the proof section

It says

(*) φ ↔ ∀ y [ δ(#(β),y) → ψ(y)] ↔ ∀ y [ (y = #(β(#(β))) → ψ(y)].   

We analyze two cases.
1. Assuming φ holds, substitute #(β(#(β)) for y in the rightmost formula in (*), and obtain:

(#(β(#(β)) = #(β(#(β))) → ψ(#(β(#(β))),

Since φ = β(#(β)), it follows that ψ(#(φ)) holds.
2. Conversely, assume that ψ(#(β(#(β))) holds. Then the final formula in (*) must be true, and φ is also true.

I don't understand the second case. It says ψ(#(β(#(β))) means the final formula in (*) must be true

∀ y [ (y = #(β(#(β))) → ψ(y)]

So if y is #(β(#(β))), you've got ψ(y) for one value of y. Even if you had ∀y [ψ(y)], how would that make the final formula true? I don't get it. Vibritannia (talk) 14:16, 22 October 2008 (UTC)

Suppose that ψ(#(β(#(β))) holds. Then, if you give me any natural number y such that y happens to equal #(β(#(β))), you have to agree that ψ(y) holds as well. In other words, for any y, if y = #(β(#(β)) then ψ(y) holds. This informal argument corresponds to a proof in T that if ψ(#(β(#(β))) holds then

∀ y [ (y = #(β(#(β))) → ψ(y)]

holds as well. That's all the article is saying. If you prefer to think of it in terms of inference rules, the following inference rule is being used, along with universal generalization.

φ(x) ⊦ (y = x) → φ(y)

— Carl (CBM · talk) 19:28, 22 October 2008 (UTC)

Thanks, Carl. That got me unstuck. So the lemma has been proved by finding the actual sentence, which is

∀ y [ δ(#(β),y) → ψ(y)]

which says that when the function f(#(θ)) = #(θ(#(θ))) that can "decode a Gödel number to get a formula with one free variable, then apply that formula to that Gödel number, and then get the Gödel number of the resulting sentence" holds for the Gödel number of the sentence itself, then the sentence has one unspecified property, ψ, of its Gödel number. If that property holds, then the sentence does (and if it doesn't, the sentence doesn't). But now I notice that whether ψ is a property of the sentence or just a property of a number depends of the definition ψ – which means the sentence isn't necessarily self-referential. For example, if I say number 7 has 3 reception rooms and 2 bedrooms, and the Smith's live there, I've referred to Number 7; but if I say 7 is 3 plus 4, I haven't (but it's still true). In that case, how do we know that the sentence which we've found to prove the lemma holds for the kind of reference we want it to, rather than just for things like 7 is 3 plus 4? Vibritannia (talk) 13:35, 23 October 2008 (UTC)

I don't understand what you're asking. The formula ψ takes one parameter, which is a number. This is why the conclusion of the lemma is that T proves φ ↔ ψ(#(φ)); here #(φ) is a term for the Goedel number of φ. The idea that φ is self-referential is just an informal way of stating the precise result, which is that φ holds if and only if the Goedel number of φ has the property defined by ψ. This is why that interpretation is prefaced with the word "Intuitively" in the article. — Carl (CBM · talk) 14:20, 23 October 2008 (UTC)

Point taken but... the problem I was imagining was this: ψ is a formula that when given a number produces a sentence, but then what sort of formula would be needed in order that we could interpret the number given to it as a reference to a sentence and not be confronted with jibberish? Any old formula wouldn't do. We could only make sense in that way of certain formulas. What I was imagining was that if, in the proof, it had been defined what character ψ must have to guarantee a non-jibberish interpretation of a reference was always possible rather than potentially possible, then that might have frustrated the proof. (And perhaps it might even be provable that must always be the case.) Vibritannia (talk) 11:29, 24 October 2008 (UTC)

There is no requirement that ψ interprets the number passed to it as a Goedel number. For example, if you take ψ(x) as a formula that says x is even, the corresponding φ will be a sentence such T proves that φ is true if and only if the Goedel number of φ is even. — Carl (CBM · talk) 13:42, 24 October 2008 (UTC)

That makes sense to me. Now I reread the first line of the article:

the diagonal lemma establishes the existence of self-referential sentences in formal theories

That isn't right, is it? What the lemma does is what you just said. That it was possible to interpret the number passed to ψ as a reference was not demonstrated. Just because it doesn't seem likely to someone that it couldn't be interpreted that way, doesn't mean that it definitely could. But that is what is being claimed. What if there is a surprise? Vibritannia (talk) 09:51, 25 October 2008 (UTC)

I don't know what you mean by "a surprise". Suppose that φ is equivalent to ψ(#(φ)). Then φ says, informally, "My Goedel number has property ψ". This is the sense in which the sentences generated by the diagonal lemma are self-referential. It is the same way that the Goedel sentence that says "I am not provable" is self-referential. Compare the Stanford Encyclopedia of Philosophy entry on self reference. — Carl (CBM · talk) 11:52, 25 October 2008 (UTC)

OK, there may be many formulas for ψ that are equivalent in the sense that each yields a different sentence when passed the same number, but all those different sentences will be true when the others are true (and false when the others are false). So in that sense, you could say they all describe the same property of the number passed to them. But the look of any particular formula for ψ will tend to indicate what the number passed to it represented, which won't be the same in every case. To demonstrate that the number passed can be interpreted in a certain way, don't you need to at least show that a suitable equivalent formula always exists?

Thank you for the link by the way. It looks very good. Vibritannia (talk) 12:57, 26 October 2008 (UTC)

In the proofs where the diagonal lemma is employed, the formula ψ is already known, and then the "self-referential" formula φ is constructed relative to ψ. So while it is true that there will be other formulas that are equivalent to ψ they aren't particularly interesting. — Carl (CBM · talk) 13:29, 26 October 2008 (UTC)

So supposedly you can prove the diagonal lemma for the particular case of the already known ψ if you wanted to, but that isn't done in the proof because it's an unnecessary complication. The diagonal lemma is for any ψ, making it more general. Hmm... I think I know how to ask what I'm trying to ask now: Does the diagonal lemma prove

∀ψ [φ ↔ ψ( #(φ) )]

or does it prove

∃ψ [φ ↔ ψ( #(φ) )]

Vibritannia (talk) 17:32, 27 October 2008 (UTC)

This notation doesn't really make formal sense, but this is what is proved, under the assumption that T contains a sufficient amount of arithmetic:

∀ψ ∃ φ [T ⊦ (φ ↔ ψ(#(φ)))]

In words: for any formula ψ(x) there is a sentence φ (which will depend on ψ) such that T proves φ ↔ ψ(#(φ)). — Carl (CBM · talk) 19:13, 27 October 2008 (UTC)

Let ω(ψ) = φ↔ψ(#(φ))

If ψ is arbitrary, universal generalization says (I looked it up on wiki)

ω(ψ) ⱶ ∀ψ [ ω(ψ) ]

So to infer the general case, one has to prove ω(ψ) for unspecified ψ. That means one has to prove the formula ω, not just find a sentence φ (which is β(#β)) that satisfies φ↔ψ(#(φ)). Or have I gone wrong? Vibritannia (talk) 11:28, 29 October 2008 (UTC)

Yes,you've gone wrong somewhere. I have no idea what your formula ω is supposed to be. Like I was saying, it doesn't really make sense to write formula with quantifiers for formulas. The proof, as presented in the article, does prove that, for any fixed but unspecified ψ(x) there is a formula φ such that T proves φ and ψ(#(φ)) are equivalent. — Carl (CBM · talk) 12:15, 29 October 2008 (UTC)

I think I see. Thanks, Carl, for your patience. Vibritannia (talk) 14:56, 29 October 2008 (UTC)

Typo in background section

The anon editor was right that it should say "f(n)" in the background section. The letter f is not actually in the language of T, so f can't appear in the formula. But the numeral representing f(n) can appear. — Carl (CBM · talk) 16:57, 14 November 2008 (UTC)

Whoops, sorry Zero sharp (talk) 19:08, 14 November 2008 (UTC)

Brackets Mismatch

The Mathematics on this page is infested with bracket mismatches. I refrained from fixing the mismatches myself because an incorrect bracket placement could completely alter the desired meaning. I ask that an expert fixes the errors. Thank you. --99.246.101.166 (talk) 16:07, 8 August 2010 (UTC)

No detail why it's called Diagonal

The only reference to the name Diagonal is "The lemma is called "diagonal" because it bears some resemblance to Cantor's diagonal argument." Other lemmas with descriptive names, like the Isolation Lemma or Handshaking Lemma, have wiki descriptions of the name's specific relevance. For example, the wiki page for Horseshoe Lemma states the "name of the lemma comes from the shape of the diagram illustrating the lemma's hypothesis." Diagonal lemma, however, is much vaguer. Smullyan's Diagonalization and Self Reference states the following several times, in various ways: "there is indeed an Arithmetic diagonal function d(x), but the proof of this is quite elaborate ... perfectly feasible, but as I have indicated, it is far more complex than need be, due to the complexities involved in proving the existence of an Arithmetic diagonal function." In fact he casts his description of Godel's theorem in Tarski's terms, calling it Tarskification instead of diagonalization.

I've found an odd explanation at , where Godel's 'not proveable' F is plotted on a graph as a random variable, and indeterminant G is a diagonal that increases. f crosses g, as it enters g's proposition. This isn't why Godel's method is called diagonalization, however.

Peter Smith's An Introduction to Godel’s Theorems, available online, derives the theorems from "diagonalization." I've read part of his work, and it attempts to clarify the diagonal lemma.

I think addressing the importance of ordered pairs in diagonalization is important, especially since this isn't emphasized in Godel theorem explanations. Integer construction provides a visually clear diagonalization process, and is directly implicated in the lemma.208.80.117.214 (talk) 06:52, 12 June 2014 (UTC)

Is this the same diagonal lemma?

This article has been criticized multiple times on the talk page for being too technical, and for not stating clearly enough what the diagonal lemma actually is or how it is related to Cantor’s diagonal argument.

The following argument occurred to me yesterday, and it’s very easy to understand (as well as to see how it is “diagonal”). However, I’m not sure if this is actually a restatement of the diagonal lemma, or if I actually managed to re-prove something else. If it really is the same diagonal lemma, then the article should probably describe it this way since it would be far more accessible to the average reader.

My way of putting it is:

-Use a Gödel numbering to list all the computable functions that map natural numbers to natural numbers.

-Define F_n(m) as the output of the function whose Gödel number is n, when the input is m.

-Define a new function G(n), where G(n) =F_n(n) + 1. This function samples the output of every computable function when the input is its own Gödel number, then adds one.

-As with Cantor’s diagonal argument, it seems that G(n) cannot be the same as any other computable function, since for every function F_n(m), its value differs from G(n) for at least one input value (namely, n itself).

-This causes a seeming contradiction because G(n) is indeed computable, because of how it is constructed.

-The paradox can be resolved if some of the functions F_n(m) are partial functions, meaning their output is not defined for all values of m. If F_n(n) is undefined, then F_n(n) + 1 is also undefined, and therefore the diagonal argument no longer holds and G(n) can indeed be equivalent to F_m(n), for some m. This must be the case, since we know G(n) is computable and we already assigned a Gödel number to every computable function.

-Therefore, there is no way of assigning a Gödel numbering to all computable total functions, without also including partial functions in the list. Another reason we know this is because determining whether or not a general recursive function is total is equivalent to the halting problem, and thus undecidable.

-This argument also shows that for any Gödel numbering that could be algorithmically applied to the computable functions, there must always be at least one function whose value at its own Gödel number (F_n(n)) is undefined.

2604:2D80:6984:3800:0:0:0:F474 (talk) 22:49, 27 July 2023 (UTC)

References