シークエント

数理論理学では、シークエントは非常に一般的な種類の条件付きアサーションです。

${\displaystyle A_{1},\,\dots ,A_{m}\,\vdash \,B_{1},\,\dots ,B_{n}.}$

シークエントには、条件式A _i (「前提」と呼ばれる)がm個、主張式B _j (「後続」または「帰結」と呼ばれる) がn個含まれます。シークエントは、前提条件がすべて真である場合、帰結式の少なくとも 1 つが真であることを意味します。このスタイルの条件付き主張は、ほとんどの場合、シークエント計算の概念フレームワークに関連付けられています。

シークエントは、次の 3 種類の論理的判断の文脈で理解すると最もよく理解されます。

1. 無条件の断言。先行する式はありません。
   • 例: ⊢ B
   • 意味: B は真です。
2. 条件付きアサーション。任意の数の前提条件式。
   1. 単純な条件付きアサーション。単一の結果式。
      • 例: A ₁、A ₂、A ₃ ⊢ B
      • 意味: A ₁かつA ₂かつA ₃が真である場合、Bは真です。
   2. 任意の数の連続式。
      • 例: A ₁、A ₂、A ₃ ⊢ B ₁、B ₂、B ₃、B ₄
      • 意味: A ₁かつA ₂かつA ₃ が真である場合、B ₁またはB ₂またはB ₃またはB ₄は真です。

したがって、シークエントは単純な条件付きアサーションの一般化であり、単純な条件付きアサーションは無条件アサーションの一般化です。

ここでの「OR」は包含ORです。^[1]シークエントの右側に選言的意味論を採用する理由は、主に3つの利点があります。

1. このような意味を持つシークエントに対する古典的な推論規則の対称性。
2. このような古典的なルールを直観主義的なルールに変換することの容易さと単純さ。
3. このように表現すると、述語計算の完全性を証明することができます。

これら 3 つの利点はすべて、ゲンツェン (1934、194 ページ) の創設論文で特定されました。

すべての著者がゲンツェンの「シークエント」という単語の本来の意味に従っているわけではない。例えば、レモン (1965) は「シークエント」という単語を、ただ 1 つの帰結式を持つ単純な条件付きアサーションにのみ使用していた。^[2]シークエントの同じ単一帰結の定義は、Huth & Ryan 2004、p. 5 にも示されている。

一般的な順序は次のようになります

${\displaystyle \Gamma \vdash \Sigma }$

Γ と Σ はどちらも論理式のシーケンスであり、セットではありません。したがって、式の出現回数と順序の両方が重要です。特に、同じシーケンス内に同じ式が 2 回出現する場合があります。シークエント計算の推論規則の完全なセットには、アサーション記号の左側と右側の隣接する式を交換する規則 (これにより、左側と右側のシーケンスを任意に並べ替える) と、左側と右側のシーケンス内で任意の式を挿入して重複コピーを削除する規則が含まれています。(ただし、Smullyan (1995、pp. 107–108) は、シークエントで式のシーケンスではなく式のセットを使用しています。したがって、「間引き」、「短縮」、「交換」と呼ばれる 3 組の構造規則は必要ありません。)

記号「 」は、「ターンスタイル」、「右タック」、「ティー」、「アサーション サイン」、または「アサーション シンボル」と呼ばれることがよくあります。これは、暗示的に「与える」、「証明する」、「伴う」と読まれることがよくあります。 ${\displaystyle \vdash}$

後続項 (右側) の少なくとも 1 つの式が真であると結論付けるには、前項 (左側) のすべての式が真でなければならないため、どちらかの側に式を追加すると後続項は弱くなり、どちらかの側から式を削除すると後続項は強くなります。これは、アサーション シンボルの右側で選言的意味論を使用し、左側では連言的意味論に従うことから生じる対称性の利点の 1 つです。

極端な場合、つまり、後件部の前提式のリストが空の場合、後件部は無条件です。これは、後件部の数が任意であり、必ずしも 1 つの後件部である必要はないため、単純な無条件の表明とは異なります。したがって、たとえば、「⊢ B ₁、B ₂ 」は、 B ₁または B ₂のいずれか、または両方が真でなければならないことを意味します。空の前提式のリストは、「常に真」の命題に相当し、「verum」と呼ばれ、「⊤」と表記されます。( Tee (記号)を参照してください。)

シークエントの結果式のリストが空である極端な場合でも、右側の項の少なくとも 1 つは真であるという規則は変わりませんが、これは明らかに不可能です。これは、「常に偽」の命題、つまり「falsum」によって示され、「⊥」で示されます。結果が偽であるため、前提の少なくとも 1 つは偽でなければなりません。したがって、たとえば、「A ₁、A ₂ ⊢」は、前提A ₁とA ₂の少なくとも 1 つは偽でなければならないことを意味します。

ここでも、右側の選言的意味論による対称性が見られます。左側が空の場合、右側の命題の 1 つ以上が必ず真になります。右側が空の場合、左側の命題の 1 つ以上が必ず偽になります。

二重に極端なケース「⊢」は、式の前件部と後件部のリストが両方とも空であり、「満足できない」。^[3]この場合、後件部の意味は実質的に「⊤ ⊢ ⊥」である。これは後件部「⊢ ⊥」と同等であり、明らかに有効ではない。

論理式 α と β に対する形式 ' ⊢ α, β ' のシークエントは、α が真であるか β が真であるか (または両方) を意味します。しかし、α がトートロジーであるか β がトートロジーであるかは意味しません。これを明確にするために、例 ' ⊢ B ∨ A, C ∨ ¬A ' を考えてみましょう。これは、B ∨ A が真であるか C ∨ ¬A が真であるため、有効なシークエントです。しかし、これらの式はどちらも単独ではトートロジーではありません。トートロジーとなるのは、これら 2 つの式の選言です。

同様に、論理式 α と β に対する形式 ' α, β ⊢ ' のシークエントは、α が偽であるか β が偽であることを意味します。しかし、α が矛盾であるか β が矛盾であることを意味するわけではありません。これを明確にするために、例 ' B ∧ A, C ∧ ¬A ⊢ ' を考えてみましょう。これは、B ∧ A が偽であるか C ∧ ¬A が偽であるため、有効なシークエントです。しかし、これらの式はどちらも単独では矛盾ではありません。矛盾となるのは、これら 2 つの式の結合です。

ほとんどの証明システムでは、あるシークエントから別のシークエントを推論する方法が提供されています。これらの推論規則は、線の上と下のシークエントのリストで記述されます。この規則は、線の上のすべてが真であれば、線の下のすべても真であることを示しています。

典型的なルールは次のとおりです。

${\displaystyle {\frac {\Gamma ,\alpha \vdash \Sigma \qquad \Gamma \vdash \alpha }{\Gamma \vdash \Sigma }}}$

これは、 が得られ、 が得られると推論できる場合、 が得られること も推論できることを示しています。 (シーケント計算の推論規則の完全なセットも参照してください。) ${\displaystyle \Gamma ,\alpha }$${\displaystyle \Sigma }$${\displaystyle \Gamma}$${\displaystyle \alpha}$${\displaystyle \Gamma}$${\displaystyle \Sigma }$

シークエント内のアサーション記号は、もともとは含意演算子とまったく同じ意味を持っていました。しかし、時が経つにつれて、その意味はすべてのモデルにおける意味上の真実ではなく、理論内の証明可能性を表すように変化しました。

1934年、ゲンツェンはシークエント内の主張記号「⊢」を証明可能性を表すものとして定義しなかった。彼はそれを含意演算子「⇒」と全く同じ意味であると定義した。「⊢」の代わりに「→」を、「⇒」の代わりに「⊃」を使用して、彼は次のように書いた。「シークエントA ₁ , ..., A _μ → B ₁ , ..., B _{ν は}、内容に関しては、式(A ₁ & ... & A _μ ) ⊃ (B ₁ ∨ ... ∨ B _ν )と全く同じことを意味する」。^[4] (ゲンツェンはシークエントの前件と後件の間に右矢印記号を使用した。彼は論理含意演算子に記号「⊃」を使用した。)

1939年にヒルベルトとバーナイスも同様に、シークエントは対応する含意式と同じ意味を持つと述べた。^[5]

1944年、アロンゾ・チャーチはゲンツェンのその後の主張は証明可能性を意味するものではないと強調した。

「しかし、演繹定理を原始規則または派生規則として使用することは、ゲンツェンによるSequenzenの使用と混同してはならない。ゲンツェンの矢印 → は、私たちの統語的記法 ⊢ と比較できるものではなく、ゲンツェンのオブジェクト言語に属するものである（ゲンツェンの推論規則の適用において、それを含む表現が前提と結論として現れることから明らかである）。」^[6]

この時期以降の多くの出版物では、シークエント内のアサーション記号は、シークエントが定式化された理論の範囲内で証明可能性を意味すると述べられている。 1963年のCurry ^[7] 、1965年のLemmon ^[2] 、 2004年のHuthとRyan ^[8]はいずれも、シークエントアサーション記号は証明可能性を意味すると述べている。しかし、Ben-Ari (2012, p. 69)は、ゲンツェンシステムのシークエント内のアサーション記号（彼が「 ⇒ 」と表記）は、メタ言語ではなくオブジェクト言語の一部であると述べています。^[9]

Prawitz (1965)によれば、「シークエント計算は、対応する自然演繹システムにおける演繹可能性関係のメタ計算として理解できる」^[10] 。さらに、「シークエント計算の証明は、対応する自然演繹を構築する方法の指示と見なすことができる」^[11]。言い換えれば、アサーション記号は、メタ計算の一種であるシークエント計算のオブジェクト言語の一部であるが、同時に基礎となる自然演繹システムにおける演繹可能性を意味する。

シークエントは、演繹の計算を指定するときに頻繁に使用される、証明可能性の形式化されたステートメントです。シークエント計算では、シークエントという名前は、この演繹システムに特徴的な特定の種類の判断と見なすことができる構成要素に使用されます。

シーケントの直観的な意味は、Γ の仮定の下で Σ の結論が証明可能であるということです。 古典的には、ターンスタイル左側の式は連言的に解釈でき、右側の式は選言と見なすことができます。 これは、Γ のすべての式が成り立つ場合、Σ の少なくとも 1 つの式も真でなければならないことを意味します。 後続が空の場合、これは偽と解釈されます。つまり、Γ が偽を証明し、したがって矛盾していることを意味します。 一方、空の先行項は真であると仮定されます。つまり、 Σ が仮定なしで続くことを意味します。つまり、常に真です (選言として)。 Γ が空のこの形式のシーケントは、論理的主張として知られています。 ${\displaystyle \Gamma \vdash \Sigma }$${\displaystyle \Gamma \vdash }$${\displaystyle \vdash \Sigma }$

もちろん、古典的には同等な他の直観的な説明も可能です。たとえば、は、 Γ のすべての式が真で、Σ のすべての式が偽であるということはあり得ないと主張していると解釈できます (これは、グリベンコの定理などの古典的な直観論理の二重否定の解釈に関連しています)。 ${\displaystyle \Gamma \vdash \Sigma }$

いずれにせよ、これらの直感的な解釈は教育上のものに過ぎません。証明理論における形式的な証明は純粋に統語論的なものなので、シークエント（の導出）の意味は、実際の推論規則を提供する計算の特性によってのみ与えられます。

上記の技術的に正確な定義に矛盾がなければ、シークエントをその導入論理形式で記述することができます。 は、論理プロセスを開始する一連の仮定を表します。たとえば、「ソクラテスは人間である」や「すべての人間は死ぬ運命にある」などです。 は、これらの前提の下で得られる論理的結論を表します。たとえば、「ソクラテスは死ぬ運命にある」は、上記の点を合理的に形式化することで得られるもので、回転式改札口の側面に表示されることが予想されます。この意味で、は推論のプロセス、つまり英語で「したがって」を意味します。 ${\displaystyle \Gamma }$${\displaystyle \Sigma }$${\displaystyle \Sigma }$${\displaystyle \vdash }$

ここで紹介した一般的なシークエントの概念は、さまざまな方法で特殊化できます。シークエントが直観主義シークエントと呼ばれるのは、後続に最大で 1 つの式がある場合です (ただし、直観主義論理の複数の後続計算も可能です)。より正確には、一般的なシークエント計算を、一般的なシークエントと同じ推論規則を持つ単一の後続式シークエントに制限すると、直観主義シークエント計算が構成されます (この制限されたシークエント計算は LJ で示されます)。

同様に、後件が前件において特異であることを要求することによって、 二重直観論理（矛盾無矛盾論理の一種）の計算を得ることができます。

多くの場合、シークエントはシーケンスではなく多重集合または集合から構成されると想定されます。したがって、式の出現順序や出現回数さえも無視されます。古典的な命題論理では、前提の集合から引き出せる結論はこれらのデータに依存しないため、これは問題になりません。ただし、部分構造論理では、これが非常に重要になる場合があります。

自然演繹システムは単一帰結条件アサーションを使用しますが、通常、ゲンツェンが 1934 年に導入した推論規則と同じセットは使用しません。特に、命題計算と述語計算における実用的な定理証明に非常に便利な表形式の自然演繹システムは、Suppes (1999) と Lemmon (1965) によって教科書の入門論理の指導に応用されました。

歴史的に、シークエントはゲルハルト・ゲンツェンによって、彼の有名なシークエント計算を特定するために導入されました。^[12]彼はドイツ語の出版物で「Sequenz」という単語を使用しました。しかし、英語では、「sequence」という単語がドイツ語の「Folge」の翻訳としてすでに使用されており、数学で頻繁に登場します。その後、「sequent」という用語は、ドイツ語表現の代替翻訳を探すために作成されました。

クリーネ^[13]は英語への翻訳について次のようにコメントしている。「ゲンツェンは『Sequenz』と言っているが、我々はこれを『sequent』と訳す。なぜなら、我々はすでに『sequence』をオブジェクトの連続を表すのに使用しており、ドイツ語では『Folge』だからである。」

• ゲルハルト・ゲンツェン
• 直観主義論理
• 自然演繹
• シーケント計算

• Ben-Ari, Mordechai (2012) [1993].コンピュータサイエンスのための数理論理学. ロンドン: Springer. ISBN 978-1-4471-4128-0。
• チャーチ、アロンゾ（1996）[1944]。数理論理学入門。プリンストン、ニュージャージー：プリンストン大学出版局。ISBN 978-0-691-02906-1。
• カリー、ハスケル・ブルックス（1977）[1963]。数理論理学の基礎。ニューヨーク：ドーバー出版。ISBN 978-0-486-63462-3。
• ゲンツェン、ゲルハルト(1934)。 「Untersuhungen über das logische Schließen. I」。数学的ツァイシュリフト。39 (2): 176–210。土井：10.1007/bf01201353。S2CID  121546341。
• ゲンツェン、ゲルハルト(1935)。 「Untersuhungen über das logische Schließen. II」。数学的ツァイシュリフト。39 (3): 405–431。土井：10.1007/bf01201363。S2CID  186239837。
• デヴィッド・ヒルベルト;バーネイズ、ポール(1970) [1939]。Grundlagen der Mathematik II (第 2 版)。ベルリン、ニューヨーク: Springer-Verlag。ISBN 978-3-642-86897-9。
• Huth, Michael; Ryan, Mark (2004)。Logic in Computer Science (第 2 版)。ケンブリッジ、イギリス: Cambridge University Press。ISBN 978-0-521-54310-1。
• クリーネ、スティーブン・コール（2009）[1952]。メタ数学入門。イシ・プレス・インターナショナル。ISBN 978-0-923891-57-2。
• クリーネ、スティーブン・コール（2002）[1967]。数学論理。ミネオラ、ニューヨーク：ドーバー出版。ISBN 978-0-486-42533-7。
• レモン、エドワード・ジョン（1965年）。『論理学入門』トーマス・ネルソン。ISBN 0-17-712040-1。
• プラウィッツ、ダグ（2006）[1965]。自然演繹：証明理論的研究。ミネオラ、ニューヨーク：ドーバー出版。ISBN 978-0-486-44655-4。
• スマリヤン、レイモンド・メリル（1995）[1968]。第一階述語論理。ニューヨーク：ドーバー出版。ISBN 978-0-486-68370-6。
• サップス、パトリック・コロネル（1999）[1957]。論理学入門。ミネオラ、ニューヨーク：ドーバー出版。ISBN 978-0-486-40687-9。
• 竹内, ガイシ(2013) [1975].証明理論（第2版）. ミネオラ、ニューヨーク: ドーバー出版. ISBN 978-0-486-49073-1。

• 「シークエント（論理学において）」、数学百科事典、EMS Press、2001 [1994]