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

Den informella betydelsen hos är

Jag är sann om och endast om jag är bevisbar i .

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.

ReferenserRedigera

  • 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 ävenRedigera