…ます。対話論理は、（古典論理や直観主義論理のような）論理というよりは、命題の真偽判定法の流儀です。現在主流でメジャーな判定法は、演繹的導出（手順的）とモデル論的妥当性（超越的）ですが、対話論理は、対話ゲームによる判定という第三のアプローチを提供します。対話ゲームは、議論の過程をある程度はシミュレートしてくれるので、演繹やモデル論的モデルよりは“人と人とのやり取り”の分析に使えます。とはいえ、“やり取り”のルールが固定していて限定的なので、議論過程の十分なモデリングとは言えませ…

…[\hyp]`$ は古典述語論理の素直な定式化ですが、$`\mbf{Bun}[\hyp]`$ は、論理というより依存型理論の集合論的モデルになっています。しかし、抽象的観点からは、どちらもデカルト閉ハイパードクトリンです。ファイバー付き圏とファイバー$`\cat{D}:\cat{C}^\op \to \mbf{CCCAT} \In \mbb{2CAT}`$ がデカルト閉ハイパードクトリンのとき、インデックス付き圏 $`\cat{D}`$ にグロタンディーク構成を施すと、ファイ…

…主義高階論理ですが、古典一階述語論理だと考えてもさほど不都合はありません。「依存型〈dependent type〉」という用語の曖昧性からの混乱を軽減するために、「依存性型〈type with dependency〉」という言葉を使います。依存性型はファミリーのことです（集合論ベースなので）。「依存型」は、シグマ型またはパイ型を表すことがあります。曖昧語「依存型」を使うと、次の文は正しい事実を述べた文です。 依存型から依存型を作ると依存型だが、作った依存型は単純型のこともある…

…こでのオートマトンは古典的・伝統的な意味で、状態空間に始状態〈開始状態〉と終状態〈終了状態〉があるラベル付き遷移系です。遷移写像は半決定性写像〈部分写像〉です。ソフトウェアシステムのモデル化のために、アルファベットには色々と細工と工夫をします。アルファベットに細工と工夫を施したオートマトンがホーアオートマトン〈Hoare automaton〉です（正確な定義はいずれ）。ホーアオートマトンのアルファベットと振る舞いの記述・制約には、やはり指標を用います。この目的で使われる指標は…

前回、古典解析力学とオートマトン理論のアナロジーを話題にしました。軌道集合意味論は、このアナロジーに依拠しています。が、力学系とオートマトンでは、だいぶ違った側面もあります。今回は、物理起源の力学系と、プログラムの意味論としてのオートマトンで食い違っているところに焦点を当てます。記事内で使う文字の色については「文字の色の約束（再確認）」を参照してください。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mbf}[1]{\ma…

…トンの記号バンドル 古典解析力学とオートマトン マーク・ウィリアム・ホプキンス シリーズ・ハブ記事 ホーア論理とホーアオートマトン 1/n オートマトンのアルファベットと指標のアルファベットホーアオートマトンの定義はまだしてませんが、「ホーア論理とホーアオートマトン 2/n // 単純ホーアオートマトン」で定義した単純ホーアオートマトンは、ホーアオートマトンのなかで特に簡単な部類のものです。現時点では、ホーアオートマトンとは単純ホーアオートマトンだと思ってかまいません。もっと…

…みで使いやすい論理は古典論理〈classical logic〉です。しかし、ホーア論理／ホーアオートマトンの文脈では、古典論理が使えるとは限りません。次のような論理が登場します。 決定性二値論理〈deterministic two-valued logic〉（古典論理） 半決定性三値論理〈semi-deterministic three-valued logic〉 半決定性二値論理〈semi-deterministic two-valued logic〉 非決定性四値論理〈n…

…gebra〉として、古典論理〈classical logic〉にボトム（$`\bot`$）を追加したボトム付き古典論理〈bottomed classical logic〉を採用します。プログラム代数〈program algebra〉としては単なるモノイドを扱います。つまり、プログラムの順次実行だけをモデル化します。後々、もう少し複雑な論理代数／プログラム代数を扱うかも知れません。例えば、テスト付きクリーネ代数〈Kleene algebra with test | KAT〉とか…

古典論理では、命題「Pでない ならば Qでない」の対偶である「Q ならば P」は、もとの命題と同値であり意味は変わらないとされます。しかし、対偶命題がもとの命題と同値なことは日常直感と合わない、とも言われます。そのとき出される実例のひとつに「言わないとやらない」があります。「言わないとやらない（言わない ならば やらない）」の対偶をとると「やると言う（やる ならば 言う）」ですが、意味が変わっているだろう、というわけです。ほんとに意味が変わってますかね？ なんか奇妙ですか？ …

…指摘していることは、古典的、つうか要するに普通の（IT関係者ならみんな知っている）関係データベース〈relational database〉の世界にも文脈性が在るということです。データベースは、データベース全体として何かしら現実世界を写し取っているはずです。話を簡単にするために、データベース全体に3つのカラム A, B, C があるとします。カラム A, B でテーブル AB、カラム B, C でテーブル BC、カラム C, A でテーブル CA を構成しているとします。これ…

…。 BOOL型 ： 古典二値真偽値の集合です。真は、$`\mrm{true}`$ でも $`1`$ でもどっちでもいいとします。偽は $`\mrm{false} = 0`$ 。 （[追記]ガーンッ、迂闊でした！ NATURAL はたいていは予約語です。自然数ではなくて、自然ジョインを指定するときに、NATURAL というキーワードを使うのです。この記事の NATURAL はデータ型なので、ジョインとの混同は起きないでしょうから、修正しないでそのままとします。[/追記]）$`\…

…イヤース本との違い 古典的状態遷移系 バンドルとバンドル射 バンドル射のベース・ファイバー表示 バンドルのあいだのレンズ射 レンズ射の結合 レンズ射は状態遷移系である 単純レンズ射 バックエンドとラッパー 状態遷移系のあいだの準同型射 準同型射の整合性条件 二重圏との関係 おわりに 続きの記事： 状態遷移系はホームベース形に描くと良い マイヤースのシステム理論への違和感と代替案 IOCシステムと制御ラッパーの構造 単純レンズをグロタンディーク・レンズに埋め込む マイヤース本と…

…ール代数構造を備えた古典二値ブール代数とみなします。$`\mrm{Map}(X, \{0, 1\})`$ のブール代数構造は、ベキ集合 $`\mrm{Pow}(X)`$ のブール代数構造と同じです。論理的代数構造（典型例はブール代数）達の圏である $`\cat{L}`$ の選び方は色々ありますが、ここでは小さいデカルト圏*3（デカルト・モノイド圏）達の1-圏だとします（2-圏だと話が面倒になるので）。$`\cat{L}`$ が1-圏であっても、その対象が圏であることには注意し…

…二重圏としての、単純古典テンソル計算 集合のあいだのスパン達の二重圏 単射達と関係達の二重圏 関手達とプロ関手達の二重圏 バエズ／ドーラン曲面（「バエズ／ドーラン曲面の意義と使い方」参照）達のドクトリン（「補足と続き： ベックの分配法則に基づく“一般化圏の製造工場” // ドクトリン」参照）も二重圏、あるいは三重圏を形成しそうですが、事例に使えるほどにハッキリと分かっているわけじゃないです。もしハッキリ分かれば、これもカリー／カン計算の事例になり得る可能性があります。他にも（…

…ット 米田テンソル 古典テンソル計算と米田テンソル計算 なぜにまた米田テンソル計算 オプティックの圏のホムセット最近、エンド／コエンドに関して再論（蒸し返し）をしました。 圏論のエンドとコエンドは双対なんだよ 等式の二種類の使用法： 選別条件と同一視宣言 コエンドの応用として思いつくのは、オプティックの圏の定義です。オプティック（特に具象オプティック）については以下の過去記事で述べています。 圏論的レンズ 2： 具象オプティック 上記過去記事ではコエンドを明示的には使っていま…

…数型 ブール値とは、古典論理の二値真偽値のことで、$`\True`$ または $`\False`$ のことです。Sets-as-Types〈集合が型だ〉の立場なら、ブール型とはブール値の集合のことです。$`\quad \mbf{B} := \{\True, \False\}`$ （二元集合）同様に、自然数型とは自然数の集合のことです。$`\quad \mbf{N} := \{0, 1, 2, \cdots\}`$ （無限集合）ブール値の $`\True, \False`$ は…

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

…〉とは、とりあえずは古典二値真偽値（つまり、$`\mathrm{True}, \mathrm{False}`$）と理解しましょう。述語〈predicate〉は、なんらかの集合 $`X`$ 上で定義された、真偽値を値とする関数です。構文論と意味論の両方で使われる曖昧多義語（今は「命題」）があるとき、曖昧性を解消するために、構文論の用語には語尾に「項」、意味論の用語には語尾に「実体」を付けるとする（「カリー／ハワード／ランベック対応とハイティング／ド・モルガン圏」参照）なら、次の…

…ext{二番}`$ 古典論理の含意の定義から$`\quad (\text{一番} \land \text{三番}) \Imp \lnot \text{二番}`$ 中身を展開して書き下すと：$`\quad (x, y\in P \land g\la x = y) \Imp x = y`$$`g, x, y`$ は任意だった（特に条件が付いてなかった）ので、$`\quad \forall g\in G.\forall x, y\in X.\left( (x, y\in P \la…

…ド・モルガンの法則と古典論理の法則 モノイド・ハイティング圏 おわりに ネーミング僕がネーミングに気をつけるようになったのは、名前の語感や連想から判断してしまう人が一定数いることを知ったからです。もちろん、分かりやすい名前がいいのですが、誤認・誤解を招きそうな名前はむしろ意味不明な名前に変えてしまったほうが安全だと思っています。意味不明な名前の素材によく使うのは人名です。ハイティング〈Arend Heyting〉にちなんで名付けたハイティング圏〈Heyting categor…

…語」かを区別する。 古典二値真偽値の集合 $`\mbf{B}`$ と、ポインティング関数の集合 $`\mrm{Map}(\mbf{1}, \mbf{B})`$ は適宜同一視する。 「真偽値」の曖昧性真偽値を古典二値真偽値に限定しておけば、前節の約束により、曖昧多義語「命題」も適切に運用できます。しかし、真偽値がいつでも古典二値真偽値とは限りません。真偽値の概念も一般化・抽象化されるのです。「一般化された真偽値」とか「抽象化された真偽値」とか言ってみても、一般化・抽象化の方法が…

…まいません。論理も、古典論理が圧倒的多数派なので、「論理 ＝ 古典論理」で問題ありません。しかし、型理論は何百もあり、圧倒的多数派は存在せず、現状は群雄割拠の時代です。「型とはなんぞや？」に対しても、それぞれの型理論がそれぞれの答を準備しています。「集合論・圏論 vs. 型理論」から再掲すると： Sets-as-Types Algebras-as-Types Coalgebras-as-Types Propositions-as-Types Categories-as-Typ…

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

…で書いてみましょう。古典論理の論理式： $`\text{expression in }\format{classical-logic}\\ \quad \forall x, y\in A.\, m(x, y) = m(y, x)\\ \text{end} `$圏論的等式（等式を2-射と解釈）： $`\text{expression in }\format{categorical-equation}\\ \quad \mrm{comm} :: m \Rightarrow \si…

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

…言っているだけです。古典論理では、「存在するならば 云々」は「存在しないか または 云々」なので、存在しないときは「云々」がなんであっても問答無用に真です。上記の論理式を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と呼んでもいいが）は格子点です。（[追記]以下の「内部の点かどうか」の議論は、位相が絡んでいるので…