セットを含む控除ルール $\Gamma$前提と初等教科書の自然演繹ルールの比較。それらはどのように正確に異なりますか?
小学校の教科書では、自然演繹のルールは次のように提示されています。 $\&$-イントロ
から $\phi$ そして $\psi$、推測 $\phi\&\psi$
または
$(n).....\phi$
$(m)....\psi$
$\therefore$
$(p)....\phi\&\psi$。
次のような言い方はどの程度なのか知りたいのですが $\&$-イントロは、上記の「通常の」教科書のプレゼンテーションとは異なります。私が言及している方法は、シャピロの古典論理のプレゼンテーションで見つけたものです(https://plato.stanford.edu/entries/logic-classical/#Dedu):
(&I)Γ1⊢θおよびΓ2⊢ψの場合、Γ1、Γ2⊢(θ&ψ)。
(意味: "if $\theta$ 一連の前提から導き出すことができます $\Gamma_1$ anf if $\psi$ 一連の前提から導き出すことができます $\Gamma_2$、その後 $(\theta\&\psi)$ 一連の前提から導き出すことができます $\Gamma_1\cup\Gamma_2$。 ")
シャピロのプレゼンテーションは「自然演繹」と呼ぶことができますか?それとも「シークエント計算」の場合ですか?
余談ですが、シャピロのスタイルで派生の例を表示する数理論理学の初心者向けの教科書を知っていますか?
回答
「小学校教科書」のルールは、次のとおりです。とき$\phi$ そして $\psi$ 導出される可能性があり、それから私たちはそれを推測するかもしれません $\phi\mathop\&\psi$導出される可能性があります。これらの導出が同じコンテキスト(前提と仮定)で行われることは述べられていません。この推論規則は、次のように要約できます。$$\dfrac{~\phi\qquad\psi~}{\phi\mathop\&\psi}{\small\&\mathsf I}$$
「シークエント計算」ルールはこれを拡張して、どのコンテキストで物事が派生するかを明示的にリストします。次に、上記と同じルールをコンテキストとともに提示できます($\Gamma$、一連のステートメント)明示的に述べられている: $$\dfrac{~\Gamma\vdash\phi\qquad\Gamma\vdash\psi~}{\Gamma\vdash\phi\mathop\&\psi}{\small\&\mathsf I}$$
言って私たちは、ルールを拡張することができますとき$\phi$ そして $\psi$コンテキストで派生する可能性があります$\Gamma_1$ そして $\Gamma_2$それぞれ、それから私達はそれを推論するかもしれません$\phi\&\psi$統一された文脈で導き出されるかもしれない、$\Gamma_1\cup\Gamma_2$。
$$\dfrac{~\Gamma_1\vdash\phi\qquad\Gamma_2\vdash\psi~}{\Gamma_1\cup\Gamma_2\vdash\phi\mathop\&\psi}{\small\&\mathsf I}$$
短編小説:上級プレゼンテーションは初級プレゼンテーションと同じことを言いますが、いくつかの詳細が追加されています。