Rossersats

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

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

Den informella betydelsen hos ${\displaystyle \rho }$ är

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

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

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