# Difference between revisions of "User:IssaRice/Computability and logic/Diagonalization lemma"

(→Comparison table) |
(→Comparison table) |
||

Line 46: | Line 46: | ||

|- | |- | ||

| Index of composition || <math>i</math> || <math>\ulcorner B\urcorner</math> | | Index of composition || <math>i</math> || <math>\ulcorner B\urcorner</math> | ||

+ | |- | ||

+ | | || <math>d(i)</math> || <math>\mathrm{diag}(\ulcorner B\urcorner)</math> | ||

|- | |- | ||

| Composition applied to own index (i.e. diagonalization of the composition) || <math>f\circ d(i)</math> || <math>B(\ulcorner B\urcorner)</math> | | Composition applied to own index (i.e. diagonalization of the composition) || <math>f\circ d(i)</math> || <math>B(\ulcorner B\urcorner)</math> |

## Revision as of 03:58, 8 February 2019

The **diagonalization lemma**, also called the Godel-Carnap fixed point theorem, is a fixed point theorem in logic.

## Rogers's fixed point theorem

Let be a total computable function. Then there exists an index such that .

(simplified)

Define (this is actually slightly wrong, but it brings out the analogy better).

Consider the function . This is partial recursive, so for some index .

Now since . This is equivalent to by definition of . Thus, we may take to complete the proof.

## Diagonalization lemma

(semantic version)

Let be a formula with one free variable. Then there exists a sentence such that iff .

Define to be where . In other words, given a number , the function finds the formula with that Godel number, then diagonalizes it (i.e. substitutes the Godel number of the formula into the formula itself), then returns the Godel number of the resulting sentence.

Let be , and let be .

Then is , by substituting in the definition of .

We also have by definition of . By definition of , this is , so we have .

To complete the proof, apply to both sides of the final equality to obtain iff ; this simplifies to iff .

## Comparison table

Step | Rogers's fixed point theorem | Diagonalization lemma |
---|---|---|

Theorem statement | ||

Given mapping | ||

Definition of diagonal function | ||

Composition of given mapping with diagonal function () | ||

Naming the composition | ||

Index of composition | ||

Composition applied to own index (i.e. diagonalization of the composition) | ||

Explicitly showing previous composition | ||

Definition of G | is | |

Renaming index | ||

Leibniz law to previous row |