Dedukciós tétel

A dedukciós tétel ( dedukciós lemma, dedukciós tétel ) a bizonyításelmélet egyik alapvető eredménye, egy olyan érvelési módszert formalizál, amelyben az implikáció a levezetés szükséges feltétele. Következtetések és bizonyítások létezésének megállapítására szolgál konstrukciójuk használata nélkül. Ezt először kifejezetten Herbran fogalmazta meg és bizonyította 1930 -ban, majd Herbran használta bizonyítás nélkül 1928-ban. Ezt az elvet Tarski önállóan fogalmazta meg 1930-ban. Tarski szerint ezt az elvet már 1921-ben ismerte és alkalmazta [1] . $A\jobbra nyíl B$ $A$

Formuláció propozíciószámításhoz

Ha , akkor . $A \vdash B$ $\vdash A\Rightarrow B$
Ha , akkor . $A_{1},...,A_{m-1},A_{m}\vdash B$ $A_{1},...,A_{m-1}\vdash A_{m}\Rightarrow B$

Itt - a logikai formulák (formális elmélet a propozíciószámításhoz), azt jelenti, hogy a képlet a képletből származik (az elméletben ), és azt jelenti, hogy a képlet bizonyítható (az elmélet tétele ). A jel az implikáció logikai műveletét jelenti . ${\displaystyle A,B,A_{1},...,A_{m-1},A_{m))$ $L$ $A \vdash B$ $B$ $A$ $L$ $\vdash B$ $B$ $L$ $A\jobbra nyíl B$

Elsőrendű elméletek megfogalmazása

Legyen egy részhalmaza (esetleg üres) valamely elsőrendű elmélet képleteinek , és legyen az elmélet képlete . Akkor, ha van egy olyan képlet származtatása a képlethalmazból , amelyben a képlet egyik szabad változója sem kapcsolódik az általánosítási szabály olyan képletekhez, amelyek a levezetésben szereplő képlettől függenek , akkor . $\Gamma$ $K$ $A$ $B$ $K$ $B$ $\Gamma \cup \{A\}$ $A$ $A$ $\Gamma \vdash A\Rightarrow B$

Lásd még

Herbrand tételei

Jegyzetek

↑ Matematikai logika, 1973 , p. 54-55.

Irodalom

Kleene S. K. Matematikai logika. — M .: Mir, 1973. — 480 p.