13 Axiomatické systémy

  1. 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ů
  2. co je to kalkul VL?
    pojem označující axiomatický systém, užívaný v matematickém prostředí
  3. 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.

    Image Upload 1
  4. Df. Axiom
    Axiomy axiomatického systému S jsou základní (nedokazované) vybrané formule axiomatického systému S.
  5. 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)

    Image Upload 2
  6. 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)

    Image Upload 3
  7. Modus ponens (MP)
    Image Upload 4
  8. Pravidlo substituce
    • A
    • ------------
    • A[B/a]
    • (Pomocí [B/a] vyznačujeme nahrazení všech výskytů a v A pomocí B.)
  9. 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í.
  10. Df. Důkaz
    • Image Upload 5
    • 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é)

    Image Upload 6
  11. 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ů
    • Image Upload 7


    Image Upload 8
  12. 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.
  13. 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ý
  14. formule A je zvána vyvratitelná v axiomatickém systému S, právě když ...
    v S existuje důkaz ¬A.
  15. Df. Věta o dedukci (VD)
    Image Upload 9


    Image Upload 10
  16. Nepřímý důkaz a důkaz sporem
    Image Upload 11

    Image Upload 12

    Image Upload 13
  17. Vlastnosti axiomatických systémů
    • rozhodnutelnost,
    • bezespornost/konzistentnost,
    • úplnost,
    • korektnost
  18. 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.
  19. 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)
  20. Df. Korektnost
    Image Upload 14
  21. Df. Úplnost
    Image Upload 15
Author
iren
ID
354251
Card Set
13 Axiomatické systémy
Description
VÝROKOVÁ LOGIKA
Updated