…します。限量随伴性「述語論理とインデックス付き圏と限量随伴性」で述べたように、限量子の挙動を支配している原理は随伴性〈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）とも呼ばれます。ガロア接続を圏論なしで扱うことが出来ます…

昨日の記事「述語論理とインデックス付き圏と限量随伴性」で、述語論理のモデルの基本事項を述べたので、これを元にして、個別の話をチョビチョビしていくことにします。自然演繹の悪口を書いた記事「自然演繹はちっとも自然じゃない -- 圏論による再考」で述語論理は扱わなかったので、自然演繹における「∀導入規則」について詮索（むしろダメ出し）します。内容： 全称記号の導入と除去の規則 証明ボックスを使った図示 チャンとした∀導入の方法 シーケントによるリーズニング記述 全称限量随伴性と∀導…

…その拡張があります。述語論理の圏論的対応物はトポスだと思っている方が多いでしょう。確かにトポスがあれば（高階の）述語論理の入念な議論ができますが、トポスは複雑で難しいです。もう少し簡単な圏論的構造で（一階の）述語論理を展開できないでしょうか -- ここでは、インデックス付き圏（indexed category）による述語論理の定式化を紹介します。全称限量子は随伴性（adjunction）により導入されます。この随伴性を分析すると、無意味限量（vacuous quantific…

…（次のテーブルは二項述語テーブルですが、その定義は次節で。） effect (二項述語) 感染してる 感染してない 投与する 発病10% 発病0% 投与しない 発病80% 発病0% 感染していて薬を投与しなくても、2割の人は発病せず、何の問題もありません。もしウィルスに感染して発病すると、苦しい思いをするし、仕事を休むなど様々なダメージを受けます。その損害を金銭に換算して10万円としましょう。検査には300円、治療薬には1000円かかるとします。この状況で、我々の行動には次の…

…、全称束縛された一階述語論理の論理式を、モデル論的な妥当性判断に置き換えて扱おうということです。対象レベルの論理式 ∀x∈X.p(x) の真偽を、メタレベルの妥当性判断 x∈X |= p(x) の真偽によって与えます。このようにして真偽値を与えることは、全称の標準的な解釈です。ただし多くの場合、論理式p(x)のなかに含まれる定数や関数記号に意味を付けるために、Xは単なる集合ではなくて構造であることを要求します。さて、crow(x)とblack(x)を入れ替えた「x∈Birds…

…わけです。たとえ一階述語論理であっても特別な論理ではなく、基底となる論理でもありません。数多〈あまた〉ある論理のひとつに過ぎず、それ自体の固有性も価値もないのです。こういう発想で展開される古典モデル理論の再構築版が、インスティチューション独立モデル理論（Institution-independent Model Theory）です。「インスティチューション独立」は、個々のインスティチューション（論理系）に依存しないということであり、インスティチューション理論をベースにした一般…

…きたいです。条件式（述語、論理式）pによるガードを三角で描いて、菱形は次のように定義します。とはいっても、これは好みの問題です。if(p) then f else g （菱形）をプリミティブにしても、p then f （三角）をプリミティブにしても、たいした違いはありません。参考例外の扱いは、 シーケント計算と例外処理コード ↑の記事に絵はありませんが、前節の最初の方法で絵に描けます。ストレージへの書き込みは、 ストレージの線形代数： 泥臭いデータ操作の洗練された定式化 環境…

… j 証明: まず 述語を定義する: P[自然数] とは ※（その自然数は $1） i + $1 = j + $1 ならば i = j であること。 (A1): P[0] ※帰納法のベース: i + 0 = j + 0 ⇒ i = j 証明: 次を仮定する: (B0): i + 0 = j + 0 。 このとき、 (B1): i + 0 = i その根拠は 基本命題_2 。 (B2): j + 0 = j その根拠は 基本命題_2 。 従って 目的の命題、その根拠は B0,B…

…arは、集合論と一階述語論理を組み込みで持っています。何もない所から（from scratch）、集合論＋一階述語論理により意味のある定理を記述するのは労力がかかり過ぎて現実的ではありません。付属のライブラリMML（Mizar Mathematical Library）に頼らざるを得ないのです。MMLは、ソース行で約2百8十万行、ファイル数は1257です。コンパイルにより1ファイルが10種類（たぶん）の概念的構成素に分割されます。仮に、分割された構成素をモジュールと呼ぶなら。…

… リストxsの要素で述語pを満たすものがあればtrue, なければfalse =? 整数（Z）のイコール（スコープ依存） 次に、固定サイズの配列とか長さが有限のキューのように、格納限界があるコレクションを考えてみます。以下は3個までの要素を保存できるコレクションです。 Instance IntSize3Coll : Collects := { e := Z; ce := list Z; empty := nil; insert := fun x=> fun xs=> if l…

…ので、状態点に対する述語（状態空間上で定義された真偽値関数）をp、遷移を引き起こす関数（状態空間上の自己写像）をaとして、 if (p(x)) then a(x) のような条件付き実行を「制御」と呼んでいるのでしょう。実際、クリーネ代数の演算（順次結合、非決定性選択、非決定性繰り返し）に、if (p) then a というスタイルの「制御」（ガード付きの実行）を入れると、whileプログラムをシミュレートできます。 非決定性プログラミングだって絵を描いてみれば一目瞭然 クリー…

…対応（翻訳）を適用すれば、抽象的な構成や言明から、現実的な意味を汲み取ることができるでしょう。実は、ここに書かなかった“論理との対応”もあります。クエリー名が述語記号に対応し、引数なしコンストラクタ名は定数記号に対応します。関手Fは、個体項や論理式の意味論（＝モデル）です。論理もまた異なる文化圏なので、まったく違った言葉が使用されます。同じ内実に対して、言葉だけがどうしてこうも大量にあるのか!? と溜め息が出ますが、まー、言ってもしょうがない。 関連する愚痴： 感動か効率性か

…数では、状態空間上の述語（ブール値関数）を一緒に考えます。たくさんの状態空間、型付きのプログラム、並列走行するプログラム群などは、もともとスコープ外です。工夫をして、スコープ外の現象までモデル化する手段があるかも知れませんが、「無理してる」感が否めません。僕はそういった工夫は虚しい努力だと感じるのでやる気が起きません。上記の問題点（機能不足）を克服するには、クリーネ代数を超える枠組みが必要でしょう。トレース付きデカルト圏とデカルト半加法圏クリーネ代数を超える枠組みの基本となる…

…|Mod[Σ]|上の述語の形をしています。 順序集合を定義する順序集合の定義も、ミート半束の場合と同じです。次の手順に従います。 順序集合のマグマ版OrderMagmaを定義する。 記述の簡略化のためにノーテーション（Q、≦、T）を定義する。 順序集合が満たすべき法則を記述したクラスOrderを定義する。 以下のようになります。 Class OrderMagma := { order_carrier: Set; order_relation: order_carrier ->…

…合演算を導入すると、述語論理も集合計算でシミュレートできるようになります。つまり、依存積を持つ宇宙内では、述語論理（のモデル）を構成できるのですね。「命題」という言葉は人により場合により解釈が変わってしまい曖昧な言葉ですが、確か高校あたりでは「真偽が判定できるもの」と説明していたような気がします（最近の高校のことは知りませんけど）。となると、集合も非空か空かで真偽が判定できるので「命題」と呼んでもよいでしょう。CoqのPropは、命題とみなした集合の宇宙のことです。集合の場合…

…ばれるモノは、命題、述語、条件、真偽値、プロパティなどとも呼ばれます。そのようなモノを扱う計算が論理計算です。論理計算の舞台となる代数はブール代数やハイティング代数ですが、もう少し弱い構造として、論理半環（logical semiring）を定義します。「論理半環」は一般的な用語ではありませんのでご注意。論理半環の足し算（論理和）を∨、掛け算（論理積）を∧で表し、足し算と掛け算の単位元はそれぞれ0と1とします。論理半環はその名のとおり半環ですが、次の条件を加えます。 足し算が…

…論理で言えば、A上の述語（の意味）の全体です。埋め込み A→{0, 1}A の像は、離散的なディラック関数とでも呼べるものです。a∈A に対して： δa(x) = if (a = x) 1 else 0 a|→δaの対応を、同じ記号δを使って δA:A→{0, 1}A と記します。ところで、{0, 1}Aは、{0, 1}のA回の直積とみなせます。{0, 1}に離散位相を入れて、{0, 1}Aに直積位相（無限直積かもしれない）を入れれば、{0, 1}Aは位相空間です。そしてチコ…

…で、これは命題論理と述語論理を繋ぐものです。射影に対する随伴としての定式化もできます。また、存在限量子と全称限量子というペアが存在しますが、これも随伴の枠組で説明できます。となると、積分の周辺にもなにか随伴が潜んでいるのでしょうか？ 超フィルターモナドを生成する随伴は位相的に構成できますが、ジリィ・モナドに対応する随伴はどういうものでしょう？論理にはモデル論（「コンパクト空間と論理／モデル論」参照）、さらにはインスティチューション（抽象モデル論）がありますが、確率におけるイン…

…結果です。pを二項の述語（真偽値を値とする二引数の関数）だとして、ジョインJ（の集合）は次のように書けます。 J = {(s, t)∈S×T | p(s, t) } 二項の述語 p(s, t) として最もよく使われるのは、フィールド（カラム）値の等式です。「レコードsのフィールドfの値」を s.f と書くことにすると、s.f = t.g のような等式ですね。この場合のJは： J = {(s, t)∈S×T | s.f = t.g } この形のジョインは等値ジョインと呼ばれるこ…

…atural という述語で表現します。 /** テストサンプル */ command test-sample :: void -> Logical { [ [true, false, false, true], [4, 5, 6, 7] ] | zip-is-natural "to-string" "num:inc" }; この事例では、4つの対象A, B, C, Dには次のように型（集合）が代入されます。 A = boolean, B = integer, C = stri…

…作るときに必要になる述語（predicate）や関係（relation）も定義しています。 /** 集合の包含関係 */ function s_included(a1, a2) { return a1.every(function(item) {return (a2.indexOf(item) > -1);}); } /** 集合の共通部分 */ function s_intersection(a1, a2) { // 重複は除外されない return a1.filter(f…

…「複合データ構造への述語適用」の部分は説明なしだとちょっと分かりにくいかも。[追記]説明してない「複合データ構造への述語適用」のArrayCloseとObjectCloseが間違っていたので修正しました。まったくいらんことをしてましたね。 function ArrayClose(x, parr){ return ArrayOpen(x, isUndefined, parr); } function ObjectClose(x, pobj){ return ObjectOpen…

…推測できるでしょう。述語論理で出てくる限量子（量化子）は束縛子の例です。より具体的には、全称限量子∀と存在限量子（特称限量子）∃は束縛子です。これらの記号は、直後に変数を伴って、その後に続く論理式内の変数を束縛します。∀x.F、∃x.F のとき、論理式F内の変数xは束縛変数になります*1。自由変数を含む式に構文的に作用して、自由変数を何らかの意味で束縛する記号的作用素が束縛子ってことになります。もうひとつ典型的な束縛子はラムダ記号λです。λx.E によって、式E内の変数xを束…

…は辛い作業」を人間に代わって片付けてくれるのです。メタプログラミングにより、親切で勤勉な妖精さんを創りだすことができます。レイフィケーションとメタプログラミング、それにより創り出された妖精さん達は、ゲーデルの発想からの派生物のなかでもとても実利的なものだと思います。 *1:このときの説明は、概念的には少しSmalltalkっぽくて、記法はJavaに近いものを採用しました。 *2:isCode(n) という述語があって、この述語が真である領域上で定義された部分関数なら十分です。