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] .
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 .
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 .