「モデルが在る」ことは、フィクションあるいはファンタジーだと言えるだろう。誰も存在を保証できない。実際にモデルを作るには、構文領域をいじくる以外に方法がない。つまり、「構文に先立ってモデルの世界が在る」ということは全然言えなくて、「構文領…

忘れてしまう件、メモに動機や例を書いておかないのがいけないのだと思った。そのときは、具体的な事例で考えているので自明に見えることでも、その例がなくなるとサッパリわからなくなる。リストとスタックの関係で具体例。Lispのリストのようなものを考え…

辞書的に使っている『情報科学における論理』を調べてみたら、「極大無矛盾」の定義に関して、僕が誤解していたようだ。（誤解していたのではなくて、用語法が2種類以上あるのかもしれない。）まず、矛盾（無矛盾）の用法を並べる： 公理系Aが矛盾する：A|- …

帰納性の公理化はないのかな？ あってもよさそうだが。自然数に対してしか帰納関数を定義できないのは不便だ。

圏Cに直積・直和などがあって、+, ×, 1, 0などに意味があるとする。この状況を抽象化すれば、ringoidal（または semiringoidal）圏とかも定義できるだろう。ま、それはいいとして、C上の多項式関手の概念があるとき、F(X) = 1 + X + X^2 + ... という級数で…

証明系を抽象化する目的は、証明系をインスティチューションに組み込みたいから。Moore閉包を使う定式化もいいのだけど、集合に対する関係|-を基本とすることにする。A|-Bのインフォーマルな意味は、「Aの論理式を全部仮定すれば、Bのどの論理式でも証明でき…

(L, ~)がMoore閉包を持った集合として、A|-Bを B⊆A~ として定義する。 とくに、A|-{f} をA|-fと書く。つまり、A|-f ⇔ f∈A~。これで、「B⊆AならばA|-B」と「A|-B, B|-C ならば、A|-C」を示してみる。「B⊆AならばB⊆A~」は「A⊆A~」から明らか。B⊆A, C⊆B~のとき…

証明可能性関係 |- を外から見て公理化したい。とりあえず： f∈A ならば、 A|-f 任意のg∈Bが A|-g であり、B|-hならば、A|-h この2つは必要だろう。A、Bともに論理式（その全体はL）の集合のとき、A|-Bを、「任意のg∈Bに対してA|-g」として、|-の定義を拡張…

「多項式関手と添字化」ってタイトルの書きかけ文書を見つけたのだが、自分でも、何を考えて何を書こうとしたかサッパリわからない。書いてある断片を見ると： F:C→Cというendo-functorがあると、F代数の圏Alg(F)とF余代数の圏Coalg(F)が定義できる。2変数関…

第三のアカウントを取った(苦笑)。キマイラ飼育記 本編でも、「檜山用メモ」という分類カテゴリーを設けているけど、これが多いと雑音になる。それでメモはこっちに書くことにした。キマイラ・サイトにグロッサランダムってのを書いていた時期もあるのだけど…