Rossersats

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{<}zPrf(\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

• Gödels ofullständighetsteorem
• Gödelsats
• Henkinsats

Referenser

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