Talk:Diagonal lemma/Proof with diagonal formula/Metalanguage

From Wikipedia, the free encyclopedia

Contents

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

[edit] Set-theoretic notations

  • \phi \in \mathbf{Form}_{\left\{x\right\}}^t denotes that φ 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.

[edit] Proof theoretic notations

\vdash denotes derivation

\dashv\vdash denotes interderivability [1]

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).

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

[edit] Items

[edit] Metavariables

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

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

[edit] Quantification

The theorem itself is a good example for use of metavariables in quantification — “for all property π, there is a fixed point φ, saying ‘I am of property π’”:

\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]

[edit] 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^u_g\left(\phi\right)

[edit] 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: φ 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.

[edit] Macros (meta name-functors)

Macros can have arguments. I shall use various tricks to denote parametrization of macros: super- and subscripts, substitution noatiton …[…:=…] etc. The “most elastic”, “least fixed” parameter may be denoted sometimes by putting it in parantheses (instead of superscript/subscript), e.g. g^u_g\left(\phi\right) denoting \phi[u:=\ulcorner\phi\urcorner]. We must take care in such cases: we should not think of the formula as consisting of literally something d function symbol, then argument φ on the object language level. To lessen the probability for misunderstanding, the diagonal formula will be the only metalanguage constructs where I denote parametrization also by postfixing the argument listed between parantheses. In most cases, I shall avoid this denotion 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.

[edit] Operations

[edit] Expansion

of macro or metavariable

[edit] Variable substitution

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

[edit] Quotation

maybe it can be regarded as a special macro expansion:

\ulcorner\phi\urcorner \equiv \mathfrak R_{g\left(\phi\right)}

it is composed out of

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

of the quoted formula (or maybe sometimes term).

That is the cause why constructs containing quotation are alwas parametrized with g Gödel numbering (maybe among others), e.g. in the notation for diagonal formula building macro \mathfrak D^{x,u,y}_{g,\Gamma}, among the many parameters, g is the Gödel numbering. Similar remarks concern also the notation of diagonal function d^u_g.

[edit] 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 φ, ψ etc.will be given constraints,requirements, ina kind of where clause (or let … in … construct).

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

[edit] 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 [2] 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 (s 0) \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^u_g\left(\phi\right)

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

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

They serve as the basic elements for building structural descriptive expressions.

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

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

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

[edit] 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_{g\left(\phi\right)}

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

[edit] Diagonal function
d^u_g: \mathbf{Form^t_{\left\{u\right\}}} \to \mathbf{Form^t_\emptyset}
\phi \mapsto \phi[u:=\ulcorner\phi\urcorner]

an easy thing among the many hard ones: du, 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).

[edit] 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^u_g\left(\phi\right)

Thus, diagonalization formula

\mathfrak D_{g,\Gamma}^{x,u,y} \in \mathbf{Form}^t_{\left\{x,y\right\}} (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) [3]

thus

\mathfrak D_{g,\Gamma}^{x,u,y}[x:=\ulcorner\phi\urcorner] \in \mathbf{Form}^t_{\left\{y\right\}}

where

\phi \in \mathbf{Term}^t_{\left\{u\right\}}
\psi \in \mathbf{Term}^t_\emptyset

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.