圏論図解：論理（2021）

 (abuseofnotation.github.io)
2 ポイント 投稿者 GN⁺ 2024-10-27 | 1件のコメント | WhatsAppで共有
  • 論理は、真として受け入れる原子命題から出発し、and、or、implies のような演算子でより大きな命題を作るもので、圏論と同じく合成が核心となる
  • 古典論理は命題を真/偽の Boolean 値として、論理演算子を Boolean 関数として解釈し、真理値表で否定・論理積・論理和・含意・同値を扱う
  • 直観主義論理の BHK 解釈は、命題を証明を持つ対象と見なし、A ∧ B は証明のペア、A → B は A の証明を B の証明へ変換する関数として解釈する
  • 一部の圏では、対象が命題、射が証明に対応し、順序では A ≤ B が A → B を意味する preorder または partial order として現れる
  • 直観主義論理は、順序論的には Heyting algebra、一般の圏論的には bicartesian closed category に対応し、論理積・論理和・真・偽・含意はそれぞれ meet/join、terminal/initial、exponential object に対応する

命題から始まる論理

  • 論理は、観察とは無関係にそれ自体と整合する形式的規則を扱い、あることを知っているときに別のことが真であると結論づけたり証明したりする体系である
  • 数学理論は、論理に追加の定義を加えたものと見ることができる
    • 集合論は、標準的な論理公理に集合の所属関係という原始概念を加えて定義できる
  • 論理を始めるには、真または偽として受け入れる初期命題の集合が必要である
    • これは前提、原子命題、primary proposition と呼ばれる
  • 2つ以上の命題は、and、or、implies/entails のような論理演算子によって1つの合成命題になる
    • ∧ は and
    • ∨ は or
    • → は follows または含意を意味する
  • 合成命題も原子命題と同じように、再び他の命題と合成できる

Modus ponens と恒真命題

  • Modus ponens は、A が真で A → B が真なら B も真であるという古くからある論理パターンである
    • 形式は (A ∧ (A ⇒ B)) → B
    • 「ソクラテスが人間であり、人間なら死ぬのなら、ソクラテスは死ぬ」といった例で表される
  • 論理は単一の演算だけでなく、複数の論理演算の組み合わせや関係を扱う
    • and と implies の関係は modus ponens に現れる
    • and と or の分配法則も主要な関心対象である
  • 恒真命題は、構成する命題の真偽値に関係なく常に真である命題である
    • Modus ponens は A と B が真であっても偽であっても、式全体が常に真である
    • 常に偽である命題は矛盾と呼ばれる
    • 恒真命題に not を付けると矛盾になり、矛盾に not を付けると恒真命題になる
  • 値によって真または偽が変わる命題は contingent statement と呼ばれ、論理の主な関心からは外れる
  • 最も単純な恒真命題は、各命題がそれ自身を含意するという同一律である

公理スキーマと論理体系

  • 恒真命題は公理スキーマと推論規則の基盤になる
  • 公理スキーマはプレースホルダーを含む式であり、プレースホルダーを命題に置き換えて具体的な命題を作れる
    • Modus ponens から色や具体的な命題を取り除くと一般構造が残る
    • その構造に原子命題や合成命題を差し込むことで、特定の modus ponens 命題を作れる
  • 推論規則は公理スキーマとほぼ同じ方法で使うことができ、公理スキーマも推論規則のように適用できる
  • すべての恒真命題は公理スキーマとして使える
  • 論理体系または形式体系は、公理スキーマと推論規則の集まりであり、それらを適用して可能なすべての命題を生成する
    • 例として、5つの公理スキーマと modus ponens 推論規則から成る体系が示される
    • このような論理体系が完全であるという事実は、Gödel の完全性定理と結びついている

古典論理の真理関数的解釈

  • 古典論理は、命題が真または偽のいずれかであるという二分法に基づく
  • 古典的解釈では、命題と演算子は次のように定義される
    • 命題は Boolean 値のように真または偽であるもの
    • 論理演算子は、1つ以上の Boolean 値を受け取り Boolean 値を返す関数
  • 否定 ¬p は単項演算であり、真を偽に、偽を真に変える
    • 同じ内容を真理値表で表せる
    • 二重否定除去は、否定を2回適用すると開始時の値に戻るという形で証明される
  • and は2つの Boolean 値を受け取り、両方が真のときだけ真を返す
    • p ∧ q → p
    • p ∧ q → q
  • or は2つの Boolean 値のうち少なくとも一方が真なら真を返す
    • p → p ∨ q
    • q → p ∨ q
  • implies または material condition は p → q と書かれ、p が真で q が偽のときだけ偽である
    • 古典論理において p → q は、¬p ∨ q が真である場合と同じである
  • if and only if または iff は、2つの命題が同じ値を持つとき真である
    • P ↔ Q は P → Q ∧ Q → P と同値である
  • 真理値表だけでなく、公理と推論規則によっても p → q と ¬p ∨ q の同値性を証明できる
    • 完全な同値性の証明には、両方向の証明が必要である

直観主義論理と BHK 解釈

  • 直観主義論理は、証明を普遍的真理の発見ではなく構成として見る
  • この観点では、すべての命題が必ず真または偽であるという二分法は使えない
    • ある命題は、偽だからではなく、与えられた論理体系の範囲外にあるため証明されないことがある
    • 双子素数予想がこの例としてよく挙げられる
  • Brouwer–Heyting–Kolmogorov（BHK）解釈では、命題よりも証明が中心に置かれる
    • 命題は証明を持つもの
    • 論理演算子は、他の証明から証明を作る構成
  • A ∧ B の証明は、A の証明と B の証明から成るペア、つまり product である
  • A → B は、A の証明を B の証明へ変換する関数が存在することを意味する
    • A → B の証明集合は、A から B への関数の集合、つまり hom-set として表される
    • この集合が空なら、A の証明を B の証明へ変える方法はない
  • BHK 解釈には別個の iff 演算はないが、矢印がある
    • A から B へ、B から A へ向かう関数があるとき、2つの命題は同値のように扱われる
    • 集合の観点では、2つの命題の証明集合が同型である状況である
  • 否定は単に証明がないという意味ではなく、A が真だと仮定すると矛盾に到達することを示さなければならない
    • ⊥ は証明を持たない式の証明、つまり False または bottom value の役割を果たす
    • BHK では ¬A は A → ⊥ と読まれる
    • 集合論では ⊥ は空集合として表される

論理を圏として見る

  • BHK 解釈は、論理を圏論で解釈するための高レベルな視点を提供する
  • 一部の圏は論理体系のように見ることができる
    • 対象は命題
    • 射は証明
  • すべての圏が論理体系になるわけではなく、有効な論理命題に対応する対象があり、無効な命題に対応する対象がないようにする条件が必要である
  • その条件を満たす圏は bicartesian closed category と呼ばれる
  • 単純な場合としてまず順序（order）を見ると、論理体系と原子命題の集合は圏を成す
    • A から B へ行く方法が1つだけであるか、その違いを無視すれば preorder になる
    • 互いに導かれる命題を同値と見なせば partial order になる
    • A ≤ B は A → B を意味する
  • Hasse diagram では、A が B の下にあるとき A → B が成立する

論理演算の順序論的対応

  • 論理の and と or は BHK 解釈では product と sum として現れ、順序論では meet と join に対応する
  • 論理体系になるには、任意の2つの命題を and または or で結合できなければならないため、順序はすべての要素について meet と join を持たなければならない
    • このような順序は lattice と呼ばれる
  • and と or の間の重要な法則は分配性である
    • すべての A、B、C について A ∧ (B ∨ C) ≅ (A ∧ B) ∨ (A ∧ C) が成り立つなら distributive lattice である
  • 直観主義論理を表すには、lattice に True と False に対応する要素も必要である
    • False は ⊥ と書かれ、False の証明があれば任意の命題を証明できるという爆発原理と結びつく
    • True は ⊤ と書かれ、すべての命題から導かれるが、それ自体から有意味な内容は出てこない
  • 順序において True と False はそれぞれ greatest object と least object である
    • 圏論用語では terminal object と initial object に対応する
    • least と greatest を持つ lattice は bounded lattice である

含意対象と指数対象

  • 論理体系を表す lattice には、各 A、B のペアごとに、A が B を含意するという命題を表す含意対象が必要である
  • この対象は modus ponens の構造で定義される
    • A ∧ (A ⇒ B) → B が成り立たなければならない
  • 単にこの条件だけでは十分ではない
    • A ⇒ B ∧ C や A ⇒ B ∧ C ∧ D のような別の対象も同じ位置に入れることができる
    • 実際の A ⇒ B は、A ∧ X → B を満たす X のうち最大の対象である
  • 順序論では A ⇒ B を exponential element または relative pseudo-complement と呼ぶ
    • A ∧ X ≤ B を満たす最大の X である
  • 論理的には、A ∧ X → B を満たす最も自明な命題 X が含意命題 A ⇒ B である
  • 圏論的には exponential object または internal homomorphism object として定義される
    • A × X → B という射がなければならない
    • 同じ性質を持つ他の候補対象から、実際の指数対象へ向かう一意な射が存在しなければならない
  • この含意対象の定義は直観主義論理に合っている
    • 古典論理では排中律のため A ⇒ B は ¬A ∨ B に単純化される
  • meet、join、含意対象と同様に、A ⇒ B も一意な同型を除いて定義される

Heyting algebra と bicartesian closed category

  • 直観主義論理は True、False、and、or、implies で構成される
  • これを順序として表すと Heyting algebra になる
    • join と meet を持つ
    • greatest と least object を持つ
    • 含意対象を持つ
  • 直観主義論理体系は Heyting algebra として見ることができる
    • and と or は meet と join
    • True と False は greatest と least object
    • implies は exponential object
  • 同じ定義を一般の圏に合わせて変えると bicartesian closed category になる
    • product と coproduct を持つ
    • initial と terminal object を持つ
    • exponential object を持つ
  • 直観主義論理体系は bicartesian closed category としても見ることができる
    • and と or は product と coproduct
    • True と False は terminal と initial object
    • implies は exponential object
  • 古典論理に従う lattice は bounded、distributive に加えて complemented でなければならない
    • 各命題 A について一意な ¬A があり、A ∨ ¬A = 1、A ∧ ¬A = 0 を満たす
    • このような lattice は Boolean algebra と呼ばれる

圏論的論理で見る簡単な証明

  • A ∨ ⊤ ≅ ⊤ は join の定義から直ちに従う
    • join は2つの対象以上である最小上界である
    • ⊤ 以上の対象は ⊤ 自身しかないため、任意の A と ⊤ の join は ⊤ である
    • 論理的には「任意の A または True は True」という恒真命題である
  • A → B があれば A ∨ B = B である
    • 2つの対象の一方が他方より上にあるなら、join はより上にある対象である
    • これは A ∨ ⊤ = ⊤ の一般化と見なせる
    • すべての対象 A について常に A → ⊤ が成り立つためである
  • 同一律は含意対象によっても証明される
    • A ⇒ A は A ∧ X → A を満たす最大の X である
    • この条件はすべての X について成り立つため、最大の対象 ⊤ になる
    • したがって A → A は常に真である
  • A がすべてのモデルで B を含意する semantic consequence A ⊨ B であれば、A ⇒ B も ⊤ に対応する
    • A 自体がすでに B を含意しているため、A ∧ X → B はすべての X について成り立つ
    • これは deduction theorem とも呼ばれる

Free Heyting algebra で論理を作る

  • 論理を行うには、まず問題領域に応じて使う原子命題を選ぶ
  • 選んだ論理の種類が直観主義論理なら、すべての A、B について A ∧ B、A ∨ B のような合成命題をグラフとして描かなければならない
  • 合成命題同士の合成も再び含めなければならないため、全体のリストは無限になる
  • ある命題が別の命題を含意するかどうかは、出発命題から伸びる矢印の経路をたどって確認する
  • 論理の実行とは、すでに知っていることから証明したいことまでの経路を見つけること、またはすでに持っている証明を操作して証明を構成する過程である
  • 直観主義論理では一般に、ある事実が公理から到達不能であること、つまり証明できないことを証明するのは難しい

関連記事

1件のコメント

 
GN⁺ 2024-10-27
Hacker News のコメント

  • このページは本当に素晴らしく、関連内容を勉強しているときに何度も目にしました。
    それでも、Milewski で学ぶほうに一票入れたいです。これを学ぶのは旅のようなもので、ct-illustrated の著者はまだその旅の途中にいるように思えます。
    Milewski はすでにその道を何度も歩んできた人なので、書籍とブログは良い出発点です。
    https://github.com/hmemcpy/milewski-ctfp-pdf Book
    https://bartoszmilewski.com/2014/10/28/category-theory-for-p... Blog

    • Milewski の前半十数章を読みました。最初の数章は本当に良かったのですが、厳密な定義と記法を示さない文体がだんだん苛立たしくなりました。
      軽くて不正確な散文で書けば何でも理解しやすくなると考えているようですが、そのせいで参考書としてはほとんど役に立たなくなっています。
      まったくそうではありません¹
      ¹) https://news.ycombinator.com/item?id=41756286
    • bartoszmilewski が何を言っているのか理解できないので、その本は私には役に立たなさそうです。
      ただし職場では、自分のドメインモデル全体に圏論を使っています。

  • 以前、別の URL ですでに議論されていました。
    https://news.ycombinator.com/item?id=28660131（コメント2件）
    https://news.ycombinator.com/item?id=28660157（コメント112件）

  • 本の序盤で、数学を科学や工学と比較しながら、こんな見事な一文に出会いました。
    「このため数学者は、自分たちのしていることを、ほかの学問分野にとっての価値という観点から常に弁護しなければならないという、奇妙で、独特とも言える立場に置かれる。改めて強調するが、ほかのどの学問分野についても、このようなことは馬鹿げていると見なされるだろう。」
    直接お金になる成果につながらない分野を学んだ人なら誰でも共感できる考え方ですし、数字に強い才能を持つ人たちも Milton Friedman の剃刀と戦わなければならないと聞くのはうれしいことです。

    • それなら、「文化研究」の多くのプロジェクトが実際には米国防総省と国務省から直接資金提供を受けているのは幸いですね。
      今日の「ポストコロニアル」研究全体は米国のソフトパワーのバックエンドにすぎず、戦争になればおそらくハードパワーのバックエンドにもなるでしょう。

  • 内側の円が常に垂直方向の中央に配置されるなら、円の中の円という図式は規模が大きくなったときにうまく耐えられません。

  • 圏論を使って、圏論なしでは解けなかった CS/SWE の問題を有益に解決した成功例はありますか？ モナドは該当しません。必要な状況になれば自然に発明されるものだからです。
    大学院で1年間勉強しましたが、結局あきらめました。

    • 圏論なしではモデル化できない問題はありません。
      圏論の最も基礎的な定理の一つである米田の補題は、圏の言語で表現されたあらゆる問題が集合と関数の言語に翻訳できることを直接述べています。集合として定義されるあらゆる数学的対象についても同様で、名前はいつでも定義で置き換えられます。
      圏論的な言語がある理論の暗黙の枠組みに寄与するものは、「圏」の定義を超えることはできず、その定義は非常に小さいものです。「結合法則、閉包性、単位元、逆元を持つ集合上の演算」のほうが近づきやすいのに、なぜ群を使うのか、と尋ねるのに似ています。
      抽象代数学は、十分によく現れる単純な集合上の演算の型を指す定義のライブラリに基づいています。道具や技法は、定義の中に見つかるようなものではありません。
      環、ベクトル空間、加群はそれ自体としてすぐ受け入れられることが多いのに、圏については信じる人と信じない人に分かれます。なぜそうなるのか気になります。
    • 私が知る最も近い例は UMAP の仕事です。
      Leland McInnes にインタビューしたとき、最終成果の実際のコードには必須でなくても、圏論がさまざまな点をつなげるうえで大きな役割を果たしたと詳しく説明してくれました。
      以前の最先端手法だった t-SNE に対する相対的な改善幅を見ると、ソフトウェアにおける圏論の語られ方に対する私の批判を考え直させた唯一の例です。
      https://arxiv.org/abs/1802.03426
    • 「歩いては行けなかった場所に車を使って行った成功例はあるか？」と尋ねるようなものです。
      圏論は言語であり道具なので、圏論の言語で語れることは別の言語でも語れます。
      車と同じく運転方法を覚えれば、そしてこれは学習曲線が非常に急ですが、より速く行けます。原理的には、圏論の概念を明示的に持ち出さず、歩いても行けないものはありません。
    • すでに理解しているものをより一般的な枠組みで定式化し直すと、それが実際に何を意味しているのかがよりよく見え、雑多な細部から本質を切り分けられます。
      私のごく限られた理解では、普遍性によって対象を特徴づけることが圏論の重要な部分です。
      圏論のもう一つの実用性は、コンピュータ科学者、数学者、物理学者が一緒に話すための共通言語を与える点にあります。全員が同じパターンを別々の名前と少しずつ互換性のない定義で呼んでいると、協業は簡単ではありません。
    • Topos Institute では、圏論の Kool-Aid をまだ飲んでいない人たちにもはるかに透明に見えることを期待した新しいソフトウェアを作っています。
      現在のプレアルファ版は主にシステムダイナミクス・モデリング向けですが、目標としている作業範囲には圏論的な基盤が不可欠だと考えています。誰の意見でも喜んで聞きたいです。
      https://topos.site/blog/2024-10-02-introducing-catcolab/

  • 圏論は有用だと思いますが、まだコンピューティングではそうではないように思います。
    実際に必要なことがなければ、難しく感じるのは当然です。普遍性、随伴関手、米田の補題を本当に理解する必要があるのでしょうか？ 必要がなければ、それらが何であるかを学ぶのに苦労します。
    興味深いことに、関数型プログラミングの経験は圏論の理解に役立ちますが、その逆はそれほどでもありません。たとえばパラメトリック多相は自然変換への直観を与え、自然変換は圏論のあらゆる応用で核心になります。
    圏論の説得力ある応用は非常に数学的です。代数的トポロジー、表現論、代数幾何学、非古典論理で見つかります。

  • 誤りがあります。
    「肯定式は、ここでは A と B で示した二つの命題からなる命題であり、命題 A が真で、命題 A --> B も真なら、つまり A が B を含意するなら、B も真であると言う。たとえば『ソクラテスは人間である』と『人間は死ぬ』を知っていれば、『ソクラテスは死ぬ』も知っている。」
    この例は命題論理の規則である肯定式の例ではなく、述語論理を必要とする定言三段論法です。

  • ここでは「論理は可能なものの科学」と言っていますが、論理は確定的なものの科学であるべきではないでしょうか？
    核心は、何が妥当で何が妥当でないかを確定的に言えるようにすることにあると思います。

  • 図式表記が興味深いです。
    著者は図式の真理保存変換のための推論規則も提示しているのでしょうか？