15 axiomaticke teorie

• i. jazykem (bez sémantiky) 
• ii. (konečnou) množinou základních, evidentních, a tedy důkaz nevyžadujících pravd, tzv. axiomů,
• iii. (konečnou) množinou odvozovacích pravidel (alternativně nazývaných dedukční či derivační pravidla).

• Z množiny vybraných formulí se pomocí pravidel odvození dostáváme k dalším formulím; tyto dokazované formule
• jsou teorémy, tedy formule, k nimž v daném axiomatickém systému existuje důkaz.

syntax: abeceda, gramatika, podformule

Axiom 4 bývá alternativně nazýván Axiom konkretizace anebo též Axiom univerzální instanciace ^{(angl. „universal instantiation“, srov. níže pravidlo UI)}; připomeňme si, že „A[t/x]“ znamená, že term t je substituovatelný za x.

• Pro každou formuli A, a libovolnou proměnnou x, a každou teorii T platí, že T ٟI- A platí právě tehdy, když platí T I- ٟ∀ x A.
• Dodejme, že Pravidlo generalizace nelze přeměnit na axiom A→∀x A, poněvadž tato formule není logicky pravdivá, jak lze snadno ukázat (uvažme, že A je B(x), přičemž pro nějakou hodnotu je B(x) nepravdivá, takže ∀x B(x) je nepravdivá, ač při určitém ohodnocení je B(x) pravdivá). Je-li však A logicky pravdivá nebo uzavřená formule, tak se A→∀x A chová jako logicky pravdivá. V důsledku budeme muset omezit platnost Věty o dedukci.

Axiomatická teorie T je vlastně množinou všech formulí, které lze odvodit z axiomů T pomocí odvozovacích pravidel T. Účelem každé teorie je pojednávat nějakou předmětnou oblast, třeba oblast ostrého uspořádání.

• Každá axiomatická teorie T je dána:
• i. jazykem T, jež obsahuje speciální symboly T
• ii. množinou speciálních axiomů T.

• Jazyk každé axiomatické teorie T proto obsahuje speciální symboly, často se říká i mimologické symboly, jež se týkají předmětné oblasti, o nichž daná teorie vypovídá. Například speciální symbol „<“ je prostředek vypovídání o vztahu ostrého uspořádání.
• Dále axiomatická teorie obsahuje speciální axiomy týkající se právě těchto speciálních symbolů. Tyto axiomy jsou nazývány též mimologické axiomy či vlastní axiomy, nebo jen axiomy teorie. Ze speciálních axiomů T lze vyvozovat další tvrzení této teorie. Jako speciální axiomy jsou brány vždy uzavřené formule, tj. sentence, protože pro ty splývá splnitelnost a pravdivost, takže PG se pro ně chová korektně. Nutno podotknout, že speciální axiomy nemusí být logicky platné.

• Proto teorii T vymezujeme jen tím, co přesahuje nějaký axiomatický systém PL, totiž množinou speciálních symbolů a množinou speciálních axiomů.
• Nepotřebujeme tedy stanovovat množinu odvozovacích pravidel teorie T, chápeme ji jako totožnou s tou množinou odvozovacích pravidel, kterou má přijatý axiomatický systém PL.

• = teorie s jazykem PL1, který je obohacen o speciální binární
• predikátový symbol „<“.
• Axiomy této teorie jsou:
• ireflexivita (<): ∀x ¬(x<x)
• tranzitivita (<): ∀x∀y∀z [(x<y→ ((y<z)→ (x<z))]

• Speciální axiomy teorie T implicitně definují speciální symboly (resp. jimi denotované objekty) v nich obsažené. Kdybychom dané axiomy změnili, například bychom k těmto axiomům přidali axiom
• totálnost (<): ∀x∀y ((x<y) ∨ (y<x) ∨ (x=y)) 
• tak bychom vymezili jiný vztah než <, v daném případě vztah ostrého lineárního uspořádání. Zmiňované tři axiomy tedy tvoří teorii ostrého lineárního uspořádání.

• jazyk PL1 s identitou (=), jenž je obohacen o:
• - konstantu „0“ (nula, přesněji: nejmenší přirozené číslo)
• - funkční symboly „S“ (následník, značen někdy pomocí ʹ psaným za číslem),
• - „+“ (operátor sčítání)
• - „ד (operátor násobení).

Uzávěry těchto axiomů (např. ∀x (S(x)≠0)) jsou axiomy Robinsonovy aritmetiky značené Q; na tyto axiomy je zvykem stručně referovat pomocí „Qn“.

Robinsonova (Q) aritmetika je neúplná teorie, např. v ní nejsou dokazatelné, ani vyvratitelné formule (x+y)=(y+x) či (x×y)=(y×x). Navíc je nerozhodnutelná.

• Peanova aritmetika, značená PA, vznikne z Robinsonovy aritmetiky přidáním schématu axiomu indukce (pro libovolnou vlastnost P):
• [P(0) ∧ ∀x (P(x)→ P(S(x))] → ∀x P(x)
• (Jak dokázal Kurt Gödel ve své slavné Větě o neúplnosti, Peanova aritmetika je neúplná. Peanova aritmetika je také nerozhodnutelná.)

• Presburgerova aritmetika je slabší než Peanova aritmetika, její jazyk neobsahuje symbol násobení × a z výše uvedených axiomů disponuje axiomy EA1, EA2, EA4, EA5 a schématem axiomu indukce.
• (Presburgerova aritmetika je úplná a rozhodnutelná teorie.)

• definice modelu teorie je vlastně případem modelu množiny
• formulí, neboť teorii můžeme vidět jako množinu formulí, jež jsou generovány z axiomů T.

• Model teorie
• Jestliže M je struktura pro jazyk teorie T a v M je splněn každý z axiomů T, tak M je modelem teorie T. Značíme M I= T.
• Alternativně se říká, že T platí v M nebo že T je pravdivá v M. ^{Varianta se splněním, podtrhuje senzitivitu vzhledem k ohodnocením.}
• Pro ilustrativní příklad modelu teorie, přirozená čísla jsou jakožto struktura N modelem teorií Q i PA; N je tzv. standardní model aritmetiky.

každý teorém T je pravdivý v  každém modelu T.

• (O modelech teorií byla v rámci matematické logiky zjištěna spousta zajímavých poznatků. Například Skolemova-Löwenheimova věta (ve  směru „dolů“) říká, že jestliže M je modelem T s (nejvýše) spočetným jazykem, tak existuje
• model Mʹ této T, který je (nejvýše) spočetný.)

• Formule A je sémantickým důsledkem teorie T, značeno T I= A, právě tehdy, když je formule A splněna každým modelem teorie T.
• Alternativně se říká, že formule A je pravdivá v teorii T, nebo že je (tauto)logicky odvoditelná z teorie T.
• (Pro srovnání: v rámci VL jsme mluvili o (tauto) logickém důsledku množiny formulí T.) Například formule jako (x+y)=(y+x) je sémantickým důsledkem PA, nikoli ale Q, tkž PA je silnější teorie

Důkazy spočívají v syntaktické manipulaci s formulemi pomocí pravidel odvozování. (Připomeňme si též, že axiomy můžeme vidět jako bezpředpokladová pravidla.) Nevyžadují tedy odvolání na sémantiku daných formulí, natož na nějakou (třeba sémantickou) intuici.

• Nechť T je teorie. Konečná posloupnost formulí A₁, A₂, ..., A_n
• je důkazem ze systému předpokladů teorie T právě tehdy, když pro každé i takové, že 1 ≤ i ≤ n, je formule A_i buď
• 1) axiomem T nebo
• 2) je prvkem T nebo
• 3) je odvozena aplikací některého odvozovacího pravidla T na formule A_j, ..., A_k, přičemž j, ..., k < i.

Důkaz bez předpokladů má T=0, proto v něm nedochází k situaci 2).

Formule A  je dokazatelná v axiomatické teorii T  právě tehdy, když v této teorii T existuje důkaz, jehož je tato formule A posledním členem. Značíme T ٟI- A.

Formule A je vyvratitelná v axiomatické teorii T právě tehdy, když je v T dokazatelná formule ¬A. (Formule A, která není dokazatelná nebo vyvratitelná v axiomatické teorii T, je nezávislá na T.)

Formule A  je teorémem axiomatické teorie T  právě tehdy, když je dokazatelná v T. Značíme ٟT I-_T A (ev. T I- A).

VD pomáhá zkracovat důkazy, poněvadž dokážeme-li (při předpokladech T), že A ٟI- B, tak můžeme za dokázané považovat i (A→B).

• Věta o dedukci:
• Pro formuli B a každou uzavřenou formuli A (tj. sentenci) jazyka teorie T platí, že T∪{A} I- ٟ B právě tehdy, když T ٟI- A→B).

Uvědomme si závažný rozdíl vzhledem k VD námi formulované pro VL: nynější formulace se explicitně omezuje na uzavřené formule PL, tj. na sentence. Důvodem je že  A→∀x A nemusí být logicky pravdivá (protože A může být pravdivá, ale její uzávěr nikoli), čili nesmíme dovolit T I- A→∀x A (daný axiomatický systém PL či teorie jej obsahující by nebyli korektní).