Dokazatelnost

Dokazatelnost

Definice: Formální důkaz formule $\varphi$ z teorie $T$ v daném dokazovacím systému je konečná posloupnost

$${\varphi }_0,\dots ,{\varphi }_n=\varphi$$

taková, že každá položka je buď logický axiom, axiom teorie $T$, nebo je odvozena z předchozích pomocí příslušného odvozovacího pravidla.

Definice: Zamítnutím formule $\varphi$ (refutation) rozumíme formální důkaz kontradikce z teorie $T$ nebo z $T\cup \{\neg \varphi \}$.

1. Tablo metoda:
   Tablo důkaz formule $\varphi$ z teorie $T$ je sporné tableau s kořenem obsahujícím všechny axiomy $T$ jako pravdivé a formuli $\varphi$ jako nepravdivou ($F\varphi$). Příklad pro $T=\{p\to q,p\}$ a cíl $q$:

   • Kořen: $T(p\to q),T(p),F(q)$
   • Pravidlo pro $T(\phi \to \psi )$ rozvětví na $F(\phi )\mid T(\psi )$
     1. Větev $F(p)$ se uzavře proti $T(p)$.
     2. Větev $T(q)$ se uzavře proti $F(q)$.
        Všechny větve se uzavřely, takže tableau je refutující a $T\models q$.

2. Rezoluční metoda:
   Rezoluční důkaz je refutace množiny klauzulí pomocí rezolučního pravidla tak, že se odvodí prázdná klauzule $\square$.
   Příklad pro $T=\{p\to q,p\}$ a cíl $q$:

   • Přepište do CNF:
     • $p\to q\sim \neg p\vee q\to \{\neg p,q\}$
     • $p\to \{p\}$
     • Přidejte $\{\neg q\}$.
   • Rezoluční kroky:

$$\{\neg p,q\}{\cup }_{res}\{\neg q\}\to \{\neg p\},$$ $$\{\neg p\}{\cup }_{res}\{p\}\to \varnothing .$$

Dosáhli jsme prázdné klauzule, tudíž $T{⊢}_{\text{res}}\perp$ a tedy $T\models q$. 2. Hilbertovský kalkulus:
Definice: Schémata logických axiomů (pro libovolné výroky $\phi ,\psi ,\chi$):

$$\begin{array}{rl}& \phi \to (\psi \to \phi )\\ & (\phi \to (\psi \to \chi ))\to ((\phi \to \psi )\to (\phi \to \chi ))\\ & (\neg \phi \to \neg \psi )\to (\psi \to \phi )\end{array}$$

Definice: Modus ponens: z $\phi$ a $\phi \to \psi$ odvoď $\psi$. Definice: Hilbertovský důkaz ${\varphi }_0,\dots ,{\varphi }_n=\varphi$ je konečná posloupnost, kde každé ${\varphi }_i$ je logický axiom, axiomatická formule, nebo je získáno modus ponens. Příklad pro $T=\{p\to q,p\}$ a cíl $q$:

• $p\to q$ (axiom teorie)
• $p$ (axiom teorie)
• $q$ (modus ponens z 1. a 2.)
  Tudíž $T{⊢}_{H}q$.