Hoppa till innehållet

Henkinsats

Från Wikipedia

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.

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