Rossersats

Från Wikipedia
Hoppa till: navigering, sök

En rossersats 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 det för alla bevis för mig i finns ett kortare bevis för min negation.

Alla rossersatser konstruerade på detta sätt är sanna, och varken bevisbar eller motbevisbar i så snart uppfyller följande två egenskaper:

  • är tillräckligt stark, dvs kan koda alla avgörbara talteoretiska relationer
  • är konsistent.

Satsens upphovsman är J. Barkley Rosser.

Se även[redigera | redigera wikitext]

Referenser[redigera | redigera wikitext]

  • J. B. Rosser, Extensions of some theorems of Gödel and Church i Journal of Symbolic Logic, vol. 1, 1936, s. 87-91.