-
základy úvah o axiomatických (formálních) systémech podal již který antický představitel...?
- Euklidés
- množina (např. geometrických) pravd je nekonečná
- - problém, jak určit takovouto rozsáhlou množinu
- - problém, jak se ujistit, že libovolná pravda z dané množiny skutečně je pravdou
- pojem axiomatického systému řeší oba naznačované problémy najednou
- - nejprve zvolíme (konečnou) množinu základních, evidentních a tedy důkaz nevyžadujících pravd, tzv. axiomů
- - dále zvolíme (konečnou) množinu bezpečných prostředků, tzv. odvozovacích pravidel (někdy zvaných dedukční či derivační pravidla)
- - ta umožňují z množiny axiomů generovat další pravdy, tzv. teorémy
- - jednotlivé teorémy, tedy dokazované pravdy, jsou vždy demonstrovány pomocí důkazů
-
co je to kalkul VL?
pojem označující axiomatický systém, užívaný v matematickém prostředí
-
Každý axiomatický systém S je zadán:
- 1. formálním jazykem (bez sémantiky),
- 2. množinou axiomů,
- 3. množinou odvozovacích pravidel.
-
Df. Axiom
Axiomy axiomatického systému S jsou základní (nedokazované) vybrané formule axiomatického systému S.
-
volba axiomů podléhá dvěma kritériím:
- každý axiom je tautologií
- množina axiomů musí umožňovat, aby se z nich daly odvodit pokud možno všechny logicky platné formule (tautologie)
-
aby bylo možno z pravidel odvození vypustit Pravidlo substituce, jsou obvykle rovnou volena axiomová schémata:
- Axiom 1: A → (B → A)
- Axiom 2: (A → (B → C)) → ((A → B) → (A → C))
- Axiom 3: (¬B → ¬A) → (A → B)
-
-
Pravidlo substituce
- A
- ------------
- A[B/a]
- (Pomocí [B/a] vyznačujeme nahrazení všech výskytů a v A pomocí B.)
-
korektnost odvozovacích pravidel může být vyjádřena větou, jejíž platnost je následně dokazována
Věta o korektnosti pravidla Modus ponens v podobě: Jestliže formule A a A → B jsou tautologiemi, tak i B je tautologií.
Dokaž to
- Důkaz:
- Předpokládejme, že A i A → B jsou logicky pravdivé formule (tautologie); proto nemůže existovat valuace v, při níž by B mohla být nepravdivá, poněvadž to by A → B nemohla být při této v pravdivá a tedy ani tautologií.
-
Df. Důkaz
- jako důkazy označujeme posloupnosti formulí, jež jsou následky aplikací odvozovacích pravidel
- závěrečnými formulemi důkazů jsou formule dokázané, tj. tzv. teorémy
- jak pojem teorému, tak hlavně pojem důkazu je syntaktický
- k získání teorému tedy není nezbytná nějaká sémantická úvaha či snad intuice, ale pouhá manipulace symbolů proto jsou možné počítačově generované důkazy a automatické dokazování
- důkazy v tom či jiném dokazovém systému (například důkazy v hilbertovském a gentzenovském systému jsou vzájemně přeložitelné)
-
Df. Důkaz z předpokladů
- důkaz z předpoklad·, někdy nazývaný důkaz z hypotéz, odděluje předpoklady a vlastní dokazované formule, a proto je formální obdobou běžných úsudků, jež se sestávají z premis a závěrů

-
Df. Dokazatelná formule
Formule A je dokazatelná v axiomatickém systému S, právě když v tomto systému S existuje důkaz, jehož je A posledním členem.
-
Df. Teorém
Formule A je teorémem axiomatického systému S, právě když je dokazatelná v systému S. Značíme pomocí ι-S A.
někdy se teorémům říká věty, ale v případě teorémů studovaných kalkulů (tedy nikoli teorémů naší metalogiky), je tento termín spíš vzácný
-
formule A je zvána vyvratitelná v axiomatickém systému S, právě když ...
v S existuje důkaz ¬A.
-
-
Nepřímý důkaz a důkaz sporem
-
Vlastnosti axiomatických systémů
- rozhodnutelnost,
- bezespornost/konzistentnost,
- úplnost,
- korektnost
-
Df. Rozhodnutelnost
- množina axiomů daného axiomatického systému musí být rozhodnutelná v množině správně utvořených formulí
- když se hovoří o rozhodnutelnosti axiomatického systému, je tím míněn následující pojem
- Df. Rozhodnutelnost: Axiomatický systém S je rozhodnutelný, právě když o každé formuli A je rozhodnutelné (tj. existuje příslušný efektivní algoritmus), zda je či není teorémem S.
-
Df. Bezespornost
- Df. Bezespornost: Axiomatický systém S je bezesporný (konzistentní), právě když v S nejsou dokazatelné formule A a ¬A (tj. spor).
- co už tak samozřejmé být nemusí, je to, zda axiomatický systém jako teorémy generuje pouze tautologie (což je korektnost) a hlavně zda generuje všechny tautologie (což je úplnost)
-
-
|
|