証明系を抽象化する目的は、証明系をインスティチューションに組み込みたいから。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変数関…

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