過去記事「GAT〈ガット〉」で、次の論文に言及しました。 [Ste19-] Title: Algebraic Type Theory and Universe Hierarchies Author: Jonathan Sterling Submitted: 23 Feb 2019 Pages: 25p URL: https://arxiv.org/abs/1902.08848 6月にチラ見しただけなの…

公理的集合論やグロタンディーク宇宙の公理系では、順序を持たないペアが作れることは保証しています。が、順序を持つペアは頑張って作るのが普通です。作り方は一通りではありません。典型的な順序ペアの作り方を見ておきましょう。$`\newcommand{\mrm}[1]{…

公理的集合論の置換公理を「関数の像は集合である」と説明したり理解したりする人がいます。まー、そうなんですけど、ここに出てくる「関数」を普通の意味で理解すると、まったくのトンチンカンなことになります。置換公理に出てくる「関数」は、普通の関数…

型理論／型システムは何十種類、いや何百種類もあるのですが、そのなかで、「今のイチ推しは何ですか？」と聞かれれば、カートメル／ヴォエヴォドスキー／パルムグレンの型理論を挙げます。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\In}{\text{ i…

「命題」という言葉は極めて曖昧な言葉です。曖昧だから色々な意味で使えて便利ということでもあります。使う場面・文脈により次のような意味があります。 真偽値 述語 論理式 定理 （国語辞書的意味で）課題、使命、目標など この曖昧性については、「Propo…

デジタル語彙目録における“管理された名前”〈managed name〉は、何らかの対象物を一意非曖昧に名付けるために使う人工的な名前です。通常のコミュニケーション内で管理された名前を直接使うことは意図してません。通常のコミュニケーション内で使う用語〈テ…