Rossersats

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

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

T \vdash \rho \leftrightarrow \forall z (Prf(\rho, z) \to \exists y {<} z Prf(\lnot \rho, y))

Den informella betydelsen hos \rho är

Jag är sann om och endast om det för alla bevis för mig i T finns ett kortare bevis för min negation.

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

  • T är tillräckligt stark, dvs kan koda alla avgörbara talteoretiska relationer
  • T ä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.