Talk:Diagonal lemma

From Wikipedia, the free encyclopedia

Contents

[edit] 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 [1]. Physis 16:32, 23 November 2006 (UTC)

[edit] 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)

[edit] 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)

[edit] 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)

[edit] 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)

[edit] 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)

[edit] Notes

  1. ^ Csirmaz, László and Hajnal, András: Matematikai logika. Eötvös Loránd University, Budapest, 1994. (online available, in Hungarian)