サップス・レモン記法

サッペス・レモン記法^[1]は、 EJ レモンによって開発された自然演繹論理記法システムです。^[2]サッペス法^[3]から派生したこの記法は、自然演繹の証明を正当化された一連のステップとして表します。どちらの方法も、ゲンツェンの1934/1935 年自然演繹システム^[4]から派生した推論規則を使用します。ゲンツェンの自然演繹システムでは、証明はサッペスとレモンの表形式ではなく、樹形図形式で表されます。樹形図レイアウトは哲学的および教育的な目的では利点がありますが、表形式レイアウトは実際のアプリケーションでははるかに便利です。

同様の表形式のレイアウトは、クリーネによって提示されている。^[5]主な違いは、クリーネは主張の左辺を行番号に省略せず、代わりに先行命題の完全なリストを提供するか、依存関係を示すために表の左側に走るバーで左辺を示すことを好んでいることである。しかし、クリーネのバージョンは、非常に大まかではあるが、厳密なメタ数学理論の枠組みの中で提示されているという利点があり、一方、サッペス^[3]とレモン^[2]の本は、入門論理を教えるための表形式のレイアウトの応用である。

サッペス・レモン記法は等式を含む述語計算の記法であるため、その記述は一般的な証明構文とコンテキスト固有の規則の 2 つの部分に分けることができます。

証明は 4 つの列と無制限の順序付き行を持つ表です。列は左から右に次の内容を保持します。

1. 正の整数の集合（空の場合もある）
2. 正の整数
3. 整形式の式（またはwff）
4. 数字の集合（空の可能性あり）、ルール、および別の証明への参照

次に例を示します。

2 番目の列には行番号が入ります。3 番目の列には wff が入ります。wff は 4 番目の列で保持されている規則によって正当化され、他の wff (他の証明にある場合もあります) に関する補足情報も入ります。1 番目の列は、wff が依拠する仮定の行番号を表します。これは、引用された規則を文脈に適用することによって決定されます。有効な証明のどの行も、引用された行の wff を前提として、その行の wff を結論としてリストすることで、シークエントに変換できます。同様に、先行詞が接続詞である条件文に変換できます。これらのシークエントは、 Modus Tollensが上にあるように、証明の上にリストされることがよくあります。

上記の証明は有効なものですが、証明は証明システムの一般的な構文に準拠する必要はありません。ただし、シークエントの有効性を保証するには、慎重に指定された規則に準拠する必要があります。規則は、命題規則 (1-10)、述語規則 (11-14)、等号規則 (15-16)、および置換規則(17) の 4 つのグループに分けられます。これらのグループを順番に追加することで、命題計算、述語計算、等号付き述語計算、等号付き述語計算の順に構築でき、新しい規則を導出できます。MTT などの命題計算規則の一部は不要であり、他の規則から規則として導出できます。

1. 仮定のルール (A): 「A」はあらゆる wff を正当化します。唯一の仮定は、それ自身の行番号です。
2. Modus Ponendo Ponens (MPP):証明にP → QとP をそれぞれ含む行aとbが以前あった場合、「a、b MPP」は Q を正当化します。仮定は行aと行bの集合的なプールです。
3. 条件付き証明の規則 (CP): 命題 P の行aに命題 Q の仮定行bがある場合、「b、a CP」によって Q→P が正当化されます。 b を除くaの仮定はすべて維持されます。
4. 二重否定の規則 (DN): 「a DN」は、証明の前の行aで wff に 2 つの否定記号を追加または減算することを正当化し、この規則を双条件にします。仮定プールは、引用された行の 1 つです。
5. ∧ 導入 (∧ I) の規則: 命題 P と Q が行aとbにある場合、「a , b ∧ I」は P∧ Q を正当化します。仮定は結合された命題の集合的なプールです。
6. ∧消去の規則 (∧E): 行a が接続詞 P∧Q である場合、「a ∧E」を使用して P または Q のいずれかを結論付けることができます。仮定は行aのものです。∧I と ∧E は含意の単調性を可能にします。つまり、命題 P が ∧I で Q に結合され、∧E で分離されると、Q の仮定が保持されます。
7. ∨導入の規則 (∨I): 命題 P を伴う行aに対して、「a ∨I」を引用して P∨Q を導入できます。仮定はaです。
8. ∨消去の規則 (∨E): 選言 P∨Q について、 P と Q を仮定し、それぞれから別々に結論 R に至る場合、結論 R を得ることができます。 この規則は、「a、b、c、d、e ∨E」と表現されます。ここで、行a には最初の選言 P∨Q があり、行bとd はそれぞれ P と Q を仮定し、行cとe はそれぞれの仮定プールで P と Q を使って R を結論付けます。 仮定は、 R を結論付ける 2 つの行cとeから、 P と Q を仮定する行bとd を除いた集合的なプールです。
9. 帰無仮説(RAA): 行aの命題 P∧¬P が行bの仮定 Q を引用している場合、「b、a RAA」を引用して、行aの仮定からbを除いて¬Q を導くことができます。
10. Modus Tollens (MTT): 行aとb の命題 P→Q と ¬Q については、「a、b MTT」を引用して ¬P を導くことができます。仮定は行aとbの仮定と同じです。これは上記の他の規則から証明されています。
11. 普遍的導入 (UI):行aの述語については、行aの仮定のいずれにも項がどこにも含まれていない場合に限り、「UI」を引用して普遍量化を正当化できます。仮定は行aの仮定です。${\displaystyle ラ}$${\displaystyle (\forall x)Rx}$${\displaystyle a}$
12. 全称消去 (UE):行aの全称量化述語については、「 UE 」を引用して を正当化できます。仮定は行aの仮定と同じです。UE は、これらの規則を使用して量化変数と自由変数を切り替えることができるという点で、 UI と双対です。${\displaystyle (\forall x)Rx}$${\displaystyle ラ}$
13. 存在論的導入 (EI):行aの述語については、「 EI 」を引用して存在量化を正当化できます。仮定は行aの仮定と同じです。${\displaystyle ラ}$${\displaystyle (\exists x)Rx}$
14. 存在消去 (EE):行aの存在量化された述語について、行bで が真であると仮定し、行cでそれを使って P を導く場合、P を正当化するために「a、b、c EE」を引用することができます。この項は、結論 P、行b以外のその仮定、または行aに現れることはできません。このため、EE と EI は双対性を持っています。EI は項を結論から取り除くため、 を仮定して EI を使用することで、 から結論に達することができます。仮定とは、行aの仮定と、行cのb以外の仮定です。${\displaystyle (\exists x)Rx}$${\displaystyle ラ}$${\displaystyle a}$${\displaystyle ラ}$${\displaystyle (\exists x)Rx}$${\displaystyle a}$
15. 等式の導入 (=I): 任意の時点で、仮定なしに「=I」を引用して導入できます。${\displaystyle a=a}$
16. 等式消去 (=E):行aとb の命題と P について、「a、b =E」を引用して、 P 内の任意の項を に変更することを正当化できます。仮定は、行aとbのプールです。${\displaystyle a=b}$${\displaystyle a}$${\displaystyle b}$
17. 置換インスタンス (SI(S)):証明 X で証明されたシークエントと、行aおよびb の置換インスタンスについて、" a , b SI(S) X" を引用して、 の置換インスタンスの導入を正当化できます。仮定は行aおよびbの仮定です。仮定のない導出ルールは定理であり、仮定なしでいつでも導入できます。これを "シークエント" ではなく "定理" を表す "TI(S)" として引用する人もいます。さらに、置換インスタンスが必要ない場合は、どちらの場合も "SI" または "TI" のみを引用する人もいます。これは、それらの命題が参照されている証明の命題と正確に一致するためです。${\displaystyle P,Q\vdash R}$${\displaystyle P}$${\displaystyle Q}$${\displaystyle R}$

シーケント（この場合は定理）の証明の例:

含意の単調性を用いた爆発原理の証明。3-6行目で示されている次の手法を「前提の（有限）増加の規則」と呼ぶ人もいます。^[6]

置換と∨Eの例:

ルールベースで、先行命題を行番号（および縦棒やアスタリスクなどの関連方法）で示す、表形式レイアウトの自然演繹システムの歴史的発展には、次の出版物が含まれます。

• ^{1940年: クワイン[7]}は教科書の中で、先行する依存関係を角括弧で囲んだ行番号で示し、1957年のサッペスの行番号表記法を予期した。
• 1950 年: 教科書の中で、クワインは (1982、pp. 241–255)、各証明行の左側に 1 つ以上のアスタリスクを使用して依存関係を示す方法を示しました。これは、クリーネの縦棒に相当します。(クワインのアスタリスク表記が 1950 年のオリジナル版に登場したのか、それとも後の版で追加されたのかは完全には明らかではありません。)
• 1957年: Suppes の教科書 (1999、pp. 25-150) に、実用論理の定理証明の入門が掲載されました。この教科書では、各行の左側に行番号を付けて依存関係 (つまり、先行命題) を示しました。
• 1963年: ストール(1979、pp. 183–190、215–219)は、自然演繹推論規則に基づいて、一連の論理的議論の行の先行依存関係を示すために行番号のセットを使用しています。
• 1965年: Lemmon (1965) による教科書全体は、Suppes の方法に基づいた方法を使用した論理証明の入門書です。
• 1967年：クリーネ（2002、pp.50-58、128-130）は教科書の中で、2種類の実用的な論理証明を簡単に示した。1つは各行の左側に先行命題を明示的に引用するシステムであり、もう1つは依存関係を示すために左側に縦線を使用するシステムである。^[8]

• 自然演繹
• シーケント計算
• 演繹システム

• ゲンツェン、ゲルハルト・カール・エーリッヒ（1934年）。 「Untersuhungen über das logische Schließen. I」。数学的ツァイシュリフト。39 (2): 176–210。土井：10.1007/BF01201353。 （英語訳：サボーの論理的演繹の調査）
• ゲンツェン、ゲルハルト・カール・エーリッヒ（1935年）。 「Untersuchungen über das logische Schließen. II」。数学的ツァイシュリフト。39 (3): 405–431。土井：10.1007/bf01201363。
• クリーネ、スティーブン・コール（2002）[1967]。数学論理。ミネオラ、ニューヨーク：ドーバー出版。ISBN 978-0-486-42533-7。
• レモン、エドワード・ジョン（1965年）。『論理学入門』。トーマス・ネルソン。ISBN 0-17-712040-1。
• クワイン、ウィラード・ヴァン・オーマン（1981）[1940]。数学論理（改訂版）。マサチューセッツ州ケンブリッジ：ハーバード大学出版局。ISBN 978-0-674-55451-1。
• クワイン、ウィラード・ヴァン・オーマン（1982）[1950]。論理の方法（第4版）。マサチューセッツ州ケンブリッジ：ハーバード大学出版局。ISBN 978-0-674-57176-1。
• ストール、ロバート・ロス（1979）[1963]。集合論と論理。ミネオラ、ニューヨーク：ドーバー出版。ISBN 978-0-486-63829-4。
• サップス、パトリック・コロネル（1999）[1957]。論理学入門。ミネオラ、ニューヨーク：ドーバー出版。ISBN 978-0-486-40687-9。
• Szabo, ME (1969).ゲルハルト・ゲンツェン論文集. アムステルダム: 北ホラント.

• ペレティエ、ジェフ、「自然演繹と初等論理学教科書の歴史」