| Title |
“Is successor-inductive (Peano-inductive)” predicate #DefInductiveClass #label-is-successor-inductive-peano-inductive-predicate |
| Classification |
Definition |
| 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/ind-pred.html}{\mathrm{Ind}} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{X} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/iff-conn.html}{\longleftrightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/emptyset-const.html}{\emptyset} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{X} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/and-conn.html}{\land} \href{../symbols/forall-binder.html}{\forall} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{a} \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/variables.html}{a} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{X} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/impl-conn.html}{\rightarrow} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/delimiters-brackets.html}{(} \href{../symbols/variables.html}{a} \href{../symbols/binunion-op.html}{\cup} \href{../symbols/singleton-op.html}{\{} \href{../symbols/variables.html}{a} \href{../symbols/singleton-op.html}{\}} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/in-pred.html}{\in} \href{../symbols/variables.html}{X} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \href{../symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
TpInd |
| Scheme of Types |
0(∀([X@Variable]:[Class@Type])(Ind([X@Class.Expression])⟷((∅∈[X@Class.Expression])∧∀([a@Variable]:[Class@Type])(([a@Class.Expression]∈[X@Class.Expression])→(([a@Class.Expression]∪{[a@Class.Expression]})∈[X@Class.Expression]))))) |
| Kernel Note |
Successor-inductive (Peano 0-successor-inductive) in the narrowest sense: closed under 0 = ∅ and ordinal successor a |-> a ∪ {a}, as distinguished from transfinite ∈-induction (3.70) or 𝒫-induction. |
| Verification |
Definitional (Kernel AST) · Standalone Entry (DefInductiveClass) → · (3.55) · #DefInductiveClass |