http://en.wikipedia.org/wiki/Diagonal_lemma
I am wondering about the proof of the "Fixed-Point Lemma"
$\text{Mod } \Sigma$ is the class of all models of $ \Sigma$. $\text{Th Mod } \Sigma$ is the set of all sentences which are true in all models of $\Sigma$. This however is just the set of all sentences logically implied by $\Sigma$. We call this set the set of consequences of $\Sigma$ or $Cn \Sigma$. Thus we have that $Cn \Sigma = \{\sigma | \Sigma | \sigma \} = Th\space Mod \space \Sigma$.
Now we let $A$ be a set of axioms for our system over the language of $R$ which is a set of relations, constants, and formulas which create a number theory. Now if we have some set of consequences $Cn\Sigma$ due to our set of axioms $\Sigma$ we create a theory $T$ which models the set of consequences $Cn \Sigma$. Now referring to Wikipedia, as it states:
"Let $T$ be a first-order theory in the language of arithmetic and capable of representing all computable functions. Let $ψ$ be a formula in the language with one free variable. The diagonal lemma states that there is a sentence $φ$ such that $φ \Leftrightarrow ψ(\#(φ))$ is provable in T. Intuitively, $φ$ is a self-referential sentence saying that $φ$ has the property $ψ$. The sentence $φ$ can also be viewed as a fixed point of the operation assigning to each formula $θ$ the sentence $ψ(\#(θ))$. The sentence $φ$ constructed in the proof is not literally the same as $ψ(\#(φ))$, but is provably equivalent to it in the theory $T$.
Let $f\colon \mathbb{N}\rightarrow \mathbb{N}$ be the function defined by: $$f(\#(θ)) = \#(θ(\#(θ)))$$
for each $T$-formula $θ$ in one free variable, and $f(n) = 0$ otherwise. The function $f$ is computable, so there is a formula $δ$ representing $f$ in $T$.
--> I don't quite understand the above sentence. I know that since $\theta$ is a $T$-formula it is a consequence of the theory $T$, so we are only looking at functions $f(n)$ which operate on consequences of $T$ (which $\theta$ is one of). Now it is claimed that since $f$ is computable there is some $\delta$ representing $f$ in $T$. I am not sure what that is supposed to mean/what $\delta$ is really doing. Now I know that we are representing the sentences $\theta$ which are the consequences of the theory $T$. Also for $f(\#(θ)) = \#(θ(\#(θ)))$ is this just saying that we are defining $f$ to be some sort of assignment of a Gödel number to a Gödel number (the $\#(θ(\#(θ)))$)?
Wikipedia goes on to say:
Thus for each formula $θ$, $T$ proves: $$(\forall y) [ δ(\#(θ),y) \Leftrightarrow y = f(\#(θ))]$$
If I can understand the above it is possible that I can crack the rest of the proof - but will try and get it posted here so that others can see the walkthrough of the proof.
Thanks much in advance,
Brian
P.S. I was also hoping to gain some understanding beyond just understanding the proof of the lemma. I see a little but here:
Gödel's Incompleteness Theorem - Diagonal Lemma
and am guessing that somehow we are generating some sentence (similar to another real number in Cantors diagonalization argument) in which ?? I don't know how to put the rest in to words as I don't understand exactly what diagonalizing the sentances does (I do a little bit by intuition but can not formalize what is going on). Any thoughts on this would be very welcome. I also am wondering how this fits in with the $\delta$ above.
The $\delta$ in the proof statement is a formula. In the language of $\text{PA}$, there is no symbol for the function $f$; but $\text{PA}$ is strong enough so that there is some formula $\delta(x, y)$ such that the following two things hold: $$f(n) = m \quad \text{ iff } \quad \text{PA} \vdash \delta(\underline{n}, \underline{m})$$ $$f(n) \neq m \quad \text{ iff } \quad \text{PA} \vdash \neg\delta(\underline{n}, \underline{m})$$
where $\underline{k}$ is the numeral for the number $k$. (A weaker statement would be to only assert the first biconditional; this weaker property of "weakly" representing a function holds of all $\Sigma_1^0$-functions).
Now, given that $f(\#(\theta)) = \#(\theta(\#(\theta)))$, where $\theta(x)$ is a formula in the language of $\text{PA}$, define a new formula as follows:
$$\alpha(x) = \exists y (\delta(x, y) \wedge \psi(y))$$
Finally, define $\varphi = \alpha(\#(\alpha))$. Then by our definitions:
$$\begin{align} \text{PA} \vdash \varphi & \leftrightarrow \alpha(\#(\alpha)) \\ & \leftrightarrow \exists y (\delta(\#(\alpha), y) \wedge \psi(y)) \\ & \leftrightarrow \exists y (y = \#(\alpha(\#(\alpha))) \wedge \psi(y)) \\ & \leftrightarrow \psi(\#(\alpha(\#(\alpha)))) \\ & \leftrightarrow \psi(\#(\varphi)) \end{align}$$
The step from $\exists y (\delta(\#(\alpha), y) \wedge \psi(y))$ to $\exists y (y = \#(\alpha(\#(\alpha))) \wedge \psi(y))$ is (if I'm not mistaken) the other step you mention. That follows from the fact that $\text{PA}$ is representing the function $f$ with $\delta$. Hence, for all $k$, if $f(n) = k$, then $\text{PA} \vdash \forall y (\delta(\underline{n},y) \leftrightarrow y = \underline{k})$.
Simiarly, if $T$ extends $\text{PA}$, it must also strongly represent all recursive functions, and so this applies to $T$ as well.