Dedukční teorém

Dedukční teorém ( dedukční lemma, dedukční teorém ) je jedním ze základních výsledků teorie důkazů , formalizuje metodu uvažování, ve které je implikace použita jako nezbytná podmínka pro stanovení derivace. Používá se ke stanovení existence závěrů a důkazů bez použití jejich konstrukce. Poprvé byl výslovně formulován a dokázán v roce 1930 Herbranem a bez důkazu byl použit Herbranem v roce 1928. Tento princip nezávisle formuloval Tarski v roce 1930. Tento princip podle Tarského znal a aplikoval již v roce 1921 [1] . $A\Šipka doprava B$ $A$

Formulace pro výrokový počet

Pokud , tak . $A \vdash B$ $\vdash A\Rightarrow B$
Pokud , tak . $A_{1},...,A_{m-1},A_{m}\vdash B$ $A_{1},...,A_{m-1}\vdash A_{m}\Rightarrow B$

Zde - logické formule (formální teorie pro výrokový počet), znamená, že formule je odvozena od formule (v teorii ), a znamená, že formule je prokazatelná (je teorémem teorie ). Znak znamená logickou operaci implikace . ${\displaystyle A,B,A_{1},...,A_{m-1},A_{m))$ $L$ $A \vdash B$ $B$ $A$ $L$ $\vdash B$ $B$ $L$ $A\Šipka doprava B$

Formulace pro teorie prvního řádu

Dovolit být podmnožinou (možná prázdný) formulí nějaké teorie prvního řádu , a být formule teorie . Pak pokud existuje takové odvození vzorce z množiny vzorců, ve kterém žádná z volných proměnných vzorce není spojena s žádnou aplikací pravidla zobecnění na vzorce, které v tomto odvození závisí na vzorci , pak . $\Gamma$ $K$ $A$ $B$ $K$ $B$ $\Gamma \cup \{A\}$ $A$ $A$ $\Gamma \vdash A\Rightarrow B$

Viz také

Herbrandovy věty

Poznámky

↑ Matematická logika, 1973 , str. 54-55.

Literatura

Kleene S. K. Matematická logika. — M .: Mir, 1973. — 480 s.