You are viewing beroal

язык, на котором не говорят - Coq. парадоксы [entries|archive|friends|userinfo]
beroal

[ website | personal website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Coq. парадоксы [Aug. 23rd, 2008|03:29 pm]
Previous Entry Share Next Entry
[Tags|]

Формализация некоторых простых парадоксов.

Парадокс Рассела.

Возникает вследствие неограниченной аксиомы свёртывания, которая формально выглядит примерно так:
∃s.∀e.(e∊s↔f)
где f — логическая формула, не имеющая свободных вхождений s и обычно имеющая свободные вхождения e. На человеческом языке эту схему аксиом можно прочитать так: «для любого свойства, заданного логически, можно сконструировать множество, содержащее те и только те элементы, которые имеют вышеозначенное свойство».

Свойство, заданное логически, — это предикат u->Prop. Если определить множество как подмножество универсального множества u, то есть, тоже как предикат, аксиома удовлетворена по определению.
Section paradox_Russel.
Variable u:Set.
(* set is a function of type u->Prop.
	so the axiom scheme of comprehension of set theory
	is satisfied by definition of set *)
Definition in_set := fun (s:u->Prop) e => s e.
(* (fun e => ~(e e)) is a set, say 'r', of all objects
	which are not members of themselves.
	is 'r' a member of 'r'? *)
(* 'Check' below raises an error.
	type checking doesn't allow us to write
	Russell's paradox. u->Prop is not in u

Check let r := fun e:u => ~(e e) in in_set r r.
*)
End paradox_Russel.

Множество Рассела содержит множества, не являющиеся элементом себя, задаётся как (fun e => ~(e e)). К сожалению, система типов не даёт возможности выразить парадокс. Аппликация (e e), обозначающая фразу «элемент себя», не проходит, u->Prop нельзя превратить в u.

Более успешная попытка.
Section paradox_Russel_all_sets.
Variable (all_sets:Set)
	(in_set : forall (set:all_sets) (element:all_sets), Prop (* element is in set *) )
	(comprehension : forall f:all_sets->Prop, exists s:all_sets,
		forall e:all_sets, in_set s e <-> f e (* axiom of comprehension *) ).
Definition rspec := comprehension (fun e => ~(in_set e e)).
Definition paradox_Russel_all_sets := (match rspec
	with ex_intro r rtheorem => complement_equiv _
		((rtheorem:forall e:all_sets, in_set r e <-> ~in_set e e) r)
	end
	) : False.
(* our assumptions imply a contradiction *)
End paradox_Russel_all_sets.

Отношение in_set/∈, как и (схема аксиом свёртывания)/comprehension, заданы явно. тип comprehension содержит в себе ∃, то есть comprehension возвращает кортеж из новосозданного множества и доказательство «элемент множества имеет свойство …». Противоречие возникает тогда, когда мы захотим проверить это доказательство, взяв в качестве элемента само множество Рассела. Множество Рассела принадлежит множеству Рассела тогда и только тогда, когда множество Рассела не является элементом себя.

Используется лемма (forall p, p<->~p) -> False
Definition complement_equiv := fun p (equiv:p<->~p)
=> (match equiv
	with conj impf impb =>
		(fun np:~p => (np (impb np)):False)
		(fun p1:p  => ((impf p1) p1):False)
	end
	):False.


Парадокс Кантора.

В простейшей форме. Мощность показательного множества некоторого множества t строго больше мощности множества t. Мощность множества t нестрого больше мощности подмножества t. Рассмотрим множество всех множеств, назовём его all_sets. Любое показательное множество есть множество подмножеств, то есть оно состоит только из множеств. Значит, оно является подмножеством all_sets. (Я говорю именно о показательных множествах, а не о любых, так как а вдруг в нашей теории множеств есть объекты, не являющиеся множествами.)

Мощность показательного множество от all_sets одновременно и нестрого меньше мощности all_sets (по определению all_sets), и строго больше (потому что показательное, следует из теоремы Кантора).

Формально отношение «быть подмножеством» задаётся как существование сюръекции from_all, которая отображает all_sets на любое показательное множество. from_all можно построить так: если элемент области значений есть в показательном множестве, отобразить на него, иначе к примеру на пустое множество. from_all является сюръекцией, так как для каждого элемента показательного множества найдётся такой же в all_sets (all_sets содержит все множества). Я же задаю свойство сюръективности как существование функции to_all, такой, что from_all обращает to_all, или from_all ∘ to_all = id (см. alls_rev).

Отношение мощностей «строго меньше» задаётся как невозможность сюръекции, так что вывод противоречия элементарен.
Section paradox_Cantor.
Section powerset.
	Variable t:Type.
	Definition powerset := t->Prop.
	Definition ps_equiv := fun p1 p2:powerset
		=> forall x:t, p1 x <-> p2 x.
End powerset.
Variable (all_sets:Type).
Record all_sets_spec (t:Type):Type
	:= alls_intro
	{ from_all : all_sets->powerset t; to_all : powerset t->all_sets
	; alls_rev : forall ps, ps_equiv _ (from_all (to_all ps)) ps}.
Variable all_sets_spec1 : forall t, all_sets_spec t.
Theorem paradox_Cantor : False.
Proof.
refine (match all_sets_spec1 all_sets
	with alls_intro from_all0 to_all0 alls_rev0 => _ end).
set (Cantor_ps := (fun s => ~(from_all0 s s)) : powerset all_sets).
set (equiv1 := alls_rev0 Cantor_ps (to_all0 Cantor_ps)).
unfold Cantor_ps in equiv1.
refine (complement_equiv _ equiv1).
Defined.
End paradox_Cantor.

ps_equiv — это равенство показательных множеств, более слабое, чем стандартное в Coq равенство eq. Cantor_ps — это специальное множество, которое создаётся в процессе доказательства теоремы Кантора, то самое множество, которое предполагаемая сюръекция не покрывает, и поэтому не является сюръекцией.
LinkReply

Comments:
From: nivanych
2008-08-24 02:07 pm (UTC)

(Link)

Вот ещё тоже в тему -
Cic: the Calculus of Inductive Construction with impredicative Set
http://coq.inria.fr/doc/Reference-Manual006.html#toc31