集合論・序章

集合論・序章 2012/8/2 (Thu.)
1. 論理体型

体系を考える．この体系は object, truth value, function, predicate 等の
概念を含む．その概念を type(型) と称する関数の category(体系) と対応
附ける．例えば
obj (object)
bool (truth value)
obj -> .. -> obj -> obj (n変数関数)
obj -> .. -> obj -> bool (n変数述語)
bool -> .. -> bool -> bool (論理記号)
obj -> bool -> bool (束縛記号, 量子化)

各typeにはいくつかの 定数(const)と変数(var)が記号として対応附く．
例えば a,b..x,y.. みたいな記号が変数として用いられる．

定数として
not :: bool -> bool
or :: bool -> bool
and ::
implies ::
=== ::
for_all :: obj -> bool -> bool
∃::
などだ．

そういった変数、定数の組み合わせが言語である．

# 形式的表現 (formal expression)
形式的表現のあつまりEとは以下を満たすクロージャ(最小の集合)である
 -- 定数および変数はEに含まれる
 -- t1 -> t2 -> .. -> tn -> t という型を持つ定数または変数fと
 　tn という型を持つ定数または変数 sn とがEに含まれる時
 　f(s1 .. sn) は tという型を持ってこれもまた E の元である．

上のようなEの構成に沿った帰納法によって次が言える．
仮定として
 - 全ての定数と変数は性質pを持つ
 - t1 .. tn が p を持つなら f(t1 .. tn) も p を持つ
がある時
Eの全ての元は性質pを持つことになる．

type obj のものを項、type bool のものを論理式という．
だから例えば
 -- AやBが論理式ならば (not A) (and A B) なんかも論理式
 -- Aが論理式でxが項なら
    ∀x . A(x) , ∃x . A(x)
　  これも論理式

変数は2つに分類され、つまり、free var と bound var である．
∀と ∃によって束縛されるのが bound var で他は全て
free var である．

「LKによる推論規則」、「証明可能」省略します．

# ブール代数
命題の正しさを表す量として truth value (真偽値)があるが、
それを代数的に表現するのが boolean algebra (ブール代数)である．

ブール代数 B (script B) は演算 (-), (+), (*) の3つを持っていて
(それぞれ not, or, and に相当する)次の3つの性質を持つ．
中置記法の*は寒冷に従ってしばしば省略する．

 -- a+b = b+a , a*b = b*a (交換律)
 -- a + (bc) = (a+b)(b+c) , a(b+c) = ab+ac (分配律!)
 -- a + (b * -b) = a , a * (b + -b) = a (補元)

+ と * は上から分かるように双対関係にある．

定数として 0 と 1 があるが、その定義は
 -- 0 := a * -a
 -- 1 := a + -a

もちろん明らかに false と true に相当するのである．
これについて以下の性質  
 -- a + 0 = a , a + 1 = 1
 -- a * 0 = 0 , a * 1 = a

次のような吸収律とべき等律もまた成り立つ．
 -- a + ab = a , a * (a+b) = a
 -- a + a = a , a * a = a

例えば次のように証明できる
 a * (a+b) = (a+0)(a+b) = a+0b = a+0 = a

吸収律の a = a(a+b) より
a+b = b <=> a=ab
という同値関係が得られるだろう．

順序 <= を "a <= b" <=> "a+b = b" で定義する．この順序は
半順序を与えるものである．つまり
 -- a <= a (REFL)
 -- if a <= b and b <= a then a = b (SYM)
 -- if a <= b and b <= c then a <= c (TRANS)
この三つが成り立っている．

# Zermelo-Fraenkel の集合論
外延の公理 (Axiom of extensionality)
(∀x in a . x isin b) and (∀x in b . x isin b) => a = b
集合というものはその元によって決定されることを言う．

また包含関係 sub の定義は次
def a sub b (aはbに含まれる) :
    ∀x in a . x isin b

pair(対) { , } を次のような関数である．
つまり集合a,b のそのpairは
∀x . ( x isin {a,b} === (x isin a) or (x isin b))
を満たすようなaよりひとつ次元が上の集合だ．

明らかに
    {a,b} = {b,a}
である．
これが aとbのor であるので順序は関係がない．
順序を覚えておく(直和?) pair を ordered pair と言って
    <a,b>
と記述する．そしてこれは
    <a,b> = <c,d> => a=c and b=d
である．
例えば
    def <a, b> :
        {{a,a}, {a,b}}
とすれば順序を保つという性質が満たされ ordered pair を実装
できる．しかし実装方法は他にもいくつかある．ここでは上を
定義としておく．

和集合、べき集合を直観通りに定義する．
演算を Sum(a) , P(a) と書こう．
またSum({a,b})をSum(a,b)
Sum(a, {a}) を a+1 と書く．

空集合も直観通りで
    ∀x . x not isin empty
となるemptyのこと．
emptyを0と書くことにする．

無限公理 (axiom of infinity)
    ∃a . (0 isin a and (∀x in a . x+1 isin a))
このようなaの元というのはつまり
    -- 0
    -- 1 = {0} = 0+1
    -- 2 = {0,1} = 1+1
    -- 3 = {0,1,2} = 2+1
と列挙されるものであり、自然数全体を表すだろうと伺える．

ただそれを言うために次の公理が提示される．

comprehension の公理
「特定の性質を有するものの全体は集合である」
∃c . c === (a and A(x in a)) : Aは任意の論理式

集合と定まった a について性質Aを有するものを集めたものは
集合なのである．制限なしに単に性質Aを持つとするもの全体
は集合として構成する方法としては誤っている (Russelのパラドクス)

置換公理 (axiom of replacement)
「集合の関数による像はまた集合である」
∀x in a . ∃y . A(x,y)
    => ∃b . 
        ∀x in a . ∃y in b . A(x,y)

写像を作る関係Aによってaがbに移されたのである．
コメ(0) | トラ(0)
intime o'
