قضیه استنتاج

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

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

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

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

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

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

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

منابع

• الگو:یادکرد