Rossersats
Från Rilpedia
Texten från svenska Wikipedia
En rossersats för ett formellt system T ä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 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.
Referenser
- J. B. Rosser, Extensions of some theorems of Gödel and Church i Journal of Symbolic Logic, vol. 1, 1936, s. 87-91.
Se även:
