Fixed point theorem

The fixed point theorem (also fixed point theorem or diagonalization lemma ) is a sentence in mathematical logic for the description of self-referential statements in formal theories. It was used by Kurt Gödel in 1931 to construct his proof of the incompleteness of logical systems that are so expressive that one can axiomatize the natural numbers with them, and thus implicitly proven, but not explicitly mentioned under this name. The theorem is derived from the Diagonalisierungslemma that so following the Diagonalisierungsargument of Georg Cantor called.

Content at Gödel

The formalized object language is the first-level predicate logic with the Peano axioms. The fixed point theorem says that for every (one-digit) predicate there is a statement that ascribes this predicate to itself. This form of self-reference for the provability predicate Bew (x) constructed by him is - in addition to the object-language representation of the metalanguage through Godelization - the basis of his proof, in that it is shown that the sentence "This sentence is not provable" can be proven, which for Contradiction leads (details see there ).

Let be a predicate logic formula with the free variable . Then the predicate logic sentence exists with ${\ displaystyle \ varphi (x)}$ ${\ displaystyle x}$ ${\ displaystyle \ psi}$

{\ displaystyle \ psi \ longleftrightarrow \ varphi (\ ulcorner \ psi \ urcorner) \ quad}

, where the god number is from .

{\ displaystyle \ ulcorner \ psi \ urcorner}

{\ displaystyle \ psi}

This makes it possible to form the sentence in predicate logic that expresses something about a predicate logic sentence in its numerical representation, ie metalinguistic relationships can be formulated in the object language. The object language says something about itself. ${\ displaystyle \ varphi (\ ulcorner \ psi \ urcorner)}$ ${\ displaystyle \ psi}$

Tarski sentences

Alfred Tarski published his theorem of indefiniteness in 1936, which states that it is not possible in certain formal systems to define a truth predicate. The argument is similar about the so-called. Tarski sets , self-referential sentences of the form: "I am a member of M " for a lot of M . If one chooses for M the set of all wrong sentences of a system, the construction of a Tarski theorem leads to a contradiction in the definition of this set. From this it can be concluded that the set of all true propositions of a system cannot be defined within this system.

Modal logic instances
A (p)	Fixed point B
${\ displaystyle \ Box p}$	${\ displaystyle \ top}$
${\ displaystyle \ neg \ Box p}$	${\ displaystyle \ neg \ Box \ bot}$
${\ displaystyle \ Box \ neg p}$	${\ displaystyle \ Box \ bot}$
${\ displaystyle \ Box p \ rightarrow q}$	${\ displaystyle \ Box q \ rightarrow q}$
${\ displaystyle \ Box (p \ rightarrow q)}$	${\ displaystyle \ Box q}$
${\ displaystyle q \ lor \ Box p}$	${\ displaystyle \ top}$
↑ Since there is already a tautology. ${\ displaystyle \ Box p}$

Modal logic interpretation

In modal logic , Gödel's provability predicate is understood as a sign of necessity ( i.e. box ). This results in the following proof of the fixed point theorem: ${\ displaystyle \ Box}$

If there is a formula that only appears in a box in the scope , then there is a formula that does not appear and no propositional variables occur that do not already appear in , so that: ${\ displaystyle A (p)}$ ${\ displaystyle p}$ ${\ displaystyle B}$ ${\ displaystyle p}$ ${\ displaystyle A}$

{\ displaystyle \ vdash _ {GL} B \ longleftrightarrow A (p)}

.

Here's fixed point of , GL stands for Godel-Lob , a modal logic that to the set of Leib is enhanced as an axiom. ${\ displaystyle B}$ ${\ displaystyle A (p)}$

Web links

Wikibooks: Mathematics: Logic - Learning and teaching materials

Wikibooks: Math for Non-Freaks: Propositional Logic - Learning and Teaching Materials

literature

Volker Beeh: Truth, theorem, provability and the corresponding "liar sentences". In: Journal of Linguistics. 7.2 (1988): 151-172.
Graeme Forbes: Logic, philosophy of. In: E. Craig (Ed.): Routledge Encyclopedia of Philosophy . London 1998. History also on modal logic.
Peter H. Starke: Logical Foundations of Computer Science. Extensive script, which can also be downloaded as a PDF, HU Berlin.
Michael Pucher: Formal theories of truth according to Alfred Tarski (PDF), clear thesis on the subject
Alfred Tarski: The Concept of Truth in Formal Systems. 1936 ( thatmarcusfamily.org PDF).

Individual evidence

↑ Jesús Padilla Gálvez : Truth and self-reference. In: Journal for General Philosophy of Science. March 1991, Volume 22, pp. 111-132.
↑ Hans-Jürgen Heringer, Georg Stötzel (ed.): History of language and language criticism: Festschrift for Peter von Polenz for the 65th De Gruyter Berlin, New York 1993, p. 38 ff.
↑ Boolos: The Logic of Provability. Cambridge University Press 1993, Chapters 1-3.
↑ Wolfgang Stegmüller (Ed.): Self-reference, Tarski sentences and the indefinability of arithmetic truth. Springer Verlag Berlin, Heidelberg 1984 p. 375 f.
↑ Boolos: The Logic of Provability. Cambridge University Press 1993, p. 104.

[6] Since there is already a tautology. ${\ displaystyle \ Box p}$

[1] Jesús Padilla Gálvez : Truth and self-reference. In: Journal for General Philosophy of Science. March 1991, Volume 22, pp. 111-132.

[2] Hans-Jürgen Heringer, Georg Stötzel (ed.): History of language and language criticism: Festschrift for Peter von Polenz for the 65th De Gruyter Berlin, New York 1993, p. 38 ff.

[3] Boolos: The Logic of Provability. Cambridge University Press 1993, Chapters 1-3.

[4] Wolfgang Stegmüller (Ed.): Self-reference, Tarski sentences and the indefinability of arithmetic truth. Springer Verlag Berlin, Heidelberg 1984 p. 375 f.

[5] Boolos: The Logic of Provability. Cambridge University Press 1993, p. 104.