Přehledově dokazatelnost ve výrokové logice

Dokazatelnost VL

Odvozovací pravidlo modus ponens

• Odvozovací pravidlo = předpis pomocí nějž ze vstupních formulí odvozujeme další formule $MP:\frac{\varphi ,\varphi \Rightarrow \psi }{\psi }$
• Z formulí $\varphi$ a $\varphi \Rightarrow \psi$ odvodíme formuli $\psi$

Axiomy VL

• Axiomy = formule, které automaticky přijímáme jako “platné”
• Axiomy popisují vlastnosti logických spojek a jejich vzájemný vztah
• Axiomová schémata:
  • (A1): $\varphi \Rightarrow (\psi \Rightarrow \varphi )$
  • (A2): $(\varphi \Rightarrow (\psi \Rightarrow \chi ))\Rightarrow ((\varphi \Rightarrow \psi )\Rightarrow (\varphi \Rightarrow \chi ))$
  • (A3): $(\neg \psi \Rightarrow \neg \varphi )\Rightarrow (\varphi \Rightarrow \psi )$

Důkaz, syntaktické vyplývání

• Důkaz formule $\psi$ z množiny formulí $T$ je libovolná posloupnost formulí ${\psi }_1,...,{\psi }_n$ taková, že ${\psi }_n=\psi$ a každá ${\psi }_i(i=1,...,n)$:

  • je axiomem
  • nebo náleží do $T$
  • nebo vzniká z předchozích formulí důkazu pomocí odvozovacího pravidla MP
    • tedy existují indexy $j,k<i$ tak, že ${\psi }_k$ je formule ve tvaru ${\psi }_j\Rightarrow {\psi }_i$

• Formule $\psi$ je dokazatelná z $T$ (zapisujeme $T⊢\psi$), pokud existuje důkaz formule $\psi$ z $T$. Pokud $⊢\psi$, pak říkáme, že $\psi$ je dokazatelná

• Dokazatelnosti budeme také říkat syntaktické vyplývání, abychom tím zdůraznili, že jde o protějšek sémantického vyplývání

  • $T\models \psi$ = sémantické vyplývání
  • $T⊢\psi$ = syntaktické vyplývání

Tvrzení

• Pro každou množinu formulí $T$ a formule $\psi ,\varphi$ platí, že z $T⊢\psi \Rightarrow \varphi$ a $T⊢\psi$ plyne $T⊢\varphi$.

Věta

• Pro každou formuli $\psi$ platí $⊢\psi \Rightarrow \psi$.

Monotonie dokazatelnosti (MD)

• Nechť $T$ a $S$ jsou množiny formulí a $\psi ,\varphi$ jsou formule.
• Pak platí: Pokud $T⊢\psi$ a pro každou $\varphi \in T$ máme $S⊢\varphi$, pak $S⊢\psi$.

Věta o dedukci (VoD)

• Pro každou množinu formulí $T$ a formule $\psi ,\varphi$ platí:
• $T⊢\psi \Rightarrow \varphi$, právě když $T,\psi ⊢\varphi$.

Spornost a bezespornost

• Množina formulí $T$ se nazývá sporná (nekonzistentní), jestliže je z ní dokazatelná jakákoliv formule.
• Není-li $T$ sporná (tedy existuje formule, která není z $T$ dokazatelná), nazývá se bezesporná (konzistentní)

Věta o důkazu sporem

• Nechť $T$ je množina formulí, nechť $\psi$ je libovolná formule. Pak platí: $T⊢\psi$, právě když $T⊢\neg \psi$ je sporná množina.
  • Předpokládáme neplatnost tvrzení a dojdeme ke sporu, čímž dokážeme platnost daného tvrzení

Věta o důkazu rozborem případů

• Pro množinu formulí $T$ a formule $\psi ,\varphi ,\chi$ platí $T,\psi \vee \varphi ⊢\chi$, právě když $T,\psi ⊢\chi$ a $T,\varphi ⊢\chi$

Věta o neutrální formuli

• Pro množinu formulí $T$ a formule $\psi$ a $\varphi$ platí $T⊢\varphi$, právě když $T,\psi ⊢\varphi$ a $T,\neg \psi ⊢\varphi$.

Věta o korektnosti

• Pro libovolnou množinu formulí $T$ a formuli $\psi$ platí, že je-li $T⊢\psi$, pak $T\models \psi$.
  • Speciálně tedy, každá dokazatelná formule je tautologií

Churchovo lemma (ChL)

• Pro libovolnou formuli $\psi (p_1,...p_n)$ platí $p_1^e,...,p_n^e⊢{\psi }^e$

Věta o úplnosti, slabá verze

• Pro libovolnou konečnou množinu $T$ formulí a formuli $\psi$ platí, že z $T\models \psi$ plyne $T⊢\psi$.
  • Speciálně, každá pravdivá formule je dokazatelná

Navigace

Předchozí: Základní syntaktické a sémantické pojmy výrokové logiky Následující: Syntax a sémantika predikátové logiky Celý okruh: 1. Teoretické základy informačních technologií