選択公理なしの型理論でZFの無矛盾性を形式化
CIC + EM $\vdash$ Con(ZF): the consistency of ZF in type theory with excluded middle and no choice
この論文をやさしく読む
ひとことで言うと
排中律だけを仮定したLeanの型理論で、ZF集合論の無矛盾性を形式的に証明した研究。
何に役立つ？
型理論と集合論の証明能力の関係を理解し、形式証明の基礎を検討するのに役立つ。
この研究の面白いところ
選択公理がないと弱くなるという予想に対し、到達可能性上の再帰から順序数を扱う構成で反例を示す点。
どこまで分かった？
要旨で示されるのは指定した型理論での形式化された無矛盾性証明であり、型理論一般や集合論の絶対的な無矛盾性を証明したものではない。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
命題の非可述的宇宙を持つ依存型理論で、集合を木として解釈すると、ツェルメロ集合論が成り立つ。関数的関係を関数に変える選択演算子や記述演算子があれば置換公理も成り立つため、そうした演算子がなければ理論の強さはZF集合論より大幅に弱くなると考えられてきた。本研究はそうではないことを示す。二つの可述的宇宙を持つLeanの型理論で、排中律だけを仮定し、選択公理、命題の外延性、商型を含む他の公理を使わずに、一階論理の証明体系で明示したZFの無矛盾性を証明し、形式化した。 鍵となるのは集合の型と同じほど大きな型に対する到達可能性述語の大きな除去である。命題で再帰呼び出しを制御し、後続の呼び出しの添字を先行する呼び出しの値で決める到達可能性上の再帰により、特定の形の整礎な木を通じて命題で指定される任意の順序数を項として計算できる。あるVρがすでにZFのモデルである場合を除き、各順序数にそのような木を与える規則を示す。この規則は極限順序数への共終写像を選ぶのではなく、定義可能なものをすべて同時に扱う。前者の場合、集合を木として解釈したモデルで任意の命題的関係について置換公理が成り立つ。いずれの場合もZFはモデルを持つ。さらに、排中律の二重否定で十分であり、残る仮定は安定的な集合解釈で所属関係が二重否定の意味で整礎であることと正確に一致する。これはマルコフの原理の二重否定を含意する。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-19（UTC）
- 最新改訂
- 2026-09-19 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-19 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
The sets-as-trees interpretation of set theory in a dependent type theory with an impredicative universe of propositions validates Zermelo set theory, and it validates Replacement if the type theory has a choice or description operator, which turns a functional relation into a function. It has been natural to expect that without such an operator the strength of the type theory drops well below that of $\mathrm{ZF}$. We show that it does not. In the type theory of Lean with two predicative universes, from excluded middle as the only assumption and with no axiom (no choice, no propositional extensionality, no quotients), we prove the consistency of $\mathrm{ZF}$, stated outright for a first-order proof system. The proof is formalized. The mechanism is the large elimination of the accessibility predicate over a type as large as the type of sets: a recursion on accessibility whose recursive calls are guarded by propositions, and whose later calls are indexed by the value of an earlier call, computes as a term any ordinal that is specified by a proposition through a well-founded tree of a certain shape. We give a rule that produces such a tree for every ordinal, unless some $V_\rho$ is already a model of $\mathrm{ZF}$; the rule does not choose a cofinal map into a limit ordinal but takes all definable ones at once. In the first case the sets-as-trees satisfy Replacement for arbitrary propositional relations. Either way $\mathrm{ZF}$ has a model. Finally, the double negation of excluded middle suffices, and what remains of it is exactly that membership is not not well-founded in the stable reading of sets; this in turn implies the double negation of Markov's principle.
著者のコメント
13 pages. Lean 4 formalization at https://github.com/digama0/ConZF
arXiv ID: 2609.23143 ／ 要約の誤りについて