スーピーズ＝レモン記法

スーピーズ＝レモン記法（スーピーズ＝レモンきほう、）は、によって開発された自然演繹論理の記法体系であるレモンの自然演繹体系の入門的な解説については を参照。。の方法から派生したものでありスーピーズの自然演繹体系の入門的な解説については を参照。、自然演繹の証明を、根拠づけられた段階の列として表す。両方の方法とも、ゲンツェンの1934年／1935年の自然演繹体系に由来する推論規則を用いる, .。ゲンツェンの体系では、証明はスーピーズとレモンの表形式ではなく、樹形図の形式で示されていた。樹形図によるレイアウトは哲学的・教育的な目的においては利点があるが、表形式によるレイアウトは実用上はるかに便利である。

同様の表形式のレイアウトはクリーネによっても提示されている。主な違いは、クリーネは主張の左辺を行番号に短縮せず、代わりに先行する命題の完全な一覧を与えるか、あるいは表の左側を下方に走る棒線によって依存関係を示すことを好む点である。しかし、クリーネの版は、たとえごく大まかにではあれ、メタ数学理論の厳密な枠組みの中で提示されているという利点があるのに対し、スーピーズとレモンの著書は、論理学入門を教えるための表形式レイアウトの応用である。

演繹体系の記述

スーピーズ＝レモン記法は、等号を伴う述語計算のための記法であり、その記述は、一般的な証明の統語論と、文脈に固有の規則の2つの部分に分けることができる。

一般的な証明の統語論 証明とは、4つの列と無制限に並んだ行を持つ表である。左から右へ、各列は次のものを保持する。

正の整数の集合（空でありうる） 正の整数 整式（wff） 数の集合（空でありうる）、規則、および他の証明への参照（あることもある） 以下はその例である。

p → q, ¬q ⊢ ¬p [否定後件肯定式（MTT）]仮定番号行番号論理式（wff）使用行と根拠1(1)p → q A2(2)¬q A3(3)p A（RAAのため）1, 3(4)q 1, 3, MPP1, 2, 3(5)q ∧ ¬q 2, 4, ∧I1, 2(6)¬p 3, 5, RAA証明終

第2列は行番号を保持する。第3列はwffを保持し、これは第4列に保持されている規則と、他の証明中にありうる他のwffについての補助情報とによって正当化される。第1列は、引用された規則の文脈における適用によって定まる、そのwffが依拠する仮定の行番号を表す。妥当な証明のどの行も、引用された行にあるwffを前提として、その行にあるwffを結論として列挙することで、シークエントに変換できる。同様に、それらは前件が連言であるような条件文に変換することもできる。これらのシークエントは、上記の否定後件肯定式（Modus Tollens）のように、証明の上に列挙されることが多い。

等号を伴う述語計算の規則 上記の証明は妥当なものであるが、証明が証明体系の一般的な統語論に従う必要はない。しかし、あるシークエントの妥当性を保証するためには、注意深く規定された規則に従わなければならない。規則は4つのグループに分けることができる。命題規則（1〜11）、述語規則（12〜15）、等号の規則（15〜16）、そして代入の規則（18）である。これらのグループをこの順に加えていくことで、まず命題計算を、次に述語計算を、次に等号を伴う述語計算を、そして最後に新しい規則の導出を可能にする等号を伴う述語計算を構築することができる。以下の表では、導出された命題規則（10〜11）が強調表示されている。これらは原始的な（強調されていない）ゲンツェン規則から従う。規則8（『二重否定除去』）と規則9（『背理法』）は同値である。どちらか一方は省くことができる（あるいは導出された規則に吸収させることができる）。 規則名 記法 説明 仮定+ 推論規則の一覧1 仮定 A 「A」は任意のwffを正当化する。唯一の仮定はそれ自身の行番号である。 唯一の仮定はそれ自身の行番号である。2 連言導入 a,b ∧I 命題 と が行 a と b にあるならば、「a,b ∧I」は を正当化する。 仮定は、連言をなす命題の仮定を集めた集まりである。3 連言除去 a ∧E 行 a が連言 であるならば、「a ∧E」を用いて または のいずれかを結論できる。∧I と ∧E は含意の単調性を可能にする。命題 が ∧I によって と結合され、∧E によって分離されるとき、それは の仮定を保持し続けるからである。 仮定は行 a の仮定である。4 選言導入 a ∨I 命題 を持つ行 a に対して、「a ∨I」を引用して を導入できる。 仮定は a の仮定である。5 選言除去 a,b,c,d,e ∨E 選言 について、 と をそれぞれ仮定し、それぞれから独立に結論 に至るならば、 を結論できる。この規則は「a,b,c,d,e ∨E」として引用される。ここで行 a は最初の選言 を持ち、行 b と d はそれぞれ と を仮定し、行 c と e はそれぞれの仮定の集まりに と を含んだ状態で を結論する。 仮定は、 を結論する2つの行 c と e の仮定の集まりから、 と を仮定する行 b と d を除いたものである。6 条件的証明（→I） b,a CP 命題 を持つ行 a が、命題 を持つ仮定行 b を持つならば、「b,a CP」は を正当化する。 a の仮定のうち b を除くすべてが保たれる。7 前件肯定式（→E） a,b MPP それぞれ と を含む行 a と b が証明中にすでにあるならば、「a,b MPP」は を正当化する。 仮定は行 a と b の仮定を集めた集まりである。8 二重否定（¬¬E） a DN 「a DN」は、証明中にすでにある行 a のwffに2つの否定記号を加えるか取り除くかを正当化し、この規則を双条件的にする。 仮定の集まりは、引用された行のものである。9 背理法 b,a RAA 行 b の仮定 を引用する行 a の命題 について、「b,a RAA」を引用し、行 a の b を除く仮定から を導出できる。 行 a の b を除く仮定。10 選言三段論法 a,b DS 行 a の と行 b の から を推論できる。行 a の と行 b の から を推論できる。 仮定は行 a と b の仮定を集めた集まりである。11 モーダストレンス a,b MTT 行 a と b の命題 と について、「a,b MTT」を引用して を導出できる。これは上記の他の規則から証明される。 仮定は行 a と b のものである。12 全称導入 a UI 行 a の述語 について、行 a のいかなる仮定にも項 がどこにも現れない限り、「a UI」を引用して全称量化 を正当化できる。 仮定は行 a のものである。13 全称除去 a UE 行 a の全称量化された述語 について、「a UE」を引用して を正当化できる。UE はUIと双対の関係にあり、これらの規則を用いて量化変数と自由変数の間を行き来できる。 仮定は行 a のものである。14 存在導入 a EI 行 a の述語 について、「a EI」を引用して存在量化 を正当化できる。 仮定は行 a のものである。15 存在除去 a,b,c EE 行 a の存在量化された述語 について、行 b で を仮定し、それを用いて行 c で を導出するならば、「a,b,c EE」を引用して を正当化できる。項 は結論 、行 b を除くその仮定のいずれ、あるいは行 a に現れてはならない。EE と EI は双対であり、 を仮定して EI を用いることで からの結論に至ることができる。 仮定は、行 a の仮定と、b を除く行 c の仮定である。16 等号導入 =I いつでも、仮定なしに「=I」を引用して を導入できる。 仮定なし。17 等号除去 a,b =E 行 a と b の命題 と について、「a,b =E」を引用して 中の項 を に変更することを正当化できる。 仮定は行 a と b の集まりである。18 代入事例 a,b SI(S) X 証明Xで証明されたシークエント と、行 a と b における と の代入事例について、「a,b SI(S) X」を引用して の代入事例の導入を正当化できる。 行 a と b の仮定。 仮定を持たない導出規則は定理であり、仮定なしにいつでも導入できる。「シークエント」の代わりに「定理」を表すものとして「TI(S)」と引用する者もいる。さらに、代入事例が必要ない場合（その命題が参照される証明のものと完全に一致する場合）、いずれの場合も単に「SI」あるいは「TI」とだけ引用する者もいる。

例 シークエント（この場合は定理）の証明の例：

⊢p ∨ ¬p仮定番号行番号論理式（wff）使用行と根拠1(1)¬(p ∨ ¬p)A（RAAのため）2(2)pA（RAAのため）2(3)(p ∨ ¬p)2, ∨I1, 2(4)(p ∨ ¬p) ∧ ¬(p ∨ ¬p)3, 1, ∧I1(5)¬p2, 4, RAA1(6)(p ∨ ¬p)5, ∨I1(7)(p ∨ ¬p) ∧ ¬(p ∨ ¬p)1, 6, ∧I(8)¬¬(p ∨ ¬p)1, 7, RAA(9)(p ∨ ¬p)8, DN証明終 含意の単調性を用いた爆発律の証明。3〜6行目で示されている次の手法を「前提の（有限）増強規則」と呼ぶ者もいる。 p, ¬p ⊢ q仮定番号行番号論理式（wff）使用行と根拠1(1)pA（RAAのため）2(2)¬pA（RAAのため）1, 2(3)p ∧ ¬p1, 2, ∧I4(4)¬qA（DNのため）1, 2, 4(5)(p ∧ ¬p) ∧ ¬q3, 4, ∧I1, 2, 4(6)p ∧ ¬p5, ­∧E1, 2(7)¬¬q4, 6, RAA1, 2(8)q7, DN証明終 代入と∨Eの例： (p ∧ ¬p) ∨ (q ∧ ¬q) ⊢ r仮定番号行番号論理式（wff）使用行と根拠1(1)(p ∧ ¬p) ∨ (q ∧ ¬q)A2(2)p ∧ ¬pA（∨Eのため）2(3)p2 ∧E2(4)¬p2 ∧E2(5)r3, 4 SI(S) 上記の証明を参照6(6)q ∧ ¬qA（∨Eのため）6(7)q6 ∧E6(8)¬q2 ∧E6(9)r7, 8 SI(S) 上記の証明を参照1(10)r1, 2, 5, 6, 9, ∨E証明終

表形式の自然演繹体系の歴史

規則に基づき、行番号（および縦棒やアスタリスクなどの関連手法）によって先行する命題を示す、表形式レイアウトの自然演繹体系の歴史的な発展には、以下の出版物が含まれる。

1940年：ある教科書の中で、クワイン. 先行する依存関係に対するクワインの行番号記法については特に91〜93頁を参照。は、角括弧内の行番号によって先行する依存関係を示しており、これは1957年のスーピーズの行番号記法に先立つものであった。 1950年：ある教科書の中で、は、証明の各行の左に1つ以上のアスタリスクを用いて依存関係を示す方法を示した。これはクリーネの縦棒と同等である。（クワインのアスタリスク記法が1950年のオリジナル版に現れていたのか、それとも後の版で追加されたのかは完全には明らかでない。） 1957年：による教科書における、実用的な論理定理証明への入門。これは各行の左の行番号によって依存関係（すなわち先行する命題）を示した。 1963年：は、自然演繹の推論規則に基づく逐次的論理論証の行の先行する依存関係を示すために、行番号の集合を用いている。 1965年：による教科書全体が、スーピーズの方法に基づく手法を用いた論理証明への入門となっている。 1967年：ある教科書の中で、は、実用的な論理証明の2つの種類を簡潔に示した。一つは各行の左に先行する命題を明示的に引用する体系であり、もう一つは依存関係を示すために左側に縦棒を用いる体系であるクリーネの表形式自然演繹体系の特筆すべき利点は、彼が命題計算と述語計算の両方について推論規則の妥当性を証明していることである。を参照。。

関連項目 自然演繹 シークエント計算

注釈

出典

(English translation Investigations into Logical Deduction in Szabo.)

外部リンク Pelletier, Jeff, "A History of Natural Deduction and Elementary Logic Textbooks."