Jump to content

Talk:Diagonal lemma/Proof with diagonal formula/Metalanguage

Page contents not supported in other languages.
From Wikipedia, the free encyclopedia

Non-interlarded things

[edit]

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

[edit]
  • 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 . See exact details below at #Structural descriptive names.

Proof theoretic notations

[edit]

denotes derivation

denotes interderivability [1]

Let us extend the above notion slightly: iff and .

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

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

exctly then, if

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

Interlarded things

[edit]

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.

Items

[edit]
Metavariables
[edit]

for formulas by small Greek letters: , … Variable substitutions, if any, are added like .

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

Quantification
[edit]

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 ’”:

Clause
[edit]

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

Example:

where
Pattern naming (grouping)
[edit]
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:

We can use term/formula identities to express our exploring repeating patterns. Motivating example: A good news: if we look at the formula

carefully, we can explore a new occurence of repeating patern: forming on the left-hand side, because :

Our exploration can be registered by formula identity

in a concise way.

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

Macros (meta name-functors)
[edit]

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. denoting . 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. the correspondent of natural number 4 in th object language.

Macros will be denoted by fraktur capitals: , the arguments, if any, are added as superscript or subscript.

Operations

[edit]
Expansion
[edit]

of macro or metavariable

Variable substitution
[edit]

in a formula of the object language, denoted by

Quotation
[edit]

maybe it can be regarded as a special macro expansion:

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 , among the many parameters, g is the Gödel numbering. Similar remarks concern also the notation of diagonal function .

Enlarging metalanguage

[edit]

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 letin … construct).

Definition

[edit]

E.g. macro defintion, consisting of a triple of the definiendum, the equivalence sign , and the definiens. Equivalence sign 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: defines the “representation” macro (see below).

Specification

[edit]

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:

is represented in the object language through iff

(Here, is used as the “macro” for representing natural numbers in the object language, thus, itself does not belong to the object language. alltogether n times).

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

where

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.

Structural descriptive names

[edit]

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.

Strong object language

[edit]

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 , , , … 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
[edit]

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!):

Thus 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 of this macro, the fracture equivalent of “R”. Thus, maps a part of the meta language in the object language.

Gödel numbering
[edit]

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

Quotation
[edit]

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 . Thus, both the source and the target are part of the object language, but the definition itself below

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

Diagonal function
[edit]

an easy thing among the many hard ones: , 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
[edit]

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.

where

Thus, diagonalization formula

(note that if u is a different variable from both x and y) [3]

thus

where

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

  1. ^ An algebraization of many-sorted logic can be read the following book: On the algebraization of many-sorted logics, written by Carlos Caleiro and Ricardo Gonçalves. The book also can be used as introductory material.
  2. ^ Csirmaz, László and Hajnal, András: Matematikai logika. Eötvös Loránd University, Budapest, 1994. (online available, in Hungarian)
  3. ^ This snetence may be misunderdstood. x, u, y etc. are not literally the variables of the object language themselves, but are there metavariables over them.