قضیه استنتاج

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

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

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

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

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

جستارهای وابسته

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

منابع

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