Mizar/証明法
< Mizar
|
この項目「Mizar/証明法」は、あるテーマを構成する一部分を分岐して作成されたものですが、まだ閲覧者の調べものの参照としては役立たない書きかけの項目です。分岐元のテーマを確認し加筆、訂正などをして下さる協力者を求めています。 |
証明法
基本的な論理記号
[編集]∧,￢,∃,＝,∈
公理
[編集]| 集合 | 外延性の公理 | Extensionality | ∀x,y (∀z (z∈x⇔z∈y)⇒x=y) |
| 内包の公理 | Comprehension Schema | ∃y,∀x(x∈y⇔x∈z∧φ) | |
| 対の公理 | Pairing | ∀x,y,∃z(x∈z∧y∈z) | |
| 和集合の公理 | Union | ∀ʄ,∃A,∀Y,∀x(x∈Y∈ʄ⇒x∈A) | |
| 置換公理 | Replacement | ||
| 自然数 | 無限の公理 | Infinity | ∃x(0∈x∧∀y∈x(S(y)∈x)) |