数理論理学をマッピングする

#🌱

ChatGPTのDeep Research、Gemini、Wikipediaを見つつまとめたものであるため怒られそうだが、叩き台ぐらいにはなるはず

Handbook of Mathematical Logic(1977)時点の分類によると以下になる。

集合論

モデル理論

再帰理論

証明論と構成的数学

形式論理体系

命題論理(PL)

一階述語論理(FOL)

二階述語論理(SOL)

高階述語論理(HOL)

計算型理論(Computational Type Theory)

直観主義型理論≒Martin-Löf型理論

Homotopy Type Theory(HoTT)

Univalent Foundations

Cubical Type Theory

etc

モデル論

圏論的論理(型理論 + モデル理論)

ETCS (= ZFC公理系)

計算可能性理論(computability theory)

集合論

型理論は直観主義論理からの派生であるらしい

再帰理論は現在では古い呼び方であるため計算可能性理論の方がよい

数理論理学のカテゴリマッピング

code:mermaid

flowchart LR

mathLogic --> proofTheory証明論

mathLogic数理論理学 --> modelTheoryモデル理論

mathLogic --> setTheory集合論

mathLogic --> compTheory"計算可能性理論(再帰理論)"

proofTheory --> formalLogic形式論理体系

formalLogic --> cl古典論理

formalLogic --> ncl非古典論理

ncl --> ml様相論理

ml --> temporal時相論理

ml --> epistemic認識論理

temporal --> CTL計算木論理

temporal --> LTL線形時相論理

temporal --> MTLMetric 時相論理

temporal --> STL信号時相論理

ncl --> linear線形論理

ncl --> mv多値論理

ncl --> fuzzyファジィ論理

ncl --> para矛盾許容論理

ncl --> rel関係論理

ncl --> algLogic代数的論理学

ncl --> il直観主義論理

click il "https://en.wikipedia.org/wiki/Intuitionistic_logic" "Intuitionistic Logic"

il -- Curry-Howard同型対応 --> typeTheory型理論

%% noteCH"※Curry–Howard対応は直観主義論理と型理論の間の同型関係" %%

%% noteCH -.-> il %%

%% noteCH -.-> typeTheory %%

typeTheory --> dtt依存型理論

typeTheory --> constructiveMath構成的数学

dtt --> ctt計算型理論

dtt --> itt直観主義型理論

dtt --> mlofMartin-Löf型理論

mlof --> HoTTホモトピー型理論

HoTT --> cubicalTT立方型理論

HoTT --> UFUnivalent Foundation

itt -.->|ほぼ同義| mlof

cl --> proL命題論理

cl --> preL述語論理

preL --> FOL一階述語論理

preL --> SOL二階述語論理

preL --> HOL高階述語論理

FOL --> manySorted多ソート論理

manySorted --> orderSorted順序付きソート論理

setTheory --> zAxZ公理系

zAx --> zfAxZF公理系

zfAx --> zfcAxZFC公理系

setTheory --> etcetc ...

compTheory --> compTheoryNarrwow計算可能性理論（狭義）

compTheoryNarrwow --> turingMachineチューリングマシン

compTheoryNarrwow --> recursiveFunction再帰関数

compTheory --> complexity計算量理論

il --> constructiveMath

il -- Curry–Howard同型対応 --> itt

modelTheory --> catLogic圏論的論理

typeTheory --> catLogic

catLogic --> ETCS"集合の圏の初等理論 (ETCS)"

ETCS -.->|同等| zfcAx

code:mermaid

flowchart LR

mathLogic数理論理学 --> setTheory集合論

setTheory --> zAxZ公理系

zAx --> zfAxZF公理系

zfAx --> zfcAxZFC公理系

setTheory --> NBGNBG集合論

NBG --> MKMorse-Kelley集合論

setTheory --> MacLaneSTMacLane集合論

setTheory --> AckermannSTAckermann集合論

setTheory --> NFNew Foundations

%% NFは層化の概念が型理論的であるため、NFの子として位置づける　%%

NF --> TSTTyped Set Theory

setTheory --> PocketSTPocket集合論

setTheory --> DescriptiveST記述集合論

setTheory --> UrelementST非有基底集合論

参考

Mathematical logic - Wikipedia

数理論理学 - Wikipedia

ChatGPT.iconhttps://chatgpt.com/share/68345a3b-9c20-800d-bc40-79eb2941a717

ChatGPT.iconhttps://chatgpt.com/share/683892d4-a2b8-800d-9cff-4a48b9e04d09

Many-sorted logic - Wikipedia

再帰理論 - Wikipedia

色々な集合論の公理系 - 進捗置き場というわけでもない場所

メモ

論理学の歴史 - Wikipedia