14.3 Some cardinal arithmetic (2)
今回は，任意の集合Aについて，その冪集合2^AからAへの単射が存在しないこと(Cantor)の証明です．
先に示した単射による基数の大小関係の特徴付け
# let INJECTIVE_IFF_LEFT_INVERSE = MESON[
MESON`(!a1:A a2:A. f(a1)=f(a2) ==> a1=a2)
<=>(!b:B. ?a1:A. !a2:A. f a2 = b ==> a2 = a1)`;
MESON`(!b:B. ?a1:A. !a2:A. f a2 = b ==> a2 = a1)<=>(?g:B->A. !a:A. g(f(a))=a
)`]
`(!a1:A a2:A. f(a1)=f(a2) ==> a1=a2)<=>(?g:B->A. !a:A. g(f(a))=a)`;;
0..0..1..2..5..solved at 11
0..0..1..2..7..15..solved at 24
0..0..1..4..11..27..58..128..263..503..959..solved at 973
0..0..1..2..5..9..15..22..29..36..47..58..73..solved at 88
0..0..1..5..16..57..117..258..593..solved at 1121
0..0..1..2..12..24..82..159..solved at 177
val ( INJECTIVE_IFF_LEFT_INVERSE ) : thm =
|- (!a1 a2. f a1 = f a2 ==> a1 = a2) <=> (?g. !a. g (f a) = a)
を参照します．
# g `~( ?f:(A->bool)->A. (!x y. f(x)=f(y)==>x=y) )` ;;
val it : goalstack = 1 subgoal (1 total)`~(?f. !x y. f x = f y ==> x = y)`
# e ( REWRITE_TAC[INJECTIVE_IFF_LEFT_INVERSE] THEN
STRIP_TAC );;
val it : goalstack = 1 subgoal (1 total)0 [`!a. g (f a) = a`]
`F`
このgはAから2^AつまりA->boolへの写像なのですが，とくにa∈2^Aとして~(x∈g(x))となるx全体の集合を用いると，f(a)∈a，~(f(a)∈a)は等価となります．なぜなら，f(a)∈aならaの定義により~(f(a)∈g(f(a)))となるが，g(f(a))=aなので，これは~(f(a)∈a)であり，同じく，~(f(a)∈a)ならば~(f(a)∈g(f(a)))だが，これはaの定義によりf(a)∈aに他ならないからです．
# g `~( ?f:(A->bool)->A. (!x y. f(x)=f(y)==>x=y) )` ;;
val it : goalstack = 1 subgoal (1 total)`~(?f. !x y. f x = f y ==> x = y)`
# e ( REWRITE_TAC[INJECTIVE_IFF_LEFT_INVERSE] THEN STRIP_TAC );;
val it : goalstack = 1 subgoal (1 total)0 [`!a. g (f a) = a`]
`F`
# e ( FIRST_ASSUM( MP_TAC o (SPECL[`({x:A | ~(x IN g x)})`]) ) );;
val it : goalstack = 1 subgoal (1 total)0 [`!a. g (f a) = a`]
`g (f {x | ~(x IN g x)}) = {x | ~(x IN g x)} ==> F`
# e( REWRITE_TAC [EXTENSION] );;
val it : goalstack = 1 subgoal (1 total)0 [`!a. g (f a) = a`]
`~(!x. x IN g (f {x | ~(x IN g x)}) <=> x IN {x | ~(x IN g x)})`
# e ( REWRITE_TAC [NOT_FORALL_THM] );;
val it : goalstack = 1 subgoal (1 total)0 [`!a. g (f a) = a`]
`?x. ~(x IN g (f {x | ~(x IN g x)}) <=> x IN {x | ~(x IN g x)})`
# e( EXISTS_TAC `f( {x:A | ~(x IN g x)} ):A` );;
val it : goalstack = 1 subgoal (1 total)0 [`!a. g (f a) = a`]
`~(f {x | ~(x IN g x)} IN g (f {x | ~(x IN g x)}) <=>
f {x | ~(x IN g x)} IN {x | ~(x IN g x)})`# e( REWRITE_TAC [IN_ELIM_THM] );;
val it : goalstack = 1 subgoal (1 total)0 [`!a. g (f a) = a`]
`~(f {x | ~(x IN g x)} IN g (f {x | ~(x IN g x)}) <=>
~(f {x | ~(x IN g x)} IN g (f {x | ~(x IN g x)})))`# e( MESON_TAC[] );;
0..0..solved at 2
0..0..solved at 2
val it : goalstack = No subgoals<<
