13 Axiomatické systémy

• 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ů

pojem označující axiomatický systém, užívaný v matematickém prostředí

• 1. formálním jazykem (bez sémantiky),
• 2. množinou axiomů,
• 3. množinou odvozovacích pravidel.

Axiomy axiomatického systému S jsou základní (nedokazované) vybrané formule axiomatického systému S.

• 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)

• Axiom 1: A → (B → A)
• Axiom 2: (A → (B → C)) → ((A → B) → (A → C))
• Axiom 3: (¬B → ¬A) → (A → B)

• A
• ------------
• A[B/a]
• (Pomocí [B/a] vyznačujeme nahrazení všech výskytů a v A pomocí B.)

• 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í.

• 
• 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é)

• 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ů
• 

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.

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ý

v S existuje důkaz ¬A.

• rozhodnutelnost,
• bezespornost/konzistentnost,
• úplnost,
• korektnost

• 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: 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)