Q instead of the elementary metatheory β° ∈ {IΣ1, π―, NBG, MK}, lacked explicit typed term interpretation μA notes, and lacked algorithmic symbol hyperlinking. Please use the canonical Standard ML-generated manual generated/manual.html (or generated/metatheory.html).
Machine-checked specification of classical propositional logic, first-order predicate logic, Morse–Kelley class theory, and type-theoretic side conditions directly generated from Standard ML kernel data structures.
Classical propositional calculus axioms A01–A12 and Modus Ponens rule.
| Num | Class | Title | Semantic Formula (Morse–Kelley Object Level) | Side Condition Formula | Verification |
|---|---|---|---|---|---|
| 1.01 | Axiom | A01 | (β¦πβ§β(β¦πβ§ββ¦πβ§))(β¦[π@Fm.Expression]β§β(β¦[π@Fm.Expression]β§ββ¦[π@Fm.Expression]β§)) | — | Verified (Kernel) |
| 1.02 | Axiom | A02 | ((β¦πβ§β(β¦πβ§ββ¦πβ§))β((β¦πβ§ββ¦πβ§)β(β¦πβ§ββ¦πβ§)))((β¦[π@Fm.Expression]β§β(β¦[π@Fm.Expression]β§ββ¦[π@Fm.Expression]β§))β((β¦[π@Fm.Expression]β§ββ¦[π@Fm.Expression]β§)β(β¦[π@Fm.Expression]β§ββ¦[π@Fm.Expression]β§))) | — | Verified (Kernel) |
| 1.03 | Axiom | A03 | ((β¦πβ§β§β¦πβ§)ββ¦πβ§)((β¦[π@Fm.Expression]β§β§β¦[π@Fm.Expression]β§)ββ¦[π@Fm.Expression]β§) | — | Verified (Kernel) |
| 1.04 | Axiom | A04 | ((β¦πβ§β§β¦πβ§)ββ¦πβ§)((β¦[π@Fm.Expression]β§β§β¦[π@Fm.Expression]β§)ββ¦[π@Fm.Expression]β§) | — | Verified (Kernel) |
| 1.05 | Axiom | A05 | (β¦πβ§β(β¦πβ§β(β¦πβ§β§β¦πβ§)))(β¦[π@Fm.Expression]β§β(β¦[π@Fm.Expression]β§β(β¦[π@Fm.Expression]β§β§β¦[π@Fm.Expression]β§))) | — | Verified (Kernel) |
| 1.06 | Axiom | A06 | (β¦πβ§β(β¦πβ§β¨β¦πβ§))(β¦[π@Fm.Expression]β§β(β¦[π@Fm.Expression]β§β¨β¦[π@Fm.Expression]β§)) | — | Verified (Kernel) |
| 1.07 | Axiom | A07 | (β¦πβ§β(β¦πβ§β¨β¦πβ§))(β¦[π@Fm.Expression]β§β(β¦[π@Fm.Expression]β§β¨β¦[π@Fm.Expression]β§)) | — | Verified (Kernel) |
| 1.08 | Axiom | A08 | ((β¦πβ§ββ¦πβ§)β((β¦πβ§ββ¦πβ§)β((β¦πβ§β¨β¦πβ§)ββ¦πβ§)))((β¦[π@Fm.Expression]β§ββ¦[π@Fm.Expression]β§)β((β¦[π@Fm.Expression]β§ββ¦[π@Fm.Expression]β§)β((β¦[π@Fm.Expression]β§β¨β¦[π@Fm.Expression]β§)ββ¦[π@Fm.Expression]β§))) | — | Verified (Kernel) |
| 1.09 | Axiom | A09 | ((Β¬β¦πβ§)β(β¦πβ§ββ₯))((Β¬β¦[π@Fm.Expression]β§)β(β¦[π@Fm.Expression]β§ββ₯)) | — | Verified (Kernel) |
| 1.10 | Axiom | A10 | ((β¦πβ§ββ¦πβ§)β((β¦πβ§βΒ¬β¦πβ§)βΒ¬β¦πβ§))((β¦[π@Fm.Expression]β§ββ¦[π@Fm.Expression]β§)β((β¦[π@Fm.Expression]β§βΒ¬β¦[π@Fm.Expression]β§)βΒ¬β¦[π@Fm.Expression]β§)) | — | Verified (Kernel) |
| 1.11 | Axiom | A11 | (β₯ββ¦πβ§)(β₯ββ¦[π@Fm.Expression]β§) | — | Verified (Kernel) |
| 1.12 | Axiom | A12 | (β¦πβ§β¨Β¬β¦πβ§)(β¦[π@Fm.Expression]β§β¨Β¬β¦[π@Fm.Expression]β§) | — | Verified (Kernel) |
| 1.13 | Inference Rule | Modus Ponens | β¦πβ§, (β¦πβ§ββ¦πβ§) ⊢ β¦πβ§β¦[π@Fm.Expression]β§, (β¦[π@Fm.Expression]β§ββ¦[π@Fm.Expression]β§) ⊢ β¦[π@Fm.Expression]β§ | — | Verified (Kernel) |
First-order predicate calculus with typed domain and Bernays rules.
| Num | Class | Title | Semantic Formula (Morse–Kelley Object Level) | Side Condition Formula | Verification |
|---|---|---|---|---|---|
| 2.01 | Axiom | Discourse domain is non-empty | (β(K:Class)β€)(β([K@Variable]:[Class@Type])β€) | — | Verified (Kernel) |
| 2.02 | Inference Rule | Forall Instantiation | ((β(β¦xβ¦:β¦Xβ§)β¦πβ§)ββ¦π[t/x]β§)((β([β¦[x@Variable.Expression]β¦@Variable]:[β¦[X@Type.Expression.Expression]β§@Type])β¦[π@Fm.Expression]β§)ββ¦[π@Fm.Expression][[t@LCEWIP]/[x@Variable.Expression]]β§) | β¦term t is free for substitution instead of all samely typed free occurences of the variable x in the formula πβ§β¦term [t@Class.Expression.Expression] is free for substitution instead of all samely typed free occurences of the variable [x@Variable.Expression] in the formula [π@Fm.Expression]β§ | Verified (Kernel) |
| 2.03 | Inference Rule | Exists Instantiation | (β¦π[t/x]β§ββ(β¦xβ¦:β¦Xβ§)β¦πβ§)(β¦[π@Fm.Expression][[t@LCEWIP]/[x@Variable.Expression]]β§ββ([β¦[x@Variable.Expression]β¦@Variable]:[β¦[X@Type.Expression.Expression]β§@Type])β¦[π@Fm.Expression]β§) | β¦term t is free for substitution instead of all samely typed free occurences of the variable x in the formula πβ§β¦term [t@Class.Expression.Expression] is free for substitution instead of all samely typed free occurences of the variable [x@Variable.Expression] in the formula [π@Fm.Expression]β§ | Verified (Kernel) |
| 2.04 | Inference Rule | Forall Abstraction | (β¦πβ§ββ¦πβ§) ⊢ (β¦πβ§ββ(β¦xβ¦:β¦Xβ§)β¦πβ§)(β¦[π@Fm.Expression]β§ββ¦[π@Fm.Expression]β§) ⊢ (β¦[π@Fm.Expression]β§ββ([β¦[x@Variable.Expression]β¦@Variable]:[β¦[X@Type.Expression.Expression]β§@Type])β¦[π@Fm.Expression]β§) | β¦name x does not occure free as a variable of type X in formula πβ§β¦name [x@Variable.Expression] does not occure free as a variable of type [X@Type] in formula [π@Fm.Expression]β§ | Verified (Kernel) |
| 2.05 | Inference Rule | Exists Abstraction | (β¦πβ§ββ¦πβ§) ⊢ ((β(β¦xβ¦:β¦Xβ§)β¦πβ§)ββ¦πβ§)(β¦[π@Fm.Expression]β§ββ¦[π@Fm.Expression]β§) ⊢ ((β([β¦[x@Variable.Expression]β¦@Variable]:[β¦[X@Type.Expression.Expression]β§@Type])β¦[π@Fm.Expression]β§)ββ¦[π@Fm.Expression]β§) | β¦name x does not occure free as a variable of type X in formula πβ§β¦name [x@Variable.Expression] does not occure free as a variable of type [X@Type] in formula [π@Fm.Expression]β§ | Verified (Kernel) |
| 2.06 | Inference Rule | Generalisation (admissible rule) | β¦πβ§ ⊢ (β(β¦xβ¦:β¦Xβ§)β¦πβ§)β¦[π@Fm.Expression]β§ ⊢ (β([β¦[x@Variable.Expression]β¦@Variable]:[β¦[X@Type.Expression.Expression]β§@Type])β¦[π@Fm.Expression]β§) | — | Verified (Kernel) |
Morse–Kelley axiomatic class theory with Dunaev tagged ordered pairs, class comprehension, and Ordinal Induction.
| Num | Class | Title | Semantic Formula (Morse–Kelley Object Level) | Side Condition Formula | Verification |
|---|---|---|---|---|---|
| 3.01 | Inference Rule | Class comprehension | ((β¦xβ¦β{β¦xβ¦|β¦πβ§})β·((β¦xβ¦ set)β§β¦πβ§))(([β¦[x@Variable.Expression]β¦@Class.Expression]β{[β¦[x@Variable.Expression]β¦@Class.Expression]|β¦[π@Fm.Expression]β§})β·(([β¦[x@Variable.Expression]β¦@Class.Expression] set)β§β¦[π@Fm.Expression]β§)) | β¦(x:Name)β§ ∧ β¦(π:Fm)β§β¦([x@LCEWIP]:Name)β§ ∧ β¦([π@LCEWIP]:Fm)β§ | Verified (Kernel) |
| 3.02 | Definition | βIs a setβ predicate | (β(X:Class)((X set)β·(β(Y:Class)(XβY))))(β([X@Variable]:[Class@Type])(([X@Class.Expression] set)β·(β([Y@Variable]:[Class@Type])([X@Class.Expression]β[Y@Class.Expression])))) | — | Verified (Kernel) |
| 3.03 | Definition | βIs a proper classβ predicate | (β(K:Class)((K proper)β·(Β¬(K set))))(β([K@Variable]:[Class@Type])(([K@Class.Expression] proper)β·(Β¬([K@Class.Expression] set)))) | — | Verified (Kernel) |
| 3.04 | Definition | Empty set | (β ={x|β₯})(β ={[x@Class.Expression]|β₯}) | — | Verified (Kernel) |
| 3.05 | Definition | Universal class | (V={x|β€})(V={[x@Class.Expression]|β€}) | — | Verified (Kernel) |
| 3.06 | Definition | Subclass relation | (β(X:Class)β(Y:Class)((XβY)β·(β(a:Class)((aβX)β(aβY)))))(β([X@Variable]:[Class@Type])β([Y@Variable]:[Class@Type])(([X@Class.Expression]β[Y@Class.Expression])β·(β([a@Variable]:[Class@Type])(([a@Class.Expression]β[X@Class.Expression])β([a@Class.Expression]β[Y@Class.Expression]))))) | — | Verified (Kernel) |
| 3.07 | Theorem | Example: βThe empty class is a subclass of any classβ statement | (β(X:Class)(β βX))(β([X@Variable]:[Class@Type])(β β[X@Class.Expression])) | — | Verified (Kernel) |
| 3.08 | Axiom | βMembership respects equality from the leftβ | (β(X:Class)β(Y:Class)((X=Y)ββ(z:Class)((zβX)β·(zβY))))(β([X@Variable]:[Class@Type])β([Y@Variable]:[Class@Type])(([X@Class.Expression]=[Y@Class.Expression])ββ([z@Variable]:[Class@Type])(([z@Class.Expression]β[X@Class.Expression])β·([z@Class.Expression]β[Y@Class.Expression])))) | — | Verified (Kernel) |
| 3.09 | Axiom | βMembership respects equality from the rightβ | (β(X:Class)β(Y:Class)((X=Y)ββ(W:Class)((XβW)β·(YβW))))(β([X@Variable]:[Class@Type])β([Y@Variable]:[Class@Type])(([X@Class.Expression]=[Y@Class.Expression])ββ([W@Variable]:[Class@Type])(([X@Class.Expression]β[W@Class.Expression])β·([Y@Class.Expression]β[W@Class.Expression])))) | — | Verified (Kernel) |
| 3.10 | Axiom | βExtensionalityβ | (β(X:Class)β(Y:Class)((β(z:Class)((zβX)β·(zβY)))β(X=Y)))(β([X@Variable]:[Class@Type])β([Y@Variable]:[Class@Type])((β([z@Variable]:[Class@Type])(([z@Class.Expression]β[X@Class.Expression])β·([z@Class.Expression]β[Y@Class.Expression])))β([X@Class.Expression]=[Y@Class.Expression]))) | — | Verified (Kernel) |
| 3.11 | Theorem | βIntensionalityβ(admissible) | (β(X:Class)β(Y:Class)(((X set)β§(Y set))β((β(W:Class)((XβW)β·(YβW)))β(X=Y))))(β([X@Variable]:[Class@Type])β([Y@Variable]:[Class@Type])((([X@Class.Expression] set)β§([Y@Class.Expression] set))β((β([W@Variable]:[Class@Type])(([X@Class.Expression]β[W@Class.Expression])β·([Y@Class.Expression]β[W@Class.Expression])))β([X@Class.Expression]=[Y@Class.Expression])))) | — | Verified (Kernel) |
| 3.12 | Axiom | βHeredityβ(a subclass of a set is also a set) | (β(A:Class)β(B:Class)(((AβB)β§(B set))β(A set)))(β([A@Variable]:[Class@Type])β([B@Variable]:[Class@Type])((([A@Class.Expression]β[B@Class.Expression])β§([B@Class.Expression] set))β([A@Class.Expression] set))) | — | Verified (Kernel) |
| 3.13 | Axiom | βExponentβ(powerclass of a set is also a set) | (β(X:Class)((X set)β(π«(X) set)))(β([X@Variable]:[Class@Type])(([X@Class.Expression] set)β(π«([X@Class.Expression]) set))) | — | Verified (Kernel) |
| 3.14 | Axiom | βRegularityβ(only universal class is equal to its powerclass) | (β(X:Class)((π«(X)βX)β(VβX)))(β([X@Variable]:[Class@Type])((π«([X@Class.Expression])β[X@Class.Expression])β(Vβ[X@Class.Expression]))) | — | Verified (Kernel) |
| 3.15 | Definition | Transitivity predicate | (β(A:Class)(Tr(A)β·(β(B:Class)((BβA)β(BβA)))))(β([A@Variable]:[Class@Type])(Tr([A@Class.Expression])β·(β([B@Variable]:[Class@Type])(([B@Class.Expression]β[A@Class.Expression])β([B@Class.Expression]β[A@Class.Expression]))))) | — | Verified (Kernel) |
| 3.16 | Definition | Ordinality predicate | (β(A:Class)(Ord(A)β·(Tr(A)β§β(B:Class)((BβA)βTr(B)))))(β([A@Variable]:[Class@Type])(Ord([A@Class.Expression])β·(Tr([A@Class.Expression])β§β([B@Variable]:[Class@Type])(([B@Class.Expression]β[A@Class.Expression])βTr([B@Class.Expression]))))) | — | Verified (Kernel) |
| 3.17 | Definition | Class of all ordinal sets(ordinal numbers) | (On={w|Ord(w)})(On={[w@Class.Expression]|Ord([w@Class.Expression])}) | — | Verified (Kernel) |
| 3.18 | Theorem | The class of all ordinals is an ordinal class | Ord(On)Ord(On) | — | Verified (Kernel) |
| 3.19 | Definition | Union of the elements of a class | (β(K:Class)(βK={x|β(y:Class)((yβK)β§(xβy))}))(β([K@Variable]:[Class@Type])(β[K@Class.Expression]={[x@Class.Expression]|β([y@Variable]:[Class@Type])(([y@Class.Expression]β[K@Class.Expression])β§([x@Class.Expression]β[y@Class.Expression]))})) | — | Verified (Kernel) |
| 3.20 | Definition | Intersection of the elements of a class | (β(K:Class)(βK={x|β(y:Class)((yβK)β(xβy))}))(β([K@Variable]:[Class@Type])(β[K@Class.Expression]={[x@Class.Expression]|β([y@Variable]:[Class@Type])(([y@Class.Expression]β[K@Class.Expression])β([x@Class.Expression]β[y@Class.Expression]))})) | — | Verified (Kernel) |
| 3.21 | Definition | Domain (includes arguments with proper class values) | (β(F:Class)(Dom(F)={x|β(b:Class)((x,b)βF)}))(β([F@Variable]:[Class@Type])(Dom([F@Class.Expression])={[x@Class.Expression]|β([b@Variable]:[Class@Type])(([x@Class.Expression],[b@Class.Expression])β[F@Class.Expression])})) | — | Verified (Kernel) |
| 3.22 | Definition | IF-THEN-ELSE-FI (Class conditional with NFV side condition and context turnstile) | (β(Ξ:Ctx)β(v:Variable)β(π:Fm)β(A:Class)β(B:Class)((Β¬(Enc(β¦vβ¦)βFV(π:Bool)))β(,Ξβ’βΉβ¦IF β¦πβ§ THEN A ELSE B FIβ§={β¦vβ¦|(β¦πβ§β§(β¦vβ¦βA))β¨((Β¬β¦πβ§)β§(β¦vβ¦βB))}βΊ)))(β([Ξ@Variable]:[Ctx@Type])β([v@Variable]:[Variable@Type])β([π@Variable]:[Fm@Type])β([A@Variable]:[Class@Type])β([B@Variable]:[Class@Type])((Β¬(Enc([β¦[v@Variable.Expression]β¦@LCEWIP])βFV([π@Fm.Expression]:Bool)))β(,[Ξ@Ctx.Expression]β’βΉβ¦IF β¦[π@Fm.Expression]β§ THEN [A@Class.Expression] ELSE [B@Class.Expression] FIβ§={[β¦[v@Variable.Expression]β¦@Class.Expression]|(β¦[π@Fm.Expression]β§β§([β¦[v@Variable.Expression]β¦@Class.Expression]β[A@Class.Expression]))β¨((Β¬β¦[π@Fm.Expression]β§)β§([β¦[v@Variable.Expression]β¦@Class.Expression]β[B@Class.Expression]))}βΊ))) | — | Verified (Kernel) |
| 3.23 | Definition | simple_if (polymorphic non-dependent conditional over arbitrary Type) | (Evaluated Rule Definition) | — | Verified (Kernel) |
| 3.24 | Definition | dependent_if (polymorphic dependent conditional with type computation) | (Evaluated Rule Definition) | — | Verified (Kernel) |
| 3.25 | Definition | Evaluation of a [function|class-function|family] | (β(F:Class)β(a:Class)(Fa=β¦IF (β(s:Class)((a,s)βF)) THEN β{s|(a,s)βF} ELSE V FIβ§))(β([F@Variable]:[Class@Type])β([a@Variable]:[Class@Type])([F@Class.Expression][a@Class.Expression]=β¦IF (β([s@Variable]:[Class@Type])(([a@Class.Expression],[s@Class.Expression])β[F@Class.Expression])) THEN β{[s@Class.Expression]|([a@Class.Expression],[s@Class.Expression])β[F@Class.Expression]} ELSE V FIβ§)) | — | Verified (Kernel) |
| 3.26 | Definition | Image class | (β(f:Class)β(A:Class)(fA={b|β(a:Class)((aβA)β§(fa=b))}))(β([f@Variable]:[Class@Type])β([A@Variable]:[Class@Type])([f@Class.Expression][A@Class.Expression]={[b@Class.Expression]|β([a@Variable]:[Class@Type])(([a@Class.Expression]β[A@Class.Expression])β§([f@Class.Expression][a@Class.Expression]=[b@Class.Expression]))})) | — | Verified (Kernel) |
| 3.27 | Definition | βHas exactly one elementβ predicate | (β(s:Class)((s singleton)β·(β!(x:Class)(xβs))))(β([s@Variable]:[Class@Type])(([s@Class.Expression] singleton)β·(β!([x@Variable]:[Class@Type])([x@Class.Expression]β[s@Class.Expression])))) | — | Verified (Kernel) |
| 3.28 | Definition | βIs set-valuedβ predicate | (β(F:Class)((F set-valued)β·(β(x:Class)((xβDom(F))β(Fx set)))))(β([F@Variable]:[Class@Type])(([F@Class.Expression] set-valued)β·(β([x@Variable]:[Class@Type])(([x@Class.Expression]βDom([F@Class.Expression]))β([F@Class.Expression][x@Class.Expression] set))))) | — | Verified (Kernel) |
| 3.29 | Definition | βHas concentrated set valuesβ predicate | (β(F:Class)((F concentrated set values)β·(β(x:Class)((xβDom(F))β((Fx set)ββ!(y:Class)((x,y)βF))))))(β([F@Variable]:[Class@Type])(([F@Class.Expression] concentrated set values)β·(β([x@Variable]:[Class@Type])(([x@Class.Expression]βDom([F@Class.Expression]))β(([F@Class.Expression][x@Class.Expression] set)ββ!([y@Variable]:[Class@Type])(([x@Class.Expression],[y@Class.Expression])β[F@Class.Expression])))))) | — | Verified (Kernel) |
| 3.30 | Definition | βHas flat proper valuesβ predicate | (β(F:Class)((F flat proper values)β·(β(x:Class)((xβDom(F))β((Fx proper)ββ(b:Class)(((x,b)βF)β(b singleton)))))))(β([F@Variable]:[Class@Type])(([F@Class.Expression] flat proper values)β·(β([x@Variable]:[Class@Type])(([x@Class.Expression]βDom([F@Class.Expression]))β(([F@Class.Expression][x@Class.Expression] proper)ββ([b@Variable]:[Class@Type])((([x@Class.Expression],[b@Class.Expression])β[F@Class.Expression])β([b@Class.Expression] singleton))))))) | — | Verified (Kernel) |
| 3.31 | Definition | βIs a familyβ predicate | (β(F:Class)((F family)β·((F concentrated set values)β§(F flat proper values))))(β([F@Variable]:[Class@Type])(([F@Class.Expression] family)β·(([F@Class.Expression] concentrated set values)β§([F@Class.Expression] flat proper values)))) | — | Verified (Kernel) |
| 3.32 | Definition | βIs a class-functionβ predicate | (β(F:Class)((F class-function)β·((F family)β§(F set-valued))))(β([F@Variable]:[Class@Type])(([F@Class.Expression] class-function)β·(([F@Class.Expression] family)β§([F@Class.Expression] set-valued)))) | — | Verified (Kernel) |
| 3.33 | Definition | βIs injectiveβ predicate | (β(F:Class)((F injective)β·(((F family)β§(F set-valued))β§β(x:Class)β(y:Class)((((xβDom(F))β§(yβDom(F)))β§(Fx=Fy))β(x=y)))))(β([F@Variable]:[Class@Type])(([F@Class.Expression] injective)β·((([F@Class.Expression] family)β§([F@Class.Expression] set-valued))β§β([x@Variable]:[Class@Type])β([y@Variable]:[Class@Type])(((([x@Class.Expression]βDom([F@Class.Expression]))β§([y@Class.Expression]βDom([F@Class.Expression])))β§([F@Class.Expression][x@Class.Expression]=[F@Class.Expression][y@Class.Expression]))β([x@Class.Expression]=[y@Class.Expression]))))) | — | Verified (Kernel) |
| 3.34 | Definition | βIs a functionβ predicate | (β(f:Class)((f function)β·((f class-function)β§(f set))))(β([f@Variable]:[Class@Type])(([f@Class.Expression] function)β·(([f@Class.Expression] class-function)β§([f@Class.Expression] set)))) | — | Verified (Kernel) |
| 3.35 | Definition | βIs not strictly larger thanβ binary relation | (β(A:Class)β(B:Class)((AβΌB)β·(β(f:Class)(((f class-function)β§(fAβB))β§(f injective)))))(β([A@Variable]:[Class@Type])β([B@Variable]:[Class@Type])(([A@Class.Expression]βΌ[B@Class.Expression])β·(β([f@Variable]:[Class@Type])((([f@Class.Expression] class-function)β§([f@Class.Expression][A@Class.Expression]β[B@Class.Expression]))β§([f@Class.Expression] injective))))) | — | Verified (Kernel) |
| 3.36 | Definition | Class cardinality | (β(K:Class)(|K|=(Onβ©β{a|(aβOn)β§(KβΌa)})))(β([K@Variable]:[Class@Type])(|[K@Class.Expression]|=(Onβ©β{[a@Class.Expression]|([a@Class.Expression]βOn)β§([K@Class.Expression]βΌ[a@Class.Expression])}))) | — | Verified (Kernel) |
| 3.37 | Definition | βIs strictly smaller thanβ binary relation | (β(A:Class)β(B:Class)((AβΊB)β·(Β¬(BβΌA))))(β([A@Variable]:[Class@Type])β([B@Variable]:[Class@Type])(([A@Class.Expression]βΊ[B@Class.Expression])β·(Β¬([B@Class.Expression]βΌ[A@Class.Expression])))) | — | Verified (Kernel) |
| 3.38 | Axiom | Size limitation axiom related statement | (β(X:Class)((XβV)β·(|X|βΊ|V|)))(β([X@Variable]:[Class@Type])(([X@Class.Expression]βV)β·(|[X@Class.Expression]|βΊ|V|))) | — | Verified (Kernel) |
| 3.39 | Definition | βIs hereditaryβ predicate | (β(A:Class)(Hereditary(A)β·(β(B:Class)((BβA)ββ(X:Class)((XβB)β(XβA))))))(β([A@Variable]:[Class@Type])(Hereditary([A@Class.Expression])β·(β([B@Variable]:[Class@Type])(([B@Class.Expression]β[A@Class.Expression])ββ([X@Variable]:[Class@Type])(([X@Class.Expression]β[B@Class.Expression])β([X@Class.Expression]β[A@Class.Expression])))))) | — | Verified (Kernel) |
| 3.40 | Definition | βIs powerfulβ predicate | (β(U:Class)(Powerful(U)β·(β(B:Class)((BβU)β(π«(B)βU)))))(β([U@Variable]:[Class@Type])(Powerful([U@Class.Expression])β·(β([B@Variable]:[Class@Type])(([B@Class.Expression]β[U@Class.Expression])β(π«([B@Class.Expression])β[U@Class.Expression]))))) | — | Verified (Kernel) |
| 3.41 | Definition | βIs pairfulβ predicate | (β(U:Class)(Pairful(U)β·(β(A:Class)β(B:Class)(((AβU)β§(BβU))β({A,B}βU)))))(β([U@Variable]:[Class@Type])(Pairful([U@Class.Expression])β·(β([A@Variable]:[Class@Type])β([B@Variable]:[Class@Type])((([A@Class.Expression]β[U@Class.Expression])β§([B@Class.Expression]β[U@Class.Expression]))β({[A@Class.Expression],[B@Class.Expression]}β[U@Class.Expression]))))) | — | Verified (Kernel) |
| 3.42 | Definition | βIs tightβ predicate | (β(U:Class)(Tight(U)β·(β(B:Class)((BβU)β((BβΊU)β·(BβU))))))(β([U@Variable]:[Class@Type])(Tight([U@Class.Expression])β·(β([B@Variable]:[Class@Type])(([B@Class.Expression]β[U@Class.Expression])β(([B@Class.Expression]βΊ[U@Class.Expression])β·([B@Class.Expression]β[U@Class.Expression])))))) | — | Verified (Kernel) |
| 3.43 | Definition | Singleton set | (β(a:Class)({a}={x|x=a}))(β([a@Variable]:[Class@Type])({[a@Class.Expression]}={[x@Class.Expression]|[x@Class.Expression]=[a@Class.Expression]})) | — | Verified (Kernel) |
| 3.44 | Definition | Unordered pair | (β(a:Class)β(b:Class)({a,b}={x|(x=a)β¨(x=b)}))(β([a@Variable]:[Class@Type])β([b@Variable]:[Class@Type])({[a@Class.Expression],[b@Class.Expression]}={[x@Class.Expression]|([x@Class.Expression]=[a@Class.Expression])β¨([x@Class.Expression]=[b@Class.Expression])})) | — | Verified (Kernel) |
| 3.45 | Definition | Set-theoretic models of natural numbers(TBI) | (Evaluated Rule Definition) | — | Verified (Kernel) |
| 3.46 | Definition | General definition of lists of classes which applicable not only for sets, but for proper classes too(TBI) | (Evaluated Rule Definition) | — | Verified (Kernel) |
| 3.47 | Definition | Ordered pair(Kuratowsky's) | (β(a:Class)β(b:Class)((a,b)={{a,a},{a,b}}))(β([a@Variable]:[Class@Type])β([b@Variable]:[Class@Type])(([a@Class.Expression],[b@Class.Expression])={{[a@Class.Expression],[a@Class.Expression]},{[a@Class.Expression],[b@Class.Expression]}})) | — | Verified (Kernel) |
| 3.48 | Definition | Binary union | (β(A:Class)β(B:Class)((AβͺB)={x|(xβA)β¨(xβB)}))(β([A@Variable]:[Class@Type])β([B@Variable]:[Class@Type])(([A@Class.Expression]βͺ[B@Class.Expression])={[x@Class.Expression]|([x@Class.Expression]β[A@Class.Expression])β¨([x@Class.Expression]β[B@Class.Expression])})) | — | Verified (Kernel) |
| 3.49 | Definition | Binary intersection | (β(A:Class)β(B:Class)((Aβ©B)={x|(xβA)β§(xβB)}))(β([A@Variable]:[Class@Type])β([B@Variable]:[Class@Type])(([A@Class.Expression]β©[B@Class.Expression])={[x@Class.Expression]|([x@Class.Expression]β[A@Class.Expression])β§([x@Class.Expression]β[B@Class.Expression])})) | — | Verified (Kernel) |
| 3.50 | Definition | βIs inductiveβ predicate | (β(X:Class)(Ind(X)β·((β βX)β§β(a:Class)((aβX)β((aβͺ{a})βX)))))(β([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]))))) | — | Verified (Kernel) |
| 3.51 | Definition | The intersection class of all inductive classes is called omega | (β(x:Class)((xβΟ)β·(β(Q:Class)(Ind(Q)β(xβQ)))))(β([x@Variable]:[Class@Type])(([x@Class.Expression]βΟ)β·(β([Q@Variable]:[Class@Type])(Ind([Q@Class.Expression])β([x@Class.Expression]β[Q@Class.Expression]))))) | — | Verified (Kernel) |
| 3.52 | Axiom | βInfinityβ(Ο is a set) | (Ο set)(Ο set) | — | Verified (Kernel) |
| 3.53 | Theorem | Class of all sets is inductive | Ind(V)Ind(V) | — | Verified (Kernel) |
| 3.54 | Theorem | Intersection of all inductive classes is an inductive class itself | Ind(Ο)Ind(Ο) | — | Verified (Kernel) |
| 3.55 | Theorem | Class of all ordinal numbers is inductive | Ind(On)Ind(On) | — | Verified (Kernel) |
| 3.56 | Theorem | Ο is transitive | Tr(Ο)Tr(Ο) | — | Verified (Kernel) |
| 3.57 | Theorem | Ο is ordinal | Ord(Ο)Ord(Ο) | — | Verified (Kernel) |
| 3.58 | Theorem | Ο is in the class of all ordinal numbers(=sets) | (ΟβOn)(ΟβOn) | — | Verified (Kernel) |
| 3.59 | Theorem | βIs cardinalβ predicate | (β(C:Class)(Card(C)β·(β(K:Class)(|K|=C))))(β([C@Variable]:[Class@Type])(Card([C@Class.Expression])β·(β([K@Variable]:[Class@Type])(|[K@Class.Expression]|=[C@Class.Expression])))) | — | Verified (Kernel) |
| 3.60 | Theorem | Ο is cardinal | Card(Ο)Card(Ο) | — | Verified (Kernel) |
| 3.61 | Theorem | On is a cardinal class | Card(On)Card(On) | — | Verified (Kernel) |
| 3.62 | Theorem | Class of all sets is not a cardinal class | (Β¬Card(V))(Β¬Card(V)) | — | Verified (Kernel) |
| 3.63 | Definition | βIs a universeβ predicate | (β(U:Class)((U universe)β·(((ΟβU)β§((Tr(U)β§Hereditary(U))β§(Powerful(U)β§Tight(U))))β§Pairful(U))))(β([U@Variable]:[Class@Type])(([U@Class.Expression] universe)β·(((Οβ[U@Class.Expression])β§((Tr([U@Class.Expression])β§Hereditary([U@Class.Expression]))β§(Powerful([U@Class.Expression])β§Tight([U@Class.Expression]))))β§Pairful([U@Class.Expression])))) | — | Verified (Kernel) |
| 3.64 | Theorem | The class of all sets is a universe | (V universe)(V universe) | — | Verified (Kernel) |
| 3.65 | Axiom | βTarski's axiomβ | (β(x:Class)((x set)ββ(u:Class)(((u universe)β§(xβu))β§(u set))))(β([x@Variable]:[Class@Type])(([x@Class.Expression] set)ββ([u@Variable]:[Class@Type])((([u@Class.Expression] universe)β§([x@Class.Expression]β[u@Class.Expression]))β§([u@Class.Expression] set)))) | — | Verified (Kernel) |
| 3.66 | Theorem | General form of the induction principle on a transitive class | (β(K:Class)β(A:Class)((Tr(K)β§((Kβ©π«(A))βA))β(KβA)))(β([K@Variable]:[Class@Type])β([A@Variable]:[Class@Type])((Tr([K@Class.Expression])β§(([K@Class.Expression]β©π«([A@Class.Expression]))β[A@Class.Expression]))β([K@Class.Expression]β[A@Class.Expression]))) | — | Verified (Kernel) |
| 3.67 | Axiom | Soundness of the theory | (β(π:Fm)((,[]β’π)βeval(π)))(β([π@Variable]:[Fm@Type])((,[]β’[π@Fm.Expression])βeval([π@Fm.Expression]))) | — | Verified (Kernel) |
| 3.68 | Axiom | Soundness of the theory | (β(π:Fm)((,[]β’π)βeval(π)))(β([π@Variable]:[Fm@Type])((,[]β’[π@Fm.Expression])βeval([π@Fm.Expression]))) | — | Verified (Kernel) |
| 3.69 | Definition | Completeness of the theory | (β(π:Fm)(eval(π)β(,[]β’π)))(β([π@Variable]:[Fm@Type])(eval([π@Fm.Expression])β(,[]β’[π@Fm.Expression]))) | — | Verified (Kernel) |
| 3.70 | Axiom | If a formula is derivable in , then it is derivable in | (β(Ξ:Ctx)β(π:Fm)((,Ξβ’π)β(,Ξβ’π)))(β([Ξ@Variable]:[Ctx@Type])β([π@Variable]:[Fm@Type])((,[Ξ@Ctx.Expression]β’[π@Fm.Expression])β(,[Ξ@Ctx.Expression]β’[π@Fm.Expression]))) | — | Verified (Kernel) |
Reflected metatheory in Morse–Kelley and checkable syntactic side conditions.
| Num | Class | Title | Semantic Formula (Morse–Kelley Object Level) | Side Condition Formula | Verification |
|---|---|---|---|---|---|
| 4.01 | Axiom | Instantiation(meta,WIP) | (β(A:Type)β(G:Ctx.Expression)β(π:Fm)β(t:eval(A).Expression)β(v:Variable)(,β¦Gβ§β’βΉ(β(β¦vβ¦:β¦Aβ§)β¦πβ§)β(let β¦vβ§ = β¦tβ§ in β¦πβ§)βΊ))(β([A@Variable]:[Type@Type])β([G@Variable]:[Ctx.Expression@Type])β([π@Variable]:[Fm@Type])β([t@Variable]:[eval([A@Type.Expression.Expression]).Expression@Type])β([v@Variable]:[Variable@Type])(,β¦[G@Ctx.Expression.Expression]β§β’βΉ(β([β¦[v@Variable.Expression]β¦@Variable]:[β¦[A@Type.Expression.Expression]β§@Type])β¦[π@Fm.Expression]β§)β(let β¦[v@Name.Expression]β§ = β¦[t@Class.Expression.Expression]β§ in β¦[π@Fm.Expression]β§)βΊ)) | — | Verified (Kernel) |
| 4.02 | Axiom | Generalisation(meta,WIP) | (β(A:Type)β(Ξ:Ctx)β(π:Fm)β(v:Variable)((Β¬(Enc(β¦vβ¦)βCtx.FV(Ξ)))β((,Ξβ’π)β(,Ξβ’βΉβ(β¦vβ¦:A)β¦πβ§βΊ))))(β([A@Variable]:[Type@Type])β([Ξ@Variable]:[Ctx@Type])β([π@Variable]:[Fm@Type])β([v@Variable]:[Variable@Type])((Β¬(Enc([β¦[v@Variable.Expression]β¦@LCEWIP])βCtx.FV([Ξ@Ctx.Expression])))β((,[Ξ@Ctx.Expression]β’[π@Fm.Expression])β(,[Ξ@Ctx.Expression]β’βΉβ([β¦[v@Variable.Expression]β¦@Variable]:[[A@Type]@Type])β¦[π@Fm.Expression]β§βΊ)))) | — | Verified (Kernel) |
| 4.03 | Inference Rule | CoNecessitation(meta,WIP) | (β(Ξ:Ctx)β(π:Fm)((,[]β’βΉ,Ξβ’πβΊ)β(,Ξβ’π)))(β([Ξ@Variable]:[Ctx@Type])β([π@Variable]:[Fm@Type])((,[]β’βΉ,[Ξ@Ctx.Expression]β’[π@Fm.Expression]βΊ)β(,[Ξ@Ctx.Expression]β’[π@Fm.Expression]))) | — | Verified (Kernel) |
| 4.04 | Definition | Quantifier βuniqueβ(meta,WIP) | (β(π:Fm)((!(z:Class)β¦πβ§)β·(β(x:Class)β(y:Class)((β¦π[(x:Class)/βΉzβΊ]β§β§(let z = y in β¦πβ§))β(x=y)))))(β([π@Variable]:[Fm@Type])((!([z@Variable]:[Class@Type])β¦[π@Fm.Expression]β§)β·(β([x@Variable]:[Class@Type])β([y@Variable]:[Class@Type])((β¦[π@Fm.Expression][([x@Class.Expression.Expression]:Class)/βΉzβΊ]β§β§(let z = [y@Class.Expression] in β¦[π@Fm.Expression]β§))β([x@Class.Expression]=[y@Class.Expression]))))) | — | Verified (Kernel) |
| 4.05 | Definition | Quantifier βexists and uniqueβ(meta,WIP) | (β(π:Fm)(,[]β’βΉ(β!(x:Class)β¦πβ§)β·((β(x:Class)β¦πβ§)β§!(x:Class)β¦πβ§)βΊ))(β([π@Variable]:[Fm@Type])(,[]β’βΉ(β!([x@Variable]:[Class@Type])β¦[π@Fm.Expression]β§)β·((β([x@Variable]:[Class@Type])β¦[π@Fm.Expression]β§)β§!([x@Variable]:[Class@Type])β¦[π@Fm.Expression]β§)βΊ)) | — | Verified (Kernel) |
| 4.06 | Axiom | Class comprehension axiom schema(meta,WIP) | (β(π:Fm)β(x:Name)β(k:Class.Expression)(FFI((k:Class),βΉxβΊ,(π:Bool))β(,[]β’βΉ(β¦kβ§β{β¦xβ¦|β¦πβ§})β·((β¦kβ§ set)β§(let x = β¦kβ§ in β¦πβ§))βΊ)))(β([π@Variable]:[Fm@Type])β([x@Variable]:[Name@Type])β([k@Variable]:[Class.Expression@Type])(FFI(([k@Class.Expression.Expression]:Class),βΉ[x@Name.Expression]βΊ,([π@Fm.Expression]:Bool))β(,[]β’βΉ(β¦[k@Class.Expression.Expression]β§β{[β¦[x@Variable.Expression]β¦@Class.Expression]|β¦[π@Fm.Expression]β§})β·((β¦[k@Class.Expression.Expression]β§ set)β§(let [x@Name.Expression] = β¦[k@Class.Expression.Expression]β§ in β¦[π@Fm.Expression]β§))βΊ))) | — | Verified (Kernel) |
Goedel-Loeb provability logic and Second Incompleteness formalized over Robinson arithmetic Q and base class theory T.
| Num | Class | Title | Semantic Formula (Morse–Kelley Object Level) | Side Condition Formula | Verification |
|---|---|---|---|---|---|
| 5.01 | Theorem | LΓΆb's theorem(WIP) | (β(π:Fm)(,[]β’βΉ(,[]β’βΉ(,[]β’π)ββ¦πβ§βΊ)β(,[]β’π)βΊ))(β([π@Variable]:[Fm@Type])(,[]β’βΉ(,[]β’βΉ(,[]β’[π@Fm.Expression])ββ¦[π@Fm.Expression]β§βΊ)β(,[]β’[π@Fm.Expression])βΊ)) | — | Verified (Kernel) |
| 5.02 | Theorem | GΓΆdel's second incompleteness theorem(WIP) | (,[]β’βΉ(Β¬(,[]β’βΉβ₯βΊ))βΒ¬(,[]β’βΉΒ¬(,[]β’βΉβ₯βΊ)βΊ)βΊ)(,[]β’βΉ(Β¬(,[]β’βΉβ₯βΊ))βΒ¬(,[]β’βΉΒ¬(,[]β’βΉβ₯βΊ)βΊ)βΊ) | — | Verified (Kernel) |