…合 $`X`$ 上に述語 $`p`$ があると、$`p`$ を満たす $`X`$ の要素達からなる部分集合が特定できます。この部分集合は次のように書きます。$`\quad \{x\in X\mid p(x)\}`$ これはお馴染みですよね。この書き方は、部分集合の内包的定義〈intensional subset definition | intensional definition of a subset〉と言ったりします。包括〈comprehension〉は内包〈inten…

…unctor〉」（「述語論理： ハイパードクトリンとパルムクイスト二重圏 // エス関手」も参照）をしばらく使ってましたが、ステップ〈step〉と同様、色が無さすぎなので、型理論／論理／インスティチューション理論の文脈では宣言関手にします。なお、「k-特性関手とk-特性付き圏」で述べた特性関手は完全に一般的概念なので、そのままとします。具現化次の概念も同じことです。 型理論のインスタンス〈instance〉 論理の証明〈proof〉 インスタンスを表す構文的対象物〈synta…

…が、イコライザーには述語としてのイコールが登場しません。命題と真偽値を扱う論理から見た方程式（等式的論理式）は現れないのです。が、トポス内でイコライザーの定義をいじると、等値述語を絡ませることが出来ます。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\mbf}[1]{\mathbf{#1}} %\newcommand{\twoto}{\Rightarrow …

…す。（限量子の話は「述語論理： ハイパードクトリンとパルムクイスト二重圏」に書いています。）$`\quad P: \cat{C}^\op \to \cat{L} \In 2\mathbb{CAT}`$ 2-圏 $`\cat{L}`$ が1-圏に退化していて、サイズもあまり大きくないなら、次のようにみなすことが出来ます。$`\quad P: \cat{C}^\op \to \cat{L} \In \mbf{CAT}`$ $`P`$ が反変関手であることは次のようにも書けます。$…

…$内容： 薄い前層と述語 クラッシュ・オペレーター 論理演算と限量子 ダイアモンド・オペレーター ※色付きテキストは次の約束で使います。 青い文字： 重要な概念・用語だがこの記事内では定義・説明してないもの。 赤い文字： この記事内で導入・定義した概念・用語。過去の定義の再掲・繰り返しのときもある。 マゼンタの文字： この記事内の後方で定義されるか参照〈リンク〉される概念・用語。 薄い前層と述語集合 $`X`$ は離散圏とみなせます。「集合を離散圏とみなす」といちいち断るのは…

…predicate〈述語〉」、「property〈性質〉」などと呼ばれます。それじゃピー関手か？ となります。一般的な状況では「declaration〈宣言〉」だろうし、宣言が図形的なとき（「CW指標とCWテレスコープ（実例）」参照）は「attachment〈添加〉」です。当たり前ですが、最初の一文字はバラバラになります。それと、エス関手の余域が集合圏ではないケースも多くて、エス関手がインデックス付き圏〈indexed category〉となることもあります。つまり、一般には…

…バタしていました。 述語論理： 二重圏的ハイパードクトリン 述語論理： シード付き二重圏 -- 訂正と再論 結局、ハッキリとした定式化は得られず、締りのないままに放置。ですが、アイディアと方向性は正しかったように思います。道具・手段が足りてなかった、と。ディスプレイクラスやC-システムを知った2024年の秋に、次の過去記事でもう一度“二重圏ベースのハイパードクトリン”に触れています。 コンテキストの圏と指標の圏と限量子 // エス関手とハイパードクトリン 2023年に「シード…

…た依存型理論であり、述語論理とそのモデル理論を吸収できます。包括圏とデカルト関手ν-インスティチューションを鳥の視点で見るときは、包括圏として扱います。包括圏 $`\msc{K}`$ の構成素は次のものです。 全体圏〈total category〉 $`\mrm{Tot}(\msc{K}) \in |\mbf{CAT}|`$ ベース圏〈base category〉 $`\mrm{Base}(\msc{K}) \in|\mbf{CAT}|`$ 射影関手〈projection f…

…イド多圏（簡約版） 述語論理： 様々な多圏達の分類整理 で結局、マジメに多圏を定義してみるか（今ここ）、と。アイディア・手法は、「多圏の必要性、煩雑さ、そして単純化」で紹介しているユルゲン・コスロウスキ〈Jürgen Koslowski〉、リチャード・ガーナー〈Richard Garner〉にだいたい従います。準備： モナド基礎とする圏は集合圏〈小さい集合達の圏〉$`\mbf{Set}`$ に固定します。一般的な圏 $`\cat{C}`$ にしてもいけますが、話がややこしくな…

…呼びます。過去記事「述語論理： カリー／ハワード／ランベック対応と推論・型つけ規則」では、フェンス記号に '$`|`$' を使っていますが、'$`|`$' は OR の意味を持った区切り記号にしたいので、コンテキストの区切り（OR の意味は持たない、むしろ AND）には '$`\|`$' を使うことにします。さて、型理論の演繹定理ですが、$`T`$ を型理論の導出システムとして、次の2つのメタ命題が、メタに同値であることを主張します。 $`\Sigma \Vvdash_T \…

…イコール／等式 古典述語論理のイコール／等式 圏論のイコール／等式 まとめ 集合論のイコール／等式現在の数学的議論は、建前としては集合論に帰着させることになっています（実際にそうするとは言ってない）。$`x = y`$ を集合論の意味で解釈するなら、次の命題〈論理式〉と同じです。$`\quad x\subseteq y \land y \subseteq x`$ 集合の包含関係を所属関係で書き下せば、以下のようになります。$`\quad \forall z.\, z\in x…

…のこと 命題実体： 述語のこと 型項： 型を表現する構文的対象物〈項 | 式〉 型実体： 型の意味論的対象物（意味論により解釈が異なるが、例えば集合） 上の対応表のような相互翻訳を提示すると、各分野ごとの用語が持つ語感、ニュアンス、連想などを持ち出して、「意味が違う、翻訳になってない」と言う人がいますが、それを言い出すと翻訳は不可能です。多少の意味的ズレとか気持ち・感情の問題には目をつぶってください。基本導出ステップ、導出ルール導出系には基本導出ステップ〈primitive …

…理における「論理式／述語の変数水増し」に対応するからで、他の文脈・観点からは別な名前が付いています（前節の最後参照）。標準射影 $`\rho^{\Gamma, A}`$ は依存射影の特別なものなので、$`\F{S}(\rho^{\Gamma, A})`$ は水増しです。余包含的なコンテキストの圏では、一般の依存射影は標準射影の結合で書けるので、標準射影の水増しを考えれば十分です。標準射影の水増しを次のように書きます。$`\quad \Delta_{\Gamma, A} := …

…命題」を真偽値または述語（ここは曖昧）の意味で使う。 意味論の文脈で、「命題」を真偽値の意味で使う。 意味論の文脈で、「命題」を述語の意味で使う。 これを図示すると次のようです。 説明を追加します。構文論〈syntax〉とは、語彙〈ボキャブラリー〉と文法〈グラマー〉の議論です。文字・名前・記号などから、文法の規則に従って記号的表現を組み上げます。記号的表現は項〈term〉とか式〈expression〉と呼びます。一般的には、項と式は同義語ですが、論理では項〈term〉と論理式…

…でしょう。ハイティング圏を強くして古典論理に向かう方向性があります。一方で、デカルト積を弱めてモノイド積にすることにより、古典論理とは全然違った世界を見せてくれます。また、「命題」「真偽値」のような厄介な曖昧多義語をうまく解釈する道具としても、ハイティング圏は大変に有用です。命題実体＝述語 とは、ハイティング圏を余域とする関手のことだし、真偽値とはハイティング圏の対象だと定義すれば丸く収まります。ハイティング圏は、論理／型理論／圏論を互いに結び合わせる良い位置に居る構造です。

…値という意味 2. 述語という意味 3. 論理式という意味 4. 定理という意味「命題」の曖昧性に関する分析は「「命題」の曖昧性から前層意味論へ」に書いています。型理論側の「型」と「項」もアンバランスな用法です。「型理論の「代入」の分析」から引用しましょう。 次のようなアンバランスな規約が多数派です。 「ソート〈型〉」はソート項〈型項〉を意味する。 単に「項」と言ったら、それはオペレーション項〈関数項〉を意味する。 「ソート」が（文脈により）ソート実体を意味することもある。 …

…て、新しい関係（二項述語）を定義するかも知れません。$`\T{define }\T{isNextOf} := \lambda\, (y, x\in U).\, y = s(x)`$実装者Bさんは、指標 $`\T{Succ}`$ に対して次のようなモデル〈実装 | 具体例〉を定義するかも知れません。$`\quad (\\ \qquad U := \{0, 1\} \, ,\\ \qquad i := \lambda\, ().\,0 \, ,\\ \qquad s := \la…

…ド／ランベック対応のより詳しいことは、以下の過去記事を参照してください。 述語論理： カリー／ハワード／ランベック対応と推論・型つけ規則 [/追記] *1:[追記]ある文脈・スコープ内での「いつでもどこでも」です。グローバルに同義語なんてのは、そもそも考えないです。すべての語義は文脈・スコープに相対的なので。[/追記] *2:[追記]ここでのナカグロ記号は、形容詞のかかり方を明示する目的で使っています。「バナナ・リンゴ・オレンジ」のような列挙の区切りではありません。[/追記]

…ることもできます（「述語論理： 様々な多圏達の分類整理」参照）。ゲンツェンのシーケントは多圏では解釈できません。ゲンツェンのシーケントにおける両辺とも空なシーケント $`(,)\Ent (\mid)`$ は矛盾を表すので、証明〈導出〉されては困るシーケントです。しかし、コンパクトシーケントにおける両辺とも空なシーケント $`(,)\Ent (,)`$ は常に導出可能〈証明可能〉な当たり前のシーケントです。矛盾と当たり前の区別が出来ないのはほんとに困ります。このような事情で、区…

…は型理論に譲った）。述語と部分集合の一対一対応を強調するときは、エンテイルメント記号に '$`\sqsubseteq`$' を使うこともあります。 「エンテイルメント記号に '$`\sqsubseteq`$'」 -- ん？ これいいかも！ 記号 '$`\sqsubseteq`$' のポピュラーな用法ってないよね。これをエンテイルメント記号にすれば、'$`\to`$' と '$`\vdash`$' のオーバーロード／コンフリクト問題は軽減しますね。$` \newcommand{…

…） ： 論理式または述語に対する“とある演算”を表す記号〈論理結合子記号〉 エンテイルメント〈entailment | 伴意〉記号（関係記号） ： 論理式または述語のあいだの関係を表す記号。 導出可能性〈derivability〉記号（関係記号） ： 演繹系（後述）において、文（後述）が導出可能であることを示す記号〈メタレベルの記号〉 演繹ステップ〈deduction step〉区切り記号（ステップ構文の一部） ： 演繹系の演繹ステップの仮説〈前提〉と結論を区切る記号 妥当性…

…iv`$' は、二項述語としての等号ではなくて、両辺が等しいことの証拠あるいは保証としての等号です。言い方を変えれば、'$`\equiv`$' は、両辺が等しい保証込みなのです。「『述語としての等号を含む命題がすべての $`x, y, x`$ に対して真』である保証がある」と「すべての $`x, y, x`$ に対して、『等号が真である保証』が対応している」は、内容的には同じですが、発想が違います。集合 $`\msf{U}`$ における「等号が真である保証」が何であるか気にな…

…ことが形式的に（一階述語論理で）証明できるので、$`w`$ を $`\{x, y\}`$ と書きます。順序ペア順序ペア〈ordered pair | 順序対 | 順序付きペア〉は、公理的集合論では後から定義します。もちろん、事前に直感的・素朴な意味での順序ペアを理解してないと、順序ペアの形式的定義を見ても意味不明でしょう。順序ペア $`(a, b)`$ は、「具体的にどう作るか？」はさして重要ではなくて、次の性質が成立することが重要です。 $`(a, b) = (a', b'…

…＋選択公理）は、一階述語論理をベースに構築されます。一階述語論理に理論固有の関係記号〈二項述語記号〉として '$`\in`$' を入れて、上記の公理達を表現する論理式を仮定した形式理論〈formal theory〉がZF集合論です。一階述語論理を定義する段階で、変数の集合だの論理式の集合だの、論理式にその自由変数の集合を対応させる関数だのと、さんざん集合・関数を使いまくっています。つまり、ZF集合論によって集合概念が導入されるわけではなくて、素朴集合論と一階述語論理の土台を十…

…立場により、真偽値や述語も型理論のなかで議論できるようになります（「「命題」の曖昧性から前層意味論へ」参照）。もう少し ◯◯◯s-as-Types の例を挙げましょう。 Objects-as-Types（対象が型だ） Families-as-Types（ファミリーが型だ） Presheaves-as-Types（前層が型だ） Copresheaves-as-Types（余前層が型だ） Functors-as-Types（関手が型だ） Objects は“圏の対象”のことです。…

…あります。 真偽値 述語 論理式 定理 （国語辞書的意味で）課題、使命、目標など この曖昧性については、「Propositions-As-Typesを曲解しないで理解するために // 「命題」を排除したい！」で書きました。曖昧多義語の使用は、コミュニケーションに支障をきたす問題はあるのですが、なんらかの共通性を持つから同じ言葉で一括りにしている、ということもあります。国語辞書的意味は除いて、「真偽値、述語、論理式、定理」という意味での「命題」の用法は、論理の前層意味論の枠組み…

…の名前、集合の名前 述語の名前 名前の種別 省略可能フィールド「リスト」、「タプル」、「ディクショナリ」、「構造体」、「配列」、「シーケンス」、「オブジェクト」、「テーブル・ロー」など、大差ない概念に言葉が矢鱈に溢れかえっていて、まったくウンザリしますが、ここでは「レコード」という言葉を使います。レコードを構成する成分はフィールドです。フィールドはフィール名とフィールド値のペアです。フィールドのあいだには順番があるとします。つまり、「3番名のフィールド」という言い方は意味があ…

…つまり、指標の名前は述語として使えるということです。述語とは、広義の真偽値を返す関数です。広義の真偽値とは、必ずしも $`\mrm{True}, \mrm{False}`$ に限定しなくてもよいが、$`\mrm{True}/\mrm{False}`$ の代わりに使えるナニカのことです。「Propositions-As-Typesを曲解しないで理解するために」で導入したベリティ型は広義の真偽値の一種です。「整域である」を意味する述語はラムダ式で次のように書けます。$`\quad…

…と所属関係記号だけを述語記号とする古典論理の形式的体系にこれらの公理を追加すれば、ZF集合論の形式的体系になります。分出公理図式と置換公理図式は、論理式をパラメータとする無限個の公理の集まりです。$`U`$ がグロタンディーク宇宙とするとき、$`U`$ はZF集合論のモデルになります。$`U`$ はZF集合論のなかの集合だし、二値ブール値集合 $`\mbf{B}`$ や関数集合 $`\mrm{Map}(\hyp, \hyp)`$ は既に在るので、$`U`$ に関するZF集合論…

…ティ型とその型宇宙 述語 ＝ ベリティ型ファミリー 同義語・曖昧多義語 「命題」を排除したい！「贅沢なグロタンディーク宇宙とPropositions-As-Types」より： "logic"はそのまま形容詞的にも使います。logical〈ロジカル〉を使って、「論理的な人」とか「論理的に考える」とかを連想されるとチョット困るからです。言葉の印象による誤解・曲解は非常に多いので、気を使ってます。 テクニカルタームとして使う言葉の選択には気を使います。テクニカルタームは定義により約…