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

اگر ${\displaystyle \Gamma \cup \{A\))$ مجموعه‌ای از گزاره‌ها باشد، ${\displaystyle \Gamma \cup \{A\}\vdash B}$ اگر و فقط اگر ${\displaystyle \Gamma \vdash A\to B}$

به بیان دیگر اگر ${\displaystyle \Gamma }$ مجموعه‌ای از گزاره‌ها باشد و ${\displaystyle A}$ و ${\displaystyle B}$ دو گزاره باشند، آنگاه اگر ${\displaystyle \Gamma ,A\vdash B}$ آنگاه ${\displaystyle \Gamma \vdash A\to B}$ و برعکس.

در حالت خاص اگر ${\displaystyle \Gamma =\emptyset }$ باشد، ${\displaystyle A\vdash B}$ بیان می‌کند ${\displaystyle \vdash A\to B}$. توضیح آنکه در این حالت گزارۀ ${\displaystyle A\to B}$ بدون هیچ فرضی، تنها با استفاده از اصول نتیجه می‌شود.

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

• دستگاه استنتاجی

• محمد اردشیر (۱۳۸۳)، منطق ریاضی، هرمس، ص. ۴۳، شابک ۹۶۴-۳۶۳-۲۲۹-۶