Object Membership
– Basic Structure

An abstract structure is described which provides a general model for the innermost core of object-oriented programming and modelling. The structure is called basic structure of ϵ and is introduced in the signature (O, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ) with a single sort O of objects. • ϵ is the object membership relation, an indirect counterpart to set membership. • ϵ¯⁽*⁾ is a left-infinite sequence …, ϵ¯-1, ϵ¯0, ϵ¯1 of relations, whose 0-th member is – the inheritance relation, corresponding to inclusion between sets. The 1-indexed member is the power membership relation ϵ¯ which, if .ec is total, equals the composition (.ec) () (in general, ϵ¯ is an abstraction of this composition). • r is the inheritance root, a distinguished object containing all objects, including r itself, as members in ϵ, thus playing the role of the universal set. • .ec is the powerclass partial map, corresponding to a relativized powerset operator. • .ɛɕ is the primary singleton partial map, corresponding to set membership between non-singleton sets and singleton sets.

As a key characteristics induced by the structure, each object is assigned a rank between 0 and a fixed limit ordinal ϖ. Objects with rank ϖ are unbounded, the remaining ones are bounded. For unbounded objects x, the images of {x} under ϵ and ϵ¯ are coincident. Therefore, object membership is formed as the union

where is the domain-restriction of ϵ to bounded objects.

It is shown that every basic structure is a substructure of an (ϖ+1)-superstructure and thus can be embedded in the von Neumann universe of sets. The inheritance root r appears as the ϖ-th cumulation of urelement-like sets. The above equality for object membership is expressed as

Preface

Author
Ondřej Pavlata
Jablonec nad Nisou
Czech Republic
Document date
Initial releaseMarch 12, 2015
Last major release March 12, 2015
Last updateAugust 21, 2016
(see Document history)
PDF Version
A PDF version of this document is available via the following link: However, the HTML version is considered primary and can be more up-to-date.
Warning
This document has been created without any prepublication review except those made by the author himself.
Membership glyphs
This document uses HTML entities to display mathematical symbols. In particular, there are multiple glyphs used for different relation symbols of membership. Best readability is achieved when the sequences of symbols from the following two lines look (almost) identically.
(PNG images)
ϵ ϶ (HTML entities)

Table of contents

Introduction

The standard Zermelo-Fraenkel set theory with the axiom of choice (ZFC) can be viewed as a one-sorted structure (𝕌, ) where 𝕌 is the universal class of all sets and is the relation symbol of set membership, the only non-logical symbol of the original language of ZFC. Virtually all texts about set theory introduce a definitional extension that includes the following symbols (with / / having alternatives, e.g. 0 / / ): where is a relation symbol of set inclusion, is a constant symbol for the empty set, and are unary function symbols for powerset and union, respectively, , and are binary function symbols for difference, union and intersection, respectively, and is a unary partial function symbol for set intersection. There are also composite function symbols for enumerated sets and tuples that use curly brackets and parentheses, respectively: In particular, {x} is the singleton of x and (x,y) is the ordered pair of x and y having x as the first coordinate.

All the additional symbols denote distinguished sets or relations between sets (considering functions as right-unique relations) that are implicitly given by . The uniqueness of the definition of , (x), x y, x, , x y, {x} or (x,y) for given sets x, y as well as the antisymmetry of is ensured by the extensionality axiom which says that sets x, y are equal if and only if they have the same members:

In another words, a set is identified by its members. For instance, the set 6() (the 6-th application of the powerset operator to the empty set which is the partial von Neumann universe of rank 6) is given by its 265536 members. []

Let us single out the four relations between sets which are referred to by the symbols involved in the following two equivalences. For every sets x, y,

The 2x2 core of set theory
x (y) x y,
x y {x} y.
That is, the singled out relations are (1) set membership (), (2) set inclusion (), (3) the powerset map (x (x)) and (4) the singleton map (x {x}). Note that (3) and (4) are functional subrelations of . The distinction of (1)–(4) can be made in two steps:
  1. Single out and as the two most fundamental relations of set theory.
  2. Single out and x {x} as the two fundamental maps that provide a connection between and .
Observe that apart from the equality symbol = (and apart from symbols based on or like e.g. , or ) there is no obvious third most fundamental relational symbol of set theory. We can therefore regard (1)–(4) as a core definitional extension, the 2x2 core of set theory.

This document shows that the above 2x2 core has an abstract counterpart that can be regarded as the core of object technology. Most object-oriented programming languages (e.g. Java, C++, Python, CLOS or Perl) or ontology languages (e.g. RDF Schema or OWL) support just and and usually call the counterpart relations instance-of and inheritance, respectively. However, there are significant examples of programming languages which support links between objects that correspond to the powerset map or to its inverse []:

There are also examples of languages that support the singleton map: Dylan, Julia and Scala.
The objective
The objective of this document is to provide a connection between object technology and set theory according to the following diagram:
The connection is established through the family of basic structures (shown by the small region labelled with the ϵ symbol) which encompass abstract counterparts of the four distinguished set-theoretic relations. It is shown how
Main correspondence
By simplification, main correspondence between the 2x2 core of set theory and the core of object technology can be expressed as follows.
(Zermelo-Fraenkel) For every sets x, y
(set membership) ϵ (object membership)
(set inclusion) (inheritance)
(powerset) (x) x.ec (powerclass)
(singleton set) {x} x.ɛϲ (singleton)
x (y) x y,
x y {x} y or (x) y
(Morse-Kelley) For every classes x, y (Object technology) For every objects x, y
x є (y) x y,
x є y {x} y or (x) y
x ϵ y.ec x y,
x ϵ y x.ɛϲ y or x.ec y
That is, ϵ, , .ec and .ɛϲ are the abstract counterparts of set membership, set inclusion, powerset and singleton set maps, respectively. The correspondence is obtained via the following steps.
  1. Adjust the equivalence for x y by adding or (x) y on the right side. Since in ZFC, {x} (x) for every set x, the adjusted equivalence is equivalent to the original one.
  2. Switch to Morse-Kelley set theory [] – change the universe of discourse from sets to classes. Accordingly,
  3. Change the universe from classes to objects and introduce ϵ , , .ec and .ɛϲ as abstractions of є, , and x {x}, respectively.

Notes:

Basic structures from superstructures
Basic structures arise by abstraction of suitable partial universes of well-founded sets. A brief specification of basic structures is provided via the following abstraction steps.
(a)
(b)
  1. Start with an (ϖ+1)-superstructure (O, ). Let ϖ be a limit ordinal and let be a well-founded relation on a set O of objects such that (1) r(O), the rank of O w.r.t. , equals ϖ+1 and (2) for every non-empty subset X of O satisfying r(X) ϖ there is a unique object x whose pre-image under equals X.

    The (a) diagram on the right partially shows a restriction of an (ϖ+1)-superstructure to objects whose rank is less than 3 and thus form the third stage. Objects are depicted as circles and are aligned into columns according to their rank. There are just two objects with zero rank – the terminals which form the first stage (ground stage). The relation is represented by blue arrows.

  2. Make a definitional extension of (O, ). Define r, , .ec and .ɛϲ as follows. Use X. and x. for the pre-image of sets X and {x} of objects under . In particular, .ɛϲ is a distinguished subrelation of and so is the restriction of .ec to O.. Objects from the range of .ec (resp. of .ɛϲ) are powerclasses (resp. singletons). In the (a) and (b) diagrams, .ec is represented by horizontal blue arrows and .ɛϲ by blue arrows pointing to ◉ which indicate singletons. The (b) diagram shows the inheritance relation (green arrows, upwards directed) in the reflexive transitive reduction. The reduction of blue arrows in (b) is based on the () = (.ɛϲ) () equality (i.e. equals the composition of the singleton map with inheritance).
  3. Define metaobject structures as abstraction of (O, , r, .ec, .ɛϲ). Use the following definitional extension for the axiomatization. Let , ϵ¯, ϵ and ϵ-1 be relations between objects such that
    () = (.ɛϲ) () is the bounded membership,   (x yx.ɛϲ y)
    (ϵ¯) = (.ec) () is the power membership,   (x ϵ¯ yx.ec y)
    (ϵ) = () (ϵ¯) is the (object) membership,
    (ϵ-1) = () (.ce) is the anti-membership, with .ce denoting the inverse of .ec.
    For every integer i, let
    (ϵi) (resp. (ϵ¯i)) be the i-th relational composition of ϵ (resp. of ϵ¯) with itself whenever i > 0,
    (ϵi) = (ϵ¯i) be the -i-th relational composition of ϵ-1 with itself whenever i < 0, and let
    (ϵ0) = (ϵ¯0) = ().
    Define the rank function .d from O to ϖ+1 in terms of r and ϵi. In general, .d differs from the -rank. Adapt the nomenclature of objects to .d. Objects with zero rank are terminal(s), the other non-terminal(s), objects x whose rank is not maximal are bounded, the other (such that x.d = ϖ) are unbounded. As a particular consequence of the definition of .d, objects that are non-well-founded in ϵ are unbounded. In the axiomatization, assert that the singleton map .ɛϲ is defined exactly for bounded objects.
  4. Define basic structures as abstraction of (O, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ) where ϵ¯⁽*⁾ is the left-infinite sequence { ϵ¯i | i , i 1 } and .ɛɕ stands for the difference (.ɛϲ) (.ec). Define the rank .d of objects by the same prescription as for metaobject structures and preserve the nomenclature. Define as the domain restriction of ϵ to bounded objects. Obtain .ɛϲ back from .ɛɕ so that In contrast to metaobject structures, allow .ec and .ɛɕ to be arbitrarily partial, possibly empty. As a consequence, a basic structure might contain only finitely many objects, with O = {r} being the minimum case.

    For a natural i, let .ec(i) be the i-th composition of .ec with itself, .ec(0) being the identity on O. Subsequently, let .ec(-i) be the inverse of .ec(i). In the axiomatization, assert the following:

    1. ϵ¯ is a subrelation of ϵ.
    2. Powers of ϵ¯ compose transitively: the composition of ϵ¯i with ϵ¯j is a subrelation of ϵ¯i+j.
    3. Powers of ϵ compose transitively if they are positive on the left side: (ϵ) (ϵi) is a subrelation of ϵ1+i.
    4. Powers of ϵ¯ are antisymmetric. The intersection of ϵ¯i with its inverse equals .ec(i).
    5. Objects from O.ϵ (the range of ϵ) are inheritance descendants of r.
    6. Every object is in the domain of ϵ, i.e. O = O.϶.
    7. Singletons and terminals x are minimal w.r.t. (ϵ-i) (϶¯i) for every natural i and power members: x.ϵ = x.ϵ¯.
    8. The .ɛɕ map is an injective range-restriction of ϵ and is disjoint with ϵ¯. Moreover, if x.ɛɕ = y then
      • u ϵ-i xu ϵ1-i y for every object u and every natural i.
    9. Reserved.
    10. Every object x has a finite metalevel index, i.e. x is related to r in only finitely many negative powers of ϵ.
    11. Unbounded objects x are power members: x.ϵ = x.ϵ¯.
Complete structure
The above mentioned (ϖ+1)-superstructures, in an appropriate definitional extension, are themselves a special case of basic structures, called complete structures. Main characterization of basic structures w.r.t. set theory can be therefore obtained by comparing S = (O, ) with (𝕌, ). The following observations can be made:
  1. In contrast to 𝕌 which is a proper class, O is a set. This is because basic structures are primarily meant to provide a general model of the core part of object technology based on set theory.
  2. There can be more than one object x in the ground stage O O. of S (i.e. such that x. = ). As a consequence, S is only weakly extensional. Ground stage objects are urelements.

    Note: Objects from the ground stage are exactly the terminal objects of S. For complete structures, we tend to use this term less frequently than in the general case.

  3. There are unbounded objects, most notably r, that have maximum rank, ϖ, and therefore do not appear in the domain of .
  4. There is no counterpart to , the empty set. Ground stage objects are incomparable in the strict inheritance < to any object.
  5. On the other hand, the inheritance root r being a universal container of all bounded objects has no counterpart in (𝕌, ).
  6. The powerclass map .ec deviates from the powerset operator in two respects. The second property can be expressed as x.mli + 1 = x.ec.mli and is a consequence of the missing empty set. In contrast, the length of the shortest -path from the ground stage of (𝕌, ) to (x) equals constantly 1 for every set x (since (x) by definition of and is an element (the only element) of the ground stage).
  7. The singleton map .ɛϲ is strictly partial, having the same domain as . As a further consequence of the missing empty set, .ɛϲ is partially coincident with .ec (see the diagrams above for the common part of .ec and .ɛϲ in the third stage): (In (𝕌, ),   (x) = {x}x = .)
The observations can be summarized into the following characterization.
  1. Smallness. Although used for modelling of largeness, basic structures are themselves small by having a set (the set O of objects) as the universe of discourse. Similarly to club sets [], largeness of objects is expressed via their unboundedness relative to a limit ordinal.
  2. Presence of unbounded objects. There are objects that are not in the domain of .
  3. Presence of urelements (atoms, terminals). There are possibly multiple objects that are not in the range of .
  4. Absence of an empty set object. There is no distinguished object outside the range of that would correspond to the empty set.
Completion
A major part of this document consists of showing that every basic structure (as specified by the axioms) is a substructure of some complete basic structure. That is, every basic structure can be faithfully embedded into a complete structure. Or, concisely, every basic structure has a completion.
The completion is established gradually in the following steps:
  1. Rank pre-completion. Attach a set X of ϖ new members to each object x that is (a) not well-founded in ϵ, (b) not -ranked (i.e. the rank x.d differs from r(x), the -rank of x), and (c) not a powerclass (i.e. x is primary). The members are attached in such a way that (X, ϵ, ) is isomorphic to (ϖ, , ).
  2. Powerclass completion. Append an infinite powerclass chain to each object for which the powerclass is not defined.
  3. Singleton completion. Append an infinite singleton chain to each bounded object for which the singleton is not defined. Technically, this is performed in two steps by first adding just the missing primary singletons and subsequently performing the powerclass completion.
  4. Extensional pre-completion. To every object x that does not satisfy certain consistency conditions attach two powerclass chains each of which starts in a terminal object. The resulting structure is pre-complete, that is, In particular, the structure is fully determined by bounded membership using the prescriptions already introduced for complete structures (see Basic structures from superstructures).
  5. Cumulative embedding into an (ϖ+1)-superstructure. Let S = (O, ) be the pre-complete structure to be embedded. Choose an (ϖ+1)-superstructure V = (V, ) so that its ground stage V1 has the same cardinality as the set T of terminal objects of S. Then the requested embedding map is obtained as a limit of a transfinite sequence 0, 1, …, ϖ = of maps from O to V defined as follows:
    1. The restriction of i to terminals is for every i identical and forms a bijection between T and V1.
    2. The restriction of i to the set O. of non-terminal objects x is recursively defined by
      x.ν0. = x.¯0.ec. x.0 (where ¯ equals () (ϵ¯)),
      x.νi. = x.϶¯i-1.ec. x.0 if i is a successor ordinal,
      x.νi. = { x.νk. | k < i } if i is a limit ordinal.
    Note that the definition of 0 is by the well-founded recursion on (O, ), whereas the definition of i for i > 0 uses transfinite recursion over i.
Embedding into the von Neumann universe
The final embedding of (ϖ+1)-superstructures (and thus of basic structures) into the von Neumann universe of well-founded sets is established via powerset cumulation. For every ordinal number α let α be a map between sets defined using transfinite recursion by
α(x) = x {((β(x)) {}) | β < α }   (the α-th cumulation of x).
Equivalently, 0(x) = x, 1(x) = x ((x) {}), α+1(x) = 1(α(x)), α(x) = {β(x) | β < α } with the last equality being satisfied for every limit α. Consequently, partial von Neumann universes are cumulations of {}, i.e. for every ordinal α, (Note that the 1+-shift only makes a difference for finite ordinals α.) Given an (ϖ+1)-superstructure (O,) to be embedded into (𝕌,) as V = (V,) it is sufficient to choose the ground stage V1 of V to be a set such that (a) all elements of V1 are singletons, (b) the cardinality of V1 equals the cardinality of O O., and (c) V1 is a subset of 𝕍i+1 𝕍i for some suitably large ordinal i (so that each element of V1 has equal rank, namely i). The V set is then obtained by The inheritance root of V equals ϖ(V1) and is simultaneously the set of bounded objects of V. Correspondence between constituents of a basic structure and their set-theoretic counterparts is provided by the Set representation theorem.

Sample structure

The following diagram shows a sample basic structure of object membership. The structure is built from 4 relations between objects: The () relation represented by blue arrows is also reduced. It is the minimum relation R such that R () = (ϵ) and (.ec) R. (The minimum relation S satisfying just S () = (ϵ) has two pairs less than (): the horizontal arrows starting at c and e.ec.) Note that since R () = (ϵ) for some relation R, it follows, due transitivity and reflexivity of , that (ϵ) () = (ϵ) (the subsumption rule).
… class (bounded / unbounded)
… terminal object
… powerclass
… singleton (primary / powerclass)
(ϵ) (ϵ¯)
x y   iff   x y
x ϵ y   iff   x y
If x y then:
  x.ec = y   iff   is horizontal
  x.ɛɕ = y   iff   y is a primary singleton
  x.ɛϲ = y   iff   y is a singleton
x. = {a | a x} descendants of x
x.϶ = {a | a ϵ x} members of x
x ϵ¯ y   iff   x. y.϶
x y   iff   x ϵ y and x is bounded
O objects   = T C O.ec O.ɛɕ
O.ec powerclasses
O.pr primary objects   = T C O.ɛɕ
T terminal objects   = O r.
C classes   = O.pr (T O.ɛɕ)
O. bounded objects
O.ɛɕ primary singletons
O.ɛϲ singletons   = (T.ec O.ɛɕ).ec
H helix objects   = r.ϵ
R reduced helix   = r.ec
r inheritance root
Objects form a set denoted O. Objects are either powerclasses or primary according to whether they appear in the image of .ec or not, respectively. Components of .ec are powerclass chains. Each powerclass chain starts in a primary object. (A chain may consist of just its primary object.) Correspondingly, each object x has its primary object x.pr.

An object x is either unbounded or bounded according to whether x appears in a cycle of ϵ or not, respectively. (Note: This characterization of boundedness is applicable due to the finiteness of the structure, see Speciality of the sample.) That is, unbounded objects x are those such that x ϵi x for some natural i > 0, where ϵi is the i-th composition of ϵ with itself. Boundedness is preserved along powerclass chains: An object x is (un)bounded iff the primary object x.pr is (un)bounded. In the sample structure, the primary unbounded objects are displayed in blue. There is a distinguished unbounded object, denoted r and called the inheritance root. It is the highest unbounded object in inheritance. In fact, r is the top of O.ϵ, that is, the common ancestor of all objects that have any members. Simultaneously, r is a common container of all objects, r.϶ = O, including itself, r ϵ r. In addition, there are two distinguished sets of unbounded objects.

Observe the following inclusion chain: {r} R H O.ϵ. Moreover, all 4 sets have the same descendants – that is, r. == O.ϵ.. Objects that are not descendants of r are terminal(s). All terminal objects are primary. Objects that are neither terminal nor powerclasses nor primary singletons are classes. The sets of terminals and classes are denoted T and C, respectively, so that we can express a fundamental partition of objects into 4 sets:
Power membership
ϵ¯
ϵ, , r, .ec, .ɛɕ
ϵ-1
ϵ-2
ϵ-3
The four definitory relations , ϵ, .ec and .ɛɕ of the sample structure are among constituents of the signature of basic structures according to the diagram on the left. In particular, the inheritance relation, , appears as the 0-th member of the infinite sequence
ϵ¯⁽*⁾ = { ϵ¯i | i , i 1 },
of relations between objects, where (ϵ¯) = (ϵ¯1) is the power membership relation, and () = (ϵ¯0). As a definitional extension, we let (ϵi) = (ϵ¯i) for every i 0. Moreover, for i > 0, we let ϵi (resp. ϵ¯i) be equal to the i-th relational composition of ϵ (resp. of ϵ¯) with itself.

In the particular case of the sample structure, we assume that ϵ¯ and ϵ-i, i , are derived from , ϵ, .ec and .ɛɕ as follows:

In the sample structure, the difference (ϵ) (ϵ¯) contains exactly 8 membership pairs, indicated by blue arrows with a highlighted background. (For instance, (d,f) (ϵ¯) since n.ec d. f.϶.)
The ϵ-diamond
The diagram on the right shows significant subrelations of ϵ (note that .ec and .ɛɕ are another significant subrelations of ϵ): The point of the diagram is that the relations form a lattice w.r.t. inclusion, that is, in addition to the (not much significant) definition of ¯ we also have which is asserted by the following axioms of basic structures:
(b~1) (ϵ¯) (ϵ),
(b~11) x.ϵ = x.ϵ¯ for every unbounded object x.
Specialities of the sample
Although the sample structure appears to be fairly wild, it does not expose all features allowed by the general definition. In particular, the sample possesses the following special properties.
Powerclasses and singletons
In addition to the powerclass map, .ec, there is a second definitory constituent of the structure that is a partial map between objects: the primary singleton map, .ɛɕ. This map in turn appears to be just a difference (.ɛϲ) (.ec) where The derived partial map .ɛϲ is the singleton map. Objects from the image O.ɛϲ are singletons. The following table shows the main properties of .ec and .ɛϲ in comparison.
y is the powerclass of x, x.ec = y y is the singleton of x, x.ɛϲ = y
y is the primary singleton of x, x.ɛɕ = y
(a) x is the highest member of y x. = y.϶ {x} = y.϶ x is the only member of y (a')
(b) y is the lowest power container of x x.ϵ¯ = y. x.ϵ = y. y is the lowest container of x (b')
Note that although conditions (a) and (b) (resp. (a') and (b')) define a one-to-one relation between objects, the .ec (resp. .ɛɕ) map is given explicitly. For example, in the sample structure,
Metalevels
In the diagram of the sample structure, objects are grouped into columns in a correspondence to metalevels. The metalevel index of an object x is denoted x.mli and equals the number of ancestors of x that belong to R, the reduced helix. By (b~10), x.mli is asserted to be finite even if R is infinite. The set T of terminal objects is the 0-th metalevel. For i > 0, the top of the i-th metalevel is the i-th element from R, starting with r as the 1-st object.

Axioms of basic structures assert that when going alongside , ϵ, .ec or .ɛɕ there are the following limitations about the possible increment of the metalevel index:

If x y then y.mli - x.mli 0,
if x ϵ y then y.mli - x.mli 1,
if x.ec = y then y.mli - x.mli = 1,
if x.ɛɕ = y then y.mli - x.mli = 1.
Rank
In addition to the metalevel index, each object x has defined a rank, denoted x.d. For the purpose of the introductory sample, we provide a simplified definition of .d. Let E = {i | i } be a system of relations between objects generated by the following rules. Equivalently, for some natural n > 0, objects x0, x1, …, xn and signs i1, …, in {-1,0,1} such that i1 + ⋯ + in = i and where We might call the above sequence x0, x1, …, xn of objects an i-path. If x i y for an integer i, then x is an i-path member of y. Due to the limitations for the possible increment of metalevel index we obtain the following implication for every integer i:
Now the rank of an object x is defined by Informally, the rank maximalizes the metalevel increment along (inverted) i-paths. The diagram on the right shows such a maximalizing path for the a object from the sample structure. The values (in brown) show the contribution of each arrow (ϵ or ) to the rank. The overall increment is 7 so that a.d = a.mli + 7 = 9.

Note: In general, it is possible to have maximalizing paths with some horizontal (i.e. .ec) arrows oriented in opposite direction.

Observe that since x 0 x, the rank is at least so big as the metalevel index. Since (ϵi) (i) for every i > 0, the rank of every unbounded object x (such that x ϵi x for some i > 0) is infinite, that is, x.d = ω. This is in contrast to the metalevel index which is always finite. Moreover, we have the following classification of objects according to their rank:

Similarly to the metalevel index, the powerclas map increases the rank of bounded objects exactly by 1.

Preliminaries

Some familiarity with elementary algebra, order theory and set theory is assumed. This involves such notions as structure, substructure, sort, generating set/structure, (partial) function, relation, domain, range, restriction, extension, injectivity, reflexivity, transitivity, antisymmetry, monotonicity, isomorphism, or closure operator.

Relations are regarded as sets (or in some cases as set-theoretic classes) of ordered pairs (x,y). The domain (resp. range) of a relation R is the set of all x (resp. y) such that (x,y) is from R for some y (resp. x). Functions (maps) are regarded as functional (left-unique) relations. We speak about a total (resp. partial) function on a set X if the function's domain equals X (resp. is a subset of X).

Main notational conventions
Most set-theoretic symbols have been described in the introduction. We also use the symbol for disjoint union of sets, i.e. x y = z iff x y = z and x y = . We use set-builder notation with a vertical bar so that e.g. {x | x y} is the set of all x such that x y.

The symbol is used for relational composition. Inscribed triangle indicates the left-to-right direction, so that R S is the set of all pairs (x,z) such that there is a y such that (x,y) R and (y,z) S.

We mostly use dot notation for function application. The expression x.f refers to the application of f to x (the value of f at x) whenever f is a map and it is asserted that x is from the domain of f. In contrast, the expression X.f (with an uppercase X on the left side instead of the lowercase x) refers to the image of the set X under f, i.e.

We let the dot symbol . be the initial character of map names whenever the dot notation is used for the map application. According this rule, the f function above would be referred to by .f. If .f and .g are functions then .f.g refers to the composition (.f) (.g). Furthermore, we let the dot notation be applicable for images of relations. If ϵ is a relation then X.ϵ is the image of X under ϵ and x.ϵ is a shorthand of {x}.ϵ. If in addition, .f is a function then x.ϵ.f refers to the image of x under (ϵ) (.f).

Symbols / / indicate total / partial / injective maps, respectively.

Ordinal numbers
Let On denote the proper class of ordinal numbers (shortly ordinals). According to the standard definition, α belongs to On iff α is a transitive set strictly well-ordered by . Following standard conventions we will use special symbols for set operations on ordinals. In particular, for ordinals α, β and a set X of ordinals, If β is a successor ordinal then β-1 refers to the unique ordinal of which β is a successor. We will also sometimes use the symbol (and its variants <, and >) for relations between sets of ordinal numbers (cf. Polars of ). If X, Y and {α} are sets of ordinals then
X Y   iff   α β for every α X and β Y,
α X   iff   {α} X.
Note that this introduces ambiguity of the meaning of X Y since X or Y may themselves be ordinals. A disambiguation should be clear from the context.
Cardinal numbers
We assume axiom of choice and use the von Neumann cardinal assignment. The cardinality of a set X (notation: card(X)) is the least ordinal α such that there is a bijection between X and α. Cardinal numbers (shortly cardinals) are ordinal numbers α such that card(α) = α.
Natural numbers
We regard natural numbers as the finite ordinal numbers 0, 1, 2, …. We let the set of natural numbers be denoted by either or by ω according to which symbol is considered appropriate in the given context.
Integers
We denote the set of integer numbers and let the set of natural numbers be coincident with non-negative integers. The binary operation of addition is extended by
Well-foundedness
For a relation ϵ on a set X, an element x X is well-founded in ϵ if x is not a member of an infinite descending chain in ϵ, i.e. if there is no infinite chain of the form A relation ϵ on a set X is well-founded if all elements x X are well-founded in ϵ. Assuming the axiom of choice, this is equivalent to the condition that every non-empty subset Y X contains an element y that is minimal in (Y,ϵ), i.e. there is no u from Y such that u ϵ y.
Rank
For a well-founded relation on a set X, the rank function of (alternatively, the -rank) is a map r() from X to ordinal numbers such that for every x X, By well-founded recursion, there is exactly one such map. Obviously, r(x) = 0x is minimal in . Moreover,
Limited rank
Assume that ϵ is a (not necessarily well-founded) relation on a set X and let ϖ be a limit ordinal. Define recursively a function rϵ : X ϖ+1 by
rϵ(x) = ϖ sup {rϵ(a) + 1 | a ϵ x } if x is well-founded in ϵ,
rϵ(x) = ϖ otherwise.
For x X, we call rϵ(x) the ϖ-limited rank of x (w.r.t. ϵ).
Fixing a limit ordinal ϖ
If not stated otherwise we will further assume that a fixed limit ordinal ϖ is given in the context. This ordinal number will be the highest rank of objects under consideration. The choice of the symbol indicates that the first limit ordinal ω is considered to be sufficient with respect to object technology.

Ordinal numbers less than ϖ are bounded, the remaining (including ϖ itself) are unbounded. More generally, a set X of ordinal numbers is bounded or unbounded according to whether sup(X) is bounded or unbounded, respectively.

 

Basic structure

This section provides a formal definition of basic structures. Before stating the axioms we first introduce the family of ϵ5-structures which defines the language of basic structures.

Note: The family of basic structures can be viewed as a generalization of metaobject structures introduced later. The generalization consists of

Moreover, because of the incompleteness, the singleton map .ɛϲ is not taken as the definitory constituent. Instead, the primary singleton map, .ɛɕ, is introduced, which stands for the difference (.ɛϲ) (.ec). As a consequence, the existence of x.ec and that of x.ɛɕ for a given object x are independent of each other.
ϵ5-structure
ϵ2ϵ¯2
ϵ
ϵ¯
ϵ-1
ϵ-2
By an ϵ5-structure we mean a structure S = (O, ϵ⁽*⁾, ϵ¯⁽*⁾, r, .ec, .ɛɕ) where The remaining two definitory constituents are partial maps O O (i.e. functional relations between objects): The only additional constraint which are ϵ5-structures subject to is the following condition:
(b~0) For every positive natural i,   (a) (ϵ) (ϵi) = (ϵ1+i),   (b) (ϵ¯) (ϵ¯i) = (ϵ¯1+i).
That is, for every positive natural i,   ϵi (resp. ϵ¯i) is the i-th relational composition of ϵ (resp. of ϵ¯) with itself. Consequently, we consider the bi-infinite sequence ϵ¯⁽*⁾ to be a definitional extension of the left-infinite sequence { ϵ¯i | i , i 1 } and the bi-infinite sequence ϵ⁽*⁾ to be obtainable by a definitional extension of (ϵ, ϵ¯⁽*⁾), so that we usually drop the wildcard superscript from ϵ⁽*⁾ in the signature.

The following definitions are (almost) sufficient to state the axioms of basic structures.

Basic structure
By a basic structure (of ϵ) we mean an ϵ5-structure S = (O, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ) satisfying the following axioms:
(b~1) (ϵ¯) (ϵ).
(b~2) (ϵ¯i) (ϵ¯j) (ϵ¯i+j)   for every integer i, j.
(b~3) (ϵ) (ϵi) (ϵ1+i)   for every integer i.
(b~4) (ϵ¯i) (϶¯-i) = .ec(i)   for every integer i.
(b~5) The inheritance root r is the top of O.ϵ w.r.t. .
(b~6) Every object x has a container, x.ϵ .
(b~7) For every object x from T O.ɛɕ and every natural i,   (a) x.϶-i = {x}.ec(i), (b) x.϶-i.ϵ = x.϶-i.ϵ¯.
(b~8) If x.ɛɕ = y then: (a) {x} = y.϶, (b) x.ϵi = y.ϵi-1 for every i 1, (c) (x,y) (ϵ¯).
(b~9) Reserved for the non-member union map.
(b~10) For every object x, the metalevel index x.mli is finite.
(b~11) For every object x,   x.d = ϖ   →   x.ϵ = x.ϵ¯.     (That is, every unbounded object is a power member.)

First observations:

  1. The (b~2) condition has three important special cases: Using (b~0) (b~1) and (b~3) it follows that (b~2) is equivalent to:  
  2. Condition (b~3) has the subsumption of ϵ as an important case:   (ϵ) () (ϵ). Moreover, it follows from (b~0) that (b~3) can be equivalently stated as any of (ⅰ) or (ⅱ):
  3. For i = 0 in (b~4) we obtain the antisymmetry and reflexivity of :   () (≥) = (O, =). It follows that The case i = 1 shows that .ec is given by ϵ¯⁽*⁾.
  4. By (b~5) the inheritance root r is given by (O, ϵ, ) as the unique object x such that x. = O.ϵ.. That is, Moreover, since r ϵ x r for some object x it follows by subsumption of ϵ that r ϵ r. Since r is non-well-founded in ϵ it follows by (b~11) that r ϵ¯ r. Consequently, for every non-terminal x,   x ϵ¯ r by monotonicity of ϵ¯ and x ϵ r since (ϵ¯) (ϵ).
  5. Since it is already asserted by (b~1)(b~5) and (b~11) that x ϵ¯ r for every non-terminal x, the (b~6) condition can be stated just for terminal x, i.e. as T O.϶. Moreover, since (b~7)(b) (with i = 0) asserts x.ϵ = x.ϵ¯ for every terminal x it follows that every object has a (power) container and r is a universal (power) container: (However, r is not necessarily a unique object with this property.)
  6. Axiom (b~7)(a) can be stated as any of (ⅰ)–(ⅳ), using additional definitions. For every x from T O.ɛɕ, For (ⅲ), use well-foundedness of x and apply x.ec(i) ϵ-j x   →   i = j, see observation B3. For (ⅳ), use x.϶¯ = which is asserted by (b~8).
  7. Axiom (b~7)(b) can be stated as the equality x.ϵ = x.ϵ¯ for every x from (T O.ɛɕ).ec (which is exactly the set of terminals and singletons).
  8. In (b~8) we obtain x. = y.ϵ-1 for i = 0 in (b) and thus x ϶-1 y. It follows that .ec and .ɛɕ are disjoint subrelations of ϶-1:
    (.ec) = (϶-1) (ϵ¯),
    (.ɛɕ) ((϶-1) (ϵ¯)) (ϵ)   (where (.ɛɕ) (ϵ) is by (b~8)(a) or also by (b~8)(b) for i = 1).
    In in the (b) condition, = can be replaced by (the inverse inclusion follows by (b~3)). Moreover, the (c) condition (i.e. (x,y) (ϵ¯)) can be stated as any of (ⅰ)–(ⅲ): using (b~8)(a) for (ⅰ) and (b~4) for (ⅱ) and (ⅲ). In particular, (ⅲ) means O.ec O.ɛɕ = – powerclasses are disjoint with primary singletons.
  9. Axioms (b~11) and (b~1) can be equivalently stated as the single equality where is the domain-restriction of ϵ to bounded objects – objects x such that x.d < ϖ.
  10. A minimum basic structure is such that O = {r}. In such a case,
Observations about .ec

Observations A: Assume (b~1)(b~4).

  1. For every objects x, y, if x.ec = y then
    (a) x. = y.϶ = y.϶¯, (b) x.ϵ¯ = y.,
    (c) x. = y.ϵ¯-1, (d) x.϶-1 = y..
    It follows from x. = y.϶ that .ec is injective.
  2. If x.ec(i) = y for an integer i then (a)–(d) from the previous statement hold with ϵ-1/ϵ¯/ϵ replaced by ϵ-i/ϵ¯i/ϵi.
  3. Corollary: In a powerclass complete (pre-)basic structure, powers of ϵ¯ are given by and .ec:
  4. For every objects x, y and every integers i, j, k, if both x.ec(i) and y.ec(j) are defined then
  5. Corollary (the case i = j = 1, k = 0 in (ⅰ)):   The .ec map is an order embedding of (O.ce, ) into (O, ):
  6. If x.ec = y then:   x is well-founded in ϵ y is well-founded in ϵ.
  7. If y is well-founded in ϵ then y.ec(-i) is only defined for finitely many natural i so that y.pr exists.

Proof:

  1. (Apply:   (a) x. = y.϶iy.϶i x. y.϶i,   (b) x.ϵ¯i = y.y. x.ϵ¯i y..) Assume that x.ec(i) = y, i . Then
    1. x. = y.϶i follows from:   .ec(i) (϶i) (≥) and .ec(-i) (≥) (϶i).   (The same holds with ϶¯i instead of ϶i.)
    2. x.ϵ¯i = y. follows from:   .ec(i) () (ϵ¯i) and .ec(-i) (ϵ¯i) ().
    Cases (c) and (d) correspond to (b) and (a), respectively.

Observations B: In addition, assume (b~10).   (This condition is not asserted in pre-basic structures.)

  1. .ec is a well-founded map: If x.ec(-i) exists then (by composition of .ec(-i) and ϵ¯) x ϵ¯1-i r. It follows that there can only be finitely many natural i such that x.ec(-i) exists.

    Note: Well-foundedness of .ec is a consequence of well-foundedness of ϶-1, see anti-membership.

  2. If x ϵk x then k ≥ 0. (The case k < 0 is again disallowed by (b~10).)
  3. If x.ec(i) ϵ-j x for natural i, j then   x ϵi-j x and j i. If x is well-founded then i = j.

Definitions in detail

This section provides detailed definitions for ϵ5-structures and thus for basic structures. The already introduced definitions are repeated. In many cases, the definitions make sense only together with additional assumptions. A distinguished collection of assumptions is formed by axioms of pre-basic structures.

Note: Definitions considered to be closely related to consistency conditions are provided in the next section.

Powerclass chains
For a set Y of objects, Y.ce denotes the image of Y under .ce. For an object y (rather than a set of objects) we consider y.ce to be defined and equal to x iff {x} = {y}.ce. Similarly with .ec(i) or .ce(i).
Object membership
ϵ
ϵ¯
¯
In the definitions below we consider that the first two definitory constituents of an ϵ5-structure are of the form (ϵ, ϵ¯⁽*⁾) where ϵ¯⁽*⁾ is only left-infinite ((ϵ¯⁽*⁾ = { ϵ¯i | i , i 1 }). There are four membership relations between objects: For an integer i, the i-th power of ϵ / ϵ¯ / / ¯ is denoted ϵi / ϵ¯i / i / ¯i and defined as follows.
For i > 0,   ϵi / ϵ¯i / i / ¯i is the i-th relational composition of ϵ / ϵ¯ / / ¯ with itself.
(E.g., (1) = (), (2) = () ().)
For i 0,
  • ϵ¯i is the i-th member (item) of the definitory sequence ϵ¯⁽*⁾,
  • (ϵi) = (ϵ¯i),
  • i is defined by:   x i y   ↔   x ϵi y and x.d < ϖ,
  • (¯i) = (i).
There are one-way closures and two-way closures of membership: The respective inverses of the above relations are denoted via reversed symbols: We use dot notation for images under the above relations, both for objects and sets of objects. For an object x, An object x is said to be a power member (resp. power container) if x.ϵ = x.ϵ¯ (resp. x.϶ = x.϶¯ ).
Inheritance
The inheritance relation, , is the 0-th power of ϵ: that is, is a special notation for the 0-th member of the definitory sequence ϵ¯⁽*⁾. As usual, we use < for the strict inheritance: Similarly, let and > be the inverses of and <, respectively. There is also the bounded inheritance relation, 0, for which no special symbol is introduced. By the definitions made so far, 0 is the domain-restriction of : We let . and . denote the image and preimage operators for . We shall use these operators both for objects and sets of objects. For images of a single object under < and >, the polar maps . and . are used, respectively. For an object x,
Polars of
We also introduce notation for lower and upper bounds in . First we extend the meaning of for relationship between sets of objects. For an object a and sets X, Y of objects, Similarly with <, and >. For a set X of objects, X. denotes the set of lower bounds of X, whereas X. is the set of strict lower bounds of X, similarly for upper bounds. That is,
Anti-membership
There is an anti-relation of ϵ¯: For an object x,   x.϶-1 is the set of anti-members of x, and x.ϵ-1 is the set of anti-containers of x.
Recall the (b~10) axiom:   For every object x,   x.mli (= sup { i | x ϵ1-i r, i }) is finite.

Observations: Assume axioms of pre-basic structures.

  1. (b~10) ϶-1 is a well-founded relation in which every object has a finite rank.
  2. If ϵ-i equals the i-th relational composition of ϵ-1 for every i > 0, then is satisfied in the previous observation.
  3. O.϶-1 = r.϶-1 T.϶-1.
Distinguished sets of objects
In an ϵ5-structure (even if axioms of basic structures are assumed), there is only one distinguished object whose existence is asserted – the inheritance root r. However, there are several distinguished sets of objects:

Observations: Assume (a) reflexivity of , (b) (.ec) (ϵ¯) (ϵ), (c) (.ɛɕ) (ϵ) (.ec), (d) {x}.ɛɕ.϶ {x}.

  1. O.pr = T C O.ɛɕ.
  2. O = T C O.ec O.ɛɕ.
Singletons
Recall the last definitory constituent of an ϵ5-structure: The (derived) singleton map is denoted .ɛϲ and is defined as a partial map between objects by Objects from the image O.ɛϲ are singletons. We say that S is
primary singleton complete if x.ɛɕ is defined for every object x from O. (T O.ɛϲ),
singleton complete if x.ɛϲ is defined for every object x from O..
We call the sets O. (T O.ɛϲ) and O. the potential domain of .ɛɕ and .ɛϲ, respectively. We let the integer powers, inverses and transitive closures of .ɛɕ and .ɛϲ be denoted and defined in a similar way to that of .ec. The 0-th power of .ɛɕ and .ɛϲ is defined as the identity on the respective potential domain. In particular, The primary singleton completion provides the missing primary singletons for objects from O.ɛɕ(0) O.ɕɛ.

Observations:

  1. Condition (b~8)(a) is equivalent to (.ɛɕ) (.ɛϲ).
  2. Assume (b~1), (b~4) and (b~8)(a)(c). Then .ɛɕ is obtained from .ɛϲ :
  3. Assume all axioms of basic structures. Then the following are satisfied:
  4. Assume that S is a singleton complete basic struture. Then
Metalevels
For an object x, the metalevel index of x is denoted x.mli and defined by That is, if r.϶-i r.϶1-i for every i then x.mli is the unique ordinal such that x.mli ω and For an ordinal number i ω, the i-th metalevel is the set of all objects whose metalevel index equals i.

Observations: Assume axioms of pre-basic structures.

  1. The 0-th metalevel equals T.
  2. The 1-st metalevel contains r.
  3. The i-th metalevel, i , equals r.϶1-i r.϶-i.   (A consequence of r.϶-i r.϶1-i.)
  4. If t = r.ec(i) then
  5. (Recall that i + ω = ω for every integer i.)
    If x ϵi y for an integer i then i + x.mli ≥ y.mli.   (A consequence of r.϶1-k.϶i r.϶i+1-k, k .)   In particular,
    x y x.mli ≥ y.mli,
    x ϵ y 1 + x.mli ≥ y.mli,
    x.ec = y 1 + x.mli = y.mli. (A consequence of (.ec) (ϵ) (϶-1).)
    As a consequence, if x.ec = y then: x.mli = ωy.mli = ω.
  6. If, in addition, (.ɛϲ) (ϵ) (϶-1) (as asserted by (b~8)) then
    x.ɛϲ = y 1 + x.mli = y.mli.
  7. For every object x, if x.mli < ω then x.pr exists.
Helix number
The helix number h of an ϵ5-structure is defined by

Observations: Assume axioms of pre-basic structures and let (ϵω) = (ϵ).

  1. The helix number h equals the possibly infinite number of distinct images of r under natural powers of ϵ: (Recal that H denotes the set r.ϵ of helix objects. Also recall that i + ω = ω for every integer i.)
  2. For every natural i,  
  3. The helix number is at least 1. Moreover,
    h = 1 r.ϵ = {r} = H,
    h is finite r.ϵi = H for some natural i.
  4. The following less elegant definition of h can be used to avoid a reference to r.ϵ-1. This can be useful in ϵ-based monotonic structures where ϵ-k, k > 0, are derived from ϵ and .
    h = 1 if H = {r},
    h = sup {i + 2 | r.ϵi H, i } otherwise.
Rank
The rank of an object x is denoted x.d and defined to be an ordinal number at most equal to a fixed limit ordinal ϖ according to the following prescription. Let W be the set of all objects z such that Then .d is defined recursively using well-foundedness of (W, ϵ). For every object x,
x.d = ϖ if x O W,
x.d = ϖ (sup {a.d + 1 | a ϵ x} sup {a.mli + i-j | a x.϶i.϶-j, i,j }) if x W.

Notes:

  1. We use α β (resp. α β) to refer to the minimum (resp. maximum) of ordinal numbers α and β, see Preliminaries.
  2. The (b) condition is implicitly satisfied in basic structures. It is shortly expressed as z.϶.϶-.mli < ω.
  3. The definition of .d is better understood via the ranking product.

Observations: Assume axioms of pre-basic structures and apply the observations for metalevels.

  1. For every object x, the following sets are identical: (Therefore, (ⅱ) can be used for the definition of .d.)
  2. For every object x satisfying x.϶.϶-.mli < ω the following set is identical to (ⅰ):
    1. (ⅰ') {i-j + a.mli | a x.϶i.϶-j O.pr, i,j }.
    Similarly, the additional condition of a being a primary object can be added to (ⅱ).
  3. If ϖ = ω then x.d = sup {i-j + a.mli | a x.϶i.϶-j, i,j }.
Boundedness
Boundedness of objects is based on their rank. Note in particular, that every object that is non-well-founded in ϵ is unbounded.
Power instance-of and the .class map
Recall that the set C of classes is defined as O (T O.ec O.ɛɕ).

Note: The above definition of .class is tailored to the case of monotonic structures in which (ϵ¯) = (ϵ). We did not introduce the non-monotonic class map correspondent to direct instance-of.


Observations: Assume axioms of pre-basic structures.

  1. Every object is a (power) instance of the inheritance root r.
  2. The .class map is monotonic. That is, for every objects x, y such that both x.class and y.class are defined,

Consistency and completeness

This section is related to miscelaneous consistency conditions which express whether an ϵ5-structure resembles an (ϖ+1)-superstructure (that is, a complete structure of ϵ) in a particular respect.
ϵ-rank and -rank
The following auxiliary rank functions are based solely on ϵ / . For an object x, let That is, rϵ(x) is the ϖ-limited rank of x w.r.t. ϵ, and r(x) is the rank of x w.r.t. the well-founded relation . Moreover, for a set X of objects we let We say that an object x is -ranked (resp. ϵ-ranked) if x.d = r(x) (resp. x.d = rϵ(x)). An ϵ5-structure is -ranked (resp. ϵ-ranked) if so is every its object.

Observations:

  1. For every object x,
  2. If r is -ranked then r(O) = ϖ+1.
Groundedness
An object x is said to be The whole ϵ5-structure S is ϵ-grounded if T.ϵ = O and -grounded if T. = O.

Proposition A: Assume (a) (ϵ) = () (ϵ¯), (b) () (ϵ¯) (ϵ¯), and (c) T O..   (All of (a)–(c) are satisfied in basic structures.) Assume in addition that (d) () = () (0).

  1. For every natural i,   i is the domain-restriction of ϵi to bounded objects.
  2. Corollary: If S is ϵ-grounded then S is -grounded.
    (More specifically, if S is ϵ-grounded then T.ϵi = T.i for every natural i.)

Proof:

  1. For i equal 0 or 1 the statement holds by definition. We further proceed by induction. Assume that i > 0, x ϵi y ϵ z and x is bounded. We should prove that x i+1 z, that is, x.i z. is non-empty. By induction assumption, x i y, so that x i-1 a y for some a. By (c) there exist bounded b such that a b y.

Proposition B: Assume (b~2), (b~3) and O = r.϶ = r.϶¯. Then for every object x the following are satisfied:

  1. x is ϵ-grounded   →   x.mli < ω.  
    Corollary:   S is ϵ-grounded   →   S satisfies (b~10).
  2. For and every natural i,

Proof:

  1. Let x be and object. We show that: x.mli = ωx T.ϵ. Observe that As a consequence, if x.mli = ω then x.϶i r for every natural i, i.e. x T.ϵ.
  2. To show (a), assume that x is ϵ-grounded. If i < x.mli then x ϵ¯-i r and therefore x.϶i r (by (ϵi) (ϵ¯-i) ()). Since x.϶ r by ϵ-groundedness of x it follows that x.϶i must be non-empty. The (b) statement follows from (a).
Extensional consistency
An object x is said to be extensionally consistent if for every object y,   x. y.x y. The whole structure is extensionally consistent if so is every its object. That is, assuming the subsumption rule () () (), S is extensionally consistent iff the following equivalence is satisfied for every object x, y:
-levelling
We say that an object x is -levelled if x is -grounded (i.e. x T.) and that is, (assuming T = T.0) the metalevel index of x equals the length of the shortest -path from T to x. The whole structure is -levelled if all its objects are -levelled.

Observations:

  1. In a basic structure,   an object x is -levelled   ↔   x T.i   where i = x.mli.
  2. For a basic structure S the following are equivalent:

Proposition: If S is basic structure that is extensionally consistent and powerclass complete then S is -levelled.

Proof:
Assume that S is as in the antecedent of the proposition. Since the reduced helix R is complete it follows that for every natural i and every object x,

Assume for a contradiction that z is a non-terminal object such that z.mli z..mli. Let y be the top of the (z.mli+1)-th metalevel, i.e. y = r.ec(i) where i = z.mli. Then for every bounded object u,   u y.z.mli u.mli. Therefore, z. y.. By extensional consistency, z y, so that z.mli ≥ z.mli+1 – a contradiction.

The diagram on the right shows a powerclass complete structure in which the z object (or any object from z.ec) is not -levelled. The dashed green arrows indicate pairs (x,y) for which the condition of extensional consistency is violated.

Powerclass consistency
We call an object x powerclass-like if An object x is said to be powerclass consistent if The whole structure S is powerclass consistent if so is every its object.

Example. The diagram on the right shows a basic structure that is (a) powerclass complete and (b) extensionally consistent but in which the m object is not powerclass consistent. (Horizontal lines indicate the .ec map, with implicit left-to-right orientation.)

For every natural i,   zi. (= zi+1.϶ = zi+1.) is the set of objects x from m.϶ such that x.d i+1. Therefore, if X is a bounded subset of m.϶ and i is such that X.d i then X zi+1 ϵ m, thus X. m.϶ is non-empty.

Observations: Assume that S is a basic structure.

  1. If S is extensionally consistent and powerclass complete then:   x.϶ = x.϶¯  ↔  x.϶ is a downset w.r.t. . (Thus, (ⅰ) and (ⅱ) say that x.϶ is a boundedly complete ideal.)
  2. Every singleton is powerclass consistent (and so is every terminal object).
  3. If S is powerclass complete and extensionally consistent (as is the case of the above example) then every bounded object is powerclass consistent.
Combined consistency
For convenience, we introduce terminological shorthands. For every object x, Similarly, an ϵ5-structure S is e+p consistent if so is every its object.
Free leaf
We define a partial map .ԏ between objects by
x.ԏ = y   ↔   (a) x is terminal,
(b) y is a primary object whose metalevel index k = y.mli is finite, and (y is unique such that:)
(c) x.ϵ¯i = y.ϵ¯i-k {x}.ec(i)   for every natural i.
If x.ԏ = y then we say that x is a direct free leaf of y. We use the .ԏ(-1) for the inverse of .ԏ so that {y}.ԏ(-1) is the set of direct free leaves of y. An object x for which x.ԏ is defined is called a free leaf.

Proposition A: Assume axioms of pre-basic structures and O.mli < ω.

  1. For every terminal object x there exists at most one pair (y,k) from O.pr × such that (c) is satisfied. Moreover, if (y,k) is such a pair then k = y.mli.

Proof:

  1. Assume that x is a terminal object, (y,k) is from O.pr × and satisfies (c) and that (z,ℓ) is an alternative pair to (y,k). Then it follows from x ϵ¯k y that z ϵ¯k-ℓ y. Similarly, x ϵ¯ zy ϵ¯ℓ-k z so that (y,z) (ϵ¯ℓ-k) (϶¯k-ℓ) = .ec(ℓ-k). Since both y and z are primary it follows that (y,k) = (z,ℓ). To show that y.mli = k observe that for every integer i, The first equivalence is by definition of .mli, the second one is by (c) and the last one is by x being terminal.

Proposition B: Assume axioms of basic structures.

  1. If x.ԏ = y and k = y.mli then x.ec(k-1) is defined   (in particular, y is non-terminal).
  2. If x.ԏ = y, k = y.mli and n is a natural number such that both a = x.ec(k+n-1) and z = y.ec(n) exist then
    1. a. = z. {a}.ec.
  3. For every object z, if = z.mli and z.pr.ԏ(-1).ec(ℓ-1) has at least 2 elements then

Proof:

  1. Assume x.ԏ = y and denote k = y.mli. Observe first that k 0 (i.e. y is non-terminal) since otherwise x. = y. {x} = {x} {x}, a contradiction. It follows that x ϵ¯k y for some k > 0 and thus x ϵ¯k-1 u ϵ¯ y for some object u. By definition of .ԏ, so that either u y.ϵ-1 y.϶¯ or u = x.ec(k-1). The former case is equivalent to u.ec = y which is disallowed by the definition of .ԏ.
  2. Let x, y, z, a, k and n be as in the antecedent of the proposition. It follows by boundedness of a and by (b~7)(b) that a. = a.ϵ = a.ϵ¯ and thus
  3. Let z and be as in the antecedent of the proposition and let a and b be two different objects from z.pr.ԏ(-1).ec(ℓ-1). By the previous proposition, a. = z. {a}.ec and b. = z. {b}.ec. It follows that for every object u, This shows that z is extensionally consistent. To show the powerclass consistency of z, assume that z is primary and denote X = {a,b}. Since a. = z.ϵ-1 {a} and b. = z.ϵ-1 {b} it follows that and thus X. z.϶¯ = z.ϵ-1 z.϶¯ = , i.e. X has no upper bound in z.϶ so that z is not powerclass-like.
Completeness
(Assume that S is an ϵ5-structure such that O = O.϶.) We say that S is
powerclass complete if x.ec is defined for every object x,
singleton complete if x.ɛϲ is defined for every object x from O.,
metaobject complete if S is both powerclass complete and singleton complete,
pre-complete if S is a (ⅰ) basic structure that is (ⅱ) metaobject complete, (ⅲ) extensionally consistent, (ⅳ) powerclass consistent, and (ⅴ) -ranked,
extensionally complete if for every subset X of O. there is an object x such that x. = X,
complete if S is pre-complete and extensionally complete.

Pre-basic structure

Many important properties of basic structures are consequences of a weaker collection of conditions than (b~1)(b~11). Such a weaker collection is singled out in this section to form the family of pre-basic structures.
Pre-basic structure
By a pre-basic structure (of ϵ) we mean an ϵ5-structure S = (O, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ) satisfying the following axioms:
(ϐ~1) (ϵ¯) (ϵ).
(ϐ~2) (ϵ¯i) (ϵ¯j) (ϵ¯i+j)   for every integer i, j.
(ϐ~3) (ϵ) (ϵi) (ϵ1+i)   for every integer i.
(ϐ~4) (ϵ¯i) (϶¯-i) = .ec(i)   for every integer i.
(ϐ~5) O.ϵ r.
(ϐ~6) O.϶¯ = O.
(ϐ~7) T.϶-i r.϶-i =   for every natural i.

Observations:

  1. r ϵ¯ r,   O = r.϶ = r.϶¯.
  2. Every basic structure is a pre-basic structure.
  3. Terminal objects are those that have rank 0.

Proof:

  1. For every terminal x,   x.϶ = and (as a consequence) x.϶.϶- = x.϶- so that Since by (ϐ~7), a ϵ-i xa.mli i, it follows that x.d = x.mli - 0 = 0.

    Conversely, if x is non-terminal then x.mli > 0, and (since z.mli z.d for every object z) thus x.d > 0.

Groundedness vs ϵ-rank

Proposition: In a pre-basic structure S, the following are equivalent:

Proof:
ⅰ→ⅱ.
Assume (ⅰ) and let x be an object that is well-founded in ϵ. By definition of well-foundedness, there is an object a from x.϶ such that rϵ(a) = 0. Since

it follows that x T.ϵ. The x.mli < ω condition then follows by proposition B1.
ⅰ←ⅱ.
Assume (ⅱ). By simple observation, (in any pre-basic structure) the set of objects that are well-founded in ϵ is closed w.r.t. .϶.϶-, so that (a) is equivalent to This simplifies the definition of .d so that for every object x,
x.d = rϵ(x) = ϖ   if x is non-well-founded in ϵ. Otherwise (if x is well-founded):
x.d = ϖ (sup {a.d + 1 | a ϵ x} sup {a.mli + i-j | a x.϶i.϶-j, i,j }),
rϵ(x) = ϖ sup {rϵ(a) + 1 | a ϵ x}.
Let x be an object that is well-founded in ϵ and denote A, B and A' the respective sets over which the suprema in the definitions of x.d and rϵ(x) are taken, thus
x.d = ϖ (sup(A) sup(B)),
rϵ(x) = ϖ sup(A').
By well-founded recursion we can assume that a.d = rϵ(a) for every a ϵ x, so that A = A'. As a consequence, rϵ(x) x.d. It remains to show that rϵ(x) ≥ sup(B), that is, for every m B, Let m be from B and let (a,i,j) be a corresponding triple from O × × such that a x.϶i.϶-j and m = a.mli + i-j. Since a is ϵ-grounded, there is a pair (b,k) from T × such that b ϵk a. Denote n = k + i-j. Then the pair (b,n) is the requested pair from ():

Metaobject structure

The diagram on the right shows a basic structure that is metaobject complete – the powerclass map .ec (shown by horizontal blue arrows) is total and the singleton map .ɛϲ (shown by blue arrows pointing to a circle which indicates a singleton) is defined on the set O. of bounded objects. We have already observed that (a) in a powerclass complete basic structure, all powers of ϵ¯ are given by and that (b) in a singleton complete basic structure the bounded membership is given by Subsequently, using the last axiom of basic structures, the object membership is given by (ϵ) = () (ϵ¯). Since (.ɛɕ) = (.ɛϲ) (.ec) it follows that a metaobject complete basic structure is fully determined by , .ec and .ɛϲ. The following subsection provides an axiomatization based on these three constituents.
Metaobject structure
By a metaobject structure we mean a structure S = (O, , r, .ec, .ɛϲ) where Denote T = { x | x r } the set of terminal objects and let .ec denote the reflexive transitive closure of .ec.
The structure is subject to the following axioms (⁎):
(mo~1) Inheritance, , is a partial order.
(mo~2) The powerclass map, .ec, is an order-embedding of (O, ) into itself.
(mo~3) Objects from T.ec are minimal in .
(mo~4) Every powerclass is a descendant of r.
(mo~5) The set r.ec has no lower bound in .
(mo~6) The singleton map, .ɛϲ, is injective.
(mo~7) Objects from O.ɛϲ.ec are minimal in .
(mo~8) For every objects x, y such that x.ɛϲ is defined,   x.ɛϲ y.ec x y.
(mo~9) For every object x,   x.ɛϲ is defined   ↔   x.d < ϖ.
(⁎) The definitions introduced before the axioms are sufficient to state all axioms except the last one. The definition of the rank function, .d, used in the last axiom is provided below. Assume that (mo~1)(mo~8) are satisfied.

Let , ϵ¯ and ϵ be relations between objects with the following definition and terminology:

() = (.ɛϲ) () is the bounded membership,
(ϵ¯) = (.ec) () is the power membership,
(ϵ) = () (ϵ¯) is the (object) membership.
For an integer i, let .ec(i) be the i-th composition of .ec with itself if i ≥ 0 (with .ec(0) being the identity on O) and the -i-th composition of the inverse of .ec otherwise. Similarly with .ɛϲ(i), but with .ɛϲ(0) being the identity on O.. Subsequently, let i, ϵ¯i and ϵi be the i-th power of , ϵ¯ and ϵ, respectively, defined as follows:
(i) = .ɛϲ(i) (),   (for i < 0 we let (i) = (0) .ec(i))
(ϵ¯i) = () .ec(i) (),
(ϵi) = (i) (ϵ¯i).
The metalevel index, x.mli, and rank, x.d, of an object x are then defined like in basic structures by
x.mli = sup { i | x ϵ1-i r, i },
x.d = ϖ if x is non-well-founded in ϵ,
x.d = ϖ (sup {a.d + 1 | a ϵ x} sup {a.mli + i-j | a x.϶i.϶-j, i,j }) if x is well-founded in ϵ.
The correspondence

Proposition: There is the following one-to-one (definitional) correspondence between metaobject structures and metaobject complete basic structures:

  1. If S = (O, , r, .ec, .ɛϲ) is a metaobject structure then the ϵ5-structure S' = (O, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ) derived from S is basic structure that is metaobject complete. The new constituents of S' are defined as follows:
    (ϵ) = ((.ec) (.ɛϲ)) (), (= (ϵ¯) ((.ɛϲ) ()), see the proof below)
    (ϵ¯i) = () .ec(i) ()   for every integer i 1, (() and also for i > 1, see the proof below)
    (.ɛɕ) = (.ɛϲ) (.ec).
  2. If S = (O, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ) is a metaobject complete basic structure then S' = (O, , r, .ec, .ɛϲ) is a metaobject structure. The new constituents of S' are defined as follows:
    () = (ϵ¯0),
    (.ɛϲ) = (ϵ) (O × (T O.ɛɕ).ec).   (We can equivalently write T.ec instead of T.)

Proof:

  1. Let S and S' be as in (Ⅰ). Since () (.ec) = (.ec) () by (mo~2), it follows that for every natural i, () .ec(i) () is the i-th relational composition of ϵ¯ with itself (which equals ϵ¯i by definitional extension of ϵ5-structures) so that () is satisfied for every integer i. Moreover, it follows that for every natural i,
    (ϵ¯i) = () .ec(i) = .ec(i) (),
    (ϵ¯-i) = () .ec(-i).
    Subsequently, (b~1)(b~11) are verified as follows.
    1. (b~1) (i.e. (ϵ¯) (ϵ)) follows by the definition of ϵ.
    2. (b~2) is satisfied as a consequence of transitivity of and compositional commutativity of and .ec so that
      • (ϵ¯i) (ϵ¯j) = (ϵ¯i+j) for every integer i, j.
    3. To prove (b~3) it is sufficient (using the equality above) to prove that
      • (a) (ϵ) () (ϵ)   and   (b) (ϵ) (ϵ-1) ().
      (a) follows by transitivity of . To show (b) apply definitions of ϵ and ϵ-1 and (mo~8):
      (ϵ) (ϵ-1) = ((ϵ¯) ((.ɛϲ) ()))     (ϵ-1)  
      = ((ϵ¯) (ϵ¯-1)) ((.ɛϲ) () (ϵ-1))  
      = () ((.ɛϲ) () .ec(-1))  
      = ()   (since by (mo~8), {x}.ɛϲ..ec(-1) x. for every object x).
      Moreover, since (ϵ) (ϵ-1) = (ϵ) .ec(-1) it follows that
      • (≥) = (.ec) (϶).
    4. Axiom (b~4) follows by antisymmetry and reflexivity of . For every natural i,
      • (ϵ¯i) (϶¯-i) = .ec(i) (() (≥)) = .ec(i),
      • (϶¯i) (ϵ¯-i) = ((≥) ()) .ec(-i) = .ec(-i).
    5. To prove (b~5) (i.e. O.ϵ r), proceed as follows.
      • O.ec r.   (By (mo~4).)
      • O.ec. r.   (Since for O.ec x < t r, t would be a non-minimal terminal object (⁎), violating (mo~3).)
      • O.ɛϲ. r.   (Since O.ɛϲ O.ec. by (mo~8).)
      • O.ϵ r.   (Since by definition of ϵ, O.ϵ = O.ec. O.ɛϲ..)
      In (⁎), we have used the term terminal object according to the definition in the metaobject structure S. However, the definitions of the set T of terminal objects in S and S' are coincidient: Since r ϵ r (as consequence of r.ec r) it follows that O.ϵ. = r..
    6. Axiom (b~6) (O.϶ = O) follows by x ϵ¯ r for every object x (a consequence of x.ec r asserted by (mo~4)).
    7. To prove (b~7)(a) (x.϶-i = {x}.ec(i) for every x from T O.ɛɕ and every natural i), assume that x T O.ɛɕ. Then for every natural i,
      x.϶-i = x.ec(i).   (since (ϵ-i) = (ϵ¯-i) = () .ec(-i) and thus (϶-i) = .ec(i) (≥))
      = {x}.ec(i)   (since (.ɛɕ) (.ɛϲ) and thus O.ɛɕ O.ɛϲ so that x.ec(i) is from (T O.ɛϲ).ec and therefore x.ec(i) is minimal in due to (mo~3) and (mo~7)).
    8. Let us prove (b~7)(b), i.e. if X denotes the set (T O.ɛɕ).ec then x.ϵ = x.ϵ¯ for every x X. That is, we have to show that {x}.ɛϲ. x.ec. for every x X. Since {x}.ɛϲ {x}.ec for every object x (by (mo~8)), it follows that  
      • {x}.ɛϲ. x.ec.   ↔   x.ɛϲ is defined and x.ɛϲ < x.ec.
      By (mo~3) and (mo~7), the last strict inequality is disallowed for objects x from (T O.ɛϲ).ec and thus for all x from X.
    9. Let us prove (b~8), that is, assume that x, y are objects such that x.ɛɕ = y and show that
        (a) {x} = y.϶, (b) x.ϵi = y.ϵi-1 for every i 1, (c) (x,y) (.ec).
      The (c) property follows by definition of .ɛɕ. Since (.ɛɕ) (.ɛϲ), it follows in the first place that x.ɛϲ = y. By definition, x.ϵ = {x}.ɛϲ. x.ec.. Since x.ɛϲ is defined and x.ɛϲ x.ec it follows that (b) is satisfied for i = 1. For i 0, use
      • x u.ec(-i) x.ɛϲ u.ec(-i).ec
      which holds by (mo~8) for every object u. To show (a), assume that u is an object such that u ϵ y, that is, (by definition of ϵ) u.ɛϲ y or u.ec y. By (mo~7), y is minimal in so that u.ɛϲ = y or u.ec = y. The latter case is impossible because u.ec = y ϶ x implies x u (by (≥) = (.ec) (϶) proved before) so that either
      • x = u and thus (x,y) (.ɛɕ) (.ec)   – which contradicts the definition (.ɛɕ) = (.ɛϲ) (.ec), or
      • x < u which would imply x.ec < u.ec = y   – which would in turn violate the minimality of y.
      It follows that u.ɛϲ = y and therefore, since (mo~6) asserts the injectivity of .ɛϲ, u = x. That is, (a) is satisfied.
    10. To show (b~10) (x.mli is finite for every object x), apply (϶¯1-i) = .ec(i-1) (≥) to the definition of .mli:
      • x.mli = sup {i | x {r}.ec(i-1) }.
      Since {r}.ec(i-1)     {r}.ec(k-1) for every natural k i (by r ϵ r and .ec being an order embedding) it follows that
      • x.mli is finite   ↔   x r.ec.
      That is, (b~10) is asserted by (mo~5).
    11. It remains to verify that (b~11) is satisfied. Note that the rank functions in S and S' are identical since they have identical prescriptions based on ϵ and ϵ¯⁽*⁾. By (mo~9), for every object x,
      • x.ɛϲ is undefined   ↔   x.d = ϖ.
      Therefore, if x.d = ϖ then x.ϵ = x.ec. = x.ϵ¯.

      Finally, it also follows that (.ɛϲ) () is the domain-restriction of ϵ to objects x such that x.d < ϖ, so that the bounded membership relation in S is coincident with that in S'.

  2. Assume that S = (O, ϵ, …) is a metaobject complete basic structure and let S' = (O, , r, .ec, .ɛϲ) be the correspondent reduct of a definitional extension of S. Then except for (mo~5), all of (mo~1)(mo~9) either directly follow from the definition of a basic structure or are obtained as observations that have already been made. The (b~10)(mo~5) correspondence is established like in the proof of (Ⅰ) using
Grounded metaobject structure
Because metaobject structures are definitionally equivalent to metaobject complete basic structures, the definitions introduced for ϵ5-structures apply to metaobject structures. In particular, a metaobject structure S is grounded iff T.ϵ = O. Since there is no distinction between ϵ-groundedness and -groundedness: T.ϵ = OT. = O (see proposition A2). Moreover, As a consequence, grounded metaobject structures can be axiomatized with (mo~5) and (mo~9) replaced as follows:

Monotonic structures

Basic structures in which (ϵ¯) = (ϵ) are monotonic. Most object models in object oriented programming have core parts that can be considered to be specializations of monotonic basic structures. The (ϵ¯) = (ϵ) equality yields the monotonicity of ϵ: If every object x has a least container (as is the case of object models in OOP), i.e. x.ϵ = x.lc. for a map .lc, then the monotonicity condition further translates to x yx.lc y.lc.

There are two distinguished subfamilies of monotonic structures given by whether .ec is empty or total:

Family of structures Used in Monotonicity condition
.ec is empty Monotonic primary structure Python x yx.class y.class
.ec is total Monotonic eigenclass structure Ruby x yx.ec y.ec

Notes: In [] and [], core parts of objects models of Ruby, Python, Java, Scala, Smalltalk-80, Objective-C, CLOS, Perl and JavaScript are considered to be specializations of monotonic structures. However, only Ruby and Python can be regarded as fully conformant to the description provided below.

  1. In Smalltalk-80 and CLOS, there are built-in monotonicity breaks.
  2. In languages with a partial support of .ec (Smalltalk-80, Objective-C and Scala), there is no notational or terminological distinction between .ec and .class.
  3. In Java and Scala (which are not generally considered to belong to dynamic programming languages) there is no established consensus about whether these languages support the classes are objects paradigm.
  4. To capture the core structure of JavaScript [], one needs to introduce prototypes as additional objects on the 0th metalevel which are powerclass predecessors of objects from the 1st metalevel.
  5. The Perl 5 programming language can be regarded to support monotonic primary structure such that where ϵ is exactly what can be detected by the isa introspection method. As a consequence, every non-terminal object x is circular: x ϵ x. However, there is no evidence (known to the author) whether the above equality between membership and inheritance is a designed feature of the language.
  6. Objective-C supports multiple inheritance roots (Object, NSObject and NSProxy). As of Pharo 1.3, Smalltalk-80 contains a subsidiary inheritance root (PseudoContext).
Monotonic structure
ϵ
ϵ-1
ϵ-2
By a monotonic structure (of ϵ) we mean a structure S = (O, ϵ⁽*⁾, r, .ec) where For every natural i > 0, let ϵi be the i-th relational composition of ϵ with itself, .ec(i) be the i-th composition of .ec with itself, and .ec(-i) be the inverse of .ec(i). Let .ec(0) be the identity on O. Let T = O O.ϵ. be the set of terminal objects. Let the metalevel index of an object x be denoted and defined like in basic structures, i.e.
The structure is subject to the following axioms:
(m~1) (ϵi) (ϵj) (ϵi+j)   for every integer i, j.
(m~2) (ϵi) (϶-i) = .ec(i)   for every integer i.
(m~3) O.ϵ r.
(m~4) O = O.϶.
(m~5) For every object x from T and every natural i,   {x}.ec(i) = x.϶-i.
(m~6) For every object x, the metalevel index x.mli is finite.
The correspondence

Proposition:

  1. If S = (O, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ) is a basic structure then its reduct S' = (O, ϵ¯⁽*⁾, r, .ec) is a monotonic structure of ϵ.
  2. If S = (O, ϵ¯⁽*⁾, r, .ec) is a monotonic structure of ϵ then S' = (O, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ), where (ϵ) = (ϵ¯) and (.ɛɕ) = , is a basic structure.
  3. Corollary: There is a one-to-one correspondence between
Monotonic primary structure
By a monotonic primary structure of ϵ we mean a monotonic structure in which every object is primary, i.e. in which the powerclass map .ec is empty. Such a structure can be axiomatized in the signature (O, ϵ⁽*⁾, r) as follows:
(mp~1) The same as (m~1).
(mp~2) (a) is reflexive and antisymmetric and (b) (ϵi) (϶-i) = for every i > 0.
(mp~3) The same as (m~3).
(mp~4) The same as (m~4).
(mp~5) Terminal objects are minimal in .
(mp~6) The same as (m~6).

Observation: There is a one-to-one correspondence between

  1. monotonic primary structures and
  2. monotonic basic structures in which .ec is empty.
Membership-based monotonic structure
By a membership-based monotonic structure (alternatively, ϵ-based m. s.) we mean a monotonic primary structure in which the negative powers of ϵ are given by ϵ and . We offer three different prescriptions for ϵ-k, k > 0. Recall that H = r.ϵ is the set of helix objects.
(mp-α) x ϵ-k y x < y.ϵk and y.ϵk y.ϵk-1,
(mp-β) x ϵ-k y x < y.ϵk and y.ϵk y.ϵk-1 and y H,
(mp-γ) x ϵ-k y x < r.ϵk+i and r.ϵk+i r.ϵk+i-1 and r ϵi y for some natural i.

Observations:
Recall that h is the helix number defined by h = sup {i + 1 | r.ϵi r.ϵi-1, i } and that Y. is the set of strict lower bounds of Y.

  1. Assume that either of (mp-α)(mp-γ) is imposed.
  2. Prescriptions (mp-β) and (mp-γ) only allow helix objects in the range of ϵ-k for every k > 0.
Example
The left diagram below shows an ϵ-based monotonic structure S0 = (O0, ϵ, ≤0, r) in which all helix objects (shown in blue) have metalevel index 1. Negative powers of ϵ are given by any of (mp-α)(mp-γ). Since b < r.ϵ2 = {r,u,v} {r,u} = r.ϵ1 and r.ϵ3 = r.ϵ2 it follows that the metalevel index of b equals 3.

The right diagram shows a monotonic basic structure S = (O, ϵ, …) that is a powerclass extension of a basic structure definitionally equivalent to S. Negative powers of ϵ in S are powerclass based, i.e. (ϵ-i) = () .ec(-i) for every positive natural i. Extensions of ϵ and 0 is to ϵ and , respectively, are given by

a.ec(i) ϵ b.ec(j)   iff   a ϵ1+i-j b,
a.ec(i) b.ec(j)   iff   a ϵi-j b,
where a, b are (primary) objects from O and i, j are natural numbers such that a.ec(i) and b.ec(j) are defined (see powerclass completion of basic structures).

Observations:

  1. There can be gaps in metalevels. (Consider the left diagram without the a object.)
  2. The ϵ-2 relation is not decomposable in S0 since b ϵ-2 r but there is no x such that b ϵ-1 x ϵ-1 r.
The (mp-γ) prescription
Since the helix number h is such that r.ϵj r.ϵj-1j < h for every natural j, the (mp-γ) prescription can be stated as:
x ϵ-k y there is a natural i such that:   x < r.ϵk+i and k+i < h and r ϵi y.
(mp-γ~1) is a partial order.
(mp-γ~2) (ϵ) () (ϵ) = (ϵ).
(mp-γ~3) O.ϵ r.
(mp-γ~4) O = O.϶.
(mp-γ~5) Objects from T are minimal.
(mp-γ~6) If h = ω then H. = .
(mp-γ~7) r.϶-k.϶ r.϶1-k for every k > 0.
The proposition below shows that if (mp-γ) is imposed then (mp~1) and (mp~2) can be equivalently replaced by a conjunction of the following conditions: The resulting axiomatization of structures (O, ϵ, , r) is shown in the box on the right. (Use the usual definitions of ϵi for i ≥ 0, ϵ, T, H, and .. For negative powers of ϵ, use the original (mp-γ) prescription and then apply the definition of h which refers to r.ϵ-1.)

Proposition:
Assume that the prescription (mp-γ) applies.

  1. The (m~1) axiom, (ϵi) (ϵj) (ϵi+j) for every integer i, j, is asserted by the following conditions:
    () () () (transitivity of ),
    (ϵ) () (ϵ) (subsumption of ϵ),
    () (ϵ) (ϵ) (monotonicity of ϵ),
    (◈) (ϵ) (ϵ-i) (ϵ1-i) for every positive natural i.
  2. The (◈) condition can be equivalently replaced by any of the following:
    (ⅰ) For every object x,   x.ϵ.mli x.mli + 1. (That is,   x ϵ y  →  y.mli x.mli + 1.)
    (ⅱ) For every natural k,   r.϶-k.϶ r.϶1-k. (That is,   x ϵ y ϵ-k r  →  x ϵ1-k r.)

Proof:

  1. Let k, be positive natural numbers. We show that
    1. Let x, y, z be such that x y ϵ-k z, i.e. for some natural i such that i + k < h,
      • x y < r.ϵi+k and r ϵi z.
      Then x < r.ϵi+k, so that x ϵ-k z.
    2. Let x, y, z be such that x ϵ-k y ϵ z, i.e. for some natural i such that i + k < h,
      • x < r.ϵi+k, and r ϵi y ϵ z.
      Then (i+1) is a natural number such that (α) r ϵ(i+1) z, (β) x < r.ϵ(i+1)+(k-1), and (γ) (i+1) + (k-1) < h. As a consequence, x ϵ1-k z. (For k = 1 it follows from (α) and (β) that x < z.)
    3. Let x, y, z be such that x ϵ-k y z, i.e. for some natural i such that i + k < h,
      • x < r.ϵi+k and r ϵi y z.
      Since (ϵi) () equals (ϵi), we obtain r ϵi z so that x ϵ-k z.
    4. Let x, y, z be such that x ϶-k y ϶-ℓ z, i.e. for some natural i, j such that i + k < h and j + ℓ < h,
      • r ϵi x, r ϵj y < r.ϵi+k, and z < r.ϵj+ℓ.
      As a consequence of the underlined condition, i+k < j so that z < r.ϵi+k+ℓ.
  2. By definition of the metalevel index, u.mli > iu ϵ-i r for every natural i, so that for every objects x, y, This shows (ⅰ)↔(ⅱ). Since (◈)→(ⅱ) trivially it remains to show that (◈)←(ⅱ). Assume therefore that (ⅱ) is satisfied and let x, y, z be such that x ϵ y ϵ-k z, i.e. for some natural i such that i + k < h, Then y ϵ-i-k r so that by (ⅱ) x ϵ1-i-k r and thus x < r.ϵi+k-1 and therefore x ϵ1-k z.
Structures with a canonical helix
In canonical primary structures [] the helix structure (H, ϵ, , r) looks like in the diagram on the right. That is, helix classes are As a consequence, r.ϵ0 r.ϵ1 = r.ϵ2 – the helix number h equals 2. It follows 2 is the highest possible metalevel index of an object, whenever any of (mp-α)(mp-γ) is used for the definition of ϵ-k, k > 0. Condition (mp-γ~7) about the possible metalevel increment along ϵ then reduces to However, the actual condition used in canonical primary structures reads This is because the least helix class c, the metaclass root, (whose existence is asserted by an additional condition of finiteness of C) is considered to be extensionally equivalent to r.ec, the powerclass of r in a powerclass extension.
Monotonic eigenclass structure
There are of course no problems with the definition of ϵ-k, k > 0 in the case opposite to that of the previous subsection. If .ec is total, then (ϵi) = () .ec(i) () for every integer i. This simplifies the axiomatization.
By a monotonic eigenclass structure we mean a structure S = (O, , r, .ec) such that and the first 5 axioms of metaobject structures are satisfied:
(e~1) is a partial order.
(e~2) () = (.ec) () (.ce),   where .ce is the inverse of .ec.
(e~3) (O × T.ec) (<) = ,   where T = O r. and .ec is the reflexive transitive closure of .ec.
(e~4) O.ec r.
(e~5) r.ec. = .   (The set r.ec has no lower bounds w.r.t. .)

Proposition: There is a one-to-one correspondence between

Powerclass-based structures

Another family of basic structures which we consider as distinguished is that which has no primary singletons (and thus T.ec.ec are the only singletons) and in which power membership and anti-membership are based on .ec:
(ϵ¯) = () (.ec) ()    (ϵ) (T × O),
(ϵ-1) = () (.ce) ()   and for i > 1, (ϵ-i) is the i-th relational composition of ϵ-1 with itself.
Powerclass-based structure
By a powerclass-based structure (of ϵ) we mean a structure (O, ϵ, , r, .ec) where Let .ec be the reflexive transitive closure of .ec, let .ce be the inverse of .ec. Let T = O O.ϵ. be the set of terminal objects.
The structure is subject to the following axioms. The definitions of .mli, .d and ϵ¯ used in the last two axioms are provided subsequently.
(pb~1) is a partial order.
(pb~2) (ϵ) () (ϵ).
(pb~3) (a) (ϵ) (.ce) (),   (b) () (.ec) (ϵ),   (c) (.ce) () (.ec) ().
(pb~4) The inheritance root r is the top of O.ϵ, w.r.t. .
(pb~5) Every object has a container, O = O.϶.
(pb~6) Objects from T.ec are minimal in .
(pb~7) For every object x, the metalevel index x.mli is finite.
(pb~8) For every object x,   x.d = ϖ   →   x.ϵ = x.ϵ¯.
The power membership, ϵ¯, and its -1-st power, ϵ¯-1, are relations between objects defined by
(ϵ¯) = () (.ec) ()    (ϵ) (T × O),
(ϵ¯-1) = () (.ce) ().
Subsequently, for every integer i, the i-th power of ϵ¯ is defined as follows.
For i > 0, ϵ¯i equals the i-th relational composition of ϵ¯ with itself.
ϵ¯0 equals .
For i < 0, ϵ¯i equals the -i-th relational composition of ϵ¯-1 with itself.
Let ϵi, for an integer i, be i-th power of ϵ, defined to be equal to the i-th relational composition of ϵ with itself if i > 0 and equal to ϵ¯i for i 0. The metalevel index and rank functions .mli and x.d are defined like in metaobject structures:
x.mli = sup { i | x ϵ1-i r, i },
x.d = ϖ if x is non-well-founded in ϵ,
x.d = ϖ (sup {a.d + 1 | a ϵ x} sup {a.mli + i-j | a x.϶i.϶-j, i,j }) if x is well-founded in ϵ.

Observations:

  1. r.ec must be defined.
  2. r.ec.ec can be undefined. Moreover, O = {r, r.ec} in the minimum powerclass-based structure.
  3. If (pb~5) is replaced by T O.ce (every terminal has a powerclass) then we obtain more pure definition since we could simply define

Proof:

  1. Since r ϵ r (by the same arguments as for basic structures) it follows by (pb~8) that r.ϵ = r.ϵ¯. Since r. = {r} it follows that r..ec. = {r}.ec.. Since r..ec. = r.ϵ¯ and this set is non-empty (by r ϵ¯ r) it follows that {r}.ec is non-empty.
The correspondence

Proposition: There is the following one-to-one (definitional) correspondence between powerclass-based structures and basic structures (O, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ) in which

() (ϵ¯) = () (.ec) ()    (ϵ) (T × O),
(ϵ¯-i) = (() (.ce) ())i for every natural i > 0 in the usual sense of relational composition, and
(.ɛɕ) = .
  1. If S = (O, ϵ, , r, .ec) is a powerclass-based structure then the ϵ5-structure S' = (O, ϵ, …) derived from S by the above prescription () (with (ϵ¯0) = ()) is a basic structure.
  2. If S = (O, ϵ, …) is basic structure satisfying () then S' = (O, ϵ, , r, .ec) is a powerclass-based structure.

Proof:

  1. Proceed similarly to the case of metaobject structures. (b~2) and (b~3) are shown by the following inclusions:
    (ϵ¯-1) (ϵ¯) = () (.ce) () () (.ec) ()  
    = () ((.ce) () (.ec)) ()  
    () () ()   (since (.ce) () (.ec) () by (pb~2)(c))
    = ().  
    (ϵ¯) = () (.ec) ()  
    (ϵ) ()   (since () (.ec) (ϵ) by (pb~2)(b))
    (ϵ)   (by subsumption).
    (ϵ) (ϵ¯-1) = (ϵ) () (.ce) ()  
    (ϵ) (.ce) ()   (by subsumption)
    () ()   (since (ϵ) (.ce) () by (pb~2)(a))
    = ().
    (ϵ¯) (ϵ¯-1) (ϵ) (ϵ¯-1)   (since (ϵ¯) (ϵ))
    ().
Powertype-based structure
The following definition provides an intermediate family of structures between basic structures and abstract power type systems introduced in the specialized document [].

By a powertype-based structure (of ϵ) we mean a structure (O, ϵ, .ec, r) where

Let .ec be the reflexive transitive closure of .ec, let .ce be the inverse of .ec. Let be the inheritance relation between objects defined by
The structure is subject to the following axioms. (The definition of .d is again postponed.)
(ptb~1) O.ce = r..   (The powerclass map .ec is defined exactly for descendants of r.)
(ptb~2) O.ϵ r.   (Every container is a descendant of r.)
(ptb~3) O = O.϶.   (Every object has a container.)
(ptb~4) (.ec) (ϵ).   (Powerclass-of is a special case of container-of.)
(ptb~5) (ϵ) () (ϵ).   (The subsumption rule.)
(ptb~6) (.ce) () (.ec) ().   (Monotonicity of .ec.)
(ptb~7) (<) (>) = .   (Antisymmetry of .)
(ptb~8) r.ec. = .   (Every object has a finite metalevel index.)
(ptb~9) For every object x,   x.d = ϖ   →   x.ϵ = x.ec..
The definitions of ϵ¯, ϵ¯i, ϵi (i ), .mli, and .d are identical to those introduced for powerclass-based structures.

Observations:

  1. (Definitional correspondence.) For a structure S = (O, ϵ, , r, .ec) the following are equivalent:
  2. (Powerclass completion correspondence.) There is a one-to-one correspondence between

Extensions

Let S = (O, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ) and S0 = (O0, …) be ϵ5-structures. We say that
S is an extension of S0 if S0 is a restriction of S   (see below for the precise meaning),
S is a powerclass extension of S0 if S0 is a restriction of S with the same set of primary objects,
S is a primary extension of S0 if S0 is a restriction of S with the same set of powerclasses.
If S is an extension of S0 then the following notation and terminology apply. We call objects from O0 old and objects from O O0 new. We will use the subscript to distinguish between symbols for S0 and S, as has already been applied for O. In particular, .ec0 and .ɛɕ0 are the powerclass and primary singleton maps in S0, respectively, T0 is the set of terminal objects in S0. Similarly with other symbols that are used to denote either a set of objects, or a (partial) map on objects, e.g. .pr0, .mli0 or .d0.

For ϵ and similar symbols, we use a special (ligature) marker: , so that ϵ / ϵ¯ / denote the membership / power membership / bounded membership in S0. Similarly with ϵi / ϵ¯i / i for an integer i.

We can therefore express S0 = (O0, ϵ, ϵ¯⁽*⁾, r, .ec0, .ɛɕ0). An ϵ5-structure S = (O, ϵ, …) is an extension of S0 iff

S is a powerclass (resp. primary) extension of S0 iff O0.pr0 = O.pr (resp. O0.ec0 = O.ec).
Faithful extension
Let S = (O, ϵ, …) and S0 = (O0, ϵ, …) be ϵ5-structures. We say that S is a faithful extension of S0 if S is an extension of S0 and the following additional conditions are satisfied:
(A) For every old object x,   {x}.pr = {x}.pr0.   (That is, O0.pr0 O.pr.)
(B) For every natural i,   ϵi equals the restriction of ϵi to the set O0 of old objects.
(C) For every natural i,   ϵ¯i equals the restriction of ϵ¯i to the set O0 of old objects.
(D) For every old object x,   x.d = x.d0.
Observe that for powerclass extensions as well as for primary extensions, (A) is satisfied implicitly.
Embedding
For ϵ5-structures, S1 = (O1, ϵ, …) and S2 = (O2, ϵ, …) a map from O1 to O2 is an embedding of S1 into S2 if it is an isomorphism between S1 and the restriction of S2 to O1, that is, If S1 denotes the restriction of S2 to O1 then S2 is an extension of S1. If this extension is faithful then is said to be faithful.
Summary of provided extensions
Extension name Provided for Preserved (P) / Extended (E)
.ec .ɛɕ O.pr
1 Ranking product Pre-basic structure P P E
2 Powerclass completion Basic structure E P P
3 Primary singleton completion P E P
4 Singleton completion (32') E E P
5 Extensional pre-completion Metaobject complete b.s. E E P
6 Rank pre-completion Basic structure P P E
7 Pre-completion (62325) E E E
8 Completion of a Pre-complete structure
9 Completion (78) Basic structure

Notes:

  1. Except for the ranking product, every listed extension is a completion in the sense of idempotency of the extension.
  2. Extensions 2,3,4 and 8 are true completions in the sense of least extension. If S0 is a basic structure (resp. pre-complete structure in the case 8), and S is the respective extension of S0 then S is the least extension of S0 that is a basic structure that is
    (2) powerclass complete (x.ec is defined for every x O),
    (3) primary singleton complete (x.ɛɕ is defined for every x O. (T O.ɛϲ)),
    (4) singleton complete (x.ɛϲ is defined for every x O.),
    (8) complete (S is an (ϖ+1)-superstructure).

Ranking product

This section describes embedding of a pre-basic structure S into an ϵ-ranked pre-basic structure S' called the ranking product of S. Such an embedding allows to express the rank function .d in S via the (simpler) ϵ-rank function rϵ() in S'. The set Ƣ of objects of S' consists of indexed objects – pairs (x,-i) where Embedded objects are then those indexed by 0. The desired embedding of the rank function is expressed by
Example
The diagram on the right shows the ranking product S' = (Ƣ, …) of a basic structure S = (O, …). Negatively indexed objects are displayed in khaki color. The original structure S can be identified with the restriction of S' to zero-indexed objects.

Observations:

  1. S' is a basic structure of ϵ.
  2. For every (x,-i) from Ƣ, the metalevel index of (x,-i) equals x.mli - i.
Informally, each primary object is equipped with an ϵ-chain to reach the 0-th metalevel. (The old objects have zero index, the new objects are those with a negative index.)
Ranking product
For an ϵ5-structure S = (O, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ) the ranking product of S is an ϵ5-structure S' = (Ƣ, ϵ, ϵ¯⁽*⁾, , .ec, .ɛɕ) defined as follows.

Notes:

  1. If x.mli = ω then -x.mli i is understood as a void condition.
  2. Assuming reflexivity of in S, the grayed condition j < 0 can be left out.
  3. (⁎) Since there is no constraint for primary singletons x, the definition does not preserve basic structures – if S is a basic structure in which .ɛɕ is non-empty then S' is not a basic structure. This can be presumably resolved by disallowing pairs (x,i) with i 0 for primary objects x such that However, we only need embedding of pre-basic structures so that we avoid such a complication.

Observations:

  1. For every (x,-i) from Ƣ such that i 0 the following is satisfied:
Assume (ϵ¯) (ϵ) in S.
  1. The map x (x,0) is an embedding of S into S'.
Embedding of pre-basic structures

Proposition: Let S' be the ranking product of a pre-basic structure S and denote the map x (x,0) from O to Ƣ. Then

As a particular consequence of (B) and (C), for every object x from O,   x.d = rϵ(x,0) = (x,0).d.

Proof:
The proof is divided into (proofs of) claims below.


Claim A: S' satisfies the axioms of pre-basic structures:

  1. (ϐ~1) is satisfied:   (ϵ¯) (ϵ) in S'.
  2. (ϐ~2)(ϐ~4) are satisfied.
  3. For every (x,-i) from Ƣ,   (x,-i) i < x.mli.   Corollary:
  4. (ϐ~6) is satisfied:   Ƣ.϶¯ = Ƣ.
  5. (ϐ~7) is satisfied:   For every natural k,   .϶-k .϶-k = .

Proof:

  1. This follows directly from the prescription for ϵ and ϵ¯1 in S'.
  2. Assume that for every natural k > 1, the ϵ¯k relation in S' is defined the same way as for k 1. It is then sufficient to prove that for every , , ż from Ƣ, and for every integers m, n and natural k the following is satisfied: To prove (b~0), let = (x,i) ϵ¯k (y,j) =. Then the requested and p, q are obtained according to the following: To prove (b~2), assume (x,i) ϵ¯m (y,j) ϵ¯n (z,ℓ). Then (x,i) ϵ¯m+n (z,ℓ) is a consequence of the following: To prove (b~3), assume (x,i) ϵ (y,j) ϵ-k (z,ℓ). If (x,i) ϵ¯ (y,j) then (b~2) applies. We can therefore assume further that ((x,i),(y,j)) (Ƣ, ϵ¯) so that condition (c) in the definition of (Ƣ, ϵ) is satisfied: x ϵ y and i = j = 0. Consequently, = 0, so that (x,0) ϵ1-k (z,0) follows by the embedding of ϵ and its powers.

    To prove (b~4), assume (x,i) ϵ¯m (y,j) ϵ¯-m (x,i).

    This shows the direction in the (b~4) equivalence. The reverse direction is verified similarly.
  3. This is a consequence of:   (x,-i) (r,0)x ϵ¯-i ri < x.mli.
  4. This is a consequence of:   (x,-i) ϵ¯ (r,0)x ϵ¯1-i ri x.mli.
  5. Let (y,j) be from and k a natural number. We should show that If j 0 then (y.j).϶-k k = 0 so that () follows by . = . If j = 0 then y is terminal so that for every (x,-i) from Ƣ, Since by (ϐ~7) in S there is no object x such that x ϵ¯-i-k r and x ϵ¯-i-k y, the equality () follows.

Claim B:

  1. For every (x,-i) from Ƣ,  
  2. S' is ϵ-ranked.

Proof:

  1. (a) follows by the equivalence (x,-i) ϵ¯-k (r,0)x ϵ¯-i-k r.   (b) follows by definition of (Ƣ, .ec).
  2. By groundedness in pre-basic structures, S' is ϵ-ranked iff Assume that (x,-i) is from Ƣ and x is primary. Then by definition of (Ƣ, ϵ), This shows that () holds for all primary . Finally, assume that is well-founded in (Ƣ, ϵ) and not primary. Then

Claim C:

  1. For every object x from O the following are equivalent:
  2. The ranking product S' preserves the rank:   For every object x from O,   (x,0).d = x.d.
  3. S is a faithfully embedded in S'.

Proof:

  1. The ¬(ⅰ)→¬(ⅱ) implication follows by the x (x,0) embedding. To show ¬(ⅰ)←¬(ⅱ), assume that x is an object such that a.mli is finite for every a from x.϶.϶- and (x,0) is non-well-founded in (Ƣ, ϵ), i.e. there is an infinite chain in (Ƣ, ϵ). Since (y,-j).϶y.mli+1 = for every (y,-j) from Ƣ such that j 0 and y.mli is finite, it follows that ik = 0 for every natural k. As a consequence, x is non-well-founded in (O, ϵ).
  2. Denote W the set of all x from O such that (ⅰ) from C1 is satisfied, and the set of from Ƣ that are well-founded in (Ƣ, ϵ). Define recursively functions r1() / r2() on W / by
    r1(x) = sup { r1(a) + 1 | a ϵ x } sup {a.mli + i-j | a x.϶i.϶-j, i,j } (so that x.d = r1(x) ϖ),
    r2(ẋ) = sup { r2(ȧ) + 1 | ȧ ϵ ẋ } (so that rϵ(x) = r2(x) ϖ).
    We show that r1(x) = r2(x,0) for every x from W so that, consequently, for every object x from O, Let x be from W and let = (x,0). Denote
    A = { r1(a) + 1 | a ϵ x }, B = { a.mli + i-j | a x.϶i.϶-j, i,j },
    A' = { r2(ȧ) + 1 | ȧ ϵ ẋ, ȧ O × {0} }, B' = { r2(ȧ) + 1 | ȧ ϵ ẋ } A',
    so that r1(x) = sup(A B) and r2(ẋ) = sup(A' B'). It is therefore sufficient to show that A B = A' B'. By well-founded recursion, we can assume that A = A'.

    To show B A' B', let a ϵ-j y ϵi x for some natural i, j and denote m = a.mli (so that m+i-j B). By observations about .d, we can assume that a is primary. Since j a.mli it follows that (a,-j) Ƣ. Subsequently,

    To show B' B, let ȧ = (a,-1-j) ϵ (x,0), j so that r2(ȧ) = a.mli -1-j and a ϵ-j x. Subsequently, therefore r2(ȧ)+1 B.
  3. Embedding of constituents of the signature has already been observed. Embedding of .pr follows by definition of (Ƣ, .ec). Embedding of positive powers of ϵ / ϵ¯ follows from the closedness of the set O of embedded object w.r.t. .ϵ. Finally embedding of .d has been proved in C2.
Rank in pre-basic structures
The following proposition provides a summary of main properties of the rank function .d. Properties (3)–(6) are obtained as consequences of the embedding into the ranking product.

Proposition: In a pre-basic structure S the following are satisfied.

  1. For every object x,   0 x.mli x.d ϖ.
  2. For every object x,   x.d = 0x T.
  3. For every objects x, y,   x yx.d y.d.   (That is, .d is monotone w.r.t. .)
  4. For every objects x, y,   x yx.d < y.d.
  5. For every object x such that x.ec is defined,   x.ec.d = ϖ (x.d + 1), i.e.
    x.ec.d = x.d + 1 if x.d < ϖ,
    x.ec.d = x.d if x.d = ϖ.
  6. If, in addition, (b~7) and (b~8) are satisfied then

Proof: Let S' = (Ƣ, …) be the ranking product of S.

  1. For every x,y O,
    x y (x,0) (y,0)   (by embedding of )
    (x,0).϶ (y,0).϶   (by subsumption in S')
    rϵ(x,0) rϵ(y,0)   (by definition of rϵ)
    (x,0).d (y,0).d   (since S' is ϵ-ranked)
    x.d y.d   (by embedding of .d).
  2. For every x,y O,
    x y (x,0) (y,0)   (by embedding of )
    rϵ(x,0) < rϵ(y,0)   (by definition of rϵ)
    x.d < y.d.
  3. For every x,y O,
    x.ec = y (x,0). = (y,0).϶   (by embedding of .ec)
    ϖ (rϵ(x,0) + 1) = rϵ(y,0)   (since rϵ(u,i) rϵ(x,0) for every (u,i) from (x,0).)
    ϖ (x.d + 1) y.d.
  4. For every x,y O,
    x.ɛɕ = y {(x,0)} (y,-1).϶ = (y,0).϶   (by embedding of ϵ and the additional assumptions)
    (rϵ(x,0) + 1) (rϵ(y,-1) + 1) = rϵ(y,0)   (since rϵ(ẏ) rϵ(y,-1) for every from (y,-1).϶)
    (x.d + 1) y.mli = y.d   (by definition of (Ƣ, ϵ))
    x.d + 1 = y.d   (since y.mli y.d).

Powerclass completion

In this section we show that every basic structure can be faithfully embedded into a powerclass complete basic structure.
Powerclass completion
Let S = (O, ϵ, …) be an ϵ5-structure and S0 = (O0, ϵ, …) a pre-basic structure. We say that S is a powerclass completion of S0 if S is an extension of S0 that is created in the following steps:
  1. Extend (O0, .ec) to (O, .ec) so that There is obviously exactly one such extension, up to isomorphism.
  2. Extend ϵ and ϵ¯⁽*⁾ to ϵ and ϵ¯⁽*⁾ according to the following.
    For every primary objects a, b and every natural i, j such that at least one of a.ec(i) or b.ec(j) is a new object, the following holds:
    (α) a.ec(i) ϵ b.ec(j)   iff   a ϵ¯1+i-j b,
    (β) a.ec(i) ϵ¯k b.ec(j)   iff   a ϵ¯k+i-j b     for every integer k.
Since this definition asserts the existence of a unique, up to isomorphism, ϵ5-structure S for any given pre-basic structure S0 we can also speak about the powerclass completion of S0.

Observations:

  1. In (Ⅱ), primary can be replaced by old and natural i, j by integer i, j.
  2. For a pre-basic structure S0 and an ϵ5-structure S the following are equivalent:
    1. S is a powerclass completion of S0.
    2. S is the least extension of S0 that is powerclass complete.
The powerclass completion theorem

Proposition:

Proof:
The proof consists in verifying that S satisfies (b~1)(b~11) and is a faithful extension of S0. This is done in a series of claims below.


Claim A:

  1. Axioms (b~2)(b~4) are satisfied. For every integers m, n,
    1. (ϵ¯m) (ϵ¯n) (ϵ¯m+n),
    2. (ϵ) (ϵn) (ϵ1+n),
    3. (ϵ¯m) (϶¯-m) = .ec(m).
  2. Every new object x is both a power member and power container: x.ϵ = x.ϵ¯ and x.϶ = x.϶¯.
    Corollary: For every old object x,  
  3. (a) (O O0) r,   (b) O.ϵ = O.ϵ (O O0),   (c) O.ϵ = O.ϵ O0.  
    Corollary: (b~5), (b~6) and (b~7)(b) are satisfied.
  4. For every old object x, if x.ec0- = x.϶¯- then x.ec- = x.϶¯-.   Corollary: (b~7)(a) is satisfied.
  5. Axiom (b~8) is satisfied: If x.ɛɕ = y then: (a) {x} = y.϶, (b) x.ϵi y.ϵi-1 for every i 1, (c) (x,y) (ϵ¯).
  6. Axiom (b~10) is satisfied: For every object x,   x.mli < ω.

Proof:

  1. Let a, b, c be primary objects, i, j, k natural numbers and m, n integers.
  2. This follows directly from the prescriptions (α) and (β) (k = 1) for ϵ¯ and ϵ.
  3. Let x be a new object, x = a.ec(i) for a primary a and a natural i > 0. Then To show (c), assume that x ϵ y and y is old. (That is y O.ϵ O0.) Then
  4. Assume that x is an old object such that x.ec0- = x.϶- and let y be from x.϶-. That is, where b is a primary object and j a natural number such that y = b.ec(j). By definition of ϵ¯i,
  5. Assume x.ɛɕ = y. Then both x, y are old (since .ɛɕ0 = .ɛɕ). Therefore, (a) and (c) are satisfied. If i is an integer, i 1, and z is a new object from x.ϵi then which shows that also (b) is satisfied.
  6. This is a consequence of the following equivalence: For every object x, and every natural j, (Therefore, x.mli = sup { j | x ϵ1-j r, j } = sup { j | a ϵ1+i-j r, j } = i + a.mli0.)

Claim B:

  1. For every old objects x, y and every natural i,   (a)   x ϵi y   ↔   x ϵi y,   (b)   x ϵ¯i y   ↔   x ϵ¯i y.
  2. For every old object y,   (a) y.϶ y.϶., (b) y.϶¯ = y.϶¯..

Note: We let ϵ¯k be defined in (β) just for k 1.

Proof:

  1. To prove (a), assume n > 1 and let x, y be old objects such that x ϵn y. That is, there are old objects x = x0, x1, …, xn-1, xn = y and natural numbers 0 = i0, i1, …, in-1, in = 0 such that We can assume that all of x1.ec(i1), …, xn-1.ec(in-1) are new objects – otherwise the proof follows by induction over n. We can therefore apply the definition (α) of (ϵ) (ϵ) and write which implies x ϵ¯n y (and thus x ϵn y).

    To prove (b), assume n > 0 and let x, y be old objects such that x ϵ¯n y, that is, x.ec(n) y.

  2. Assume that y is an old object. Let a be an old object and i a natural number such that x = a.ec(i) is a new object from y.϶ so that a ϵ¯1+i y by definition of ϵ. In particular, there exists an old object u such that a ϵ¯i u ϵ¯ y. It follows from x.ec(-i) = a ϵ¯i u that x u. This shows (a) y.϶ y.϶. and also y.϶¯ y.϶¯.. The y.϶¯ y.϶¯.϶¯0 inclusion follows by (b~2).

Claim C:

  1. S preserves the rank of old objects, i.e. for every old object x,   x.d = x.d0.
  2. Axiom (b~11) is satisfied:   x.ϵ = x.ϵ¯ for every x from O O..

Proof:

  1. Consider the ranking products (Ƣ0, ϵ, …) and (Ƣ, ϵ, …) of S0 and S, respectively. Since S is already known to be a pre-basic structure, (Ƣ, ϵ, …) is an extension of (Ƣ0, ϵ, …), in particular w.r.t. ϵ and . It is then sufficient to show that Assume that (y,-j) is from Ƣ0 and let (x,-i) be from (y,-j).϶. We should prove that (x,-i) (u,k) for some (u,k) from Ƣ0.
  2. Apply claims A2 and C1.

Singleton completion

The diagram on the right shows an extension of a basic structure S0 = (O0, …) to a basic structure S = (O, …) by primary singletons. New objects are those from {a,b,e}.ɛɕ (indicated by orange circles (). The difference between (O, ϵ, ) and (O0, ϵ, ) is indicated by dashed arrows. Moreover, the (ϵ) (ϵ¯) difference is indicated by blue arrows with a highlighted background, similarly as with the introductory sample. In S0, the difference is {(a,w)}.

Since {a,b,e} = O. (T O.ɛϲ), the resulting extension S is primary singleton complete – every bounded object that is not terminal or a singleton has a singleton. A subsequent partial powerclass completion of S, applied just for the set T O.ɛϲ, makes S singleton complete, so that all bounded objects have a singleton.

Primary singleton completion
Let S = (O, ϵ, …) be an ϵ5-structure and S0 = (O0, ϵ, …) a basic structure. We say that S is a primary singleton completion of S0 if S is a primary extension of S0 such that
The singleton completion theorem

Proposition:

Proof:
We consider an ϵ5-structure S = (O, ϵ, …) created from a basic structure S0 = (O0, ϵ, …) in the following steps:

Now the proof consists in verifying that S is a basic structure that is a faithful extension of S0 and is singleton complete.

Claim A:

  1. For every old objects x, y and every natural i,   (a)   x ϵi y   ↔   x ϵi y,   (b)   x ϵ¯i y   ↔   x ϵ¯i y.
  2. For every old object y,   y.϶ y.϶..

Proof:

  1. Let x, y be old objects and i a natural number. We can assume that i > 1. Then
  2. Assume that y is an old object and let a and b be objects such that a.ɛɕ = b ϵ y and b is new. By definition of b.ϵ, there is an old object u such that a ϵ u ϵ¯ y. By definition of b., it follows that b < u.

Claim B:

  1. (b~2) is satisfied. For every object y, and every integer i, j,     (ⅰ) y.ϵ¯i.ϵ¯j y.ϵ¯i+j   and   (ⅱ) y.϶¯i.϶¯j y.϶¯i+j.
  2. (b~3) is satisfied: For every objects x, y, z and every natural i,   if x ϵ y ϵ-i z then x ϵ1-i z.
  3. (b~4) is satisfied: For every objects x, y and every integer i,   x ϵ¯i y ϵ¯-i x x.ec(i) = y.
  4. (b~5) is satisfied: O.ϵ r.
  5. (b~6) is satisfied: T O.϶.
  6. (b~7)(a) is satisfied: y.϶-i {y}.ec(i) for every y T O.ɛɕ and every natural i.
  7. (b~7)(b) is satisfied: x.ϵ = x.ϵ¯ for every x (T O.ɛɕ).ec.
  8. (b~8) is satisfied: If x.ɛɕ = y then: (a) {x} = y.϶, (b) x.ϵi = y.ϵi-1 for every i 1, (c) (x,y) (ϵ¯).
  9. For every new object y = x.ɛɕ,   y.mli = x.mli + 1.
    Corollary: (b~10) is satisfied. (Every object has a finite metalevel index.)

Proof:

  1. For every new object u and every integer i it follows by definition that This shows that (ⅰ) is satisfied for all old objects y and (ⅱ) is satisfied for all objects y. It remains to show that (ⅰ) is satisfied if y is new. Assume therefore that x.ɛɕ = y and y is new. Denote Y = y.ϵ¯i.ϵ¯j.
  2. We first show that for every object y and every natural i,   (ⅰ) y.ϵ.ϵ-i y.ϵ1-i   and   (ⅱ) y.϶-i.϶ y.϶1-i.
    Assume that y is new and let x be such that x.ɛɕ = y. Then (ⅱ) is satisfied since To show (ⅰ), write y.ϵ.ϵ-i = x.ϵ.ϵ¯.ϵ¯-i x.ϵ.ϵ¯1-i. Denote Z = x.ϵ.ϵ¯1-i. It is sufficient to show that y.ϵ1-i Z. Thus, (ⅰ) and (ⅱ) hold for every new y. This shows that is satisfied for every objects x, y, z such that at least one of x or z are new. (Note that this time the y variable is used in the middle place.) It remains to show that () holds if y is new. Assume therefore that x, y, z are objects such that x ϵ y ϵ-i z and y is new. Then necessary x.ɛɕ = y and it is sufficient to show that x.ϵ.ϵ-i x.ϵ1-i.
  3. If x and y are old then (b~4) in S0 applies. If x or y is new then
  4. If x.ɛɕ = y and y is new then y. x.ϵ r.
  5. This is a consequence of new objects being non-terminal.
  6. Let y be from T O.ɛɕ and let u be from y.϶-i for a natural i. We should prove that y.ec(i) = u. For u and y both being old this is asserted by (b~7) in S0. If y is new then by the prescription for primary singleton completion, i = 0 and u = y so that the requested equality is satisfied.
  7. Let x be from (T O.ɛɕ).ec. If x is old then x.ϵ = x.ϵ (since x.ɛɕ is undefined) and thus x.ϵ = x.ϵ¯. If x is new then the same equality holds by the prescription for primary singleton completion.
  8. Assume that x.ɛɕ = y. If y is old then so is x and (b~8) in S0 applies: For a new object y the definition of primary singleton completion applies.
  9. Let x.ɛɕ = y and y be new. By definition, y.ϵ-i = x.ϵ1-i for every i > 0, so that Since x is non-terminal it follows that x ϵ1-i r is satisfied for i > 0 (put i = x.mli). As a consequence, y.mli = x.mli+1.

Claim C:

  1. S preserves the rank of old objects, i.e. for every old object x,   x.d = x.d0.
  2. Axiom (b~11) is satisfied:   x.ϵ = x.ϵ¯ for every x from O O..

Proof:

  1. Consider the ranking products (Ƣ0, ϵ, …) and (Ƣ, ϵ, …) of S0 and S, respectively. Let y be an old object. To prove that y.d = y.d0 it is sufficient to show that Assume (x,-i) ϵ (y,0) and (x,-i) is not from Ƣ0 so that x is a new object. Let a be such that a.ɛɕ = x. The requested pair (u,-k) in () is then found as follows. If i = 0 then x ϵ y so that, by claim A2, x u ϵ y for some u and thus (u,0) is the requested pair. Assume further that i > 0. Then Since a.mli = x.mli-1, it follows that (x,-i).d (a,1-i).d and thus (a,1-i) is the requested pair.

    Finally, assume that y is new and x.ɛɕ = y. Since y.϶ = {x} and x is bounded it follows that

    Because (y,-1).d = y.mli-1 = x.mli x.d = (x,0).d the equality y.d = x.d+1 follows.
  2. By claim C1, S and S0 have the same unbounded objects. If x is an unbounded (and therefore old) object then, x.ϵ = x.ϵ = x.ϵ¯ = x.ϵ¯.

Extensional pre-completion

The diagram on the right shows an extension of a powerclass complete basic structure S0 = (O0, …) to a powerclass complete basic structure S = (O, …) by an attachment of a free leaf u. New objects are those from u.ec. The difference between (O, ) and (O0, ) is indicated by dashed brown arrows (again in the reflexive transitive reduction). The extension causes the following change for the m object (of which u is a direct free leaf in S, i.e. u.ԏ = m): As a result, m becomes extensionally consistent (which was not the case in S0 since m. = n. and m n). Moreover, all new objects are extensionally consistent as well as all old objects that were extensionally consistent in S0.

The above method can be used to achieve extensional consistency and powerclass consistency for all objects.

Extensional pre-completion
Let S = (O, ϵ, …) be an ϵ5-structure and S0 = (O0, ϵ, …) a basic structure that is metaobject complete. We say that S is an extensional pre-completion of S0 if S is an extension of S0 such that the following conditions are satisfied:
  1. .ec is total, well-founded and injective. (So is therefore (.ec) (.ec0) in the restriction to new objects.)
  2. .ɛɕ is the same as .ɛɕ0.
  3. For every new primary object x and every i ≥ 0, j 1, In particular, the set O0 of old objects is closed w.r.t. .ϵ-.
  4. For every new primary object x, there is a unique old primary object y such that, denoting k = y.mli, for every i ≥ 0, j 1,
  5. For every old object y, the set y.ԏ(-1) O0 of new direct free leaves of y has exactly (There can be a finer prescription which adds exactly 1 new direct free leaf of y in relevant cases.)

Observation: Every metaobject complete basic structure S0 has an extensional pre-completion S.

Proof:
Let S0 = (O0, ϵ, ϵ¯⁽*⁾, r, .ec0, ɛɕ0) be a metaobject complete basic structure and construct S as follows.

  1. Let (N, O0, .ec1, .ԏ1) be a two-sorted structure that is isomorphic to (Ṅ, O0, .ec1, .ԏ1) where
  2. Let S = (O, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ) be an ϵ5-structure that is an extension of S0 defined by:
The extensional pre-completion theorem

Proposition:

Proof:
Let S = (O, ϵ, …) be an extensional pre-completion of a metaobject complete basic structure S0 = (O0, ϵ, …).


Claim A: (Observations)

  1. For every old objects x, y and every natural i,   (a)   x ϵi y   ↔   x ϵi y,   (b)   x ϵ¯i y   ↔   x ϵ¯i y.
  2. For every new object x and every integer i,

Claim B:

  1. (b~2) is satisfied. For every objects x, y, z and every integer k,   if x ϵ¯k y ϵ¯ z then x ϵ¯k+ℓ z.
  2. (b~3) is satisfied: For every objects x, y, z and every natural k,     if x ϵ y ϵ-k z then x ϵ1-k z.
  3. (b~4) is satisfied: (ϵ¯i) (϶¯-i) = .ec(i) for every integer i.
  4. (b~5) is satisfied: O.ϵ r.
  5. (b~6) is satisfied: O = O.϶.
  6. (b~7)(a) is satisfied: z.϶-i {z}.ec(i) for every z T O.ɛɕ and every natural i.
  7. (b~7)(b) is satisfied: x.ϵ = x.ϵ¯ for every x (T O.ɛɕ).ec.
  8. (b~8) is satisfied: If x.ɛɕ = y then: (a) {x} = y.϶, (b) x.ϵi = y.ϵi-1 for every i 1, (c) (x,y) (ϵ¯).
  9. (b~10) is satisfied: O.mli < ω.
  10. (b~11) is satisfied: x.ϵ¯ = x.ϵ for every unbounded object x.

Proof:

  1. Let x ϵ¯k y ϵ¯ z, k, ℓ . Moreover, let (a,i) = (x.pr,x.eci) so that x = a.ec(i). Since the set O0 of old objects is closed w.r.t. .ϵ- there are 3 cases to check:
  2. Let x ϵ y ϵ-k z, k . If x is new then x ϵ¯ y and thus (b~2) applies. Otherwise, all of x, y and z are old and thus (b~3) in S0 applies.
  3. (b~4) follows by O0.ϵ- = O0 and claim A2.
  4. Let x be a new object and let a,i,y be such that a.ec(i) = x and a.ԏ = y. Denote k = y.mli. Then It follows that x.ϵ cannot contain an old object z that is terminal in S0. (It would follow from z y.ϵ¯1+i-k T that z = y and k = 0 and thus z ϵ¯1+i z for i ≥ 0 which is not possible.) Since by definition a.ec(i+1). = a.ϵ¯i+1 it follows that and thus a.ec(i+1) < r. This shows that x.ϵ r and, consequently, O.ϵ r.
  5. The O = O.϶ equality follows by:   x ϵ x.ec for every new object x.
  6. Assume that z T O.ɛɕ and i . If z is new then z.϶-i = {z}.ec(i) by definition of extensional pre-completion. Assume further that z is old and let a be a new primary object, j and denote k = a.ԏ.mli. Then the following equivalences are satisfied: Since z satisfies the (◉) condition the a.ԏ = z is disallowed. This shows that all objects from z.϶-i are old and thus z.϶-i = z.϶-i = {z}.ec(i) by (b~7) in S0.
  7. (b~7)(b) follows by O0.ϵ- = O0 and the x.ϵ = x.ϵ¯ equality which holds for every new object x.
  8. Assume that x.ɛɕ = y so that both x and y are old objects. To show that y.϶ cannot contain new objects and thus (b~8)(a) is satisfied, proceed similarly as in the proof of (b~7). Subsequently, (b~8)(b) follows by O0.ϵ- = O0 and (b~8)(c) follows by embedding of ϵ¯.
  9. By embedding of ϵ¯i, the metalevel index of old objects is preserved. Since new objects are from T.ec and S is already asserted to be pre-basic, it follows that for every new object x, x.mli = x.eci which is finite by definition. (Apply (a) x.mli = 0 for x T and (b) x.ec(i).mli = x.mli + i.)
  10. Since new objects are from T.ec, every unbounded object x is old and is subject to the x.ϵ¯ = x.ϵ equality as a consequence of O0.ϵ = O0.

Claim C:

  1. S preserves the rank of old objects, i.e. for every old object x,   x.d = x.d0.
  2. S is metaobject complete and e+p consistent (extensionally consistent and powerclass consistent).

Proof:

  1. Observe first that since new objects are from T.ec and S is pre-basic it follows that Consider the ranking products (Ƣ0, ϵ, …) and (Ƣ, ϵ, …) of S0 and S, respectively. Observe that since new objects of S are from T.ec it follows that new objects of (Ƣ, ϵ, …) have zero index, that is, they are of the form (x,0) where x is a new object of S. Let z be an old object that is well-founded in (O, ϵ) and thus in (Ƣ,ϵ). It is sufficient to show that Assume therefore that = (x,0) is a new object from (z,0).϶ so that x ϵ z and let a, i, k be such that a.ec(i) = x and k = a.ԏ.mli. Then the requested object is found according to:
    x ϵ z a.ԏ ϵ¯1+i-k z (a) i k and (a.ԏ, i-k) ϵ (z,0)   (by definition of (Ƣ,ϵ))   or
    (b) i ≥ k and a.ԏ.ec(i-k) ϵ z   (by properties of .ec).
    In the (a) case, put = (a.ԏ, i-k), in the (b) case, put = (a.ԏ.ec(i-k),0). In both cases, ḃ.d = k + (i-k) = ẋ.d.
  2. Since S0 is metaobject complete, and, in the restriction to new objects, .ec is total and identical to .ɛϲ, it follows that S is metaobject complete. To show that S is e+p consistent, let x be an object.

Rank pre-completion

The diagram on the right shows a basic structure S that is
  1. powerclass complete,
  2. extensionally consistent (for every natural i, r.ec(i). = b.ec(i).ec and b.ec(i+1). = {b}.ec(i) and thus x. y.x y for every non-terminal x,y),
  3. singleton complete (since T.ec = O.), and
  4. powerclass consistent (r is not powerclass-like since {b,b.ec} has no upper bound).
If ϖ = ω (recall that ϖ is a fixed limit ordinal and ω is the least limit ordinal) then S is also
  1. -ranked
and thus pre-complete. If ϖ > ω then S is not -ranked and needs to be equipped with additional bounded objects to become pre-complete.

Note: The S structure shown by the diagram is a minimal basic structure such that (a) and (b) are satisfied and thus minimal such that (a)–(d) are satisfied. It follows that if ϖ = ω then S is a minimal pre-complete structure.

The omissible case ϖ = ω

Proposition: Let S be a basic structure such that (a) () = () (0) and (b) T.ϵ = O (i.e. S is ϵ-grounded and therefore ϵ-ranked). Then the following are satisfied:

  1. For every object x, (recall that r(x) denotes the -rank of x)
    r(x) = x.d if x is well-founded in ϵ,
    r(x) ≥ ω otherwise.
  2. Corollary: If ϖ = ω then S is -ranked.

Proof:

  1. Let W be the set of objects that are well-founded in ϵ and denote r() the rank function in (W,ϵ). Let x be an object from W. If r(x) ϖ then x.϶ = x. and thus r(x) = r(x) = rϵ(x) = x.d. Assume that r(x) > ϖ. Then ϖ r(u) for some u from x.϶ and thus
    ϖ = u.d = sup(u..d)   (by the induction assumption)
    sup(u.0.d)   (since () = () (0))
    sup(x..d)   (since u ϵ¯ x so that u.0 x.)
    = r(x).
    It follows that r(x) = rϵ(x) = x.d = ϖ. Finally, if x O W then
    x.϶i for every natural i   (a consequence of non-well-foundedness of x),)
      ↔   x O.ϵi for every natural i
      →   x T.ϵi for infinitely many natural i   (since T.ϵ = O)
      ↔   x T.i for infinitely many natural i   (by proposition A2)
      →   r(x) ≥ ω   (by definition of -rank).
Rank pre-complete structure
We say that a basic structure S is rank pre-complete if every primary object that is non-well-founded in ϵ is -ranked.

Observation: Let S be a basic structure that is rank pre-complete.

  1. If () = () (0) then every non-well-founded object is -ranked.
  2. Corollary: If, in addition, S is extensionally consistent and metaobject complete then S is -ranked.

Proof:

  1. This is shown by As a consequence, for every object x,   r(x) = ϖ   ↔   r(x.pr) = ϖ.
  2. Let S be a basic structure that is (a) is extensionally consistent, (b) metaobject complete (i.e. (b1) powerclass complete and (b2) singleton complete) and (c) rank pre-complete. By the -levelling proposition, it follows from (a) and (b1) that S is -levelled, in particular T.ϵ = O. Moreover, it follows from (b2) that () = () (0) so that, denoting W the set of objects that are well-founded in ϵ, for every object x,
Rank pre-completion
Let S = (O, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ) be an ϵ5-structure and S0 = (O0, ϵ, …) a basic structure. We say that S is a rank pre-completion of S0 if S is an extension of S0 such that
(1) .ec = .ec0 and .ɛɕ = .ɛɕ0,
and there is a (necessarily unique) map from O O0 to O0 such that the following are satisfied:
(2) O is the set all non-well-founded primary objects of S0 that are not -ranked in S0.
(3) For every object y from O, if X = {y}.τ(-1) (i.e. X is the fiber of y under ) then the following holds:
(a) X is closed w.r.t. .϶-.
(b) For every natural k > 0,   both y.϶-k X and X.϶-k are empty.
(c) X y.϶ y.϶¯ y..
(d) (X, ϵ¯) = (X, ϵ) = (X, <) (ϖ, <).  
In (d), (X, <) (ϖ, <) means that (X, <) is isomorphic to the strict order between ordinals less than ϖ.
(4) For every new object x, every old object z such that z x.τ and every integer k 1,  
  • x ϵk z  ↔  x ϵ¯k z  ↔  x.τ ϵ¯i z for some integer i k.
Note that ϵk and ϵ¯k can be used interchangeably here since x.τ is unbounded.

Observation: Every basic structure S0 has a unique rank pre-completion S, up to isomorphism.

Proof:
Given a basic structure S0 = (O0, ϵ, …), proceed in the following steps.

  1. Let be the set of all pairs (x,i) where x an old primary objects that is not -ranked in S0 and i is an ordinal number less than ϖ. Define relations ϵ, , ϵ¯ and ϵ-k, k > 0, on by
  2. Let (N, ϵ, ϵ¯⁽*⁾) be isomorphic to (Ṅ, ϵ, ϵ¯⁽*⁾) via .ν : Ṅ N and let be the unique map N O0 such that (x,i).ν.τ = x.
  3. Let S = (O, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ) be an extension of S0 such that
The rank pre-completion theorem

Proposition:

Proof:
The proof is accomplished in a series of claims below. Assume that S = (O, ϵ, …) is a rank pre-completion of a basic structure S0 = (O0, ϵ, …).


Claim A: (Observations)

  1. The set O0 of old objects is closed w.r.t. .ϵ-.
    Corollary: For every old objects x, y and every natural i,   (a) x ϵi yx ϵi y,   (b) x ϵ¯i yx ϵ¯i y.
  2. For every new object x,   x.mli = x.τ.mli.
  3. For every new object x and every integer k,   x.϶¯k = x.϶k and x.ϵ¯k = x.ϵk.   (In particular, x.ϵ = x.ϵ¯.)
  4. For every new object x and every integer k,   x ϵk x.τx ϵ¯k x.τk ≥ 0.
  5. The set O0. of old bounded objects is closed w.r.t. .϶-.
  6. The set of old objects that are well-founded in (O0, ϵ) is closed w.r.t. .϶-.

Proof:

  1. The O0 = O0.ϵ- equality is a consequence of (3a).
  2. Let x be a new object and k a natural number. If x.τ = r then x ϵ1-k rk 1 by (3bc). Otherwise (4) applies: It follows in both cases that x.mli = x.τ.mli.
  3. The equalities follow directly from (3) and (4).
  4. Let x be a new object and k an integer. For k 1 the requested equivalences are asserted by (3bc). Assume that k > 1 and denote X = {x}.τ.τ(-1). Then it follows from (3d) that x.ϵ¯k-1 X = x.ϵk-1 X (the non-emptiness is a consequence of ϖ being a limit ordinal) so that x.τ x.ϵ¯k-1.ϵ¯ x.ϵk-1.ϵ.
  5. Assume that x is a new object, and z is an old object such that x ϵk z for some integer k 1. We have to show that z is unbounded in S0. If x.τ = z then z is unbounded by definition of O. For x.τ z condition (4) applies so that x.τ ϵi z for some integer i k. Since x.τ is unbounded in S0, so must be z.

Claim B:

  1. (b~2) is satisfied. For every objects x, y, z and every integer k,   if x ϵ¯k y ϵ¯ z then x ϵ¯k+ℓ z.
  2. (b~3) is satisfied: For every objects x, y, z and every integer ,     if x ϵ y ϵ z then x ϵ1+ℓ z.
  3. (b~4) is satisfied: For every objects x, y and every integer k,   x ϵ¯k y ϵ¯-k x  ↔  x.ec(k) = y.
  4. (b~5) is satisfied: O.ϵ r.
  5. (b~6) is satisfied: T O.϶.
  6. (b~7)(a) is satisfied: x.϶-i {x}.ec(i) for every x T O.ɛɕ and every natural i.
  7. (b~7)(b) is satisfied: x.ϵ = x.ϵ¯ for every x (T O.ɛɕ).ec.
  8. (b~8) is satisfied: If x.ɛɕ = y then: (a) {x} = y.϶, (b) x.ϵi = y.ϵi-1 for every i 1, (c) (x,y) (ϵ¯).
  9. (b~10) is satisfied: O.mli < ω.

Proof:

  1. Assume x ϵ¯k y ϵ¯ z, k,ℓ 1, k+ℓ 1.
  2. Apply claims A3 and A5.
  3. Let x, y be objects and k an integer such that x ϵ¯k y ϵ¯-k x or x.ec(k) = y. Since O0.ϵ- = O0 and .ec = .ec0, it follows that either both x and y are old or both are new.
  4. O.ϵ r since x r for every new object x and T0.϶ = .
  5. (b~6) is a consequence of:   Every terminal object is old.
  6. If x T O.ɛɕ then x is necessarily an old object that is bounded in S0 so that claim A5 applies.
  7. All objects from (T O.ɛɕ).ec are old so that O0.ϵ- = O0 applies.
  8. If x.ɛɕ = y then both x and y are old and bounded in S0. Consequently, apply the closedness of O0. w.r.t. .϶-, the closedness of O0 w.r.t. .ϵ-, and ϵ¯i being embedded into ϵ¯i for every integer i.
  9. This follows from x.mli = x.τ.mli for every new object x (claim A2).

Claim C:

  1. For every old object x,   x.d = x.d0.   (I.e. S preserves the rank of old objects.)
  2. For every new object x,   x.d = x.mli + rϵ(x) < ϖ   (and thus r(x) = rϵ(x)).
  3. Axiom (b~11) is satisfied:   x.ϵ = x.ϵ¯ for every x from O O..
  4. Every non-well-founded primary object x is -ranked.   (That is, S is rank pre-complete.)

Proof:

  1. Let X be the set of all old objects that are well-founded in ϵ. Since X is closed w.r.t. w.r.t. .϶- it follows that x.d = x.d0 for every x from X. Objects from O0 X stay non-well-founded in ϵ and have therefore rank ϖ both in S0 and S.
  2. Denote N = O.τ(-1) the set of new objects and proceed by well-founded induction on (N, ϵ). Let x be from N. Since N.϶-k is empty for every k > 0 and x.϶.mli = {x}.mli it follows by definition of .d that If x.϶ = (i.e. rϵ(x) = 0) then a ϵi xi = 0 so that x.d = ϖ (x.mli + 0) = x.mli. Assume further that rϵ(x) > 0. By induction assumption, Since rϵ(x) ≥  sup {i | a ϵi x, i } it follows that x.d = ϖ (x.mli + rϵ(x)). Finally, rϵ(x) < ϖ since by definition of rank pre-completion, (X, ϵ) (ϖ, <) where X = {x}.τ.τ(-1).
  3. This follows by the closedness of O0 w.r.t. .ϵ.
  4. Let x be a non-well-founded primary object and denote X = x.τ(-1). It follows that (X, ) = (X, ϵ) (ϖ, <) and thus r(X) = ϖ. Since X x. the statement follows.

 

ϵ-structure

In this section we develop a formal language for families of structures based on a single relation of membership on a set.
ϵ-structure
By an ϵ-structure we mean a structure (O, ϵ) where There are no additional constraints for (O, ϵ). Let rϵ() be the ϖ-limited rank function O ϖ+1, i.e. rϵ(x) = ϖ for every object x that is non-well-founded in ϵ, and An object x is bounded if rϵ(x) < ϖ, otherwise x is unbounded. Similarly, a set Y O is bounded (resp. unbounded) if sup { rϵ(x) | x Y } is less (resp. equal to) ϖ.

The following derived relations , , 0 and ϵ¯ between objects are distinguished. Like in ϵ5-structures, we use the symbols .ϵ/.϶ and ./. for the respective image/preimage operators of ϵ and . Similarly for , 0 and ϵ¯.

Observations:

  1. is a well-founded relation of rank at most ϖ+1.
  2. For every objects x and y the following are satisfied:
  3. (ϵ) () = (ϵ) and () () = ().
-rank
In an ϵ-structure S = (O, ϵ) we let r(x) denote the -rank of an object x, i.e. We say than a object x is -ranked if rϵ(x) = r(x). The structure S is -ranked if rϵ(x) = r(x) for every object x.

Observations:

  1. For every object x, the following holds.
  2. If (•) is assumed then (ⅰ)–(ⅲ) hold:

Proof:

  1. Note first that in both (•) and (ⅰ) we can replace by since the direction is satisfied implicitly. Assume that (•) is satisfied.

-structure

As a counterpart to ϵ-structures we develop a language of -structures. We start with the symbol which stands for an (intentionally) well-founded membership.
-structure
x y   ↔   x = y or x. y.
x 0 y   ↔   x y and x O.
x ϵ¯ y   ↔   x.0 y.
x ϵ y   ↔   x y or x ϵ¯ y
By an -structure we mean a structure (O, ) where The derived relations , 0, ϵ¯ and ϵ between objects are defined according to the table to the right. The terminology for these relations is the same as in ϵ-structures. Moreover, the i-th power of ϵ, ϵ¯ and for a positive natural i is defined in the usual sense of relational composition. The 0-th power of ϵ or ϵ¯ equals .

Observations:

  1. Like in ϵ-structures, (a) is a pre-order, (b) 0 is transitive, (c) () () = (), (d) (ϵ) () = (ϵ).
  2. equals the domain restriction of ϵ to O..
  3. O. = O.ϵ.

Proof:

  1. We should prove that for every objects x, y,   x y   ↔   x ϵ y and x O.. The direction follows by () (ϵ). To show , assume x ϵ y and x O..

Proposition:

  1. For every objects x, y the following holds:  
    1. x. y.   →   x.϶¯ y.϶¯.
    2. x. y.   ↔   x.϶ y.϶.
    3. x y   ↔   x = y or x.϶ y.϶.
  2. Assume (a) () = () (0) and (b) O = O. O.. Then for every objects x, y the following holds:  
    1. x. =   →   x. = x.0 = {x}.
    2. {x} = y.   →   y. = y.0 {y}.   (If antisymmetry of is asserted then can be replaced by =.)
    3. x.0 is non-empty.
    4. x y   ↔   x.0 y.0.
    5. x. y.϶   ↔   x.0 y.   (↔ x ϵ¯ y by definition of ϵ¯).
    6. x. = y.϶   ↔   x.0 = y..
    7. x. = y.϶   →   x.ϵ¯ = y..
    8. x. = y.϶   ↔   x.ϵ¯ = y.   assuming x. = z.϶ for some object z.

Proof:

    1. Assume x. y.. Then for every object u,   u ϵ¯ xu.0 x.u.0 y.u ϵ¯ y.
    2. The direction follows by being a domain-restriction of ϵ, follows from A1.
    3. Apply the previous statement and the O.ϵ = O. equality.
    1. Let x be such that x. = . Then x. = {x} by definition of . By definition of 0, x.0 = x. O.. Since x O. by (b), the equality x.0 = {x} follows.
    2. Apply condition (a).
    3. For x. = apply B1. Otherwise, apply condition (a): a xa b 0 x for some b.
    4. If x y then x. y.. Since z.0 = z. O. for every object z, the inclusion x.0 y.0 follows. Conversely, assume x.0 y.0.
      • If x. = then {x} = x.0 and thus x 0 y, in particular x y.
      • If x. then apply (a):   x.0 y.0   →   x.0. y.0.   →   x. y.   →   x y.
    5. The direction follows by 0 and being the domain-restriction of and ϵ, respectively, to O.. To show , assume x.0 y., i.e. x ϵ¯ y. Then for every object u,
      • u x   →   u.0 x.0 y.   →   u ϵ¯ y   →   u ϵ y.   (The first implication uses (a).)
      This shows x. y.϶.
    6. The direction follows by the same argument as with the previous statement. To show , assume x.0 = y.. Let u be an object from y.϶. Then
      • u ϵ¯ y   ↔   u.0 y.   →   u.0 x.0   ↔   u x,
      • (u,y) (ϵ¯)   →   u y   →   u x.0   →   u x.
      This shows x. y.϶. The converse inclusion is shown like in the previous statement.
    7. Assume x. = y.϶. (In particular y.϶ .) Then for every object u,
      • x ϵ¯ u   ↔   x. u.϶   ↔   y.϶ u.϶   ↔   y u.   (The last equivalence is due A3.)
      This shows x.ϵ¯ = y..
    8. Assume x. = z.϶ and x.ϵ¯ = y.. Using the previous statement we obtain
      • y. = z.   →   y z y   →   y.϶ = z.϶.
-ϵ-structure
By an -ϵ-structure we mean an -structure (O, ) satisfying the following conditions:
(-ϵ~1) is well-founded.
(-ϵ~2) O. equals the set of objects whose -rank is strictly less than ϖ. (In particular, O = O. O..)
(-ϵ~3) () = () (0).
(-ϵ~4) (ϵ) = () (ϵ¯). (Bounding monotonicity)
(-ϵ~5) For every objects x, y,   x. y.   →   x.϶ y.϶. (Extensional consistency)
(-ϵ~6) For every objects x, y,   x.0 y.   →   x. y.϶. (Power-extensional consistency)
The horizontal line indicates that conditions (-ϵ~4)–(-ϵ~6) are redundant. They are used for further reference.
Correspondence of ϵ-structures and -structures

Proposition: Let S = (O, ϵ, , , 0, ϵ¯) be a structure of 5 relations on a set O of objects satisfying (-ϵ~1)–(-ϵ~6). Then the following are equivalent:

That is, assuming (-ϵ~1)–(-ϵ~6), conditions (ⅰ) and (ⅱ) in the following table are equivalent:
Relation (ⅰ)
Definition in ϵ-structure
(ⅱ)
Definition in -structure
x ϵ y and rϵ(x) < ϖ   ↔   x y
x = y or x.϶ y.϶   ↔   x = y or x. y.
0 x y and rϵ(x) < ϖ   ↔   x y and x O.
ϵ¯ x. y.϶   ↔   x.0 y.
ϵ x ϵ y   ↔   x y or x ϵ¯ y

Proof:

  1. ⅰ→ⅱ. Assume that (O, ϵ) is an ϵ-structure in which (-ϵ~1)–(-ϵ~6) are satisfied. Observe first that (-ϵ~2) has already been considered for ϵ-structures as B(•). As a particular consequence of this condition, Using this, we can check the equivalences for the 5 relations. For there is nothing to check. For 0, apply (β). For ϵ, use (-ϵ~4).
  2. ⅰ←ⅱ. Assume that (O, ) is an -ϵ-structure. Let r() be the -rank function so that (-ϵ~2) can be expressed as Since is a domain-restriction of ϵ to O. (see observation 2) it follows that (O., ) coincides with (O., ϵ). Recall that the .d function is by definition the ϖ-limited rank w.r.t. ϵ. We therefore obtain As a consequence, Using this, we can check the equivalences for the 5 relations. (): Apply (•) and the fact that is a domain-restriction of ϵ to O.. (): Apply Proposition A3. (0): Apply (•). (ϵ¯): Apply Proposition B5. (ϵ): There is nothing to check.
Disallowed structures
The following diagrams show examples of ϵ-structures that are disallowed by (-ϵ~4)–(-ϵ~6). Each example violates just the indicated condition. As usual, ϵ equals the composition () () where is the (exact) relation indicated by blue arrows, and is indicated by green arrows (with possibly implicit arrow heads on the higher ends) in its reflexive transitive reduction.
(ⅰ)
¬(-ϵ~4):
(a,b) (ϵ) (() (ϵ¯))
(ⅱ)
¬(-ϵ~5):
a. = b. and a.϶ b.϶
(ⅲ)
¬(-ϵ~6):
a.0 b. and (a,b) (ϵ)
It is assumed that ϖ = ω. Bounded objects are shown in beige color, the unbounded objects are in blue.
Bounded -ϵ-structures
In contrast to basic structures, -ϵ-structures need not have unbounded objects. (Even an empty structure is allowed.) Moreover, the following observation can be made:

Observation: For every -ϵ-structure (O, ), the restriction (O., ) is an -ϵ-structure (in which every object is bounded).

 

Pre-complete structure of ϵ

In this section we introduce a subfamily of basic structures that is closed w.r.t. hitherto described completion constructions. As a particular consequence, the structures appear as a (definitional extension of a) subfamily of -ϵ-structures.
Pre-complete structure of ϵ
We say that an ϵ5-structure S is pre-complete if it is a basic structure such that the following are satisfied.
(A) S is extensionally consistent: For every objects x, y,   x y   ↔   x = y or x. y..
(B) S is metaobject complete: (a) S is powerclass complete and (b) S is singleton complete.
(C) S is powerclass consistent: For every object x,   x is powerclass-like x is a powerclass.
(D) S is -ranked: For every object x,   r(x) (the -rank of x) equals x.d.
Similarly, a metaobject structure is pre-complete if its correspondent basic structure is pre-complete.

Note: In case ϖ = ω the (D) condition is redundant.

Proposition: A pre-complete ϵ5-structure S = (O, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ) is uniquely given by ϵ or by according to the following table. Moreover, S is an -ϵ-structure.

Relation
(subset)
(ⅰ)
Derived from ϵ
(ⅱ)
Derived from
x ϵ y and rϵ(x) < ϖ   ↔   x y
x = y or x.϶ y.϶   ↔   x = y or x. y.
0 x y and rϵ(x) < ϖ   ↔   x y and x O.
ϵ¯ x. y.϶   ↔   x.0 y.
ϵ x ϵ y   ↔   x y or x ϵ¯ y
.ec x. = y.϶   ↔   x.0 = y.
.ɛϲ {x} = y.϶   ↔   {x} = y.
r. = O.ϵ
=
O.

Proof: Let S = (O, ϵ, …) be a pre-complete structure. Make the following observations:

  1. O = O. O.   (since x r for every non-terminal object x and (A) applies).
  2. () = () (0)   (since S is singleton-complete so that () = (.ɛϲ) (0)).
  3. O.0 = O   (by the previous two equalities).
  4. O. equals the set of objects with bounded -rank   (since S is -ranked and O. = r.).
For every objects x, y, the following holds:
  1. x.϶ y.϶   ↔   x. y.   (since S is extensionally consistent).
  2. x. = y.϶   ↔   x.0 = y..
  3. x. y.϶   ↔   x.0 y..
This shows the determination of S via ϵ or as well as that conditions (-ϵ~1)–(-ϵ~6) are satisfied.
We have proved that the family of pre-complete ϵ5-structures is definitionally equivalent to a family of -structures. The next subsection provides the corresponding axiomatization via and the definitional extension of -structures. The last axiom refers to powerclass consistency which we let be defined in -structures the same way as in ϵ5-structures.
Pre-complete structure via
We say that an -structure (O, ) is pre-complete if the following are satisfied:
(ep~1) is well-founded.
(ep~2) is weakly extensional:   for every x, y from O.,   if x. = y. then x = y.
(ep~3) O. is the set of all objects x with bounded -rank:   x O.r(x) < ϖ.
(ep~4) O. = r. for some (necessarily unique) object r.
(ep~5) For every object x,   there is an object y (= x.ec) such that x.0 = y..
(ep~6) For every object x O., there is an object y (= x.ɛϲ) such that {x} = y..
(ep~7) For every object x,   if x is powerclass-like then x is a powerclass.

Observations:

  1. A pre-complete -structure is an -ϵ-structure. (The () = () (0) equality is follows by (ep~6).)
  2. The induced -structure of a pre-complete ϵ5-structure is pre-complete.

Proposition:

x y   ↔   x = y or x. y.
r.   =   O.
x.ec = y   ↔   x.0 = y.
x.ɛϲ = y   ↔   {x} = y.
x 0 y   ↔   x y and x O.
x ϵ¯ y   ↔   x.0 y.
x ϵ y   ↔   x y or x ϵ¯ y
Let Sa = (O, ) be a pre-complete -structure and let Sb = (O, , r, .ec, .ɛϲ) be a structure definitionally derived from Sa according to the table on the right. Then Sb is a metaobject structure that is pre-complete.

Proof:
Assume that Sa and Sb are as in the antecedent of the proposition. Note first that in Sa (due (ep~6)),

which is exactly how is derived in Sb – thus is disambiguated. Observe also that since r. , we have x rx. so that T = O O.. Subsequently, we verify that Sb satisfies the properties of a grounded metaobject structure:
  1. (mo~1): Inheritance, , is a partial order.
  2. (mo~2): x yx.ec y.ec   for every objects x, y.
  3. (mo~3): Objects from T.ec are minimal in .
  4. (mo~4): For every object x,   x.ec r.
  5. (mo~5)': T. = O.
  6. (mo~6): The singleton map, .ɛϲ, is injective.
  7. (mo~7): Objects from O.ɛϲ.ec are minimal in .
  8. (mo~8): x yx.ɛϲ y.ec   for every objects x, y such that x.ɛϲ is defined.
  9. (mo~9)': For every object x,   x.ɛϲ is defined   ↔   rϵ(x) < ϖ.
(1). is a preorder by definition. The antisymmetry of is asserted by (ep~2). (2). Apply proposition A3: x yx.0 y.0. (3). Apply propositions B1 and B2. (4). Apply x.0 (proposition B3). (5). Apply well-foundedness of . (6). Injectivity of .ɛϲ follows by definition. (7). Apply proposition B2. (8). By (ep~3) and (ep~6), x.ɛϲ is defined iff x O.. Therefore, if x.ɛϲ is defined then x.ɛϲ y.ecx.ɛϲ. y.ec.{x} y.ec.x y.ecx y. (9). Apply x O.rϵ(x) < ϖ which holds in -ϵ-structures.

Finally, being a definitional extension of an -ϵ-structure, Sb is -ranked. The powerclass consistency condition is explicitly asserted by (ep~7).

Alternative formulation of (ep~7)

Proposition: Assume that S = (O, ) is an -structure satisfying (ep~1)(ep~6) (that is, S is pre-complete up to (ep~7)). Let x be an object such that x is a powerclass-like. Then for every object u the following are equivalent:

  1. u. = x.϶   (↔ x.϶ is a principal ideal ↔ u.ec = xu.0 = x.x is a powerclass).
  2. u. = x..   or   {u} = x..

Note: By (ep~2), u in (ⅱ) is unique whenever x.. is non-empty, that is, whenever x T.ec.

Proof:
(ⅰ)→(ⅱ). If u. = x.϶ then u. = u.. = x.϶. = x... If in addition u. = , that is, x T, then {u} = {x}.ϲɛ = {x}.ce = x.. To prove (ⅰ)←(ⅱ), assume that x is an object such that x is powerclass-like, that is,

() x.϶ = x.϶¯ and
for every X x. such that the -rank of X is bounded, there is an object y such that X y x.϶.
Now let u be an object satisfying (ⅱ). If {u} = x. then u. = {u} = x. = x.϶. Assume that u. = x.. . We prove that u.0 = x.. The inclusion is immediate. To prove u.0 x., let a be from u.0, (that is, a u. O.) and denote X = a..ɛϲ the singleton image of a.. Make the following observations about X: Now apply condition () to X: there is an y from X. x.϶. Since a y x.϶ = x.϶¯, it follows that a ϵ x and therefore a x. This proves u.0 x..

Corollary:

  1. Axiom (ep~7)' can be equivalently replaced by
    (ep~7)' For every object x,   if x is powerclass-like   then   x.. = u. for some object u.
The pre-completion theorem

Proposition: Every basic structure S0 has a faithful extension S that is pre-complete. Such an extension can be obtained in the following steps:

Proof: In each step, Si+1 is a basic structure that is a faithful extension of Si therefore S is a basic structure that is a faithful extension of S0. By the extensional pre-completion theorem, S is metaobject complete, extensionally consistent and powerclass consistent. Since S1 is rank pre-complete so is S. By the observations about rank pre-complete structures, S is -ranked and thus pre-complete.

Pre-completion
If S is obtained from S0 as in the pre-completion theorem above, we call it the pre-completion of S0.
(a)
S0
The following diagrams shows a pre-completion of a basic structure S0 that contains two objects, O0 = {r, a}. It is assumed that ϖ = ω so that rank-precompletion is skipped. Instead, metaobject completion is shown in 2 steps.
(b)
S1 … powerclass completion of S0
(c)
S2 … singleton completion of S1
(d)
S … extensional pre-completion of S2
(and thus a pre-completion of S0)

Complete structure of ϵ

By a complete structure of (or a complete -structure) we mean a structure (O, ) where O is the set of objects and is a relation between objects satisfying the following conditions:
(co~1) is well-founded.
(co~2) is weakly extensional:   for every x, y from O.,   if x. = y. then x = y.
(co~3) O. is the set of all objects whose -rank is less than ϖ.
(co~4) For every subset X of O. there is an object x such that x. = X.

Observation: (O, ) is complete (O, ) is pre-complete and satisfies (co~4).

Proof: (ep~1)(ep~3) are the same as (co~1)(co~3). Subsequently, (co~4) implies (ep~4)(ep~7) (use (ep~7)').

x y   ↔   x = y or x. y.
r.   =   O.
x.ec = y   ↔   x.0 = y.
x.ɛϲ = y   ↔   {x} = y.
x 0 y   ↔   x y and x O.
A metaobject structure (O, , r, .ec, .ɛϲ) is complete if it is definitionally derived from a complete -structure according to the table on the right.
An ϵ5-structure S = (O, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ) is complete if it is a metaobject complete basic structure whose correspondent metaobject structure is complete. That is, S is (further) derived by
(ϵ¯) = (.ec) (),
(ϵ) = () (ϵ¯),
(ϵ-k) = () .ec(-k) for every natural k > 0,
(.ɛɕ) = (.ɛϲ) (.ec).
We might also say that S is a complete structure of ϵ. By the correspondence between pre-complete ϵ5-structures and pre-complete -structures, an ϵ5-structure S is complete iff it is a basic structure such that
(A) S is extensionally consistent: For every objects x, y,   x y   ↔   x = y or x. y..
(B) S is metaobject complete: (a) S is powerclass complete and (b) S is singleton complete.
(C) S is extensionally complete: For every subset X of O. there is an object x such that x. = X.
(D) S is -ranked: For every object x,   r(x) (the -rank of x) equals x.d.
Adding a bottom
By (co~2)+(co~4) there is a one-to-one correspondence between non-empty subsets of O. and elements of O.. For the purpose of convenience in expressing meet and join operations in we introduce a bottom, r0, that represents the empty set. If S = (O, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ) is a complete ϵ5-structure then a structure S = (Θ, ϵ, ϵ¯⁽*⁾, r, .ec, .ɛɕ) is called a lifted version of S if it is an extension of S such that Obviously, S is uniquely given up to isomorphism. We did not introduce S as an ϵ5-structure in order to preserve the notions of S. (Otherwise we would have to change the definition of .mli since r0 is a lower bound of H.) The metalevel index and rank functions are extended by: r0.mli = ω and r0.d = ϖ. We let the relation be the same so that r0 is regarded as unbounded (i.e. = r0. = r0.). For a subset X of O, we let the values of X., X., X. or X. be the same as in S, so that e.g. H. is empty as before. Similarly for images and pre-images under ϵi or ϵ¯i, i . Note that this convention only needs to be introduced for pre-images, since O is closed w.r.t. images of ϵi and ϵ¯i. When referring to objects we mean elements of O.

We denote () and () the join and meet operations in (Θ, ), respectively. That is, if {x, y} X Θ then

Furthermore, we also introduce the binary operation of a difference between elements of Θ.ϵ:

Observations:

  1. Θ.ϵ = O. {r0}.  
    (Recall that O. = O.ϵ = O T, therefore, Θ.ϵ is the set of non-terminal objects together with r0.)
  2. (Θ.ϵ, ) is a complete atomic Boolean algebra, isomorphic to ((O.), ). The set of atoms equals the set O.ɛϲ of singletons. The join and meet operations are the restrictions of and to subsets of Θ.ϵ.
  3. For every X Θ, the join X is defined iff either X T = or X {x,r0} for some terminal x.
  4. For every non-terminal object x,   x = x..ɛϲ.
  5. For every non-empty set X of non-terminal objects,   (X).d = X.d.
  6. For every objects x, y,   x.ec y.ec   =   (x y).ec.

Proof:

  1. Let X O. and u = X so that u. = X..
  2. Let x and y be objects. Then for every bounded object a the following holds:
    a (x y).ec   ↔   a (x y)
      ↔   a x and a y
      ↔   a x.ec and a y.ec
      ↔   a (x.ec y.ec).
The union map
In a complete structure (O, ), the union map is denoted .υ and is defined as a partial map between objects by In the lifted version S we let r0.υ = r0. We let the integer powers of .υ be denoted and defined in a similar way to that of .ec or .ɛϲ. The 0-th power of .υ is the identity map on O.϶-1 (which is the domain of .υ, see observations below).

Observations:

  1. Each of the following conditions is equivalent to x = y.υ:
    1. x. = y.2 and x ϶-1 y.
    2. x. = y.ϵ-1.
  2. The domain of .υ equals the set O.϶-1 of anti-members. Since O.϶-1 = r.϶-1 T.϶-1 and T.϶-1 = T.ec = T.ɛϲ,
  3. The following inclusion chain applies:
  4. The .ec and .ɛϲ maps are subrelations of the inverse of .υ.   (A consequence of (.ec) (.ɛϲ) (ϵ) (϶-1).)
  5. If x = y.υ then x.d = sup { i | i < y.d }. That is,
    x.d + 1 = y.d   if y.d is a successor ordinal,
    x.d = y.d   if y.d is a limit ordinal.
Stages
For every ordinal number i, the i-th stage of S is denoted Vi and defined by That is, Vi is the set of objects whose rank is strictly less than i. In particular, Accordingly, for each 0 < i ϖ,   the i-th stage object is denoted ri and defined as the unique object such that The additional bottom r0 is regarded as the 0-th stage object.
Each of the following diagrams shows a powerclass complete structure that is a restriction of a complete structure of ϵ to powerclass chains of terminal or stage objects. In the (a) case there is exactly one terminal object, the (b) structure contains at least two terminals.
(a)
(b)

Observations:

  1. Each stage object belongs to the 1-st metalevel.
  2. Each stage object is primary except for r1 in the (a) case.

Proposition A:

  1. For every object x and every ordinal i ϖ,  
  2. rϖ = r.
  3. For every non-zero ordinal i < ϖ,  

Proof:

  1. (a) follows by definition. To show (b), assume that x is a non-terminal object. Then
    x.d i   ↔   x..d < i   (by definition of -rank)
      ↔   x. ri.   (by (a))
      ↔   x ri   (by definition of ).
  2. rϖ. = {ri. | i < ϖ} = O. = r.. It follows that rϖ = r.

Proposition B: For every non-terminal object x and every ordinal i < ϖ, the following are satisfied.

  1. x.ec ri+1   =   (x ri).ec.
  2. x.ec = { (x ri).ec | i < ϖ }.

Proof:

  1. Assume that x is a non-terminal object and 0 < i < ϖ.
    x.ec ri+1 = x.ec (r1 ri.ec)   (by A3)
    = x.ec ri.ec   (since x.ec is disjoint with r1)
    = (x ri).ec   (by observation 6).
  2. Apply the previous proposition.
    { (x ri).ec | i < ϖ } = { x.ec ri+1 | i < ϖ }   (by previous proposition)
    = x.ec { ri | i < ϖ }   (by infinitive distributivity)
    = x.ec rϖ   (by definition of rϖ)
    = x.ec   (since x.ec rϖ = r).
Existence and uniqueness

Proposition:

  1. For every non-zero cardinal number κ there is a complete structure whose ground stage has cardinality κ.
  2. Two complete structures are isomorphic   iff   they have the same cardinality of the ground stage.
    If is an isomorphism between (O, ) and (V, ) then is uniquely given by its restriction to the ground stage of (O, ) by

Proof:

  1. Proceed by transfinite recursion. For each ordinal i ϖ+1, define a set Vi by
    V0 = ,
    V1 = κ × {0},
    Vi+1 = Vi { (X,i) | X Vi and for every j < i, X Vj } if i > 0,
    Vi = {Vj | j < i} if i is a limit ordinal.
    Subsequently, let (V, ) be an -structure such that V = Vϖ+1 and for every (X,i), (Y,j) from V, We claim that (V, ) is a complete structure whose i-th stage is Vi for every i ϖ+1. In particular, the ground stage is V1 and thus has cardinality κ. To prove this, make the following observations. Assume that (X,i) and (Y,j) are from V and k ϖ+1. Then the following holds:
  2. By weak extensionality and well-founded recursion, is injective. As a consequence, is an embedding of (O,) into (V,). The surjectivity of is proved by well-founded recursion over (V, ).
Powerclass cumulation
For an ordinal i, the i-th (powerclass) cumulation, .c(i), is a map Θ.ϵ Θ.ϵ defined by transfinite recursion:
x.c(0) = x,
x.c(i) = x x.c(i-1).ec if i is a successor ordinal,
x.c(i) = {x.c(j) | j < i} if i is a limit ordinal.
There is a single recursive formula for every ordinal i:
x.c(i) = x { x.c(j).ec | j < i }.
We also introduce special notation for .c(1) and .c(ϖ):
x.c = x x.ec (the first cumulation of x),
x.c() = x.c(ϖ) (the full cumulation of x).
For convenience, the following table shows the definition with x.c(i) abbreviated to xi.
Expressed using Expressed via .
i = 0 x0 = x x0. = x.
i is a successor ordinal xi = x xi-1.ec xi. = x. { u | u. xi-1. }
i is a limit ordinal xi = {xj | j < i} xi. = { xj. | j < i }

Observations:

  1. The set O is closed w.r.t. each .c(i).
  2. The bottom r0 is a fixpoint of .c(i) for every ordinal i.
  3. An object x is a fixpoint of .c x ϵ x.

    Proof: x ϵ xx ϵ¯ xx.ec xx x.ec = x.

  4. Stage objects arise by powerclass cumulation of the ground stage object r1:
  5. (A consequence of monotonicity of .ec.) For every x, y from Θ.ϵ and every ordinals i, j,
    i j   →   x.c(i) x.c(j),
    x y   →   x.c(i) y.c(i).
    That is, for every non-zero ordinal i,   .c(i) is (a) increasing and (b) monotone.

Proposition:
Assume that x is a non-terminal object and i, j ordinal numbers.

  1. x.c(i).c(j) = x.c(i+j).
  2. x.c(i).d = (x.d + i) ϖ.   (That is, the i-th cumulation increases the rank of x by i whenever x.d + i ϖ.)

Proof:

  1. Assume that x is a non-terminal object, i, j ordinal numbers and proceed by transfinite induction over j.
    x.c(i).c(j) = x.c(i) {x.c(i).c(k).ec | k < j}   (by definition of .c(j))
    = x.c(i) {x.c(i+k).ec | k < j}   (by the induction assumption)
    = x.c(i) x {x.c(i+k).ec | k < j}   (since x x.c(i))
    = x.c(i) x {x.c(i+k).ec | i+k < i+j}   (since k < ji+k < i+j)
    = x.c(i) x.c(i+j)   (by definition of x.c(i+j), using x.c(n) x.c(i) for n i)
    = x.c(i+j)   (since x.c(i) x.c(i+j)).
  2. Assume that x is a non-terminal object and proceed by transfinite induction.
    x.c(i).d = (x {x.c(k).ec | k < i}).d   (by definition of .c(i))
    = x.d {x.c(k).ec.d | k < i}   (by properties of .d)
    = x.d {(x.c(k).d + 1) ϖ | k < i}   (by properties of .ec)
    = x.d {(x.d + k + 1) ϖ | k < i}   (by the induction assumption)
    = x.d + {(k + 1) ϖ | k < i}
    = (x.d + i) ϖ.
The .c() operator
The following proposition shows that the ϖ-th cumulation map .c() is a closure operator on the set Θ.ϵ = O. {r0}. The fully cumulated objects are exactly the circular objects, i.e. for every object x, That is, O.c() are the fixpoints of .c – using the observation that x ϵ xx.c = x.

Proposition:

  1. For every x from Θ.ϵ and every ordinals i, j, the following are satisfied.
    1. x.c(j) ri     x.c(i).
    2. x.c().ec     x.c().
    3. x.c(ϖ+i) = x.c().
  2. Corollary: .c() is a closure operator on Θ.ϵ. That is, .c() is increasing, monotone and

Proof:

  1. Let x be from Θ.ϵ.
    1. Proceed by transfinite induction over pairs (i,j). For i = 0 the inequality reduces to r0 x which is satisfied by definition of r0. For j = 0 the inequality reduces to x ri x.c(i) which follows by x x.c(i). If i and j are both successor ordinals then
      x.c(j) ri = (x x.c(j-1).ec) ri   (by definition of .c(j))
      = (x ri) (x.c(j-1).ec ri)   (by distributivity of and )
      x (x.c(j-1).ec ri)   (since x ri x)
      = x (x.c(j-1) ri-1).ec   (using proposition B1)
      x x.c(i-1).ec   (since x.c(j-1) ri-1     x.c(i-1) by the induction assumption)
      = x.c(i)   (by the definition of .c(i)).
      If j is a limit ordinal then
      x.c(j) ri = { x.c(k) | k < j } ri   (by definition of .c(j))
      = { x.c(k) ri | k < j }   (by infinite distributivity)
      { x.c(i) | k < j }   (by the induction assumption)
      = x.c(i).  
      If i is a limit ordinal then
      x.c(j) ri = x.c(j) { rk | k < i }   (by definition of ri)
      = { x.c(j) rk | k < i }   (by infinite distributivity)
      { x.c(k) | k < i }   (by the induction assumption)
      = x.c(i).  
    2. x.c().ec = { (x.c() ri).ec | i < ϖ }   (by proposition B2)
      { (x.c(i).ec | i < ϖ }   (by the previous proposition (a))
      { (x x.c(i).ec | i < ϖ }
      = x.c()   (by definition of .c() = .c(ϖ)).
    3. By the previous proposition, .ec is decreasing on O.c(), therefore, for every x from O.c(),
      • x.c = x x.ec = x,
      which shows that .c().c = .c().

Completion

This section describes the final step of completion of basic structures of ϵ: For a given pre-complete structure S = (O, ) we construct a faithful embedding of S into a complete structure V = (V, ) whose ground stage V1 = V V. has the same cardinality as the set T = O O. of terminal objects of S. As a consequence we obtain the following:

Completion theorem:

Every basic structure can be faithfully extended to (embedded into) a complete structure.
Since every complete structure is pre-complete and both the pre-completion as well as the embedding described in this section are idempotent, we can speak about completion of basic structures. The completion theorem can be shortly stated as:
Every basic structure has a completion.
Embedding sequence
Let S = (O, ) and V = (V, ) be -structures such that S is pre-complete and V is complete. We say that a transfinite sequence of maps from O to V is an embedding sequence (w.r.t. S and V) if the following are satisfied:
  1. The restriction of i to terminals is for every i identical and forms a bijection between T and V1. (⁎)
  2. The restriction of i to the set O. of non-terminal objects x is defined according to the following table.
    Expressed via . Expressed using
    i = 0 x.ν0. = x.¯0.ec. x.0 x.ν0 = (x.¯0.ec x.0.ɛϲ)
    i is a successor ordinal x.νi. = x.϶¯i-1.ec. x.0 x.νi = (x.϶¯i-1.ec x.0.ɛϲ)
    i is a limit ordinal x.νi. = { x.νk. | k < i } x.νi = { x.νk | k < i }

Notes:

  1. (⁎) To avoid notational conflicts, we refer to the set of terminals of V by V1 (the ground stage of V). Similarly, the inheritance root of V is referred to by rϖ (the ϖ-th stage object).
  2. We can consider i to be defined for every ordinal i. Since .ec and commute (as shown below) it follows that

Observations A:

  1. For a non-terminal x,
  2. By definition, .ec. = .0. In case of i = 0, we can even use . instead of .0.

Observations B:

  1. For a bounded object x,   x.ν0 = x.νi = x.ν   for every ordinal i.
  2. For every object x,         x.νi x.νi+1 x.ν   for every ordinal i.

Proof:

  1. If x is a bounded non-terminal object then x.϶¯ = x.¯ so that the prescriptions for x.ν0 and x.ν1 are coincident.
  2. Proceed by transfinite induction over i. The case i = 0 follows by definition of 0 and 1 (using the fact that is a restriction of ϵ). For a successor ordinal i we apply the induction assumption (in particular, x.϶¯i-1.ec. x.϶¯i.ec.):
The embedding theorem

Theorem: Let 0, 1, …, ϖ = be an embedding sequence w.r.t. S and V as in the previous subsection. Then is a faithful embedding of S into V. That is,

Proof:
The proof is accomplished in the series of claims A–E below.

Claim A

Claim A: For every objects x, y from O the following holds.

  1. x.ν0.d = x.ν.d = x.d.
    1. x y   ↔   x.ν0 y.ν0.   (That is, y.0 = y.ν0. O0 whenever y is non-terminal.)
    2. x y   ↔   x.ν0 y.ν0.   (That is, y.0 = y.ν0. O0. In particular, 0 is injective.)

Proof:

  1. Proceed by well-founded induction on (O, ).
    x.ν0.d = sup { b.d + 1 | b x.¯0. x.0 }
    = sup { b.d + 1 | b x.0 }   (since .d is monotone in V)
    = sup { a.ν0.d + 1 | a x }
    = sup { a.d + 1 | a x }   (since a.ν0.d = a.d by the induction assumption)
    = x.d.
    If x is bounded, then x.ν0 = x.ν. If x is unbounded, then ϖ = x.d = x.ν0.d x.ν.d ϖ. In both cases, we obtain x.ν0.d = x.ν.d as a consequence.
  2. We first show the direction. By (1), if x is bounded then so is x.ν0. Therefore The direction is shown by well-founded induction on (V, ). If y.ν0 has rank 0 (i.e. y is terminal), then the implications are trivially satisfied. Otherwise denote d = y.d and assume that for every non-terminal object u such that u.d < d, (a) u.0 = u.ν0. O0 and (b) u.0 = u.ν0. O0.
    1. Let x.ν0 y.ν0. By definition of y.ν0, there exists an object b from O such that either
      • x.ν0 b.ν0 and b ¯ y, or
      • x.ν0 = b.ν0 and b y.
      If b is such that (ⅱ) is satisfied then x = b (since by the induction assumption, 0 is injective on objects of rank less than d), thus x y. If b is such that (ⅰ) is satisfied then we obtain
      • x b   (by induction assumption for x and b – both x and b have rank less than d),
      • x ¯ y   (since x b ¯ y).
    2. For a non-terminal x we obtain
      x.ν0 y.ν0   ↔   x.ν0. y.ν0.
        →   x.ν0. O0 y.ν0. O0
        ↔   x.0 y.0   (by the just proved (a)),
        ↔   x. y.   (by injectivity of 0 due to the induction assumption),
        ↔   x y.
Claim B

Claim B: For every objects x, y from O and every ordinal i, the following are satisfied.

    1. x y   ↔   x.ν0 y.νi.   (That is, y.0 = y.νi. O0 whenever y is non-terminal.)
    2. x y   ↔   x.νi y.νi.   (That is, y.i = y.νi. Oi. In particular, i is injective.)
  1. As a particular consequence for i = ϖ,
    1. x y   ↔   x.ν y.ν,
    2. x y   ↔   x.ν y.ν.

Proof:
Proceed by transfinite induction over i. The case i = 0 has been proved in A2. Assume that i > 0 and that

for every k < i. We proceed similarly as in A2 and show first the direction.
  1. →:
  2. ←:
    1. Let x.ν0 y.νi and assume that i is a successor ordinal. By definition of y.νi, there exists an object b from O such that either
      • x.ν0 b.νi-1 and b ϵ¯ y, or
      • x.ν0 = b.ν0 and b y.
      If (ⅱ) is satisfied then x = b and thus x y. If (ⅰ) is satisfied we obtain
      • x b   (by the induction assumption),
      • x ¯ y   (since x b ϵ¯ y and x is bounded).
      Assume now that i is a limit ordinal. Then
      x.ν0 y.νi   ↔   x.ν0 { y.νk. | k < i }   (by definition of y.νi).
        ↔   x.ν0 y.νk for some ordinal k < i
        ↔   x y   (by the induction assumption).
    2. For a non-terminal x we obtain
      x.νi y.νi   ↔   x.νi. y.νi.
        →   x.νi. O0 y.νi. O0
        ↔   x.0 y.0   (by the just proved (a))
        ↔   x. y.   (by injectivity of 0)
        ↔   x y.
Claim C

Claim C: For every object x from O and every ordinals i, j, the following is satisfied.

  1. (x.νj ri) x.νi.   Corollary: If i j then x.νj ri = x.νi ri.
  2. x.ec.νi+1 = x.νi.ec.
  3. x.ec.ν = x.ν.ec.
  4. x.pr.ν = x.ν.pr.   (That is, preserves primary objects.)

Proof:

  1. The inequality holds trivially for bounded objects x. (Recall that if x O. then x.νi = x.νj.) Assume further that x is unbounded and proceed by transfinite induction over pairs (i,j). For i = 0 the inequality holds by definition of r0 as the artificial bottom object. For j = 0 the inequality holds by the monotonicity of the embedding sequence (if j i then j i). If i is a limit ordinal then
    x.νj ri = x.νj { rk | k < i } = { x.νj rk | k < i }   (by infinite distributivity)
    { x.νk | k < i }   (by the induction assumption)
    = x.νi.
    Similarly, if j is a limit ordinal then
    x.νj ri = { x.νk | k < j } ri = { x.νk ri | k < j }   (by infinite distributivity)
    { x.νi | k < j }   (by the induction assumption)
    = x.νi.
    Assume finally that both i and j are successor ordinals. By definition, x.νj. = x.϶¯j-1.ec. x.0. By B1a, x.0 x.νi., therefore, it is sufficient to show that for every object a from x.϶¯, If a is bounded then a.νj-1.ec = a.ν0.ec x.ν0 x.νi. Assume further that a is unbounded, in particular, a.νj-1 is non-terminal. Then for every bounded object b from V,
    b (a.νj-1.ec ri)   ↔   b (a.νj-1 ri-1).ec   (by proposition B1 (a.νj-1 is non-terminal))
      ↔   b (a.νj-1 ri-1)   (by definition of .ec)
      →   b a.νi-1 (by the induction assumption)
      →   b x.϶¯i-1.ec.   (since a is from x.϶¯)
      →   b x.νi   (since x.϶¯i-1.ec. x.νi.).
  2. The equality is shown by
    x.ec.νi+1. = x.ec.϶¯i.ec. x.ec.i   (by definition of i+1, using 0 =i on O.)
    = x.ec.϶¯i.ec.   (since x.ec. = x.ec.¯ x.ec.϶¯)
    = x.i.ec.   (since . = .ec.϶¯)
    = x.νi.ec.   (by monotonicity of i.ec).
  3. If x is bounded then, using the previous statement,   x.ec.ν = x.ec.ν0 = x.ec.ν1 = x.ν0.ec = x.ν.ec. Assume that x is unbounded, in particular, non-terminal. Then
    x.ec.ν = x.ec.ν rϖ   (since x.ec.ν rϖ)
    = x.ec.ν { ri | i < ϖ }   (by definition of rϖ)
    = { x.ec.ν ri | i < ϖ }   (by infinite distributivity)
    = { x.ec.νi ri | i < ϖ }     (since x.ec.ν ri = x.ec.νi ri by C1)
    = { x.ec.νi+1 ri | i < ϖ }     (since y.νi y.νi+1 y.ν for y = x.ec)
    = { x.νi.ec ri | i < ϖ }   (since .ec.νi+1 =i.ec by C2)
    = { (x.νi ri).ec | i < ϖ }   (by proposition B1 (x.νi is non-terminal))
    = { (x.ν ri).ec | i < ϖ }   (since x.νi ri = x.ν ri by C1)
    = x.ν.ec   (by proposition B2).
  4. Let x be an object from O such that x.ν is a powerclass, that is x.ν = u.ec for some u from V. Recall that by definition of .ec, We should prove that x is a powerclass as well (equivalently, that u is from O). If x.϶ contains a terminal object a then, since a.ν is also terminal (in V), {a.ν} = x.ν.϶, so that a.ν = u. We can therefore further assume that x.϶ T = . By pre-completeness of S it is sufficient to show that x is powerclass-like, that is The (a) equality follows from the embedding properties of w.r.t. ϵ and ϵ¯. To prove (b), assume that X is a non-empty bounded subset of x.϶. We obtain
Claim D

Claim D:

  1. For every object x from O such that x ϵ x and every ordinal i, the following is satisfied.
  2. r= rϖ.

Proof:

  1. Let x be such that x ϵ x. (a) follows directly by definition of i+1. (b) is proved by transfinite induction over i. For i = 0, (b) reduces to x.ν0 x.νi which holds by observation B2. If i is a successor ordinal then
    x.ν0.c(i) = x.ν0 x.ν0.c(i-1).ec   (by definition of .c(i))
    x.ν0 x.νi-1.ec   (by the induction assumption)
    x.ν0 x.νi   (since x.νi-1.ec x.νi by (a))
    = x.νi   (since x.ν0 x.νi by observation B2).
    If i is a limit ordinal then
    x.ν0.c(i) = { x.ν0.c(k) | k < i }
    { x.νk | k < i }   (by the induction assumption)
    = x.νi.
  2. The equality r= rϖ is shown by
    rϖ = r1.c(ϖ) r0.c(ϖ)   (since r1 r0 and .c(ϖ) is monotonic)
    r   (since r ϵ r so that (1b) applies for i = ϖ)
    rϖ   (since rϖ is the top of V.).
Claim E

Claim E:

  1. For every bounded object x from O,   x.ɛɕ.ν = x.ν.ɛɕ.
  2. For every objects x, y from O and every integer n,   x ϵ¯n y   ↔   x.ν ϵ¯n y.ν.
  3. For every objects x, y from O and every natural n,   x ϵn y   ↔   x.ν ϵn y.ν.

Proof:

  1. Let x, y be objects from O such that x.ɛɕ = y, i.e. {x} = y. and y is primary. We should prove that x.ν.ɛɕ = y.ν, equivalently, (a) {x}.ν = y.ν. and (b) y.ν is primary. The (b) condition follows by claim C4. The (a) condition is shown by
    y.ν. = y.¯.ν. y.   (since y is bounded )
    = y.   (since y.¯ = )
    = {x}.ν   (since {x} = y.).
  2. This follows by powerclass completeness of both S and V (so that (ϵ¯i) = () .ec(i) () in both S and V).
  3. Let x, y be objects from O and n a positive natural number. For n = 1 we have Assume further that n > 1. It is then sufficient to show that x.ν ϵn y.νx ϵn y. (The opposite implication follows by embedding of ϵ.) Assume therefore that x.ν ϵn y.ν. Since x.ν.ϵ¯n = x.ν.ϵn for unbounded x, we can in addition assume that x is bounded so that x.ν n y.ν.
    x.ν n y.ν   ↔   x.ν n-1 b y.ν for some b from V   (by relational composition)
      ↔   x.ν n-1 b u.ν y.ν for some b from V and u from y.   (by definition of y.ν.)
      →   x.ν n-1 u.ν y.ν for some u from y.   (since (n) () (n))
      →   x n-1 u y for some u from O   (by the induction assumption)
      ↔   x n y.

Superstructures

Recall that the set O of objects of a complete -structure S = (O, ) equals the (ϖ+1)-th stage of S. In this section we provide an axiomatization for an arbitrary stage. This introduces a generalization in which the complete structures of ϵ are viewed as (ϖ+1)-superstructures.
Superstructure
By an (abstract) superstructure we mean an -structure (V, ) (so that V is a set of objects and is a relation between objects) such that the following conditions hold.
(as~1) is well-founded.
(as~2) is weakly extensional:   for every x, y from V.,   if x. = y. then x = y.
(as~3) For every non-empty set X of objects such that r(X) < r(V) (⁎) there is an object x such that x. = X.
By an α-superstructure we mean a superstructure (V, ) whose -rank equals α.

Note: (⁎) We use r(X) to refer to the -rank of a subset X of V. Similarly, for an object x we let r(x) be the rank of x in .

Observations:

  1. The only 0-superstructure is the empty structure.
  2. Every 1-superstructure is of the form (V, ) where V is non-empty.
  3. V. = V   ↔   α is a limit ordinal or zero.
  4. Axiom (as~2) can be left out if in (as~3), an object x is replaced by a unique object x.
  5. If r(V) is a successor ordinal α+1 then (as~3) can be replaced by a conjuction of the following conditions:
    (a) V. is the set of all objects x such that r(x) < α. (co~3) if α = ϖ
    (b) For every subset X of V. there is an object x such that x. = X. (co~4)
    The labels on the right indicate the correspondence to axioms of complete -structures.
  6. Corollary: For a structure S = (O, ) the following are equivalent:
Definitional extension
The following table shows the definitional extension of an α-superstructure (V, ).
Inheritance x y   ↔   x = y or x. y.
Bounded inheritance x 0 y   ↔   x y and x V.
Power membership x ϵ¯ y   ↔   x.0 y.
Object membership x ϵ y   ↔   x y or x ϵ¯ y
Anti-membership x ϵ-1 y   ↔   x. y.0
Powerclass map x.ec = y   ↔   x.0 = y.
Singleton map x.ɛϲ = y   ↔   {x} = y.
Union map x = y.υ   ↔   x. = y.2 and y ϵ-1 x
Metalevel index x.mli   =   min {i | x V1.i, i }
Rank x.d   =   sup {a.d + 1 | a x}
i-th cumulation map x.c(i) = y   ↔   x V. and y = x {x.c(j).ec | j < i }
i-th stage Vi   =   { x | x.d < i }
(1+i)-th stage object r1+i   =   r1.c(i)   where r1. = V1 = V V.
For a natural i > 0, let ϵi/ϵ¯i/ϵ-i/i be the i-th relational composition of let ϵ/ϵ¯/ϵ-1/ with itself. The 1-st stage V1 = V V. is the ground stage of terminal objects. Objects from V. are bounded, the remaining are unbounded. Lifting by an additional bottom r0 is defined like for complete -structures.

Observations:

  1. There is no (common) definition of inheritance root r since if α is a limit ordinal then V = V. and thus there is no object x such that x. = V..
  2. The metalevel index function .mli is defined using -levelling.
  3. Definitions of ϵ¯ and .ec are adjusted by the additional condition x.0. This is because in (α+2)-superstructures, this condition is not implicitly guaranteed. (In particular, there are unbounded singletons.) As a consequence, the .ec map is not total in general.
  4. The i-th cumulation map .c(i) is total on V. for every ordinal i   iff   α is a successor of a limit ordinal.

Embedding of superstructures

In this section we make the final preparation for the embedding of object membership into the von Neumann universe. We aim at the identification where 𝕍ϖ+1 is the partial von Neumann universe of all well-founded pure sets whose rank is at most ϖ. We are then interested in (α+1)-superstructures (Z,), where α is a limit ordinal, which are regularly embedded into S = (O, ): Subsequently, we can change the choice of ϖ to α and regard (Z,) as an embedded complete structure of ϵ.
In the rest of the section we assume that S = (O, ) is a complete -structure (equivalently, (ϖ+1)-superstructure), with the definional extension introduced before.
Strata and the bottom stratum operator
For objects s, x,   s is said to be a stratum of x if either s is terminal and s = x or s is non-terminal and there is a (necessarily unique) ordinal number i such that An object is called a stratum if it is a stratum of itself. For an object x,

Observations:

  1. For every object x,
  2. For every ordinal i < ϖ,   ri+1 ri is a stratum or r. Moreover, for every object s,
  3. The ground stage object r1 is the bottom stratum of every stage object ri, 0 < i ϖ.

Proposition:

  1. .ϱ and .ec commute. In particular, if s is a stratum then so is s.ec.
  2. Powerclass cumulation preserves the bottom stratum, i.e.

Proof:

  1. Assume first that x is a terminal object. Then {x} = x.ec. so that x.ec is a stratum and thus x.ec.ϱ = x.ec. Since by definition x.ϱ = x it follows that x.ec.ϱ = x.ϱ.ec. Assume further that x is non-terminal. Then for every non-terminal a,
    a x.ec.ϱ   ↔   a x.ec and a.d b.d for every b x.ec   (by definition of .ϱ)
      ↔   a. x. and a.d b.d for every b such that b. x.   (by definition of .ec)
      ↔   a. x. and a..d u.d for every u x   (by definitin of .d)
      ↔   a x.ϱ.ec.
  2. Assume that x is a non-terminal object and i is a non-zero ordinal. Then for every non-terminal a,
    a x.c(i+1). x.   ↔   a. x.c(i).   (by definition of .c(i+1))
      →   u.d < a.d for some u from x.c(i).   (by definition of .d)
      →   u.d < a.d for every u from x.ϱ.   (by the induction assumption).
    This shows x.ϱ..d x.c(i+1)..d. Since x.ϱ x x.c(i+1) the statement follows.
Regularly cumulated objects
We say that an object b is a (regular) cumulation base if it is a non-terminal stratum such that An object z is said to be regularly cumulated if z = b.c(α) for some cumulation base b and some ordinal α.

Observations:

  1. Every regularly cumulated object z has a unique cumulation base b given by
  2. If z is a regularly cumulated object then so is z.c(i) for every ordinal i.
  3. Stage objects ri, 0 < i ϖ, are regularly cumulated.
  4. If b.d > 1 then b.υ exists and thus b.υ.d refers to the ordinal predecessor of b.d.

Proof:

  1. This is a consequence of .c(α) preserving the bottom stratum (proposition 2).

Proposition: Let z be a regularly cumulated object and denote b = z.ϱ its cumulation base and Z = z..

  1. For every object x,
  2. The following are equivalent:   (ⅰ) z ϵ z   (i.e. z is fully cumulated).    (ⅱ) z.d = ϖ.   (i.e. z is unbounded).
  3. Let i be the unique ordinal such that b.d + i = z.d. (That is, z. = 1+i is the height of z.) Then
      z = b.c(i).
  4. The following closure properties are satisfied:
    1. Z. = Z.
    2. Z. Z = Z b.,   that is, b. = Z Z.,   that is, b. is the set of -minimal objects in (Z, ).
    3. Z. Z = Z. b.2,   that is, (Z b.). Z.
    In particular, (Z, , ) is a substructure of (O, , ).
  5. Let α0 be such that b.d = α0 + 1 and let r() be the rank function in the well-founded relation (Z, ). Then
    1. α0 + r(x) = x.d   for every object x from z. = Z,
    2. α0 + r(x.) = x.d   for every object x from z..
  6. (Z, ) is an α-superstructure where α = z. is the height of z.

Proof:
Assume that b, z and Z are as in the antecedent of the proposition.

  1. Let i be an ordinal such that z = b.c(i). Proceed by transfinite induction over i. If i = 1 then z = b is a stratum so that x.d = z.d for every object x from z. and the requested implication follows trivially. Assume now that i is a successor ordinal, i > 1, and let y = b.c(i-1) so that z = b y.ec. Let x be an object from z..

    Assume finally that i is a limit ordinal and let again x be an object from z..

  2. (ⅰ)→(ⅱ) follows by definition of .d. For the reverse implication assume that z.d = ϖ. Then for every object x, The last implication is by (1). This shows that z.0 z., i.e. z ϵ¯ z.
  3. Let i be such that b.d + i = z.d and let j be such that b.c(j) = z. Apply proposition 2 about the rank increment by cumulation.
  4. The statements follow by definition of powerclass cumulation. (For (a) use b. = b.. which follows by minimality of objects from b..)
  5. Assume that α0 is such that b.d = α0 + 1. To show (a), let x be an object from Z. Assume first that x b. Then x. Z = and thus r(x) = 0. Since x.d = α0 the (a) equality follows. Assume further that x is from Z.. Then
    x.d = sup { a.d + 1 | a x }   (by definition of .d)
    = sup { α0 + r(a) + 1 | a x }   (by the induction assumption)
    = α0 + sup { r(a) + 1 | a x }   (by properties of ordinal numbers)
    = α0 + r(x)   (by definition of r(x)).
    To show (b) let x be from z., that is, x. Z. Then
    x.d = sup { a.d + 1 | a x }
    = sup { α0 + r(a) + 1 | a x }   (by (a))
    = α0 + r(x.)   (by definition of r(x.)).
  6. Let α0 be such that b.d = α0 + 1. Well-foundedness of (Z,) follows by well-foundedness of (and has already been used for the definition of r()). Similarly, weak extensionality of (Z,) follows by weak extensionality of and (Z b.). Z (by 4c). To verify that (as~3) is satisfied in (Z,), assume that X is a non-empty subset of Z. Z such that r(X) < r(Z) (where r() is again the rank function in (Z,)). By extensional completeness in (O,), there is an object x such that X = x..
    r(X) < r(Z)   ↔   r(x.) < r(z.)   (since X = x. and Z = z.)
      →   α0 + r(x.) < α0 + r(z.)   (by properties of ordinal numbers)
      →   x.d < z.d   (since x z so that (5b) applies)
      →   x z   (by (1)).
    This shows that (Z,) is a superstructure. Let α = z. be the height of z, i.e. α = 1+i where i is such that b.d + i = z.d. Then That is, (Z,) is an α-superstructure.
Cardinality assertion

Proposition:

  1. For every ordinal i < ϖ,   the cardinality of Vi+1 Vi is at least i.
  2. Let (α, κ) be a pair of non-zero ordinals such that κ is in addition a cardinal and κ + α < ϖ. Then there is a regularly cumulated object z whose superstructure (Z,) (where Z = z.) has the following properties:

Proof:

  1. First note that the cardinality of Vi is at least i since for every k < i there is an object xk from Vi such that xk.d = k (we can choose xk = rk for k 0). Consider now the difference D = Vi+1 Vi. For i = 0 the statement holds trivially so that we can further assume that i > 0. By axioms (co~2) and (co~4), That is, there is a bijection between Vi+1 V1 and (Vi) {} (where (Vi) is the powerset of Vi). Since V1 Vi we can make the following observations: In both cases it follows that D is of cardinality at least i.
  2. Let α be an ordinal and κ a cardinal such that κ + α < ϖ. By the previous proposition, there is a subset X of Vκ+1 Vκ such that card(X) = κ. Consequently, X.ɛϲ is a subset of Vκ+2 Vκ+1 such that card(X.ɛϲ) = κ (since .ɛϲ is injective and increases rank by 1). Let b be the unique object such that b. = X.ɛϲ and denote z = b.c(i) where α = 1+i and Z = z.. Then
Embedded (α+1)-superstructure

Proposition: Let z be a regularly cumulated object of height α+1 where α is a limit ordinal. Denote Z = z.. Assume that z.υ exists. Then the following table describes a definitional extension of the (α+1)-superstructure (Z,). (The z subscript is used to distinguish between definitional extensions of (Z,) and (O,).)

Inheritance root r   =   z z.υ r. = Z Z.
Ground stage object b   =   z r.ec b. = Z r.
For every x, y from Z :
Inheritance x ≤z y   ↔   x y   ↔   x. y.
Union map x = y.υz   ↔   x = y.υ   ↔   x. = y.2
Singleton map x.ɛϲz = y   ↔   x.ɛϲ = y   ↔   {x} = y.
Powerclass map x.ecz = y   ↔   r x.ec = y   ↔   r. x. = y.
Rank b.υ.d + x.dz   =   x.d

Proof:
Let r be the inheritance root of (Z,), i.e, the unique object such that r.z = Z.z. Let b be the ground stage object of (Z,), i.e, the unique object such that r.z = Z Z.z. Let x be an arbitrary object from Z. Then prescriptions for r, b and .ecz follow from the following equalities:

The difference between .d and .dz follows by proposition 5.
Embedded basic structure

Proposition: Let again z be a regularly cumulated object of height α+1 where α is a limit ordinal, z.υ exists and Z = z.. Assume in addition that So = (O, …) is a basic structure (of rank α+1) such that (Z,) is a faithful extension of So. Let T be the set of terminals of So and r the inheritance root. Then

T = (O. O).ɛϲ O (the set of terminal objects of So),
r. = O. T. (the inheritance root of both So and (Z,)),
Z = r. r. (i.e. z = r r.ec = r.c).
In particular, Z is given by O (in the ambient (ϖ+1)-superstructure (O, )). The definitional extension of (Z,) described in the previous subsection is applicable to So.

Proof:
Let r be the inheritance root of (Z,), i.e, the unique object such that r.z = Z.z. Let b be the ground stage object of (Z,), i.e, the unique object such that r.z = Z Z.z. Let T be the set of terminal objects of So. Then

By embedding of So into (Z,), This shows the equalities for T and r. The z = r.c equality follows by r = b.c(α).

Embedding into the von Neumann universe of sets

In this section we provide the final embedding of bounded object membership into set membership between well-founded sets. If not stated otherwise, we will use the term class in the sense of set theory as a collection of sets. Let 𝕍 denote the universal class and assume the ZFC axiom of foundation (a.k.a. axiom of regularity): As a consequence, 𝕍 coincides with the von Neumann universe of well-founded sets. Note that the axiom says that (𝕍, ) is a well-founded relation provided that we extend the definition of well-foundedness to proper classes.

In addition to the standard powerset operator 𝕍 𝕍 which is denoted by we define two sub-operators, + and . For every set x, let

+(x) = (x) {}   (+(x) is the set of non-empty subsets of x),
(x) = { {u} | u x }   ((x) is the set of singleton subsets of x).
For a natural number i we let i denote the i-th power of in the usual sense (i.e. 0(x) = x and i+1(x) = (i(x))). Similarly with + and .
Powerset cumulation
For every ordinal α, the α-th (powerset) cumulation is denoted α and defined recursively as an operator 𝕍 𝕍 by
0(x) = x,
α(x) = x +(α-1(x)) if α is a succesor ordinal,
α(x) = { β(x) | β < α } if α is a limit ordinal.
By a single recursive formula,

Note: We deviate from standard definitions [] [] by using + instead of in the above formulae. A correspondence is then obtained by a substitution x x {}.

The von Neumann hierarchy
The von Neumann universe 𝕍 is the class of all well-founded sets. If the axiom of foundation is not assumed and 𝕌 denotes the universal class of all sets, then 𝕍 is obtained as a subclass of 𝕌 by transfinite recursion via the cumulative hierarchy of sets 𝕍α:
𝕍α = { (𝕍β) | β < α },   that is, 𝕍0 = ,
𝕍α = (𝕍α-1) if α is a successor ordinal,
𝕍α = { 𝕍β | β < α } if α is a limit ordinal,
𝕍 = { 𝕍α | α On }.
The axiom of foundation can be expressed as 𝕍 = 𝕌. The rank function r() on 𝕍 is defined by 𝕍α then contains exactly the sets x such that r(x) < α.

Proposition: For every ordinal α, the following are satisfied:

  1. 𝕍1+α = α({}).
  2. (𝕍α, ) is an α-superstructure whose ground stage equals {} (whenever α > 0).
  3. For every non-terminal bounded object x of (𝕍α, ), the powerclass of x equals +(x).
The set-representation theorem

Theorem:
Every basic structure S0 = (O0, …) can be represented as a well-founded set O according to the following table. In particular, there is a set V such that

Terminal objects T   =   O (O O)
Inheritance root r   =   O T
For every x, y from O :
Bounded membership   x y   ↔   x y
Inheritance x y   ↔   x y
Singleton map x.ɛϲ = y   ↔   {x} = y
Powerclass map x.ec = y   ↔   r (x) = y
Power membership x ϵ¯ y   ↔   r (x) y
Object membership x ϵ y   ↔   r (x) y or x y
Anti-membership x ϵ-1 y   ↔   r (y) x
Complete extension (V,)
Last stage V   =   r +(r)
Ground stage V1   =   V (r)
Ground rank α0   =   r(V1)
The i-th stage Vi   =   V 𝕍α0+i
The i-th metalevel (i < ω)   =   i(r) i+1(r)
Union map x.υ   =   x

Proof:
Proceed in the following steps:

  1. Let S0 = (O0, …) be a basic structure of ϵ.
  2. Let S1 = (O1, …) be a completion of S0. Express S1 as an -structure (O1, ).
  3. Let i be the cardinality of the ground stage of S1.
  4. Let α = i + ϖ + ω.
  5. Let V be a regularly cumulated object in the (α+1)-superstructure (𝕍α+1, ) such that
  6. Let be an isomorphism between (O1, ) and (V, ).
  7. Let O be the set O0.
The existence of S1 follows by the completion theorem. The existence of V follows by the cardinality assertion. (The roles of α and ϖ are exchanged.) The equivalences and equalities stated in the table follow from the equalities
x.ecv = +(x),    x.υv = x,
x.ɛϲv = {x}, X.ɛϲv = (X)
which hold in the (α+1)-superstructure (𝕍α+1, ) for every sets x and X that are both elements and subsets of 𝕍α {}. (The equalities show the correspondence between set theoretic notation and the abstract notation of superstructures so that the last two propositions of the previous section can be applied. In addition, we have used instead of + in the table where applicable.)

Union in basic structures

Consider the definitional extension of a complete structure S = (O, ). The following table suggests that the union map .υ is another candidate to be introduced into basic structures by abstraction, just like .ec and .ɛϲ.
Power membership (ϵ¯) = (.ec) () (x.ec is the least power container of x)
Bounded membership () = (.ɛϲ) () (x.ɛϲ is the least bounded container of x)
Anti-membership (ϵ-1) = (.υ) () (x.υ is the least anti-container of x)
We have already observed that in complete structures, (ϵ-1) (϶) is a subrelation (thus a submap) of .υ (which is in turn a subrelation of ϵ-1). This suggests to regard (ϵ-1) (϶) as the implicit part of the abstraction of .υ in basic structures. We let the complementary, explicit part of .υ be denoted by . and call it the non-member union map. The situation is then summarized by the following table. (We can already consider the table to apply to the general case of basic structures, with Domain replaced by Potential domain.)
Map between objects Domain Map parts
Implicit Explicit
Powerclass map .ec O .ec = (ϵ¯) (϶-1)
Singleton map .ɛϲ O. (.ɛϲ) (.ec) .ɛɕ = (.ɛϲ) (ϵ¯) (primary singleton map)
Union map .υ O.϶-1 (ϵ-1) (϶) . = (.υ) (϶) (non-member union map)
The (b~9) axiom
The corresponding generalization of basic structures would be based on ϵ6-structures (instead of ϵ5-structures) which would contain . as an additional constituent of the signature. The presumed axiomatization of . is established by the reserved (b~9) axiom which is shown below together with the similar axiom (b~8).
(b~8) If x.ɛɕ = y then: (a) {x} = y.϶, (b) x.ϵi = y.ϵi-1 for every i 1, (c) (x,y) (ϵ¯).
(b~9) If x = y. then: (a1) x.϶¯ = y.϶.϶¯, (a2) x.϶ = y.϶2, (b) x.ϵi = y.ϵi-1 for every i 0, (c) (x,y) (ϵ).
Subsequently, the union map, .υ, is defined as a partial map between objects by We say that S is
union complete if x.υ is defined for every object x from O.϶-1.
The domains of ϵ-1 and of (ϵ-1) (϶) are the potential domains of .υ and ., respectively. We let the integer powers, inverses and transitive closures of .υ and . be denoted and defined in a similar way to that of .ec. The 0-th powers are identities on the respective potential domain.

Observations: Assume axioms of pre-basic structures.

  1. (ϵ-1) (϶) is a partial map between objects.
  2. Every pair (y,x) from (ϵ-1) (϶) satisfies conditions (b~9)(a1)(a2)(b).
  3. If, in addition, (b~9) is assumed then for every objects x, y,
     x = y.υ 1 + x.mli = y.mli.

Proof:

  1. Assume y ϵ-1 x ϵ y and y ϵ-1 x' ϵ y. Then (a) x ϵ y ϵ-1 x' and (b) x' ϵ y ϵ-1 x so that (a) x x' and (b) x' x.
  2. Assume y ϵ-1 x ϵ y. Then:
    (a1) x.϶¯ = y.϶.϶¯: a ϵ¯ b ϵ ya ϵ¯ b ϵ y ϵ-1 xa ϵ¯ b xa ϵ¯ x.
    (a2) x.϶ = y.϶.϶: (The same proof with ϵ¯ replaced by ϵ.)
    (b) x.ϵi = y.ϵi-1 for every i 0:   x ϵi ay ϵ-1 x ϵi ay ϵi-1 ax ϵ y ϵi-1 ax ϵi a.
  3. This is a consequence of (b~9)(b).
Rank adjustment
The diagram on the right shows that the (old) definition of the rank function .d is no longer acceptable since the . map adds new constraints to it. The purple arrow indicates that a = b.. We consider the diagram to show two structures: S0 and its extension S with the dashed part being the difference. Since a.d is finite (and thus a non-limit ordinal) a faithful interpretation of .d should assert that a.d + 1 = b.d. However, this is only satisfied in the S structure. In S0, a.d0 = b.d0 = 2 (according to the not-yet-adjusted definition of the rank function).


The following is an unverified proposal for the definition of the rank function .d in an ϵ6-structure S = (O, ϵ, …, .).
  1. Define path membership to be a system E = {i | i } of relations between objects generated by the following rules.
  2. Define path-ranking product to be a structure (Ƣ, ϵ) where Ƣ equals (O {ȶ}) × (with ȶ standing for a fictitious terminal object) and ϵ is a relation on Ƣ such that for every objects x,y and every natural i, j,
  3. For every object x, let x.d be the ϖ-limited rank of (x,0) in (Ƣ, ϵ).
Union 1-completion
The below is a prescription for equipping a basic structure with missing union objects. Since new objects have . undefined we speak about 1-completion.
Let S = (O, ϵ, …) be an ϵ6-structure and S0 = (O0, ϵ, …, .0) a basic ϵ6-structure. We say that S is a union 1-completion of S0 if S is an extension of S0 such that the following are satisfied:
  1. (.ec) = (.ec0), (.ɛɕ) = (.ɛɕ0), and O.(-1) = O0.0(0).
  2. (.) (.0) is injective.   (That is, for every new object x there is exactly one old object y such that x = y..)
  3. (.) (.0) is defined according to the following table. We assume that a, b are old objects. In (ⅰ) we assume that a. and b. are defined and new, in (ⅱ) we assume that a. is defined and new in (ⅲ) we assume that b. is defined and new.
    (α) (β) (γ) (i )
    a. ϵ b. b a.ϵ-1.ϵ¯.ϵ a. ϵ¯ b. a. ϵ¯-i b. b a.ϵ¯-i a.ϵ¯-i-1.ϵ
    a. ϵ b b a.ϵ-1.ϵ¯ a. ϵ¯ b a. ϵ¯-i b b a.ϵ¯-i-1
    a ϵ b. b a.ϵ2 a ϵ¯ b. b a.ϵ¯.ϵ a ϵ¯-i b. b a.ϵ¯-i+1 a.ϵ¯-i.ϵ
Completion conjecture

Conjecture: The completion theorem holds also for basic structures with the union map (i.e. ϵ6-structures satisfying (b~1)(b~11) with an adjusted definition of .d). More specifically,

  1. If S and S0 are as in the union 1-completion then S is a basic structure that is a faithful extension of S0.
  2. Every basic structure S0 has a union completion which is the limit of ω union 1-completions.
  3. The powerclass completion theorem is preserved.
  4. The (primary) singleton completion theorem is preserved.
  5. The extensional pre-completion theorem is preserved.
  6. Rank pre-completion theorem holds if the rank-precompletion also includes powerclass completion.
  7. In the axiomatization of pre-complete structures, powerclass consistency follows from union completeness.
  8. Embedding of pre-complete structures into complete structures preserves the union map.

 

References
Luca Cardelli, Structural Subtyping and the Notion of Power Type, Proc. of the 15th ACM Symp. on Principles of Programming Languages, POPL'88, 1988, http://www.daimi.au.dk/~madst/tool/tool2004/papers/structural.pdf
C. C. Chang, H. Jerome Keisler, Model Theory, Studies in Logic and the Foundations of Mathematics (3rd ed.), Elsevier, 1990,
B.A. Davey, H.A. Priestley, Introduction to lattices and order, Cambridge University Press 2002
Kees Doets, Basic model theory, Stanford: CLSI Publications, 1996,
Thomas Jech, Set theory: the third millennium edition, Springer, 2003
Vladimir Kanovei, Michael Reeken, Nonstandard analysis, axiomatically, Springer, 2004
John L. Kelley, General Topology, Springer 1975
Mauro Di Nasso, Pseudo-superstructures as nonstandard universes, The Journal of Symbolic Logic 63.01, 1998
Ondřej Pavlata, Object Membership: The Core Structure of Object Technology, 2012–2015, http://www.atalon.cz/om/object-membership/
Ondřej Pavlata, Object Membership: The Core Structure of Object-Oriented Programming, 2012–2015, http://www.atalon.cz/om/object-membership/oop/
Ondřej Pavlata, Object Membership with Prototypes, 2015, http://www.atalon.cz/om/object-membership/prototypes/
Ondřej Pavlata, Object Membership and Powertypes, 2015, http://www.atalon.cz/om/object-membership/powertypes/
Judith Roitman, Introduction to Modern Set Theory, Orthogonal Publishing L3C, 2011, http://www.math.ku.edu/~roitman/SetTheory.pdf
Jean E. Rubin, Set theory for the mathematician, Holden-Day, 1967,
Wikipedia: The Free Encyclopedia, http://wikipedia.org
Browser compatibility browser-compatibility
To be viewed correctly, this document requires advanced browser features to be supported, including
Document history
March122015 The initial release.
March172015 Spelling corrections, url links corrections (in some cases, the fragment identifier # was missing).
March242015 Introduced symbols 𝕍 and 𝕌 instead of VV and UU, respectively. The Membership glyphs subsection added.
April82015 A PDF version added. Some accompanying styling changes made.
June212015 Adjustments to the format of the link to the PDF version.
August212016 The font of and symbols changed to Lucida Sans Unicode.
License
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 3.0 License.