…限的形容詞の意味は、述語 $`p : Y \to \mbf{B} \In \mbf{Set} `$ だと考えます。$`X = \mbf{B}, Y = \mbf{1}`$ と置きます。すると：$`\quad a : \mbf{1} \to \mbf{B} \In \mbf{Set}`$ $`\quad p : \mbf{1} \to \mbf{B} \In \mbf{Set}`$$`a = p`$ となる可能性はあります。 [/補足]同綴異義エントリ（2つのエントリ）、同綴異…

…至る経緯 整数区間 述語と論域 整数区間のk分割 弱分割と順序付き分割 公理系と包含関係 おわりに この記事に至る経緯最近の過去記事「コンウェイ不動点オペレーター： 圏論的背景と計算公式」でコンウェイ圏を紹介しました（過去記事で「コンウェイ圏」という名称は使ってませんが）。コンウェイ圏〈Conway category〉は、デカルト圏にコンウェイ不動点オペレーターを載せた圏論的構造です。双対的に、余デカルト圏に余コンウェイ余不動点オペレーターを載せた余コンウェイ圏〈coConw…

…の圏を引数に受け取る述語〈単項述語〉です。以下は、圏の性質の例です。 圏 $`\cat{C}`$ のすべての対象は自然数である。 圏 $`\cat{C}`$ の対象は有限個である。 圏 $`\cat{C}`$ は骨格的である。 圏 $`\cat{C}`$ は小さい。 圏 $`\cat{C}`$ は終対象を持つ。 論理式で書くなら： $`\forall x\in \mrm{Obj}(\cat{C}).\, x \in \mbf{N}`$ $`\mrm{isFinite}(\mr…

…にはなるでしょう。 述語論理： ベース圏と論理代数の圏 ここで扱うハイパードクトリン（と呼ばれるインデックス付き圏）は、値がデカルト閉圏であるとします。デカルト閉圏（小さくなくてもよい）達の2-圏を（それが定義されているとして）$`\mbf{CCCAT}`$ として、ハイパードクトリン $`\cat{D}`$ は次の形です*1。$`\quad \cat{D} : \cat{C}^\op \to \mbf{CCCAT} \In \mbb{2CAT}`$ハイパードクトリンの域（イ…

…デックス付き圏”は、述語論理、型付きラムダ計算、依存型理論などの定式化に便利です。多グラフポリモノイド圏の下部構造である一般化グラフは多グラフ〈polygraph | ポリグラフ〉です。「ポリグラフ」は「コンピュータッド〈computad〉」の同義語として使われることもありますが、ここでの多グラフ〈ポリグラフ〉は、コンピュータッド（「ペースティング図、コンピュータッド、ストリング図」参照）とは別物です。「ポリグラフ」という言葉の曖昧性は次の用語・用法図（「パンダ用法と用語・用…

…場合は違って、特定の述語（または論理式）からの射で保証されている、という意味になる。 型理論と論理の双方を、うまく調整すれば、きれいな対応を作ることもできる。例えば、論理の側で「仮定なしの証明しか考えない」と制限すると、型理論のインスタンスとうまく対応する。 ニュートラルな動詞 support を論理なら guarantee 、型理論なら inhabit に変えて調整しました。それだけでなく、上記注意事項のような方法論や習慣の違いも考慮する必要があります。「Proofs-as…

…て、$`X`$ 上の述語（ブール値の関数）達の集合 $`\mrm{Pred}(X)`$ を考えます。$`\mrm{Pred}(X)`$ の要素を対象として、述語のあいだの論理順序を射とする圏を $`\mbf{X'}`$ とします。論理順序とは、以下のように定義される順序です。$`\T{For }p, q \in \mrm{Pred}(X)\\ \quad p \preceq q :\Equiv \forall x\in X.\, p(x) \le q(x) `$順序 $`\l…

…論理ですが、古典一階述語論理だと考えてもさほど不都合はありません。「依存型〈dependent type〉」という用語の曖昧性からの混乱を軽減するために、「依存性型〈type with dependency〉」という言葉を使います。依存性型はファミリーのことです（集合論ベースなので）。「依存型」は、シグマ型またはパイ型を表すことがあります。曖昧語「依存型」を使うと、次の文は正しい事実を述べた文です。 依存型から依存型を作ると依存型だが、作った依存型は単純型のこともある。 より…

…-be}} &\T{述語} \ar[u]|{\T{part-of}} \ar[d]|{\T{should-be}} &\T{目的語} \ar[ul]_{\T{part-of}} \ar[d]^{\T{should-be}} \\ \T{名前} &\T{関係キーワード} &\T{名前} }`$節とは、グラフの辺とその両端のノードからなるトリプル〈三つ組〉です。節はRDFトリプルと同義です*1。「主語」、「述語」、「目的語」という構文構成素名〈syntactic constitu…

…r]_4 &{\T{述語} } \\ {} &{\T{論理式}} \\ {} &{\T{定理}} } `$[追記 date="2026-05-06"] 「～ は我々にとって永遠の命題である」という言い回しを耳にしました。この場合、「命題」は「課題」、「問題」に置き換えても意味は通じます。この文のニュアンスでは、「解けない課題・問題」、「謎」といった含みがあるのでしょう。専門用語の「命題」の意味のひとつに「定理」があります。これは、真であることが保証された命題を単に「命題」と呼…

…e}`$ ： 関数が述語（ブール値の関数）であることを示す。 $`\T{@functorObj}`$ ： 関数が関手の対象パートであることを示す。 $`\T{@functorHom}`$ ： 関数が関手のホムパートであることを示す。 アノテーション属性は、必要になったときに付け足してよいことにします。シンタックスシュガー生のラムダ式〈ラムダ項〉の書き方を少し工夫すると、視認性・可読性が向上します。より読みやすい書き方（内容は変更せず）をシンタックスシュガー〈{syntax |…

…pes の立場により述語論理も包摂します。命題と証明が、型とインスタンスによりシミュレートされます。依存型理論の定式化も色々ありますが、宇宙のラムダ計算では集合論的依存型理論を採用します。包括圏〈comprehension category〉やファミリー付き圏〈category with families〉を参照はしますが、抽象的なままで扱うわけではなくて、集合論的セマンティクスを一緒に考えます。集合論的依存型理論のためには、基盤となる集合論的インフラストラクチャが必要です。…

…が、命題（意味的には述語、構文的には論理式） $`P`$ で特定できるとします。つまり：$`\quad \xymatrix{ {} &{ \{x\in A\mid P\}} \ar@{_{(}->}[dl] \ar[dr]^{\u{f}} &{} \\ {A} &{} &{B} }\\ \quad \In \mbf{SET} `$ このとき、部分関数 $`f`$ を次の形のラムダ式〈ラムダ項〉で書き表すことにします。$`\quad f := \lambda( x\in A\m…

…理的解釈依存型理論と述語論理とのあいだには対応関係があります。単純型理論と命題論理のあいだのカリー／ハワード／ランベック対応〈Curry-Haward-Lambek correspondence〉の依存版の対応です。依存カリー／ハワード／ランベック対応〈dependent Curry-Haward-Lambek correspondence〉により、前節の2つの同型を論理的に解釈してみると、以下にようになります。$`\quad \exists x\in X.( P(x)\An…

…、依存型理論のなかで述語論理は展開できる、ということです。そういうことであれば、型理論の言葉と論理の言葉が揃っていてくれたら嬉しい。実情はどうでしょうか？ 型理論 論理 型 命題 単純型 真偽値（単純命題とは言わない） 依存型 述語（依存命題とは言わない） 単純型のインスタンス 真（インスタンスという言葉は使わない） 依存型のインスタンス ？？ 単純型のインスタンス項 命題論理の証明 依存型のインスタンス項 述語論理の証明 「？？」は適当な言葉がないということです。個人的には…

…理論から派生する依存述語論理や依存ラムダ計算の基盤にもなります。タルスキー／グロタンディーク集合論の贅沢さは、利便性の定式化です。利便性と単純さはトレードオフの関係にあり、利便性の追求は複雑さをもたらします。用途・目的に応じて、適切な利便性〈贅沢さ〉の程度を決める必要があります。 続きの記事： 贅沢なタルスキー／グロタンディーク集合論 補遺 *1:「型コスモロジー： 型宇宙、型銀河、ユグドラシル」ではボールドの $`\mbf{V}`$ 、「最近の型理論： 宇宙・世界・銀河 も…

…ンスタンス 型クラス述語とイプシロン型 記号の乱用のメカニズム 以下、ゴグエン指標には相対指標の観点からの補正が入るとします。ゴグエンが隠蔽指標〈隠蔽仕様〉／隠蔽代数を導入したのは、オブジェクト指向的なソフトウェアシステムの定式化のためです。つまり： オブジェクト指向的なソフトウェアシステムのモデルは、隠蔽指標のモデルである。 これを、ゴグエンの隠蔽の教義〈Goguen's yoga of hiding〉と呼びましょう。この教義は、外部に開示したくない内部状態を持つシステム一…

…ーアオートマトンなら述語ラベルとアクションラベルの二種類のラベルがありました。一般的なホーアオートマトンではさらにコンストラクタラベルとデストラクタラベルも追加されます。ラベル〈label〉の同義語として、記号〈symbol〉、名前〈name〉、識別子〈identifier〉などがありました。ときに、ラベルを字〈letter〉と呼ぶこともあります。すべての種類のすべてのラベルを全部寄せ集めた集合を（オートマトンの）アルファベット〈alphabet〉と呼びます。当面、アルファベ…

…か？に注目するより、述語が何であるか？と考えたほうがわかりやすいです。$`X`$ を集合だとして、それぞれの論理で“$`X`$ 上の述語”は以下のようです。（$`\mbf{1}`$ は特定された単元集合〈distinguished singleton set〉で、$`X + \bot`$ は $`X \cup \{\bot_X\}`$ の略記とします。 決定性二値論理（古典論理）： $`\mbf{Det}(X, \mbf{B})`$ の要素が述語 半決定性三値論理： $`\m…

…$ に値を持つ写像は述語〈predicate〉と呼ぶので、ホーアトリプルの意味は述語です。ただし、集合圏（集合と写像の圏） $`\mbf{Set}`$ ではなくて、半決定性写像の圏 $`\mbf{SDet}`$ で考えているので、述語の値に未定義（$`\bot`$）があるかも知れません。老婆心で言っておきますが、述語記号や論理式は構文的対象物〈syntactic object〉のことで、述語は意味的対象物〈semantic object〉です。述語記号（単なる記号・ラベル・名…

…o S`$ は写像 述語ラベル達の集合〈set of predicate labels〉 $`P`$ $`P`$ は集合 観測写像〈observation map〉 $`\omicron`$ $`\omicron : S\times P \to \mbf{B}`$ は写像（'$`\omicron`$' はラテン文字オーではなくて、ギリシャ文字オミクロン） $`\mbf{B}`$ は二値の真偽値の集合 $`\mbf{B} = \{\mrm{T}, \mrm{F}\}`$ $`P…

…河の塔 族銀河の塔 述語銀河の塔 データ型宇宙の塔 命題宇宙の塔 この記事では、グロタンディーク宇宙の塔とコア銀河の塔の2本の塔だけを説明します。2本の塔と、それらを“横に繋ぐ”関係性は、梯子の形をしたユグドラシル（有向グラフ）になります。6本の塔すべてを含むユグドラシルについては、引き続く記事達で述べるつもりでいます。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mbf}[1]{\mathbf{#1}} \newcomm…

…子 // エス関手 述語論理： ハイパードクトリンとパルムクイスト二重圏 // エス関手 k-特性関手とk-特性付き圏 インデックス付き圏（と呼ばれる反変関手）$`\msc{E}`$ の射パート $`\msc{E}_\mrm{mor}`$ の値（再インデキシング関手） $`\msc{E}(f) = \msc{E}_\mrm{mor}(f)`$ を $`f^*`$ と略記します。包括圏のグロタンディーク・ファイブレーションに対応するインデックス付き圏〈宣言関手〉は、包括圏の一部…

…) `$ ちなみに、述語論理の場合なら、対象が述語〈predicate〉で証明が射（ホムセットの要素）である圏を考えて次のようになります。$`\quad \mbf{Pred}[B](\exists_f P, Q)\cong \mbf{Pred}[A]( P, \diamondsuit_f Q) `$ $`\quad \mbf{Pred}[A](\diamondsuit_f Q, P)\cong \mbf{Pred}[B]( Q, \forall_f P) `$ $`\diam…

…se〉達を同時に扱う述語論理の記述や、テンソルネットワークの記述に好都合です。複数の分野で共通に使える記述言語とするためには、データベースでしか通用しない部分は削り落として、問い合わせ言語のエッセンスだけを抜き出したいのです。エッセンシャルな問い合わせ言語を支える下部構造は型システム〈type system〉です。型システムは次の2つの能力を持ちます。 既存の幾つかの型達から、タプル型〈tuple type〉を作れる。 既存の型から、ベキ集合型〈powerset type〉を…

…複圏は同義語です。 述語論理： 様々な多圏達の分類整理 オペラッドの話 モノイド圏から作る複圏と多圏 複圏〈オペラッド〉とプレ準同型射の圏 ワイヤリング図達の複圏を $`\cat{WD}`$ とします。$`\cat{WD}`$ が何者であるか？は、今は保留します。そういう複圏があるのだ、と思ってください。いつものように、同義語〈別名〉がイッパイあったり、一般論と具体例で呼び名が違ったりするので、表にまとめておきます。 複圏 オペラッド ワイヤリング図達の複圏 対象 色 ボック…

…ategory〉（「述語論理： 様々な多圏達の分類整理」参照）の流儀で行います。丸いノード $`f`$ はレンズ射です。レンズ射を右側横方向に繋ぐことができます。システム（四角い箱）とレンズ射、あるいはレンズ射とレンズ射はレンズ結合〈lens composition〉で横方向に連結できます。入力・出力・制御のインターフェイスを持つシステム（四角い箱）をIOCシステム〈IOC system〉と呼ぶことにして、IOCシステム達の圏を $`\mbf{IOCSys}`$ とすると、複…

…e〉かどうかを調べる述語と解釈できます。集合 $`B`$ の要素を、ラベル〈label〉、アクションラベル〈action label〉、アクション〈action〉、コマンド〈command〉、刺激〈stimulus〉などと呼びます。形式言語理論の文脈なら、記号〈symbol〉とか語〈word〉と呼ばれるでしょう。状態遷移関数 $`\mrm{trans}`$ は、現在の状態とアクションを受け取って、次の状態を返します。状態遷移系の“実行”を担うのが状態遷移関数です。古典的状態遷…

…[主語]‥ が ‥[述語]‥ であるとは、‥‥この日本語を次の構文で書くことにします。$`\For param\: \Subject subj\: \Predicate pred\: \Means \cdots`$ 可読性のために、空白や改行を挿入するのは自由です。主語〈subject〉には可能なら色を付けます。例えば次のように。$`\For param\\ \Subject \\ \quad \ora{subj}\\ \Predicate pred\\ \Means\\ \…

…とつだけ返す」です。述語に対するイプシロン記号は、集合に対するイプシロン記号を使って次のように定義できます。$`\quad \varepsilon\, x\in X.P(x) := \varepsilon\, \{x\in X \mid P(x)\}`$ ここから先では、イプシロン記号は集合に対して作用するとします。（さらに後でまた概念を変更しますが。）なお、イプシロン記号に関してより詳しくは、以下の過去記事達を参照してください。 イプシロン計算ってなんですかぁ？ こんなもん…