Talk:Diagonal lemma/Proof with diagonal 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 function symbols like 0, s, $+$, $\cdot$, but of course no diag. That diag can be represented, of course, but only through formula. I mean this way :

$f:\mathbf {N} \to \mathbf {N}$

is $\left\langle \left\langle x\right\rangle ,y\right\rangle$-represented in the object language (through $\left\langle \left\langle x\right\rangle ,y\right\rangle$ variable layout) with $\phi \in \mathbf {Form} _{\left\{x,y\right\}}^{t}$ iff

$\Gamma \vdash \phi [x:={\mathfrak {R}}_{n}]\leftrightarrow y={\mathfrak {R}}_{f(n)}$

or maybe it is more ergonomic to use the notion of interderivability:

$\phi [x:={\mathfrak {R}}_{n}]\dashv \vdash _{\Gamma }y={\mathfrak {R}}_{f(n)}$

here ${\mathfrak {R}}$ is used as the “macro” for representing natural numbers in the object language, thus, ${\mathfrak {R}}$ itself does not belong to the object language

${\mathfrak {R}}_{n}\equiv s(\dots (s0)\dots )$

n times. In fact, also diag is a macro.

All this may seem making things overcomplicated, but for me, the correctness of the proof may be more verifyable, because I have not much practice yet.

Another change: I shall use /Structural descriptive expressions, e.g.

$\phi [x:={\mathfrak {R}}_{n}]\dashv \vdash _{\Gamma }y{\hat {=}}{\mathfrak {R}}_{f(n)}$

(it is the hat on the object language symbol = that denotes that). A consequence (which may be not easy-to-see): in fact, names x, y etc. are not the variables of the object language, but the metavariables (of the meta language) over the variables of the object language. In a wonderful way, disregarding this is not a problem in most cases. My main motivation for using structural descriptive expressions: to get rid of the burden, having to kepp track

• which sign is a pure opart of the object language,
• which sign is a pure part of meta language,
• which sign is halfway by being an expanding macro, while spreading object language texts itself being part of meta language

this sophisticated variety of meanings will be avoided, and everything will be transferred to the level of meta language — that's the main trhing in /Structural descriptive expressions

Meta versus object language

See general overview about the mere concept in article Metalanguage.

We have to maintain clear distinction between the object vs meta language

object language

here, a language of arithmetic, maybe extended, it consists of formulas based on terms built out of 0, s, $+$, $\cdot$ in a straightforward way). See details for the specific object language used for the proof: in subpage /Object language

meta language

here, the language with which we discuss the theorem.

I shall use the following notation conventions: see the (for this task) specific considerations and details in subpage /Metalanguage.

Diagonal lemma

Now I try to say and prove the theorem using the above conventions. The diagonalization macro is hard for me, I have to think it through how touse it in the proof.

One more convention, before we begin the real work: let us choose a variable layout, so that we can talk about reresentation of functions with formulas. Form now on, we shall mean $\left\langle \left\langle x\right\rangle ,y\right\rangle$-representation, thus, representiation will be done through $\left\langle \left\langle x\right\rangle ,y\right\rangle$ variable layout. Thus from now on, x and y wil not denote metavariables over the variables of the object language, but the variables of the object language themselves (or their structural descriptive names in the meta languge). This is needed for being able to talk about the approriate “plugging together” with variables.

Thus, things get the following forms: We want to prove the theorem “for all property $\pi$, there is a fixed point $\phi$, saying ‘I am of property $\pi$’”:

$\forall \pi \in \mathbf {Form} _{\left\{y\right\}}^{t}\;\;\exists \phi \in \mathbf {Form} _{\emptyset }^{t}\;\;\ \phi \dashv \vdash _{\Gamma }\pi [y:=\ulcorner \phi \urcorner ]$

Motivation of signs: $\pi$: property; $\phi$: fixed point. The notation of variable substitution […:=…] does not belong to the object language. The way the roles are dealt among the varibles is important: x is used for plugging the diagonalization process, y is used for representing functions. In this aspect, this is a rather low-level language, we don't have the luxury of modern functional languages (Haskell): we have to plan resource management explicitly. It took some time to plan the variables, to get plugging fit even at the moment of diagonalization. (This plugging is the main reason for fixing a variable layout for representation).

Prerequisites

The existence of a capable diagonal formula ${\mathfrak {D}}_{g,\Gamma }^{x,u,y}$ can be proven, if we know that

• the object language is capable of representing recursive functions

It is a fact (although it is not easy to prove) that recursive functions are capable of all work that we expect the diagonal formula ${\mathfrak {D}}_{g,\Gamma }^{x,u,y}$ to do. It can be shown

• how to represent the problem of “packing and unpacking” (Gödel numbering and decoding), in summary, the whole problems of quoatation
• how to write the algorithm for diagonalization

We can write the whole algorithm directly with recursive functions and we can also build the diagonal formula ${\mathfrak {D}}_{g,\Gamma }^{x,u,y}$ by hand. See diagonal formula as a representation of a recursive function.

But there may be more direct demonstations, too. E.g. we can map the problem into the realm of another algorithm formalization (e.g. combinatory logic instead of recursive function theory), then the proof can be easier. But then, we have to prove also the equivalence between the two algorithm formalizations. See also #To do

Starting point

Let us start from a concrete instance of the following scheme:

${\mathfrak {D}}_{g,\Gamma }^{x,x,y}[x:=\ulcorner \phi _{0}\urcorner ]\dashv \vdash _{\Gamma }y{\hat {=}}\ulcorner \phi \urcorner$

where

$\phi \equiv d_{g}^{x}\left(\phi _{0}\right)$

i.e we make $\phi$ from $\phi _{0}$ with the diagonal function (around the x variable and using the g Gödel numbering), i.e. being $\phi \equiv \phi _{0}[x:=\ulcorner \phi _{0}\urcorner ]$ This seems to be an acceptable starting point, because we know it must be true by definition (of ${\mathfrak {D}}_{g,\Gamma }^{x,u,y}$ and the concept of representing functions with formulas — the most diffcult thing to grasp is that we chose deliberately the parametrization of ${\mathfrak {D}}_{g,\Gamma }^{x,x,y}$ so that the first two variable names coincide by both being x). Others: I am accustomed to using pattern-mathing in Haskell, and sometimes I use also $\ulcorner \dots \urcorner$ like this, but we must always keep in mind that $\ulcorner \dots \urcorner$ is in fact no typographical sign, but a precisely defined function (working on the level of meta language), being composed of g Gödel numbering and ${\mathfrak {R}}$ representation macro.

The above scheme seems to be correct, thus let us start from one of its possible instancees. Now we shall get a monster, but in fact, we shall do no tricky thing: we simply substitute ${\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi$ in the place of $\phi _{0}$:

${\mathfrak {D}}_{g,\Gamma }^{x,x,y}[x:=\ulcorner \overbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi } ^{\phi _{0}}\urcorner ]\dashv \vdash _{\Gamma }y{\hat {=}}\ulcorner \phi \urcorner$

it has become very nasty, but the worst will come soon: the diagonalization of $\phi _{0}$, that means, the result of the diagonal function applied to ${\mathfrak {D}}_{g,\Gamma }^{x,x,y}\land \pi$ has to be substituted in the place of $\phi$. Thus $\phi _{0}$

$\overbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi } ^{\phi _{0}}$

becomes by diagonalization $\phi$

$\overbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}[x:=\ulcorner \underbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi } _{\phi _{0}}\urcorner ]{\hat {\land }}\pi } ^{\phi }$

because we specificated the diagonal formula macro by requirement $d_{g}^{x}\left(\xi \right)\equiv \xi [x:=\ulcorner \xi \urcorner ]$ and because substitution behaves sowhat like homomorphism

$\gamma {\hat {\land }}\delta [x:=t]\equiv \gamma [x:=t]{\hat {\land }}\delta [x:=t]$

and because

• $d_{g}^{x}\left({\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi \right)\equiv ({\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi )[x:=\ulcorner {\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi \urcorner ]$ by the definition of $d_{g}^{x}$ diagonal function
• $({\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi )[x:=\ulcorner {\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi \urcorner ]\equiv {\mathfrak {D}}_{g,\Gamma }^{x,x,y}[x:=\ulcorner {\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi \urcorner ]{\hat {\land }}\pi [x:=\ulcorner {\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi \urcorner ]$ because variable substitution behaves somewhat sort of homomorphism
• ${\mathfrak {D}}_{g,\Gamma }^{x,x,y}[x:=\ulcorner {\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi \urcorner ]{\hat {\land }}\pi [x:=\ulcorner {\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi \urcorner ]\equiv {\mathfrak {D}}_{g,\Gamma }^{x,x,y}[x:=\ulcorner {\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi \urcorner ]{\hat {\land }}\pi$ becasue $x\notin {\mathcal {FV}}(\pi )$

thus the following horrible formula will be produced:

${\mathfrak {D}}_{g,\Gamma }^{x,x,y}[x:=\ulcorner \overbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi } ^{\phi _{0}}\urcorner ]\dashv \vdash _{\Gamma }y{\hat {=}}\ulcorner \overbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}[x:=\ulcorner \underbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi } _{\phi _{0}}\urcorner ]{\hat {\land }}\pi } ^{\phi }\urcorner$

That has produced nested quotations marks at $\phi$ (it is both contained by and contains quotation). Not a good news, but I hope somehow it can be clarified. I try to clarify this with introducing /Structural descriptive expressions.

Anding both sides with the same formula

From now, this horrible formula

$\overbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}[x:=\ulcorner \overbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi } ^{\phi _{0}}\urcorner ]} ^{\alpha }\dashv \vdash _{\Gamma }\overbrace {y{\hat {=}}\ulcorner \overbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}[x:=\ulcorner \underbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi } _{\phi _{0}}\urcorner ]{\hat {\land }}\pi } ^{\phi }\urcorner } ^{\beta }$

will not bother us that much. It is simply of form

$\alpha \dashv \vdash _{\Gamma }\beta$

I hope we shall not spoil it by “and”-ing $\pi$ to both “sides”:

$\alpha {\hat {\land }}\pi \dashv \vdash _{\Gamma }\beta {\hat {\land }}\pi$

and the following giant is nothing more than the mentioned acceptable step (expanded):

$\overbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}[x:=\ulcorner \overbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi } ^{\phi _{0}}\urcorner ]} ^{\alpha }{\hat {\land }}\pi \dashv \vdash _{\Gamma }\overbrace {y{\hat {=}}\ulcorner \overbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}[x:=\ulcorner \underbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi } _{\phi _{0}}\urcorner ]{\hat {\land }}\pi } ^{\phi }\urcorner } ^{\beta }{\hat {\land }}\pi$

A good news: if we look at the formula carefully, we can explore $\phi$ forming on the left-hand side, because of formula identity $\alpha {\hat {\land }}\pi \equiv \phi$:

$\underbrace {\overbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}[x:=\ulcorner \overbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi } ^{\phi _{0}}\urcorner ]} ^{\alpha }{\hat {\land }}\pi } _{\phi }\dashv \vdash _{\Gamma }y{\hat {=}}\ulcorner \overbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}[x:=\ulcorner \underbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi } _{\phi _{0}}\urcorner ]{\hat {\land }}\pi } ^{\phi }\urcorner {\hat {\land }}\pi$

Unification

Let us remember, $\pi \in \mathbf {Form} _{\left\{y\right\}}^{t}$ contains exactly one sole y free varible. Let us challange a rule like this: from premise

$y{\hat {=}}\dots {\hat {\land }}\pi$

deriving conclusion

$\pi [y:=\dots ]$

I do not know whether this is correct. Maybe it can be proven through the equality axioms of the Hilbert-style deduction system. Alternatively, if using other formalizations of deduction system, I think that part of the equation axiom scheme can be used , which asserts “compatibility of equation to each predicate”: for each predicate r of the signature

$\left\{x_{0}{\hat {=}}y_{0}\;{\hat {\land }}\dots {\hat {\land }}\;x_{n-1}{\hat {=}}y_{n-1}\;{\hat {\to }}\;({\hat {r}}(x_{0},\dots ,x_{n-1})\to {\hat {r}}(y_{0},\dots ,y_{n-1}))\;\mid \;\dots \right\}$

because, I hope, this can be extended to formulas with formula induction. Maybe we also use this part of logical axiom schemes : for each formula $\xi$ and term t

$\left\{{\hat {\forall }}x\xi \;{\hat {\to }}\;\xi [x:=t]\;\mid \;x\in \mathbf {Var} \;\mathrm {and} \;\xi \in \mathbf {Form} \;\mathrm {and} \;t\in \mathbf {Term} \right\}$

maybe it the scheme that allows us substitutions in all possible combinations during the proof. Equality axioms postulate identity to be a congruence relation. See also related notions, e.g. “equals for equals” (referential transparency), and another related notion Leibniz's law / identity of indiscernibles.

If the mentioned step is really correct, then we get

$\underbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}[x:=\ulcorner \overbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi } ^{\phi _{0}}\urcorner ]{\hat {\land }}\pi } _{\phi }\dashv \vdash _{\Gamma }\pi [y:=\ulcorner \overbrace {{\mathfrak {D}}^{x,x,y}[x:=\ulcorner \underbrace {{\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi } _{\phi _{0}}\urcorner ]{\hat {\land }}\pi } ^{\phi }\urcorner ]$

We can see the fixed point now, so we have what we wanted:

$\phi \dashv \vdash _{\Gamma }\pi [y:=\ulcorner \phi \urcorner ]$

$\phi$ fixed point saying: “I am not of property $\pi$”

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.

Summary

The most concise form to “store” the essence:

$d_{g}^{x}\left({\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi \right)\dashv \vdash _{\Gamma }\pi [y:=\left\ulcorner d_{g}^{x}\left({\mathfrak {D}}_{g,\Gamma }^{x,x,y}{\hat {\land }}\pi \right)\right\urcorner ]$

To do

The main point of the whole theorem could be seen in #Prerequisites. Maybe we can step further and formalize an equivalent of the diagonal lemma in illative combiantory logic. Advantages:

• it is not unpractical to program with combinatory logic (Haskell practice can help much!)
• instead of Gödel numbering, combinatory logic provides a pleasant way to the whole problematic of reification, quoatation.
• maybe there is a variant of the theorem where the whole quotation problem can be avoided. See the analogy of fixed point combinator Y, it does not need any notion of quoatation, either. But maybe it would raise typing problems here.