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

…準備 シャープネス 述語の外延化 準備基本的な参考文献は、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] …

…します。限量随伴性「述語論理とインデックス付き圏と限量随伴性」で述べたように、限量子の挙動を支配している原理は随伴性〈adjunction〉*1です。随伴性には色々な表現があります、ホントにウンザリするほど色々な書き方（描き方）があります。表現の多様性が目くらましとなって、単純な本質が見えにくいのです(ため息)。集合Xごとに、Xの上の“述語”と呼ばれるナニモノカを要素とする集合Pred[X]が対応しているとします。いま「述語」という言葉を使いましたが、代わりに「命題」とか「論…

…命題（ちゃんと書けば述語論理の論理式となる）です。一例を挙げると： {n∈N | nは2で割り切れる} Nは自然数（非負整数）の全体のなので、これは非負の偶数全体を表します。さて、f:X→Y の逆像と像を、集合の内包的記法で定義しましょう。 f-1(B) = {x | f(x)∈B} f(A) = {f(x) | x∈A} ちょっと雑ですが、xはX上の変数、yはY上の変数と決めれば、混乱はないでしょう。いま、A = f-1(B) と置いて、f(A) = f(f-1(B)) を…

…せんけどね。一階古典述語論理の上の公理系としてのZFC集合論のモデル（意味的世界）をVとします。Vって何なんだ？ にうまく答えることは僕にはできません(苦笑)。ともかく、したいことは何でもできる環境として、Vがあると思ってください。VをZFC宇宙と呼びます*2。ZFCの宇宙Vが一意的に存在するのかというと、そうでもないようです。ZFC集合論からは決定できない命題Pがあれば、Pが成立する宇宙とPの否定が成立する宇宙は別物です。しかしどちらもZFC集合論のモデルになれます。ここで…

…のにお手頃な集合論・述語論理について云々します。ピンクの宿題 その1 [奥野さんが言う集合論・述語論理とは、]あくまでリレーショナルモデル界隈を説明・分析する道具・枠組みのことであって、一般的集合論と一般的述語論理の話ではありません。（詳細は別途記述予定。） ピンクの宿題 その3 [奥野さんは、]述語論理のある特定の体系に対して、ある種の集合論（ZFCってことではない）の宇宙が健全な（ひょっとすると完全な）モデルになっている、ってことを言いたいのだと思います。（詳細は別途記述…

…4. 集合と集合論、述語と述語論理を混同して使っている 5. 二階論理の説明がおかしい 消極的提案： 第2章を削除する 積極的提案： 述語論理を活用した解説 奥野さんの発想の源泉（ただし想像） 「矛盾」て何なんだろう？ 演繹データベースと矛盾： 奥野さんは（まーまー）正しかった 演繹データベースで出来ること 述語論理をチャンと使おう 外部世界をチャンと考慮しよう おわりに ことの発端： zhanponさんの批判先日、次のQiita記事をみつけました。 『理論から学ぶデータベー…

…の枠組み、例えば一階述語論理において定理や証明を定義することはできるでしょうが、それこそが定理／証明だと言い切れるでしょうか。定理や証明について、もう一度考え直してもいいかも知れません -- Globularは、我々が常識だと思っているモノも再考する余地があることを教えてくれます。内容： 構築可能性判断 ワークスペースとリーズニング リーズニング記述言語とリーズニング・スクリプト 余談：n次元言語の未来 非公式自家製リーズニング記述言語 Theoremコマンド 等式的推論 テ…

「述語論理とインデックス付き圏と限量随伴性」、「全称記号の導入規則について考える」において、述語論理の背後に限量随伴性（quantification as adjunction）があって、形式的な推論の規則を支配していることを述べました。論理の真偽値がなす圏は、順序集合（むしろプレ順序集合）と考えていいことが多いので、そのときは順序構造の随伴性になります。順序構造の随伴性はガロア接続（Galois connection）とも呼ばれます。ガロア接続を圏論なしで扱うことが出来ます…