点を使わない余導関数の直観主義論理への応用
Two applications of the point-free coderivative
この論文をやさしく読む
ひとことで言うと
点に頼らない余導関数という道具で、直観主義論理の2つの性質を証明した。
何に役立つ？
Heyting代数と二階直観主義論理の意味論の限界を調べる理論的な手掛かりになる。
この研究の面白いところ
既知の非存在結果を簡潔に証明し、完全Heyting代数意味論の強完全性が成り立たないことも示した。
どこまで分かった？
要旨で述べるのは数学的な証明で、計算実験や具体的な応用例は記載されていない。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
Simmonsによる点を使わないCantor–Bendixson余導関数作用素を、直観主義論理に新たに2通り応用する。まず、この作用素を使い、2つの生成元を持つ自由Heyting代数は、どの初等トポスでも終対象の部分対象からなるHeyting代数として現れないというXuとYeの最近の結果を、より簡潔に証明する。次に、完全Heyting代数による意味論は、直観主義の二階命題論理に対して強完全ではないと証明する。つまり、任意の仮定集合からの意味論的な帰結と、通常の構文論的な帰結は一致しない。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-24（UTC）
- 最新改訂
- 2026-09-24 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-24 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
We present two new applications of Simmons' point-free Cantor-Bendixson coderivative operator in intuitionistic logic. First, we use it to give a simplified proof of the recent result of Xu and Ye that the free Heyting algebra on two generators does not occur as the Heyting algebra of subterminal objects in any elementary topos. Then we use it to prove that complete Heyting algebra semantics is not strongly complete for intuitionistic second-order propositional logic: semantic consequence from an arbitrary set of assumptions does not coincide with ordinary syntactic consequence.
著者のコメント
23 pages, 1 figure
arXiv ID: 2609.29436 ／ 要約の誤りについて