Gödelsats
Från Rilpedia
En gödelsats, efter Kurt Gödel, 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 inte finns något bevis för mig i T.
γ är mycket riktigt sann, och obevisbar 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.
Gödelsatsen är unik, i den meningen att den är bevisbart ekvivalent med konsistenspåståendet för T. Det är alltså just påståendet att T är konsistent som är det sanna (om T är ω-konsistent), obevisbara påstående som erhålls genom denna konstruktion.