Henkinsats

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

T\vdash \eta \leftrightarrow \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