قضیه استنتاج یک متاتئوری در منطق مرتبه اول است.
دستگاه استنتاجی
به بیان دیگر اگر Γ {\displaystyle \Gamma } مجموعه ای از گزاره ها باشد و A {\displaystyle A} و B {\displaystyle B} دو گزاره باشند، آنگاه اگر Γ , A ⊢ B {\displaystyle \Gamma ,A\vdash B} آنگاه Γ ⊢ A → B {\displaystyle \Gamma \vdash A\to B} و برعکس.
در حالت خاص اگر Γ = ∅ {\displaystyle \Gamma =\emptyset } باشد A ⊢ B {\displaystyle A\vdash B} بیان می کند ⊢ A → B {\displaystyle \vdash A\to B} . توضیح آنکه در این حالت گزاره A → B {\displaystyle A\to B} بدون هیچ فرضی، تنها با استفاده از اصول نتیجه می شود.
اثبات طرف برگشت واضح است. در اثبات رفت از استقرا بر طول برهان برای اثبات Γ ⊢ A → B {\displaystyle \Gamma \vdash A\to B} استفاده می کنیم.
دستگاه استنتاجی
به بیان دیگر اگر Γ {\displaystyle \Gamma } مجموعه ای از گزاره ها باشد و A {\displaystyle A} و B {\displaystyle B} دو گزاره باشند، آنگاه اگر Γ , A ⊢ B {\displaystyle \Gamma ,A\vdash B} آنگاه Γ ⊢ A → B {\displaystyle \Gamma \vdash A\to B} و برعکس.
در حالت خاص اگر Γ = ∅ {\displaystyle \Gamma =\emptyset } باشد A ⊢ B {\displaystyle A\vdash B} بیان می کند ⊢ A → B {\displaystyle \vdash A\to B} . توضیح آنکه در این حالت گزاره A → B {\displaystyle A\to B} بدون هیچ فرضی، تنها با استفاده از اصول نتیجه می شود.
اثبات طرف برگشت واضح است. در اثبات رفت از استقرا بر طول برهان برای اثبات Γ ⊢ A → B {\displaystyle \Gamma \vdash A\to B} استفاده می کنیم.
wiki: قضیه استنتاج