… `$内容： 命題 古典論理 判断 判断記号 信頼 型宣言 前提 おわりに 命題ここでは、「命題」という言葉をテクニカルタームではなくて、国語辞書的意味で使います。よくある「命題」の国語辞書的定義は： 命題とは、真偽が判定できる文である。 この定義は僕もよく引用するのですが、述語論理の話ではマズイことになります。どえらく誤解されるリスクがあります。述語論理とは、“不定の主語”を扱う論理です。“不定の主語”を扱わない論理は命題論理です。僕は、命題論理と述語論理という分類に意味が…

…言っているだけです。古典論理では、「存在するならば 云々」は「存在しないか または 云々」なので、存在しないときは「云々」がなんであっても問答無用に真です。上記の論理式を2つのケースに分けて解釈しましょう。 $`(a, b)\in R\land (a, b') \in R`$ である $`a`$ が存在しないとき： 論理式は真だから、それ以上考える必要はない。 $`(a, b)\in R\land (a, b') \in R`$ である $`a`$ が存在するとき： $`b …

…ash m:B `$古典論理のシーケント〈LKシーケント〉の場合、矢印の左側と右側では解釈が異なります。このことを明示するために、命題のリストの左肩にマーカーを付けてみましょう。$`\quad p: {^\land (A_1, \cdots, A_n)} \to {^\lor (B_1, \cdots, B_m) }`$あるいは、区切り記号を変えて：$`\quad p: (A_1, \cdots, A_n) \to (B_1\mid \cdots\mid B_m)`$しかし、…

…だけだけど）。法則は古典論理の論理式で書いています。 // 単なるひとつの集合の指標 signature SingleSet { sort U } // 付点集合の指標 signature PointedSet { sort U operation e : 1 → U in Set } // モノイドの指標 signature Monoid { sort U operation m : U×U → U operation e : 1 → U laws: ∀x, y, z∈U.…

…移性： 等式的推論は古典論理で統制されていて、ありとあらゆる分野で使われます。ただし、等号以外の関係記号／演算記号などの解釈は分野ごとに変わるでしょう。例えば、次の推論規則に出てくるセミコロンは“射の図式順結合記号”だとすれば、圏論における等式的推論になります。圏論における等式的推論も当然に古典論理の統制下にあります。古典論理の統制から逃れることは不可能です。が、しかし、圏論内で使われる等式的推論を、できる限り（古典論理ではなく）圏論内で定式化することには意味があります。自律…

…e ⇒ xi∈Z) 古典論理における含意〈ならば〉の扱いは、前件（⇒の左側）が偽ならば真になるので、 ∀i.(True) となり、定義の右辺は真です。 x∈R0 が格子点 :⇔ True R0に含まれる点はいかなる点も（実際は一個しかないが）格子点です。格子点の定義をε-格子点にしたところで、やはりいかなる点もε-格子点です。J0 = R0 であり、唯一の点が＊だったので、＊（0と呼んでもいいが）は格子点です。（[追記]以下の「内部の点かどうか」の議論は、位相が絡んでいるので…

…論理で、構成の手法は古典述語論理に似ています。PS論理は、それとはちょっと別な原理と手法で構成されます。'PS'は確率空間〈probability space〉のことです。PS論理の意味論〈モデル〉は確率空間の圏で与えられると考えます。つまり、propositions as probability spaces というモットーです。PSを、確率空間を対象として確率保存マルコフ核を射とする圏とします。構文とモデルを区別せずに、PSの対象（つまり確率空間）をPS論理の“命題”と呼…

…について説明します。古典的真偽値の集合を B = {0, 1} とします。0は偽で、1は真を表します。0 ＜ 1 という順序を入れておきます。Pred(X) := Map(X, B) と定義します。Pred(X) は集合X上の述語〈命題関数〉の集合です。Pred(X) に所属する述語達を考えるとき、Xを論域〈domain of discourse | 議論の領域〉と呼びます。述語の“主語”となのるのは、論域の要素です。Pred(X) は順序集合になります。順序集合は自然に圏と…

…いので、通常の論理（古典論理）に比べれば単純で小さい論理です。単純型付きラムダ計算は、静的で強い型システムを持つ関数型プログラミング言語だと思えばいいです -- と言っても分かりにくいですね。現存する実用的関数型プログラミング言語の原型となっている計算系ですが、メチャクチャに単純・小規模なものです。型の構成法として、直積型〈ペア型〉と関数型〈指数型 | アロー型〉が使えます。この2つの理論体系は同一の構造を持ち、双方向の同型対応があります。連言含意論理と単純型付きラムダ計算が…

…」と言える推論でも、古典論理からみて間違っていることはあります。むしろ、古典論理では間違っているとされる（許容できない）推論が興味の対象です。タイトルは「日常論理“と”数理論理」ではなく、「日常論理“の”数理論理」です。つまり、数理論理として日常論理を扱いたいわけです。ただし、数理論理の常套手段が通用しないところもあるので、そこは変更します。それでも、態度・スピリットは数理論理のそれを踏襲します。日常論理を扱うからといって、人間の認知や行動を分析しようなんて気はサラサラありま…

…な等式で書くより、（古典論理の）論理式を使ったほうが楽です。論理式を使うときは、キーワード condition を先頭に置くことにします。 signature Monoid in Set { type U function m:U×U -> U function e:1 -> U condition lunit_cond : ∀x∈U.( m(e(1), x) = x ) condition runit_cond : ∀x∈U.( m(x, e(1)) = x ) condi…

…ここでは、常識的な（古典論理の）論理式を使うことにします。論理式の文法は知られていますが、「lengthらしさ」を記述するための基本語彙〈ボキャブラリー〉が必要です。基本語彙の定義には指標〈signature〉と呼ばれる形式が使われます。以下が、「lengthらしさ」を記述するための基本語彙を定義する指標です*1。 signature ListAndLength{ type X in Set function nilX : 1 -> List(X) in Set functi…

…ェンのオリジナルの（古典論理）シーケント計算は難しすぎるので、単純化して二項論理演算はひとつだけにします。そのように単純化した論理を総称してコンパクト論理と呼びます（ジラーは「コンパクト論理」と呼んでたと思うけど、一般的な言葉ではないです）。コンパクト論理の意味論は、唯一の二項論理演算を圏のモノイド積と解釈して遂行できるのではないか？ と期待できます。コンパクト論理のシーケント計算 -- コンパクトシーケント計算であっても、意味論構成には多圏が必要そうです。やっぱり難しい！ …

…足] 論理で出てくる古典論理のシーケントでは、矢印の左側のカンマと右側のカンマの解釈が違います。簡約多圏のシーケントでは、左右のカンマの扱いに違いはありません。簡約多圏のシーケントはより単純なシーケントなので、コンパクトシーケント〈compact sequent〉と呼ぶのが正確です。が、コンパクトシーケントしか出てこないので、単にシーケントで済ませます。 [/補足]多射fのシーケント〈プロファイル〉 (A1, ..., Am)→(B1, ..., Bn) は、混乱の恐れがなけ…

…ate〉と呼びます。古典論理で使っている述語はこのタイプの述語です。決定性述語の全体を Φ{0, 1}X と書きます。下付きの [0, 1] と {0, 1} は判読しにくいのでご注意（別な記法にしろってハナシはある）。 指示関数＝指示述語 A∈ΣX に対して、χA:X→R を指示関数〈indicator function | characteristic function | 特性関数〉とします（文字'χ'はギリシャ文字カイ）。確率論では、別な意味の特性関数があるので、「指…

…参照してください。 古典的微分幾何・ベクトル解析のモダン化： 局所座標って何だ？ 「接バンドルのホロノーム座標」のときと同様に、チャート〈局所座標〉は、x:M⊇U→Rm という部分写像だとみなします。部分写像の定義域は常に開集合だとします。部分写像の扱い方については、「快適な微分計算のための圏と微分公式 // 部分逆写像」も参考になるかも知れません。概ユークリッド空間と部分写像の圏多様体とみなしたRnをユークリッド空間と呼びます。多様体Xが、多様体としてユークリッド空間と同型…

…です。期待多様体は、古典的な情報幾何の対象物、あるいは「各点が確率分布である多様体」のことです。期待多様体のリーマン計量は、フィッシャー情報計量〈Fisher information metric〉になります。情報幾何の起源とも言える計量です。共役接続ペア（の族）を作る場合も期待値を使います。期待値が関与するということは、パラメトリック統計モデルの文脈のなかで期待多様体が登場することです。純粋な幾何的文脈では期待多様体を定義できません。僕が、「多様体と確率・統計： 情報幾何の…

…性の」「二値的な」「古典的な」などに置き換えられます。そして、決定性／二値的／古典的であるシャープな世界Finは、そのままファジーな世界Chanに埋め込むことができるのです。この事実は、シャープな世界からファジーな世界への引っ越しの不安を緩和するものでしょう。述語の外延化pがA上のシャープな述語のとき、S = {x∈A | p} という集合が、述語pの外延〈extension〉として決まります。外延とは、述語pが表す性質を持つモノの全体の広がりのことです。集合Sからみたとき、…

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

… と解釈して、通常の古典論理の論理式に翻訳するなら： ∀x∈S.( P(x) ⇒ Q(C(x)) ) 今の説明は、あくまで従来型のプログラミングでのこと。ディープラーニングでの状況となると、プログラムコードCというのがハッキリしません。状態空間Sの確定も簡単ではないでしょう。古典論理やその変種をそのまま使うわけにもいきません。真偽がTrue, Falseの二値で決まるような世界ではないですから*6。先に「ホーア論理に始まりホーア論理に終わる」と言いましたが、「ホーア論理がすべ…

…条件記述の論理式は、古典一階述語論理をそのまま使えばいいでしょう。古典一階述語論理は、極めて安定した基盤です。素直に古典一階述語論理を使えば問題はありません。ただし、古典一階述語論理は計算の効率は芳しくないので、その点の考慮や工夫は別途必要です。関係とはデータベースにおいて主題的に考えるべき論理式は、“関係の性質”や“関係のあいだの関係”を記述する制約記述の論理式です。制約記述の論理式に関しては色々と問題がありますが、最大の問題は、制約記述の論理式に意識が向けられてないことで…

…デル論 2006年 古典論理は可換環論なんだよ 補足記事： “古典論理＝可換環論”の計算と種明かし 補足記事： イデアルと論理 番外の補足：ベキ等元と連結性 2013年 超フィルター（ultrafilter）って何なんだ： 点？ 確率測度？ 前層と余前層位相空間X上のC値前層とは、Open(X)op→C の形の関手です。Open(X)上で定義された反変の関手になります。共変の関手 Open(X)→C のほうは、（C値の）余前層〈copresheaf〉とか前余層〈precosh…

…は、一番ポピュラーな古典論理を使うことにします。基本記号を全部挙げる目的と論理が決まったら、使う記号をすべて列挙します。このとき、記号を分類するガイドラインが役に立ちます。 定数記号 変数記号 演算記号〈関数記号〉 述語記号〈関係記号〉 論理記号〈論理結合子記号と限量子記号〉 補助記号 説明は後にして、各種の記号を並べてしまいます。 定数記号： '0', '1' 変数記号： すぐ下で定義する 演算記号： '+', '*' 述語記号： '=', '≦' 論理記号： '∧', '…

…は、計算の論理*1は古典論理（または直観主義論理）で十分でしたが、量子現象／量子計算に関わる論理は古典論理とはどうも異なるようです。量子を扱うための非古典論理が必要なんでしょう。クリス・ヒューネン〈Chris Heunen〉のこの本は、量子計算論とそれに関わる論理を基礎的〈foundational〉な立場から解説しています。具体的な量子アルゴリズムや応用事例は少数しか載ってません。紙幅のほとんどを基礎に費やしているからです。基礎的であることは易しいことを意味しません。実際、こ…

…のままです。[/追記] *1:間違いを具体的に指摘するのが目的ではないので、URL参照はしません。 *2:画像： https://ja.wikipedia.org/wiki/手押しポンプ#/media/File:WellPump.JPG 神戸市市東灘区石屋川の公園にある井戸ポンプ *3:形式言語理論／数理言語学も言語学の一部門と考えるなら、今は数理的なアプローチしか考えない、ということ。 *4:厳密には、論理式を古典論理のシーケントの形に書いたときに、移項の原理が機能します。

…きないけど）。論理（古典論理*1）では、「Aである」と「Aでなくはない」は完全に同じです。日常言語の微妙さ・煩雑さを切り捨て、理想化・単純化することにより、強靭な推論能力が手に入るのです。日常言語を使っているかぎり、日常の論理、あるいは日常の非論理が混ざり込むことは避けられません。論理的推論のための人工言語を使うのが望ましいでしょう。そこで、プログラミング言語TypeScriptを（かなり無理クリに）使って、論理的命題の記述を試みてみます。本文中の例題を実行してみたい方は、最…

…モダン化ここ最近、「古典的微分幾何・ベクトル解析のモダン化」というシリーズ記事を書いています。この一環として、古式テンソル計算のモダン化をやりたいな、と思っています。古式テンソル計算ってなに？ -- 古いスタイルの（古典的、古式）微分幾何・ベクトル解析には、通常の（オーソドックスな）線形代数とはだいぶ違った線形計算体系が付属しています。これを、古式テンソル計算〈old-style tensor calculation〉と呼ぶことにします。上下の添字をあやつって計算する職人ワザ…

先日の記事「古典的微分幾何・ベクトル解析のモダン化： ダイレクトインデックス記法」で、上付き・下付き添字の説明をしたのですが、説明の対象である上付き・下付き添字以外に、上付き・下付き添字の記法を大量に使っている事実に気が付きました。随分とひどいオーバーロード〈多義的使用〉だわ。「過度のオーバーロードはやめよう」と主張している僕としては、ちょっと愕然としました。僕自身が上付き・下付き添字をどんな目的で使っているかを解説することにより、反省の材料にしたいと思います。また、「古典的…

…ダ記法に関しては、「古典的微分幾何・ベクトル解析のモダン化： ラムダ記法の利用 // 入力型と出力型を持つ型付きラムダ記法」をみてください。 (A・) := λx∈Mat(1, n).(A・x : Mat(1, m)) (・A) := λy∈Mat(m, 1).(y・A : Mat(n, 1)) (A・):Mat(1, n)→Mat(1, m) と (・A):Mat(m, 1)→Mat(n, 1) を組み合わせると、 ((A・), (・A)):(Mat(1, n), Mat(…

…たことがあります。 古典論理は可換環論なんだよ （2006年） 一方で、我々が常識的に想定する「空間」は距離空間なので、距離から導かれた位相はやはり重要です。距離から導かれる位相の特徴付けは熱心に研究された課題で、幾つかの距離化定理〈metrization theorems〉があります。距離は、色々な位相空間の例を提供してくれますが、距離では定義できない位相空間もあります。距離と無関係な位相空間にも目を向けましょう、というお話でした。 *1:これはこれで、全開〈フルオープン〉…