Talk:Diagonal lemma/Proof with diagonal formula/Structural descriptive expression

Structural descriptive expressions provide a clear way for separation of levels “object language” versus “meta language”, even at points where a conceptual confusion would be easy to commit.

A consequent and detailed treatment of “structural descriptive expressions” (built out of structural descriptive names) can be found in Alfred Tarski's works. The notions appears also at other authors, hidden behind such phrases like “scheme” (p. 126 of ), “syntactic operation” .

Differences (contrast to the “interlarding” approach):

• $\ulcorner \dots \urcorner$ would not denote a suspicious typographical mark, it would simply be a function
• it will be $\llcorner \dots \lrcorner$ who will be used as typographical mark, turning object language signs to their respective namings / labels in the meta language
• units of object language would be “transferred” to meta language by corresponding structural descriptive expressions

Call by name

We should be able to call certain text fragments of object language by name in the meta language. First we build a language base (or an appropriate alternative approach).

Transferring syntax

$\forall \phi ,\psi \in \mathbf {Form} ^{t}\;\;\;\;\phi {\hat {\land }}\psi ,\;\phi {\hat {\lor }}\psi ,\;\phi {\hat {\to }}\psi ,\;\phi {\hat {\leftrightarrow }}\psi ,\;{\hat {\lnot }}\phi \in \mathbf {Form} ^{t}$

They belong to the meta language! They are the structural descriptive names for the approriate object language texts, but they are not conceptually the same.

$\phi {\hat {\land }}\psi \equiv \phi \frown {\underline {\land }}\frown \psi$

$\phi {\hat {\lor }}\psi \equiv \phi \frown {\underline {\lor }}\frown \psi$

${\hat {\lnot }}\phi \equiv {\underline {\lnot }}\frown \phi$

$\phi {\hat {\to }}\psi \equiv \phi \frown {\underline {\to }}\frown \psi$

$\phi {\hat {\leftrightarrow }}\psi \equiv \phi \frown {\underline {\leftrightarrow }}\frown \psi$

In fact, subformulas should be protected by parantheses, or prefix notation should be uesed.

Quotation

$\forall \phi \in \mathbf {Form} ^{t}\cup \mathbf {Term} ^{t}\;\;\;\;\ulcorner \phi \urcorner \in \mathbf {Term} ^{t}$

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

Motivation

All this enables us to ban suspicious interlarded things: meta vs object language is more clearly separated.

Variables can remain either “rigid”, or “transferred” too.

The main point is to maintain a well defined interface between the object vs meta language. For see the advantages clearly, a good example: the problem of “double quoatation”.

Because the new usage of $\ulcorner \dots \urcorner$ is very different. In the original usage, it was a mere typographical sign, a sort of macro, preprocessor of object language text. This can raise problems (similar to those of extensive vs intensive functors in logic, see . But now in the new usage, $\ulcorner \dots \urcorner$ is clearly an ordinary function. No direct, “typographical” connotations (with hidden traps) exist any more. The interface points between object and meta language is restricted to

• the basic names ${\underline {\land }}$, ${\underline {\lor }}$, ${\underline {\lnot }}$, ${\underline {\to }}$, ${\underline {\leftrightarrow }}$,
• and the $\frown$ concatenation

but we do not need this low level any more, because the transferring (${\hat {\land }}$, ${\hat {\lor }}$, ${\hat {\lnot }}$, ${\hat {\to }}$, ${\hat {\leftrightarrow }}$) alows us to avoid jumping around near the suspicious interface of the two levels -- we do not have to cross the dangerous border for each little function call.

Questions

• Must we make a distinction between a set of parts object language metalanguage and their respective names in the meta language? Is $\mathbf {Form} ^{t}$ is the same as ${\widehat {\mathbf {Form} ^{t}}}$?
• Does it mean, a metametalangage is introduced? Must the above the distinction be handled on the metametalevel. But I am not sure.
• $\ulcorner \dots \urcorner$ is mapping
  • from strings of object language to strings of object language?
  • Or rather, the respective met language names are concerned here? Is $\ulcorner \dots \urcorner$ mapping a subset of meta language (the so-called structural descriptive expressions) to the meta language? Mapping a clearly specified subset of the meta language strings (the structural descriptive expressions) to meta language strings?
• The same question can concern other things involved in sturctural descriptive expressions: $\phi {\hat {\land }}\psi ,\;\phi {\hat {\lor }}\psi ,\;\phi {\hat {\to }}\psi ,\;\phi {\hat {\leftrightarrow }}\psi ,\;{\hat {\lnot }}\phi$