alex_dorin писал(а):
Как выразить в ZF равномощность 2-х множеств?
SMS писал(а):
В лоб
SMS прав. На самом деле ZF -- очень мощный язык, в ZF формализуема вся "обычная" математика. Формулы при этом получаются, как правило, очень навороченные, но это обстоятельство никого не волнует, так как главное для "рядового" математика -- это осознание того, что все нужные ему утверждения строго формализуемы, а не то, какими именно теоретико-множественными формулами они в точности записываются.
Что касается конкретного вопроса о формализации равномощности, то, следуя рекомендациям
SMS, это можно сделать, например, так (писал наспех, так что мог что-то напутать, но надеюсь, общая идея понятна):
Код:
"X равномощно Y" :=
\exists f "f -- биекция X на Y"
"f -- биекция X на Y" :=
"f:X->Y" & "f -- инъекция" & "образ f содержит Y"
"f:X->Y" :=
"f -- подмножество X x Y" &
\forall x,y1,y2 ("(x,y1)\in f" & "(x,y2)\in f" => y1=y2) &
\forall x\in X \exists y "(x,y)\in f"
"f -- инъекция" :=
\forall x1,x2,y ( "(x1,y)\in f" & "(x2,y)\in f" => x1=x2 )
"образ f содержит Y" :=
\forall y\in Y \exists x "(x,y)\in f"
"f -- подмножество X x Y" :=
\forall z\in f \exists x,y ( x\in X & y\in Y & "z=(x,y)" )
"z=(x,y)" :=
"z={{x},{x,y}}"
"z={x,y}" :=
\forall a (a\in z <=> a=x \or a=y)
"z={x}" :=
"z={x,x}"
"(x,y)\in f" :=
\exists z ("z=(x,y)" & z\in f)
Вход
FAQ
Поиск
