Henkinsats

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

$T⊢\eta \leftrightarrow \mathrm{\exists }yPrf(\eta ,y)$

Den informella betydelsen hos $\eta$ är

Jag är sann om och endast om jag är bevisbar i $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.

Referenser

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

Se även

• Gödels ofullständighetsteorem
• Rossersats