Henkinsats

En henkinsats för ett formellt system ${\displaystyle T}$ är en sats ${\displaystyle \eta }$ skapad med hjälp av fixpunktssatsen, sådan att

${\displaystyle T\vdash \eta \leftrightarrow \exists yPrf(\eta ,y)}$

Den informella betydelsen hos ${\displaystyle \eta }$ är

Jag är sann om och endast om jag är bevisbar i ${\displaystyle T}$.

Henkinkonstruktionen presenterades 1952 av Leon Henkin som en reaktion på Gödelsatsen. Trots henkinsatsens mer naiva utsaga dröjde det flera år innan Martin Löb lyckades bevisa att henkinsatsen är sann.

• L. Henkin, A problem concerning provability i Journal of Symbolic Logic, vol. 17, 1952, s. 160.
• M. H. Löb, Solution of a problem of Leon Henkin i Journal of Symbolic Logic, vol. 20, 1955, s. 115-118.

• Gödels ofullständighetsteorem
• Rossersats