-
Axiomatický systém je dán:
- 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).
-
jaký je vztah mezi teorémem a důkazem?
- 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.
-
-
Axiomová schémata PL1, které znáš už z VL
-
Další axiomová schémata PL1
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.
-
-
Pravidlo generalizace má úzkou souvislost s Větou o uzávěru:
- 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.
-
df axiomatické teorie PL
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é.
-
Teorii T chápejme jako jakousi nadstavbu nějakého axiomatického systému PL. Pro případy s PL1 se pak někdy hovoří o prvořádových teoriích. Axiomatické systémy PL, tedy predikátové kalkuly, můžeme na druhou stranu chápat jako axiomatické teorie s prázdnou množinou speciálních symbolů a speciálních axiomů.
Proto teorii T vymezujeme jen ...
- 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.
-
df teorie ostrého uspořádání, které tři axiomy ji tvoří?
- = 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í.
-
Axiomatizovány už byly rozsáhlé partie matematiky; problémy axiomatizace matematických teorií jsou předmětem metamatematiky. Z pohledu logiky patří k nejznámějším teoriím různé axiomatické teorie množin (ZFC, NBG). V matematické logice je velká pozornost věnována axiomatickým teoriím aritmetiky.
Zde si uvedeme nejprve příklad teorie elementární aritmetiky. Jazykem této teorie je ...
- 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í).
-
Speciální axiomy této teorie jsou tyto (kde „EAn“, pro 1≤n≤7, je pracovní označení):
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“.
-
df Robinsonova aritmetika
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á.
-
df Peanova aritmetika
- 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á.)
-
df Presburgerova aritmetika
- 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.)
-
df Model 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.
-
v důsledku toho, že axiomy T generují teorémy, tak při korektnosti T platí, že každý teorém T je pravdivý ...
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ý.)
-
df Sémantický důsledek teorie
- 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
-
V čem spočívají důkazy v rámci PL?
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.
-
df důkaz z předpokladů
- Nechť T je teorie. Konečná posloupnost formulí A1, A2, ..., An
- 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 Ai buď
- 1) axiomem T nebo
- 2) je prvkem T nebo
- 3) je odvozena aplikací některého odvozovacího pravidla T na formule Aj, ..., Ak, přičemž j, ..., k < i.
Důkaz bez předpokladů má T=0, proto v něm nedochází k situaci 2).
-
df dokazatelnost formule
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ž ...
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.)
-
df teorém
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).
-
df věta o dedukci
VD pomáhá zkracovat důkazy, poněvadž d okáž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í).
-
Uveďte, co značí následující zápisy:
|
|