قضیه استنتاج

قضیۀ استنتاج (به انگلیسی: Deduction theorem) یک متاتئوری در منطق مرتبه اول است.

اگر ${\displaystyle \mathrm{\Gamma }\cup \{A\}}$

مجموعه‌ای از گزاره‌ها باشد، ${\displaystyle \mathrm{\Gamma }\cup \{A\}⊢B}$

اگر و فقط اگر ${\displaystyle \mathrm{\Gamma }⊢A\to B}$

به بیان دیگر اگر ${\displaystyle \mathrm{\Gamma }}$

در حالت خاص اگر ${\displaystyle \mathrm{\Gamma }=\mathrm{\varnothing }}$

اثبات طرف برگشت واضح است. در اثبات رفت از استقرا بر طول برهان برای اثبات ${\displaystyle \mathrm{\Gamma }⊢A\to B}$