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.