比較的最近、述語論理の全称記号・存在記号について書きました。 論理の存在記号∃をちゃんと使えるようになろう 論理の全称記号∀も存在記号∃もちゃんと使えるようになろう 特定分野の予備知識を仮定しないことにすると、例題は自然数や整数の話になりがちですが、集合と写像をネタに例題を探してみました。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）とも呼ばれます。ガロア接続を圏論なしで扱うことが出来ます…

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

…その拡張があります。述語論理の圏論的対応物はトポスだと思っている方が多いでしょう。確かにトポスがあれば（高階の）述語論理の入念な議論ができますが、トポスは複雑で難しいです。もう少し簡単な圏論的構造で（一階の）述語論理を展開できないでしょうか -- ここでは、インデックス付き圏（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は、命題とみなした集合の宇宙のことです。集合の場合…