（参考） https://staff.fnwi.uva.nl/t.uemura/ Taichi Uemura Introduction PhD candidate at Institute for Logic, Language and Computation, University of Amsterdam. For contact, see my ILLC page. https://staff.fnwi.uva.nl/t.uemura/files/topos-and-hol.pdf トポスと高階論理 Taichi Uemura 2018 年 12 月 9 日 この文書は Category Theory Advent Calendar 2018 (https://adventar.org/calendars/3168) の 9 日目の記事です。前 は 7 日目の@mod poppo さんの「アプリカティブ関手ってなに？モノイド圏との関係は？調べてみました！」でした。次は 11 日 目の@yf0fyf さんの「直観主義線型論理の圏論的意味論について」です。
（参考） １）mathoverflow https://mathoverflow.net/questions/151286/probabilities-in-a-riddle-involving-axiom-of-choice Probabilities in a riddle involving axiom of choice Denis氏 Dec 9 '13
注： もともとは、質問でDenis氏が、（研究所の）職場の同僚から、 ”Probabilities in a riddle”として言われ、種明かしは、”axiom of choice”で非可測を使っているから まっとうな確率にならないよ”という説明に、「納得できない」と質問したものです。 Denis氏は、計算機系のＤＲで、数学専門ではない。 時枝記事否定派のAlexander Pruss先生とTony Huynhの二人の数学ＤＲが、縷々説明するも、 測度論に詳しくないDenis氏は、「最後まで理解できなかった」（測度論に無知と見た）というのがオチです
>>539 >時枝記事否定派のAlexander Pruss先生とTony Huynhの二人の数学ＤＲが、縷々説明するも、 >測度論に詳しくないDenis氏は、「最後まで理解できなかった」（測度論に無知と見た）というのがオチです サルの妄想には何の根拠もありません。 こちらは妄想ザルと違いエビデンスを示します。 Pruss「we win with probability at least (n-1)/n. That's right.」
higher-order logic topos で検索すると 高名な 下記のSteve Awodey先生がヒット Kohei Kishida Who? ” sheaf semantics, models are built on presheaves ” なるほど、層や圏から、higher-order logicへ繋がっていくのか（＾＾
参考 https://arxiv.org/pdf/1403.0020.pdf Topos Semantics for Higher-Order Modal Logic March 4, 2014 Steve Awodey? Kohei Kishida† Hans-Christoph Kotzsch‡ †Department of Computer Science, University of Oxford (抜粋) Abstract. We define the notion of a model of higher-order modal logic in an arbitrary elementary topos E. In contrast to the well-known interpretation of (non-modal) higher-order logic, the type of propositions is not interpreted by the subobject classifier ΩE , but rather by a suitable complete Heyting algebra H. The canonical map relating H and
616 名前：ΩE both serves to interpret equality and provides a modal operator on H in the form of a comonad. Examples of such structures arise from surjective geometric morphisms f : F → E, where H = f?ΩF . The logic differs from non-modal higher-order logic in that the principles of functional and propositional extensionality are not longer valid but may be replaced by modalized versions. The usual Kripke, neighborhood, and sheaf semantics for propositional and first-order modal logic are subsumed by this notion.
In many conventional systems of semantics for quantified modal logic, models are built on presheaves. Given a set K of “possible worlds”, Kripke’s semantics [11], for instance, assigns to each world k ∈ K a domain of quantification P(k) - regarded as the set of possible individuals that “exist” in k - and then ∃x Φ is true at k iff some a ∈ P(k) satisfies Φ at k. (引用終り) []
623 名前： y ∈ X は, x ≦ y または y ≦ x を満 たすとき比較可能であるという. もし任意の 2 元が比較可能, つまり, (iv) 任意の x, y ∈ X は x ≦ y または y ≦ x を満たす とき, (A, ≦) を全順序集合または線形順序集合という. 条件 (iv) を等号なしの 順序関係 < で述べれば次のようになる. 補 題 12.1 順序集合 (A, <) が全順序集合であるための必要十分条件は, 任意 の x, y ∈ X について, x < y, x = y, y < x のいずれか 1 つだけが成り立つことである.
例 12.2 (実数の大小) 実数 x, y ∈ R に対して, 通常の大小 x ≦ y は R 上に 全順序を定める. 実際, ≦ が全順序の条件 (i)–(iv) を満たすことは明らかだろ う. そうすると, (R, ≦) は全順序集合になる. R の部分集合である Q, Z, N は (R, ≦) の部分順序集合であり, それ自身が全順序集合である. これらの数の集 合に対しては, 特に断りのない限り, 通常の順序 ≦ を考えるものとする.
http://www.math.is.tohoku.ac.jp/~obata/student/subject/file/2018-13_WellOrdered.pdf 第13章 整列集合 GAIRON-book : 2018/6/21(19:23) 13.1 整列集合 順序集合 (X, ≦) は, すべての空でない部分集合が最小元をもつとき, 整列集 合であるといい, そのような順序を整列順序という. 定義から整列集合は必ず全 順序集合であることに注意しよう. 実際, a, b ∈ X に対して集合 {a, b} は X の 空でない部分集合になるから, それは最小元をもつ. 最小元は a または b であ るが, それが a であれば a ≦ b となるし, それが b であれば b ≦ a となる. これは, 任意の a, b ∈ X が比較可能であることを意味し, X は全順序集合である ことがわかる.
一方, 実数 R, 有理数 Q, 整数 Z は通常の大小関係 ≦ によって全順序集合で あるが, いずれも整列集合ではない. それらには最小元がないからである. だか らと言って, 実数や有理数を 0 以上のものに限っても整列集合にはならない. た とえば, X = [0, +∞) の部分集合 A = (0, +∞) には最小元が存在しない. (引用終り) []
定義 6.2.1. X 上の二項関係 <R が「空で無い任意の (X の) 部分集合 Y に対して, Y は極小 元を持つ」という性質を満たすとき, 整礎 (well-founded) であるという.
・ 整礎を論理式で表わすと以下のようになる. (最後は y = z と成り得るので z not≦ y ではなく z not< y となる). 略 以下は “空でない任意の部分集合 A は最小値を持つ” という自然数の性質を表している. N は全順序なので, z not< y ならば y ≦ z となる (5.4 章の例 5.4.3 参照).
数学的帰納法や構造帰納法は整礎帰納法の特別な場合である。整礎帰納法 は整礎関係 (well-founded relation) が定義されている集合の要素について成り立つ性質を 証明する際に用いる。整礎帰納法を理解すれば必要に応じて様々な帰納法を自分で作り上 げて使うことができる。 定義 1 (整礎関係 (well-founded relation)) 集合 A 上の二項関係 < は、無限降下列（infinite descending chain）が存在しない場合、 整礎（well-founded）であるという。 二項関係 < が定義されている集合 A 上の無限降下列とは、< の関係で左側に無限に続く集合 A の要素列である。 つまり、・ ・ ・ < ai < ・ ・ ・ < a1 < a0 のようなものである。 この定義から、整礎関係は irreflexive（非反射的）である。つまり、どの要素 a につい ても a < a は成立しない。
命題 1 < を集合 A 上の二項関係とする。A の任意の空でない部分集合 Q が極小（minimal）の要素を持つことは関係 < が整礎であるための必要十分条件である。 ここで、集合 A の部分集合 Q の極小の要素とは、 m ∈ Q ∧ {∀b ∈ A. b < m ⇒ b not∈ Q} を満たすような m である。 証明 まず十分条件であることを示す。 略
定義 集合あるいはクラス X 上の二項関係 R が整礎であるとは、X の空でない任意の部分集合 S が R に関する極小元を持つことをいう[1]。 X が集合であるとき、従属選択公理（英語版）（これは選択公理よりも真に弱く可算選択公理よりも真に強い）を仮定すれば、同値な定義として、関係が整礎であることを可算無限降下列が存在しないこととして定められる[3]。 つまり、X の元の無限列 x0, x1, x2, ... で、どんな n についても xn+1 R xn となるようなものはとれない。
順序集合論（英語版）では、半順序に対応する真の順序 (strict partial order) が整礎関係となるとき、その半順序を整礎（整礎半順序）と呼ぶ。全順序がこの意味で整礎であるとき、整列順序と呼ぶ。 集合 x が整礎的集合 (well-founded set) であることは、∈ が x の推移閉包上で整礎関係となることと同値である。ZF における公理のひとつである正則性の公理は、全ての集合が整礎であることを要請するものである。 関係 R が X 上で逆整礎 (converse well-founded) または上方整礎 (upwards well-founded) であるとは、R の逆関係 R?1 が X 上の整礎関係であるときにいう。このとき R は昇鎖条件を満たすという。
＜英語版＞ https://en.wikipedia.org/wiki/Well-founded_relation Well-founded relation (抜粋) In mathematics, a binary relation R is called well-founded (or wellfounded) on a class X if every non-empty subset S ⊆ X has a minimal element with respect to R, that is, an element m not related by sRm (for instance, "s is not smaller than m") for any s ∈ S.
Equivalently, assuming the axiom of dependent choice, a relation is well-founded if it contains no countable infinite descending chains: that is, there is no infinite sequence x0, x1, x2, ... of elements of X such that xn+1 R xn for every natural number n.[1][2] References [1] "Infinite Sequence Property of Strictly Well-Founded Relation". ProofWiki. Retrieved 10 May 2021.
In order theory, a partial order is called well-founded if the corresponding strict order is a well-founded relation. If the order is a total order then it is called a well-order.
In set theory, a set x is called a well-founded set if the set membership relation is well-founded on the transitive closure of x. The axiom of regularity, which is one of the axioms of Zermelo?Fraenkel set theory, asserts that all sets are well-founded.
A relation R is converse well-founded, upwards well-founded or Noetherian on X, if the converse relation R?1 is well-founded on X. In this case R is also said to satisfy the ascending chain condition. In the context of rewriting systems, a Noetherian relation is also called terminating.
642 名前：tructure. Then R is a strictly well-founded relation if and only if there is no infinite sequence ?an? of elements of S such that: ∀n∈N:an+1 R an
Proof Reverse Implication Suppose R is not a strictly well-founded relation. So by definition there exists a non-empty subset T of S which has no strictly minimal element. Let a∈T.
Since a is not strictly minimal in T, we can find b∈T:bRa. This holds for all a∈T. Hence the restriction R↑T×T of R to T×T is a right-total endorelation on T.
So, by the Axiom of Dependent Choice, it follows that there is an infinite sequence ?an? in T such that: ∀n∈N:an+1 R an It follows by the Rule of Transposition that if there is no infinite sequence ?an? of elements of S such that: ∀n∈N:an+1 R an then R is a strictly well-founded relation. □
Forward Implication Let R be a strictly well-founded relation.
Aiming for a contradiction, suppose there exists an infinite sequence ?an? in S such that: ∀n∈N:an+1 R an
Let T={a0,a1,a2,…}. Let ak∈T be a strictly minimal element of T.
That is: ∀y∈T:y notR ak But we have that: ak+1 R ak So ak is not a strictly minimal element. It follows by Proof by Contradiction that such an infinite sequence cannot exist. □
Axiom of Dependent Choice This theorem depends on the Axiom of Dependent Choice, by way of Infinite Sequence Property of Strictly Well-Founded Relation/Reverse Implication. Although not as strong as the Axiom of Choice, the Axiom of Dependent Choice is similarly independent of the Zermelo-Fraenkel axioms. The consensus in conventional mathematics is that it is true and that it should be accepted.
Sources 1996: Winfried Just and Martin Weese: Discovering Modern Set Theory. I: The Basics ... (previous) ... (next): Part 1: Not Entirely Naive Set Theory: Chapter 2: Partial Order Relations: Theorem 2 (引用終り) 以上
上昇列（ or 昇鎖>>579）と、降下列の区別があるって ↓ 上昇列と、降下列（ or 昇鎖>>579）の区別があるって
かな >>579より 「関係 R が X 上で逆整礎 (converse well-founded) または上方整礎 (upwards well-founded) であるとは、R の逆関係 R-1 が X 上の整礎関係であるときにいう。このとき R は昇鎖条件を満たすという」 だからね
日本の数学用語は、難しいね 因みに 同じ箇所を英語では（>>579より） ”A relation R is converse well-founded, upwards well-founded or Noetherian on X, if the converse relation R-1 is well-founded on X. In this case R is also said to satisfy the ascending chain condition. In the context of rewriting systems, a Noetherian relation is also called terminating.” だが、やっぱ英語でも難しいね（＾＾；
