…あります。 真偽値 述語 論理式 「命題は型だ」の解釈も少なくとも3つはあります。 真偽値は型だ。 述語は型だ。 論理式は型だ。 これらの曖昧な主張を、明確にしましょう。まず、グロタンディーク宇宙 $`U`$ をひとつに固定して、次のような別名を付けます。$`\quad \mbf{Type} := U\\ \quad \mbf{Logic} := U `$$`\mbf{Type}`$ と $`\mbf{Logic}`$ は呼び名が違うだけで実体は同じグロタンディーク宇宙です。…

…リー $`f`$ は述語として使っています。$`f(t)\ne \emptyset`$ は、述語とみなした $`f`$ の値が“偽ではない”ということです。オメガ型も贅沢なグロタンディーク宇宙〈luxury Grothendieck universe〉の装備品のひとつです。 $`U`$ は、オメガ型構成に関して閉じている： $`\forall x, f.\; x\in U \land f\in \mrm{Map}(x, U) \Imp \Omega(f)\in U`$ シグマ…

…の宇宙と型、二種類の述語」において、二元の宇宙 $`{\bf Prop}`$ を次のように定義しました。$`\quad {\bf Prop} := |{\bf Bool}|`$$`{\bf Bool}`$ は2つの対象 $`{\bf 0}, {\bf 1}`$ だけを持つ集合圏の充満部分圏です。しかし実際の証明支援系などでは、$`{\bf Prop} = |{\bf Set}|`$ としています。このことについては、以下の過去記事で書いています。 カリー／ハワード対応に親しむ…

…ー $`P`$ を“述語” と考えます。$`\quad P : A \to {\bf Prop} \In {\bf SET}`$一方 集合論ベースの論理では、集合$`A`$ から二元集合（代数構造の台）$`{\bf B}`$ への写像 $`p`$ が“述語”です。$`\quad p : A \to {\bf B} \In {\bf Set}`$このギャップをどう埋めるのでしょう？$`{\bf Set}`$ はトポスなので、部分対象分類子〈subobject classifie…

…算 | 関数}記号／述語記号 ？ 式〈expression〉 形式言語の語彙は単なる集合以上の構造を持つので、コンテキスト／指標も構造を持つことになります。型理論では、コンテキストの構造を記述する手法が色々あります（「指標の圏はコンテキストの圏の反対圏」参照）。型理論と一般代数学の相互関係のモダンな記述は、次の論文の "Part 1 Dependently sorted algebraic theories" がいいかも知れません。 [Sub21-] Title: From …

…なコンテキスト」、「述語論理： カリー／ハワード／ランベック対応と推論・型つけ規則」があります。$`\Glob`$ の推論規則は以下のようです。 $`\Rule{dummy-bdry}`$ ダミーな境界項 $`*`$ は無条件に正当 $`\Rule{new-bdry}`$ 新しい境界項の構成法と正当性 $`\Rule{trivial}`$ 自明な推論は正当な推論 $`\Rule{ctx-thin}`$ コンテキストを水増し（thinning）しても推論の正当性は維持される $…

…）なので、次のような述語〈ブール値関数〉で表現できます。以下の $`{\bf B}`$ はブール値（二値）の集合です。$`\quad \mrm{IsGroup} : |{\bf Mon}| \to {\bf B} \In {\bf SET}`$$`{\bf SET}`$ は、通常の集合よりサイズが大きい集合も含む“大きい集合達の集合圏”です。小さい集合も大きい集合なので*1 $`{\bf Set}\subseteq {\bf SET}`$ です。述語 $`\mrm{IsGro…

…で無料な木 型クラス述語とイプシロン型 結局、指標と仕様の明示的な区別は設けずに、指標の拡大〈拡張〉を使うのが融通が効いて便利だと思います。そのためには、指標の圏には拡大〈extension〉をサポートする構造が必要になります。包含構造を持つ指標の圏等式的関手インスティチューションでは、指標は有向グラフ、またはパス同値関係の集合を追加した有向グラフだと具体的に定義しています。これは具体化し過ぎでした。カバーできる範囲が狭すぎるし一般化もできないし ‥‥ ここはある程度抽象的に…

…方法で作った多圏（「述語論理： 様々な多圏達の分類整理」参照）だとします。以下のような“基本素子”、あるいはスパイダー（「述語論理： 様々な多圏達の分類整理 // 補足：スパイダー」参照）を含んだストリング図をデカルト・ストリング図〈Cartesian string diagram〉と呼ぶとして、デカルト・ストリング図は多圏 $`\mrm{Poly}(\cat{C})`$ の多射〈poly {morphism | map | arrow}〉を表します。 名称 象形文字 対象ま…

…く引用するのですが、述語論理の話ではマズイことになります。どえらく誤解されるリスクがあります。述語論理とは、“不定の主語”を扱う論理です。“不定の主語”を扱わない論理は命題論理です。僕は、命題論理と述語論理という分類に意味があるとは思えないのですが、広く採用されている分類ではあります。 述語論理では、主語が不定な（具体的に確定はしてない）文も命題と考える。 命題論理では、主語が確定している文しか命題とは考えない。あるいは、そもそも主語・述語なんて分解はしないで“ひとかたまりの…

…イド多圏（簡約版） 述語論理： 様々な多圏達の分類整理 モノイド圏から多圏を構成する場合は、対称性がないとキビシイので対称性を仮定します。ストリング図で見ると、対称性があるとは、ワイヤーの交差ができることです。$`A, B`$ の交差を与える射を $`\sigma_{A, B}`$ と書きます。$`(\cat{C},\otimes, I, \sigma )`$ を対称モノイド圏とします。対称モノイド圏から作られた多圏 $`\cat{P} := \mrm{Poly}(\cat{…

…群は前層、右加群は余前層、双加群はプロ関手 Diag構成の変種とその書き方 ローヴェア・セオリーとその周辺 亜群をベースとする圏類似構造： コステロの事例 スケマティック 昔の記事 再考： クリーネスター・圏論・計算の離散力学 単純平面タングルとカウフマン図のキャンバス・基準点について 平面タングル、空間タングル、ブレイドなんかが“もつれた”話 モノイド圏上のテンプレート・オペラッド：具体例とソフトウェア的解釈 オペラッドと型付きラムダ計算 述語論理： 様々な多圏達の分類整理

…呼びます。過去記事「述語論理： 様々な多圏達の分類整理 // ワイヤリング規律による分類」では（少し状況が違いますが）、ナロー多結合〈narrow polycomposition〉、ワイド多結合〈wide polycomposition〉という言葉を使っていました。過去記事での「ワイド」の意味は、任意の部分結合〈partial composition〉に意味ですが。ある条件のもとでは、単純結合によるオペラッドの定義とフル結合によるオペラッドの定義が同値になることを示せます。し…

…： ファミリーの圏 述語 ファミリーの圏の変種： 逆向き ファミリーの圏の変種： 写像に条件を付ける シグマ共変関手 パイ反変関手 まとめ ファミリーの圏ここでのファミリー〈family〉は、集合のインデックス付きファミリー〈indexed family of sets〉です。ファミリー $`F`$ は次のような写像です。$`\quad F: I \to |{\bf Set}| \In {\bf SET}\\ \Where I \in |{\bf Set}| `$$`{\bf…

…で扱われています。 述語論理： 様々な多圏達の分類整理 ガーナー／フーショウィッツの論文： [GH15] Title: Shapely monads and analytic functors Authors: Richard Garner, Tom Hirschowitz Submitted: 18 Dec 2015 (v1), 10 Oct 2017 (v3) Pages: 52p URL: https://arxiv.org/abs/1512.05980 細かいこと 向…

…テムスキーマ」という言葉はソフトウェアに寄り過ぎなので、呼び名を変える可能性はありますが、SSモナドが重要であることに変わりはありません。そしてそれから図式的手法に関する今までの記事で、不明瞭だったと思える幾つかの点について補足しました。枠組みだけの議論では面白くないので、具体的なインターフェイス付き圏を定義して、SS構成により新しいインターフェイス付き圏を構成する例が欲しいですね。インターフェイス付き圏として述語〈predicate〉の圏が、論理との関連もあり面白そうです。

…晰な記述のためには、述語論理をけっこうヘビーに使います／使うべきでしょう。なので、論理を勉強した人にとっては、データベースは、論理を実践的に応用する練習素材としてうってつけだと思います。この記事では、「データベース:: テーブルのキーって何なのよ？」で定義したテーブル構造をもとに、データベースの数理モデルであるデータベース構造を定義します。また、正確な議論のために、幾つか用語・記法も導入します。ところどころに補足を入れています。飛ばしてもかまいません。圏論／型理論の予備知識が…

…である」という意味の述語〈predicate〉を $`\text{isSuperkey}_{(C, S, \Gamma)}(X)`$ と書くことにします。この述語は次のように定義されます。$`\For X \in \mrm{Pow}(C)\\ \Define \text{isSuperkey}_{(C, S, \Gamma)}(X) :\Iff \\ \quad \forall T \in \Gamma.\, \lnot \exists t, t'\in T.\\ \qqua…

…す（多圏については「述語論理： 様々な多圏達の分類整理」を参照）。演繹系の利用場面は、「推論」「導出」と呼ばれるような操作を持つシステムの共通構造を粗視化して眺めたいときです。具体的な詳細や一部の構造を捨ててしまえば、演繹系の枠組みで捉えられることは多いでしょう。 *1:生成系がやせていても、それから生成された複圏〈オペラッド〉がやせている（複ホムセットが単元集合か空集合）とは限りません。 *2:この条件は、スパンに対する jointly monic 条件です。 *3:証明ツ…

…積をもつ多圏です。「述語論理： 様々な多圏達の分類整理」に書いたように、「プロップ〈PROP〉 ＝ 対称・モノイド・ワイド多圏」です。"PROP" は "product and permutation category" に由来します。対称・モノイド・ワイド多圏は対称厳密モノイド圏ともみなせるので、対称厳密モノイド圏をプロップと呼ぶこともあります（用語運用は曖昧です）。ロブスキ／ザンサイ論文における層化プロップ〈layered prop〉は、余インデックス付き対称厳密モノイド…

…真）である行列 二項述語 ： 二変数のブール値関数 これらは事実上同じモノですが、由来・出自が違います。モノに対して演算を施す場合でも、使われる演算記号は由来により違います。足し算と掛け算に相当する演算記号でも、集合由来、論理由来、算術由来では次の違いがあります。 集合由来 論理由来 算術由来 $`\cup`$ $`\lor`$ $`+`$ $`\cap`$ $`\land`$ $`\cdot`$ この対応表をもう少し伸ばしてみましょう。ベキ集合 $`\mrm{Pow}(X)…

…Y`$ に関する二項述語」と言います。ブール値の論理ORを足し算とみなすと、無限の足し算でも自由にできます。“ブール値係数の行列とみなした成分総和”と“二項述語とみなした存在限量〈existential quantification〉”は同じコト（相互に移りあえるコト）です。$`\quad \sum_{x\in X}A_x^y \longleftrightarrow \exists x\in X. p(x, y)`$関係に関する用語同じモノ／同じコトに異なるたくさんの言葉を割…

…理論： 依存型理論で述語論理が出来てしまう理由 最近の型理論： 外部化手法のもとでのパイ型と指数型 型圏化関手 $`\J`$ と、それのもとになる外延化関手 $`\mrm{Inst} = \ol{(\hyp)}\;`$ を使う手法が外部化〈externalization〉手法で、外部化手法の妥当性や有効性に関する疑問点・問題点が冒頭の引用です。インデックス付き圏 $`\cat{P}`$ は、$`\cat{C}`$ の適当なシード射／シード四角形のクラスに対してハイパードクトリ…

…理論： 依存型理論で述語論理が出来てしまう理由」で導入した概念で、$`\J`$ で表します。$`\xymatrix{ \cat{C} \ar[r]^{\mrm{Inst}} \ar[dr]_{\J} & {\bf Set} \ar[d]^{\mrm{Disc}} \\ {} & \dim{\bf CAT}{1} }\\ \In \mathbb{CAT} `$外部化手法では、型外延化 $`\mrm{Inst}`$ や型圏化 $`\J`$ を用いて、圏 $`\cat{C}`$ の…

「依存型理論で述語論理が出来てしまう理由」において、2つの圏をもとにしてハイパードクトリンを構成する方法の概略を示しました。このハイパードクトリンは、依存型理論と述語論理のどちらも記述できる汎用的な機構になっています。銀河（型をホストする圏）からハイパードクトリンを構成したい動機のひとつは、構文的に定義される“型理論の型判断”や、“論理のシーケント”にハッキリした意味を与えたいからです。「ハッキリした意味」の“意味”をこの記事で説明します。$`\newcommand{\cat…

…理論の論理的対応物が述語論理〈predicate logic〉です。述語論理の圏論的定式化にはローヴェア〈William Lawvere〉のハイパードクトリン〈hyperdoctrine〉があります。ハイパードクトリンは、依存型理論の枠組みでもあります。カリー／ハワード／ランベック対応により、“単純型理論←→命題論理”、“依存型理論←→述語論理”と対応するので、依存型理論と述語論理が共通のフレームワークに包摂されるのは当然とも言えます。適当なセッティングのもとで、依存型理論を…

…理論： 依存型理論で述語論理が出来てしまう理由 最近の型理論： 型判断／シーケントの意味論に向けて 最近の型理論： 外部化手法のもとでのパイ型と指数型 最近の型理論： デカルト閉圏の外部化・内部化とスノーグローブ現象 最近の型理論： 宇宙より銀河 最近の型理論： 具体的・構文的なコンテキスト 最近の型理論： 拡張包括構造を持ったインデックス付き圏 関連記事： 射ファミリーと圏論的コンビネータ 圏の束構造と包含的圏 一般化されたファミリーの圏 自然言語混じり形式証明の意味論と最…

昨日の記事「述語論理： 二重圏的ハイパードクトリン」で、二重圏的ハイパードクトリンという概念を出しました。二重圏的ハイパードクトリンを定義するために、シード付き二重圏を定義したのですが、どうも安直過ぎました。シード付き二重圏を再定義します。$`\newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\In}{\text{ in } } `$内容： 二重圏的ハイパードク…

…いやすい気がします。述語論理系やベック／シュバレー条件が比較的素直に定義できます。[追記]シード付き二重圏の定義が甘すぎたので、「述語論理： シード付き二重圏 -- 訂正と再論」に訂正を書いています。本文中でも、注意を追記しています。[/追記]$`\newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\In}{\text{ in } } \newcommand{\i…

…圏とシーケント計算 述語論理： 様々な多圏達の分類整理 証明と計算は同じこと： 形式証明におけるノードとコネクター 多圏をモノイド圏とみなす多圏における多射の結合は、ストリング図ならワイヤーを引き回して繋ぐことに対応します。様々なワイヤリングがありますが、次のルールによる結合なら単純です。 複射 $`f: \Gamma \to \Phi`$ と複射 $`g: \Theta \to \Psi`$ は、$`\Phi = \Theta`$ のときだけ結合可能とする。 $`\cat{…