Talk:Diagonal lemma/Proof with diagonal formula/Metalanguage

Non-interlarded things

There is less problems with things where the level of macro versus object language can be clearly spearated. The following notations are clearly part of the meta language:

Set-theoretic notations

• $\phi \in \mathbf {Form} _{\left\{x\right\}}^{t}$ denotes that $\phi$ is member of the set of formulas of the object language, whose free variables are exactly x and y, of signature t. Of course, membership and set notion are part of the meta language.
• Similar remarks concern notation $\ulcorner \phi \urcorner \in \mathbf {Term} _{\emptyset }^{t}$. See exact details below at #Structural descriptive names.

Proof theoretic notations

$\vdash$ denotes derivation

$\dashv \vdash$ denotes interderivability

Let us extend the above notion slightly: $\phi \dashv \vdash _{\Gamma }\psi$ iff $\Gamma \cup \{\phi \}\vdash \psi$ and $\Gamma \cup \{\psi \}\vdash \phi$.

There may be a lot of equivalence theorems, maybe e.g.

If the object language has a sign for $\leftrightarrow$ (or at keast it is definable), and derivation is defined “in accordance with” it, then

$\phi \dashv \vdash _{\Gamma }\psi$ exctly then, if $\Gamma \vdash \phi {\hat {\leftrightarrow }}\psi$

but I have not proved it yet (if it is true at all).

Interlarded things

The above meta things could be separated clearly form object language. But the things discussed below, it will be a little trickier: they themselves are part of meta language, but are used directly interlarded in object language texts, thus they must be read as “expanded”.

In fact, all this notion of “expanding” is a vague approximation of Tarski's solution with structural descriptive expressions, which can build from literals by concatenation the desired expressions. For comparison, see an approach to this direction.

Items

Metavariables

for formulas by small Greek letters: $\phi$, $\pi$… Variable substitutions, if any, are added like $\phi [x:=\dots ]$.

Metavariables will be used in quantifications, clauses and pattern namings. Examples:

Quantification

The theorem itself is a good example for use of metavariables in quantification — “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 ]$

Clause

Clauses can require relations between subpatterns of an expression. Clauses can be used especially in specifications (and maybe, rarely, in definitions).

Example:

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

where

$\psi \equiv d_{\phi }^{u}$

Pattern naming (grouping)

Input

Overbracings are used to denote previously known, intended pattern names.

Output

Underbracings are used to denote newly explored pattern being wonderfully the same as some (former though to be unrelated) pattern.

Example:

${\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$

We can use term/formula identities to express our exploring repeating patterns. Motivating example: A good news: if we look at the 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 }{\hat {\land }}\pi \dashv \vdash _{\Gamma }\overbrace {y{\hat {=}}\ulcorner \overbrace {{\mathfrak {D}}[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$

carefully, we can explore a new occurence of repeating patern: $\phi$ forming on the left-hand side, because $\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$

Our exploration can be registered by formula identity

$\phi \equiv \alpha {\hat {\land }}\pi$

in a concise way.

In genarally, = is used in the object language, but $\equiv$ denotes identity of terms/formulae (of the object language), the identity itself being part of the meta language.

Macros (meta name-functors)

Macros can have arguments. I shall use various tricks to denote parametrization of macros: super- and subscripts, substitution noatiton …[…:=…] etc. I shall avoid denoting parametrization of macros by postfixing them listed between parantheses. Even, I shall avoid this denoation for any parametrization of any metalanguage constructs. Because arguments notated by postfixing them listed between parantheses are usually part of the object languages. E.g. $s(s(s(s0))))$ the correspondent of natural number 4 in th object language.

Macros will be denoted by fraktur capitals: ${\mathfrak {R}}_{n}$, ${\mathfrak {D}}_{g,\Gamma }^{x,u,y}$ the arguments, if any, are added as superscript or subscript.

Operations

Expansion

of macro or metavariable

Variable substitution

in a formula of the object language, denoted by $\phi [x:=\dots ]$

Quotation

maybe it can be regarded as a special macro expansion:

$\ulcorner \phi \urcorner \equiv {\mathfrak {R}}_{(g_{\phi })}$

it is composed out of

• the representation (in object language)
• of the Gödel number

of the quoted formula (or maybe sometimes term).

Enlarging metalanguage

We mentiond macros, they are used interlarded in the object language, they should be read asexpanded. But macros have to be defined soehow before!

Sometimes also metavariables $\phi$, $\psi$ etc.will be given constraints,requirements, ina kind of where clause (or let … in … construct).

Definition

E.g. macro defintion, consisting of a triple of the definiendum, the equivalence sign $\equiv$, and the definiens. Equivalence sign $\equiv$ will be used sometimes also for asserting (not defining!) identity of terms/formulae, or sometimes also in clauses. But in all cases:

• not part of object language;
• not for any other equivalence/congruence relation (other than identity)

The commonly used identity sign = will be reserved (almost) always as part of the object language, denoting identity. The purpose is: to avoid confusion of meta vs object language at as many occasions as possible.

Example of definition: ${\mathfrak {R}}_{n}\equiv s(s(\dots 0)\dots )$ defines the “representation” macro (see below).

Specification

In some cases, we don't define things in details, but we resort to something kind of specification: we do not prescribe the specific way, just declare our requirements, knowing (hoping) that it can be fulfilled by many ways, whose details are not important.

For example, reresenting functions by formulas can be done by specification, for example:

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

is represented in the object language through $\phi \in \mathbf {Form} _{\left\{x,y\right\}}^{t}$ iff

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

(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 )$ alltogether n times).

It will be the diagonalization macro which forces me to resort to such nonconstructive tasted things.

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

where

$\psi \equiv d_{g,\phi }^{u}$

denotes that I require from a construct that it should provide enough information that we may deduce from it (using $\Gamma$) a functional relation between two forms.

Structural descriptive names

As Tarski uses this term, structural descriptive names (of sentences of object language) are part of the meta language, so that each sentence of the object language can be called by name from the meta language.

Strong object language

But our object language is strong enoght to representate these structural descriptive names itself. The natural numbers can be represented in the object languagwe with terms $0$, $s(0)$, $s(s(0))$, $s(s(s(0)))$… That is a surplus thing, not all object languages are used to achieve this. The object language can call by name its own sentences. Thus, object language can use a kind of “reification”, “nominalization”, “quotation”. I am not sure, but it is exactly that Tarski mentions as representing part of metalanguage (the structural descriptive names) inside the object language.

Representation macro

We shall use this contstruct in a systematic way. Ta achive readability, we call this construct by a macro (the macro itself belongs to the meata language!):

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

Thus ${\mathfrak {R}}$ takes a natural number (natural numbers themnselves are part of the mata language), and turns it into a term of the object language: a representation of it. This motivates the name ${\mathfrak {R}}$ of this macro, the fracture equivalent of “R”. Thus, ${\mathfrak {R}}$ maps a part of the meta language in the object language.

Gödel numbering

Main article: Gödel number

Gödel numbering, denoted here by g, turns the formulae of the object language to natural numbers.

Quotation

Now the more diabolic thing: quoatation. It is not itself part of object language, but it will be used heavily interlarded in object language texts. It take a formula of the object language, turns it into a natural number (by Gödel numbering g), then the resulting natural number will be translated back into the object language by the representation macro ${\mathfrak {R}}$. Thus, both the source and the target are part of the object language, but the definition itself below

$\ulcorner \phi \urcorner \equiv {\mathfrak {R}}_{\left(g_{\phi }\right)}$

is heavily part of the metalanguage (as macro defintions are). It makes a route like a flying fish.

Diagonal function

$d^{u}:\mathbf {Form_{\left\{u\right\}}^{t}} \to \mathbf {Form_{\emptyset }^{t}}$

$\phi \mapsto \phi [u:=\ulcorner \phi \urcorner ]$

an easy thing among the many hard ones: $d^{u}$, the u-diagonal function is not a macro. it will never be used interlarded in texts of object languge. (The sign of the function is parametrized with the variable so that plugging can be fixed and planned).

Diagonalization formula

This will be the hardest thing, and this will push us to the hell of “nested quotation”. Besides all this, it epitomizes all sophisms and traps of the above things in itself. The diagonal function is a powerful idea, but it cannot be embedded it directly in the object language, out of two reasons:

• the object language has no functions at all (expect for 0 constant, successor, plus, times). Although some simpler functions can be built directly with them, but more difficult functions (i.e. those who can to be defined only by recursion) have to represented by formula.
• the diagonalization function works on formulas, and turn them to formulas. But the object language does not know the notion of formulas! It consists of formulae, but if we want to work on formulas inside the objectl naguage, them we have to do the damned tricks with structural descriptive names, quoatations etc.

Thus, the diagonalization formula will be a nasty thing

• being a representation of function by formula
• leading argument through a reification process, diagonalizing, then undoing reification (or viece versa? maybe I mistook) — a conjoint-like process, similar to the flying fish metaphore mentioned aboved, but very nasty, leading to nested quotations etc.

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

where

$\psi \equiv d_{g,\phi }^{u}$

Thus, diagonalization formula

${\mathfrak {D}}_{g,\Gamma }^{x,u,y}\in \mathbf {Form} _{\left\{x,y\right\}}^{t}$ (note that $u\notin {\mathcal {FV}}\left({\mathfrak {D}}_{g,\Gamma }^{x,u,y}\right)$ if u is a different variable from both x and y)

thus

${\mathfrak {D}}_{g,\Gamma }^{x,u,y}[x:=\ulcorner \phi \urcorner ]\in \mathbf {Form} _{\left\{y\right\}}^{t}$

where

$\phi \in \mathbf {Term} _{\left\{u\right\}}^{t}$

$\psi \in \mathbf {Term} _{\emptyset }^{t}$

will be denoted gere as a macro (frakture capital), although it does not take arguments (it is a constant). It is a huge concrete formula of object language, but of course it would spoil readability if we would copypaste it, thus we use name ${\mathfrak {D}}_{g,\Gamma }^{x,u,y}$ as a macro, thus, we can give it macro calls interlarded in object language texts. In the superscript, we shall parametrize the macor's name with the variable layout, so that plugging formulas together with variables can be planned.