| Title |
“Regularity”(only universal class is equal to its powerclass) #AxmRegularity #label-regularity-only-universal-class-is-equal-to-its-powerclass |
| Classification |
Axiom |
| Formula |
0\(\href{../symbols/delimiters-brackets.html}{(} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{X} \href{../symbols/typing-colon.html}{:} \href{../symbols/class-type.html}{\mathsf{Class}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/power-op.html}{\mathcal{P}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{X} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/sub-pred.html}{\subseteq} \href{../symbols/variables.html}{X} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/universal-class-const.html}{\mathbf{V}} \href{../symbols/sub-pred.html}{\subseteq} \href{../symbols/variables.html}{X} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
PEpsIndAx_prf |
| Scheme of Types |
0(∀([X@Variable]:[Class@Type])((𝒫([X@Class.Expression])⊆[X@Class.Expression])→(V⊆[X@Class.Expression]))) |
| Kernel Note |
Kernel Form (Cumulative 𝒫-Induction): ∀(X:Class)((𝒫(X) ⊆ X) → (V ⊆ X)). Classically equivalent (via X = V \ A) to the textbook ∈-minimal-element Regularity / Foundation formulation ∀(A:Class)((A ≠ ∅) → ∃(x:Class)((x ∈ A) ∧ ((x ∩ A) = ∅))). |
| Verification |
Postulated (Kernel Axiom) · Standalone Entry (AxmRegularity) → · (3.14) · #AxmRegularity |