…ブール値を返す関数〈述語〉です。論理アンド（&&）や論理オア（||）も使えます。WinActiveに渡す引数は旧ディレクティブ構文を文字列にしたものです（2引数にすればいいのに、と思いますけど）。コマンドラインここからは、ホットキー設定のことは忘れて、スクリプトを書いてみます。 ; AHK-01.ahk #SingleInstance, Force InputBox, UserInput, Input Box, Please input your name. MsgBox, …

…数環／半環 ファジー述語代数 指示関数＝指示述語 ラムダ記法 カリー化、反カリー化 書字順記法と反書字順記法 ジリィ関手 記号のだいたいの約束 マルコフ核の定義 マルコフ核のラムダ記法表示 積分表示と被積分形式 ランダム要素 ランダム要素の事象への所属度 ディラック測度 チャップマン／コルモゴロフ結合 デルタ関手 暗黙のデルタ ペアリング記法 測度の前送り -- 写像の場合 関数の引き戻し -- 写像の場合 随伴公式 -- 写像の場合 測度の前送り -- マルコフ核の場合 関…

…を、等式的論理と一階述語論理に固定する。 指標Σに対するモデルの圏を、Model[Σ] := [FreeCat(Σ), Set]CAT と具体的に与える。 指標圏を固定する気はないのですが、当座の指標圏としては、有向グラフの圏を採用します。ただし、単に「有向グラフ」と言ってしまうと誤解をまねきそうです。通常の有向グラフGと、両端を共有するパスの対（スピヴァックの言葉だとパス同値関係〈path equivalence relation〉、「衝撃的なデータベース理論・関手的データ…

…理を等式的論理と一階述語論理に固定します。等式的論理／一階述語論理以外の論理を使いたいケースは少ないからです。 モデルの圏の作り方を固定する： 抽象的インスティチューションのモデルの圏は、公理的に存在が要請されているだけで、どう作るかは指定されてません。が、特殊化されたインスティチューションでは、指標Σのモデルの圏 Model[Σ] は、Model[Σ] := [FreeCat(Σ), Set]CAT と具体的に与えます。指標Σは有向グラフとみなし、FreeCat(Σ) はΣ…

…理における ∃ -| π* -| ∀ 述語論理とインデックス付き圏と限量随伴性 全称・存在限量子の色々をまとめた絵 集合達の直積と直和における Σ -| Δ -| Π カン拡張における上下左右： 入門の前に整理すべきこと // 随伴トリオとその例 加群層における f! -| f-1 -| f＊ 層に関してちょっと // グロタンディーク演算 *1:関係データベース用語のジョインがミートに相当し、ユニオンがジョインが相当します。順序構造のジョインをユニオンと呼ぶこともあります。

…集合のカン拡張と特徴述語論理」でそう呼んでます。） 優拡張のなかで最小のもの（最小優拡張）が、カン優拡張 劣拡張のなかで最大のもの（最大劣拡張）が、カン劣拡張 とかなら、まだしも覚えやすかったのだけど、実際は何の連想も働かない左と右、どうコジツケましょうか？随伴の左右と結びつける随伴の左右と結びつけることにします。随伴に関しては、左右の定義を覚えてます（僕は）。これもコジツケで覚えてるのですが、今日はそのコジツケの話はしないで、ともかくも「随伴の左右は知ってるよ」を前提します…

…産まされ［二（多）階述語論理］（上空移行）した『包摂言語』と生り・ならされたもので、［カオス］表示の（ｅ）（π）（ｉ）は幽霊的な［内在秩序］として姿が見えなくなっている。 【数そのモノ】は、［カオス］から［コスモス］・［コスモス］から［カオス］を行き来できる『包摂言語』と生り・ならされている。 このことにより［コスモス］表示内での［四則演算］は、［群］（可換群）としての［算術（算数）演算］を生得（スービタイズ）的に獲得し・獲得させられていると観る。 結局、無限（∞）の言語（数…

…然数』氏による）。「述語論理とインデックス付き圏と限量随伴性」へのコメント： ≪…トポスがあれば（高階の）述語論理の入念な議論…≫との事を、 ライプニッツの「理性に基づく自然と恩寵の原理」の『《モナド》』に『自然比矩形』を［同定］すると≪…トポス…≫に観えて、『《モナド》写像（関数）』が『次元の数』と生り［位相］の［数学概念］を［内在秩序］化し、［数学共同体の自然数］が『縮約（縮退）自然数』として『天賦』し・させていると観る。まったく意味不明ですが、スパムでもないので放置しま…

…準備 シャープネス 述語の外延化 準備基本的な参考文献は、Jacobs-Zanasi-2018です。 Title: The Logical Essentials of Bayesian Reasoning (3 Apr 2018 (v1), 27 Apr 2018 (v2)) Author: Bart Jacobs, Fabio Zanasi Pages: 29p URL: https://arxiv.org/abs/1804.01193 この論文の解説は「ベイズ確率論、ジェ…

…年9月から）では古典述語論理（普通の論理）を前回より詳しく説明・練習するつもりです。「圏論」は新しいコースです。事前には何も知らない人でもモナドまでたどり着けるのが目標です。このブログで何度か強調しているように、集合の圏のような巨大な圏ではなくて、手で触れる“可愛い圏”からスタートして、圏を身近に感じてもらえれば、と思っています。圏論の応用は多岐に渡るので、特定の話題に偏りすぎないように注意します。そういう方針なので、コンピュータやプログラムの話ばっかりってことではないです*…

…ないのなら、第2章「述語論理とリレーショナルモデル」は不要です。奥野さんは、 論理学に触れない正規化の解説は、でたらめだと言っても過言ではありません。 と思いっきり強調太字で書いてますが、過言です。実際に、第3章以降で、述語論理を実質的・本質的に使っている所はないです。 奥野本に限らず、「RDBは集合論をベースにしている」「RDBは論理を使っている」と言うだけで、実際には集合論も論理もロクに使っていない説明をみうけます。論理を使うのは、形式化のためです。何らかの形式体系〈fo…

…tion-ofが二項述語です。fとgは共端な射であることも表すには、図式を混ぜ込んだほうがいいでしょう。X is-solution-of (f, g) の意味は、Xから出る射eがあって、eが(f, g)の等値核であることですから：2行目の論理式に含まれる左上の'eq.'は、当該の図式が等値核図式であることを示します。等値核図式であること（is-equalizer-diagram）をちゃんと書けば次のようになります。（Xとバツ印が紛らわしいですからご注意。）論理記号の意味は： …

…成する 状態変換子と述語変換子 確率的状態 確率的状態変換子とチャンネル チャンネルについてもう少し 状態とチャンネルの実例 ファジー述語 ベイズ論理／ベイズ計算に向けて ベイズ確率論を整理して再構成するベイズ確率論〈Bayesian probability theory〉は幾つかの起源を持ち、たくさんの応用分野を持ちます。関連する諸分野が多い理論にありがちな事として； 各分野の概念・用語・記法がもとの理論にシッチャカメッチャカになだれ込んで、もとの理論がグチャグチャに見えて…

…算記号〈関数記号〉 述語記号〈関係記号〉 論理記号〈論理結合子記号と限量子記号〉 補助記号 説明は後にして、各種の記号を並べてしまいます。 定数記号： '0', '1' 変数記号： すぐ下で定義する 演算記号： '+', '*' 述語記号： '=', '≦' 論理記号： '∧', '￢', '∀' 補助記号： '(', ')', ',', '.' 変数記号は無限個あるので、書き並べるわけにいきません。変数記号は次のように決めます。 英字〈ラテン文字〉小文字1文字、またはその後…

…張と左カン拡張）を、述語論理の限量子と捉えてみます。内容： 圏と順序集合 基本的な言葉と記法 劣拡張と最大劣拡張 ミート完備な順序集合 最大劣拡張の構成 最小優拡張と書き方の約束 特徴述語論理 おわりに 圏と順序集合圏論に関する話を、順序集合に関する話にダウングレードすると、議論が容易になります。例えば、2つの関手が随伴対であることは、2つの単調写像がガロア接続を形成することと同じです。それについては： 順序随伴性： ガロア接続の圏論 モナドの順序的対応物に関しては： 順序集…

…// 論理記号など 述語論理とインデックス付き圏と限量随伴性 // 命題論理 述語論理とインデックス付き圏と限量随伴性 // 述語論理 僕の本音としては、含意に'⇒'を使いたくない。二本棒矢印は、別な目的で使いたいのです。一本棒矢印も含意以外で使いたいこと多いし。論理ではいろいろな矢印が出てくるので、矢印記号が不足して困るんですよ。次の記事参照。 論理におけるさまざまな「矢印」達 ところで、いま僕は「含意記号」といいましたが、「ならば」を意味する記号は条件記号〈conditi…

…論理的対象と考えての述語論理、第5章は状態空間と観測量を扱う論理です。こう書くと、オーソドックスなコースのように思えるかも知れませんが、いやいやっ、並の教科書とは違いまっせ、徹底的に圏論的〈カテゴリカル〉で公理的です。圏論的線形代数と圏論的論理のテキストなのです。次節以降でもう少し詳しく内容を紹介しますけどね。時間がない人は、最後の節に飛べ → 。以下この記事では、『圏論による量子計算と論理』を「ヒューネン本」とも呼びます。翻訳日本語本であることを強調したいときは「ヒューネン…

…な）人工言語は、古典述語論理とラムダ計算でしょう。しかし、これらの言語にどうも馴染めない、という人もいるし、ソフトウェアで構文をチェックしたり実行したりするすることが（お手軽には）できません。Coq、Isabelle、Mizarなんてプログラミング言語もありますが、これらも敷居が高いので、普通のプログラミング言語（汎用プログラミング言語）を使うことにします。そう、TypeScriptです。TypeScriptがサンプル記述に向いていることは次の記事で書いています（興味があれば…

…Pが、集合X×Y上の述語だとします。構文的には、Pは変数x, yを含む（可能性がある）とします。正確には、意味領域の述語（真偽値をとる関数） P:X×Y→{True, False} と、それを表現する構文領域の存在物である論理式は別物なんですが、ここではあまり区別しないで、同じ記号で表します。「命題」という言葉も、意味領域の述語だったり、構文領域の論理式だったり、文脈で指すものが変わります。さて、全称命題 ∀x∈X.P(x, y) や存在命題 ∃x∈X.P(x, y) を作る…

…] -- 集合X上の述語の集合。述語は、X→{True, False} という関数だと思っても、Xの部分集合だと思っても、どっちでもいいです。述語のあいだの順序関係をもとに、圏とみなします。 π2:X×Y→Y という第二射影 π2*:Pred[X]→Pred[X×Y] -- 第二射影π2から誘導される述語のあいだの写像。述語を関数だと思うなら、π2*(P) := Pπ2 。構文的には、変数水増し〈variable thinning〉オペレータです。 '-|' は随伴対を表す記…

…定した集合ではないような印象はあります。集合とは限らない類〈class〉に値をとる場合が族の雰囲気。このテの話を、印象・雰囲気で議論してもラチがあかないので、やめときます。 *4:厳密には、Map(A, X)のXは、忘却関手をUとして U(X) です。集合圏とベクトル空間の圏のあいだの随伴関手対があるのです。 *5:自然変換や圏論的オペレータです。 *6:directCoeffの定義を形式言語でしようとすると、述語論理の論理式以外にヒルベルトのイプシロン記号が必要になります。

比較的最近、述語論理の全称記号・存在記号について書きました。 論理の存在記号∃をちゃんと使えるようになろう 論理の全称記号∀も存在記号∃もちゃんと使えるようになろう 特定分野の予備知識を仮定しないことにすると、例題は自然数や整数の話になりがちですが、集合と写像をネタに例題を探してみました。f:X→Y は写像として、S⊆X, T⊆Y とします。 s∈S ⇒ f(s)∈T が成立しているとします。これは、 f*(S)⊆T と書けますね。ここで、f*(S)は、fによるSの像〈ima…

…です。正確に言えば、述語論理の論理式を表すメタ変数がPです。 xとaは変数（を表すメタ変数）ですが、xは束縛変数で、aは自由変数とします。実際に使う変数を'x', 'a'って決めてるわけじゃないですよ。メタ変数xが表す実際の変数がaのときもあります。 tは項（を表すメタ変数）です。定数、変数、関数（の記号）の組み合わせが項です。 ブラケット〈角括弧〉は置換を表します。4つのルールで、置換の仕方は微妙に違います。 ∀導入 ∀x.P[a:=x] ： 自由変数の束縛変数化 ： Pに…

…在する」の使い方は、述語論理の推論規則によって統制されているのですが、あまり分かりやすいものではありません。次の2つの記事で詳しく分析しています。が、ちょっと詳し過ぎたかも知れません。 全称記号の導入規則について考える 存在記号の除去規則について考える 命題の記述や証明がうまく出来ないと「論理的に考えていないから」と思いがちですが、そうとも限りません。単に技術的な問題、つまりノウハウが不足しているだけかもしれません。特に、∀と∃の取り扱いはノウハウが必要です。この記事は、ノウ…

…プシロン項は、Pを（述語論理の）論理式として、εx.P の形です。ヒルベルトのイプシロン計算では、論理式Pに何の制限もありません。Pが変数xを含んでいなくてもかまいません。x以外の変数がPに出現しても、もちろんOKです。いくつか例を挙げると： εx.(x = y) εx.(x = x) εx.(a ≦ y ∧ y ≦ b) εa.(a ≦ y ∧ y ≦ b) εy.(a ≦ y ∧ y ≦ b) 論理式Pに対して、Pに出現する変数xを項Eで置き換えたものを P[x := E…

…の随伴 随伴系の例：述語の引き戻し、全称限量子、存在限量子 随伴トリオとその例 “圏の圏”と関手圏 横結合積と前結合関手／後結合関手 前結合／後結合関手の随伴としてのカン拡張／持ち上げ関手 ラムダ計算と類似の記法・図法 最良な拡張、最良な持ち上げとしてのカン拡張／カン持ち上げ カン持ち上げはつまらない？ おわりに [追記 date="2018-03-10"]C, D, Eを書き間違えていた箇所があったので修正しました。[/追記] 関連する記事： カン拡張（Kan extens…

…の名前”は、構文上は述語記号になります。後から導入された述語記号は、その定義本体（':≡'の右辺）で置き換えれば消去できます。これは簡単ですね。さて、∃y.Unit(y) から単位元の存在は保証されているので、それに名前を付けたい気分になります。単位元の名前は初めからは用意してなかったので、後から導入することになります。とりあえずはインフォーマルに： u := (Unit(y)であるようなy) と書いておきましょう。名前'u'は、集合A内の特定の要素を名指す固有名詞です。つま…

…と、それは集合S上の述語の集合になります。Set(S, bool)は外部ホム（集合圏の外から見たホム）ですが、集合圏では内部ホムを作れます。内部ホムは、[S, bool]とかboolSとか書きます。次元を上げて、任意の圏Cに対して、1-ホム圏Cat(Cop, set)をとると、それは圏C上の前層の圏になります。Catでも内部ホムを作れて、[Cop, set]（あるいはsetCop）が内部的な前層の圏です。述語と前層はなんか似ていて、前層（あるいは層）の理論が述語論理の圏化のよ…

…してはブール値をとる述語関数 eq:X×X→Bool, eq(x, y) = if (x = y) True else False と考えます。ここで、Bool = {True, False} です。ブール集合（真偽値の全体）Boolは、最初から我々がいる世界Setのなかにあり、最初から見えています。屋根裏部屋に隠れているわけではありません。このギャップがとても気になります。僕が考えた（夢想した）詩的解釈は、僕らが見ているあのBoolはアバター〈化身〉であり、実身は集合圏Se…

…のは、'∈'は命題（述語論理の論理式）のなかで述語記号（関係記号）として使われるものだからです。もちろん'∈'は本来の意味 -- 要素と集合のあいだの所属関係として使います。'∈'が出てくるってことは、常識的な集合概念は仮定するってことです。公理的集合論ではなくて、素朴集合論です。素朴集合論って何だ？ ってことは、次の記事で扱っています。 現場の集合論としての有界素朴集合論 有限性の定義自然数nに対して、 [n] = {k∈N | k < n} と定義します。特に、 [0] …