| Coq. парадоксы |
[Aug. 23rd, 2008|03:29 pm]
|
Формализация некоторых простых парадоксов.
Парадокс Рассела.
Возникает вследствие неограниченной аксиомы свёртывания, которая формально выглядит примерно так:
∃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 — это специальное множество, которое создаётся в процессе доказательства теоремы Кантора, то самое множество, которое предполагаемая сюръекция не покрывает, и поэтому не является сюръекцией. |
|
|
beroal
