Teorema deducerii

Teorema deducției ( lema deducției, teorema deducției ) este unul dintre rezultatele fundamentale în teoria demonstrației , formalizează o metodă de raționament în care implicația este folosită ca o condiție necesară pentru stabilirea derivației. Se folosește pentru a stabili existența concluziilor și dovezilor fără a folosi construcția acestora. A fost formulat și dovedit pentru prima dată în mod explicit în 1930 de Herbran și folosit fără dovezi de Herbran în 1928. Acest principiu a fost formulat independent de Tarski în 1930. Potrivit lui Tarski, a cunoscut și aplicat acest principiu încă din 1921 [1] . $A\Rightarrow B$ $A$

Formulare pentru calculul propozițional

Dacă , atunci . $A \vdash B$ $\vdash A\Rightarrow B$
Dacă , atunci . $A_{1},...,A_{m-1},A_{m}\vdash B$ $A_{1},...,A_{m-1}\vdash A_{m}\Rightarrow B$

Aici - formule logice (teoria formală pentru calculul propozițional), înseamnă că formula este derivată din formulă (în teorie ) și înseamnă că formula este demonstrabilă (este o teoremă a teoriei ). Semnul înseamnă operația logică a implicației . ${\displaystyle A,B,A_{1},...,A_{m-1},A_{m))$ $L$ $A \vdash B$ $B$ $A$ $L$ $\vdash B$ $B$ $L$ $A\Rightarrow B$

Formulare pentru teorii de ordinul întâi

Fie o submulțime (posibil goală) de formule ale unei teorii de ordinul întâi și să fie formule ale teoriei . Atunci, dacă există o astfel de derivare a unei formule din setul de formule în care niciuna dintre variabilele libere ale formulei nu este asociată cu vreo aplicare a regulii de generalizare la formule care depind de formula din această derivare , atunci . $\Gamma$ $K$ $A$ $B$ $K$ $B$ $\Gamma \cup \{A\}$ $A$ $A$ $\Gamma \vdash A\Rightarrow B$

Vezi și

teoremele lui Herbrand

Note

↑ Logica matematică, 1973 , p. 54-55.

Literatură

Kleene S. K. Logica matematică. — M .: Mir, 1973. — 480 p.