15b Vlastnosti axiomatických teorií

• že jestliže T ٟI- A, tak S ٟI- A, ale existuje formule A taková, že jestliže S ٟI- A, tak neplatí T ٟI- A.
• Například Peanova aritmetika PA je silnější než Robinsonova aritmetika Q, poněvadž v PA je dokazatelná formule (x+y)=(y+x), jež není dokazatelná v Q.

• i. rozhodnutelnost – jsme s to rozhodnout o každé
• formuli, zda je či není teorémem,
• ii. bezespornost – systém negeneruje protiřečící si formule, a tím pádem pak vůbec všechny formule,
• iii. korektnost – systém generuje jen (logicky) pravdivé formule, 
• iv. úplnost – systém dokazuje všechny (logicky) pravdivé formule

VL: úplná, bezesporná i rozhodnutelná

• PL1: existují bezesporné, úplné (a  také korektní), avšak nikoli rozhodnutelné axiomatické systémy (kalkuly).
• ^{Stručně pak říkáme, že PL1 je úplná, bezesporná, avšak nikoli rozhodnutelná.}

• PL2: bezesporná, nerozhodnutelná, a  není úplná.
• ^{(Existují ovšem její dokazovací systémy, které jsou korektní vzhledem k tzv. henkinovským modelům.) Důkaz neúplnosti je proslulým výsledkem práce Kurta Gödela (původní důkaz byl později zjednodušen např. Johnem Barkleym Rosserem). Jím dokázaná věta bývá obvykle formulována následovně (viz dále, ot. 12)}

Teorie T je sporná právě tehdy, když je v T dokazatelná jak A, tak ¬A. Teorie T, která není sporná, je bezesporná, tj. konzistentní.

• pojem spornosti/konzistence teorií je beze změn aplikovatelný i na teorie bez speciálních axiomů, tedy formální systémy (kalkuly) PL.
• To, že teorie je sporná, obnáší, že je v  ní dokazatelná každá formule daného jazyka. (Dále: platí-li T ٟI- A, tak T∪{¬A} je sporná.) Sporná teorie nemá žádný model, je to totiž vlastně množina formulí, která není splnitelná.
• Každá bezesporná teorie naopak má alespoň jeden model; tato vlastnost teorií je někdy označována jako sémantická bezespornost ^{(příslušný teorém pak angl. „model existence theorem“)}. Formule A dokazatelná v T, tj. T ٟI- A, je pravdivá v každém modelu T.

• Teorie T je rozhodnutelná právě tehdy, když existuje efektivní procedura (algoritmus), která o každé formuli jazyka T rozhodne, zda je či není teorémem T.
• _{Alonzo Church a  Alan Turing ovšem nezávisle dokázali nerozhodnutelnost PL1 (otázka rozhodnutelnosti byla v té době diskutována pod názvem „Entscheidungsproblem“, jako výzkumný úkol ji stanovil matematik David Hilbert). Následující není definice, ale tvrzení, k němuž existuje důkaz.}

• Žádná axiomatická teorie T zahrnující systém PL1 není rozhodnutelná.
• Daný výsledek ovšem neznamená nějakou absolutní nerozhodnutelnost: pravdivé formule PL rozhodnutelné jsou (což dokázal rovněž Church), pouze některé nepravdivé formule nejsou rozhodnutelné.
• ^{Dokonce platí, že všechny formule tzv. monadického fragmentu PL1 jsou rozhodnutelné. Rozhodnutelné nejsou pouze některé nepravdivé formule polyadického (relačního) fragmentu PL1.}
• přenáší se i na PL2

• Axiomatická teorie T je korektní právě tehdy, když platí, že jestliže T ٟI- A, tak T I= A.
• Speciálně platí, že jestliže ٟI- A, tak I= A.

• Pro každou (prvořádovou) teorii T, a to vč. PL1, a každou formuli A jazyka teorie T platí, že každá formule A, která je dokazatelná z T, tj. T ٟI- A, je sémantickým důsledkem T, tj. T I= A.
• Speciálně platí, že pro každou formuli A, jestliže ٟI- A, tak I= A.

_{o korektnosti někteří autoři mluví až v souvislosti s deduktivními systémy: korektní je ten deduktivní axiomatický systém PL, který neumožňuje odvodit neplatnou formuli}

• Axiomatická teorie T je úplná právě tehdy, když platí, že jestliže T I= A,tak T ٟI- A.
• Speciálně platí, že jestliže I= A, tak ٟI- A.

• Pokud se někdy hovoří o silné úplnosti, pak je míněno: T I= A právě tehdy, když T ٟI- A, načež slabou úplností je míněno: I= A právě tehdy, když ٟI- A.
• Někteří autoři pod silnou úplností rozumí to, že T je konečnou množinou formulí.
• Někdy je úplnost teorie T zase definována takto: teorie T je úplná, když pro každou uzavřenou formuli A z T platí, že ٟI-A nebo ٟI-¬A. Příkladem úplné prvořádové teorie je Presburgerova aritmetika

Kurt Gödel

Každá logicky pravdivá formule PL1 je dokazatelná, takže je-li I=A, pak ٟI- A, kde A je formule jazyka PL1.

Přesněji, Gödel dokázal, že teorie T je konzistentní právě tehdy, když T má model, tj. existuje struktura, v níž jsou všechny věty T pravdivé. V důsledku to znamená, že T ٟI-_PL A právě tehdy, když A je pravdivá v každém modelu T.

^{Mnozí autoři formulují na rozdíl od nás Větu o úplnosti PL1 jako ekvivalenci, tj. T ٟI- A právě tehdy, když T I= A, a proto už nemluví o korektnosti, poněvadž ji mají zahrnutu do jejich pojmu úplnosti. O korektnosti mluví tito autoři až v souvislosti s deduktivními systémy: korektní je ten deduktivní axiomatický systém PL, který nám nedovolí odvodit neplatnou formuli.}

Žádné bezesporné a rekurzivně axiomatizovatelné rozšíření Robinsonovy aritmetiky Q (např. PA), jejímž modelem je N, není úplnou teorií T.

• ^{Znamená to, že existuje formule pravdivá v N, která není dokazatelná, ani vyvratitelná v takové T, jež by měla uváděné charakteristiky. Taková Gödelova, resp. Rosserova formule zní}: „Nejsem dokazatelná v T“. (Rekurzivní axiomatizovatelnost znamená algoritmickou rozhodnutelnost množiny axiomů, tj. vlastně efektivní zadání T.)
• ^{Stojí za poznámku, že tato neúplnost je principiální}: tzv. zúplnění T vzniklé přidáním dané Gödelovy, resp. Rosserovy formule je právě tak neúplnou teorií.
• ^{Gödelův důkaz je založen na aritmetizaci syntaxe; díky tomu může kódovat formule, vč. problémové formule „Nejsem dokazatelná v T“, a dále na autoreferenci, tj. tzv. diagonálním lemmatu.}

Žádné bezesporné a rekurzivně axiomatizovatelné rozšíření PA není teorií T, v níž je dokazatelná konzistentnost T.

_{Druhá Gödelova věta o neúplnosti už ve své době vzbudila nemenší rozrušení, poněvadž protiřečila směrujícím ideám Hilbertova programu, podle něhož měly být všechny matematické problémy řešeny uvnitř jednoho formálního systému finitními prostředky}