Object Membership
– Basic Structure

Preface

Author Ondřej Pavlata Jablonec nad Nisou Czech Republic

Document date Initial release March 12, 2015 Last major release March 12, 2015 Last update August 21, 2016 (see Document history)

PDF Version

• http://www.atalon.cz/pdf/om/om-basic-structure.pdf  

Warning

Membership glyphs

						(PNG images)
∊	ϵ	∈	∋	϶	∍	(HTML entities)

Table of contents

Introduction

⊆, ∅, ℙ, ∖, ∪, ∪ ∩, ∩,

• { , … , } and ( , … , ).

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:

• x = y ↔ for every set a, a ∈ x ↔ a ∈ y.

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,

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 ⊆.

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 []:

The objective

• core parts of object models of established languages like Ruby or Python arise as special cases of basic structures, and, on the other hand, how
• basic structures can be gradually completed to superstructures, which can be considered a generalization of partial von Neumann universe allowing more than one element in the ground stage.

Main correspondence

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,
   • the singleton map becomes strictly partial (⁎),
   • let the ℙ map be total by extending its semantics from powerset to powerclass,
   • change the ∈ symbol to є in order to reflect the semantic change of ℙ.
3. Change the universe from classes to objects and introduce ϵ , ≤, .ec and .ɛϲ as abstractions of є, ⊆, ℙ and x ↦ {x}, respectively.

Notes:

• (⁎) In [] the singleton map is total – {x} equals the universal class whenever x is a proper class. Interestingly, this extension would not change the definition of є.
• We further introduce slight adjustment of the definition of powerclass as known from set theory [] [], shifting the meaning from the class of subsets of x to the class of non-empty subsets of x. As a result, there will be no fixed point of .ec.

Basic structures from superstructures

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 ∊.
   • Let r be the inheritance root – the unique object x such that
     • x.∍ = O.∍.
   • Let ≤ be the inheritance relation defined by
     • x ≤ y  ↔   x = y or ∅ ≠ x.∍ ⊆ y.∍.
   • Let .ec be the powerclass map – the unique map O → O such that
     • u ∊ x.ec   ↔   u ≤ x and u ∈ O.∍.
   • Let .ɛϲ be the singleton map – the unique partial map O ↷ O such that
     • x.ɛϲ = y   ↔   {x} = y.∍.
   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 ∊ y ↔ x.ɛϲ ≤ y)
   (ϵ¯)	=	(.ec) ○ (≤)	is the power membership,	(x ϵ¯ y ↔ x.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 ϵⁱ. 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 ≤ 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
   • (a) (.ɛɕ) ⊆ (.ɛϲ),   (b) .ɛϲ.ɛϲ = .ɛϲ.ec   and   (c) x.ɛϲ = x.ec for every terminal x.
   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 ϵ¯ⁱ with ϵ¯^j is a subrelation of ϵ¯^i+j.
   3. Powers of ϵ compose transitively if they are positive on the left side: (ϵ) ○ (ϵⁱ) is a subrelation of ϵ¹⁺ⁱ.
   4. Powers of ϵ¯ are antisymmetric. The intersection of ϵ¯ⁱ 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) ∖ (϶¯ⁱ) 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 x ↔ u ϵ^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

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.
   • .ec is not a subrelation of ∊ (a consequence of the existence of unbounded objects: x ∊ x.ec ↔ x ∈ O.∍).
   • .ec increases the metalevel index, the length of the shortest ∊-path from the ground stage.
   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):
   • x.ɛϲ = x.ec ↔ x is terminal or a singleton.
   (In (𝕌, ∈),   ℙ(x) = {x} ↔ x = ∅.)

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

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,
   • extensionally consistent   (x ≤ y   ↔   x = y or ∅ ≠ x.∍ ⊆ y.∍     for every objects x, y),
   • powerclass consistent   (if x is powerclass-like then x is a powerclass),
   • powerclass complete,   (every object x has a powerclass x.ec),
   • singleton complete   (every bounded object x has a singleton x.ɛϲ), and
   • ∊-ranked   (for every object x,   x.d = r_∊(x)).
   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 V₁ 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 .ν₀, .ν₁, …, .ν_ϖ = .ν 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 V₁.
   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 .ν₀ 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

• 𝕍_1+α = ℙ_⋆^α({∅})   (the set of of well-founded pure sets of rank less than 1+α).

• V = ℙ_⋆^ϖ+1(V₁).

Sample structure

• ≤, the inheritance relation, is a partial order which is shown in its reflexive transitive reduction by green arrows.
• ϵ, the (object) membership relation, is shown via both blue arrows and green arrows. Specifically, ϵ equals the composition (→) ○ (≤) where → is the (exact) relation indicated by blue arrows.
• .ec, the (partial) powerclass map, is a subrelation of ϵ indicated by horizontal blue arrows. (That is, x.ec = y iff there is a horizontal blue arrow from x to y.)
• .ɛɕ, the (partial) primary singleton map, is another subrelation of ϵ – the range-restriction of ϵ to primary singletons, indicated by orange circles () (That is, x.ɛɕ = y iff there is a blue arrow from x to y and the y object is displayed as an orange circle. There are just two such objects in the sample structure.)

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 ϵⁱ x for some natural i > 0, where ϵⁱ 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.

• H, the set of helix objects, is the set of all direct or indirect containers of r, i.e. x ∈ H iff r ϵⁱ x for some i.
• R, the reduced helix, is the powerclass chain whose primary object is r. Note that R is linearly ordered by inheritance, inversely to .ec.

• O = T ⊎ C ⊎ O.ec ⊎ O.ɛɕ.

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

• ϵ¯ is defined by:   x ϵ¯ y ↔ x.↧ ⊆ y.϶   (x is a power member of y if all descendants of x are members of y),
• (ϵ^-1)  =  (≤) ○ ((.ce)∪(.ɕɛ)) ○ (≤),   (.ce / .ɕɛ denote the inverse of .ec / .ɛɕ.), and
• for every natural i > 1,   ϵ^-i equals the i-th relational composition of ϵ^-1 with itself.

The ϵ-diamond

• ϵ¯, the power membership, has been introduced above.
• ∊, the bounded membership, is the domain-restriction of ϵ to bounded objects, that is,
  • x ∊ y   ↔   x ϵ y and x is bounded.
• Additionally, ∊¯ denotes the bounded power membership, that is, (∊¯) = (∊) ∩ (ϵ¯).

• (ϵ) = (∊) ∪ (ϵ¯),

Specialities of the sample

• As described above, ϵ¯ and ϵ^-i, i ∈ ℕ, are derived from ≤, ϵ, .ec and .ɛɕ.
• There are only finitely many objects. In particular, the set C of classes is finite. This allowed us to define unboundedness of objects via their circularity in ϵ.
• H = R.↥ – that is, helix objects are ancestors of R. This simplifies the description of metalevels below.

Powerclasses and singletons

• x.ɛϲ = y    ↔    (ⅰ) x.ɛɕ = y or   (ⅱ) x.ec = y and x.pr ∈ T ∪ O.ɛɕ.

• the (q.ec, v) pair satisfies both (a) and (b) but v is not a powerclass,
• the (g, s) pair satisfies both (a') and (b') but s is not a singleton.

Metalevels

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

Rank

• (ϵ) ⊆ (ℇ¹).
• (≤) ⊆ (ℇ⁰).
• (.ce) ∪ (.ɕɛ) ⊆ (ℇ^-1).   (.ce / .ɕɛ denote the inverse of .ec / .ɛɕ.)
• (ℇ^j) ○ (ℇ^k) ⊆ (ℇ^j+k) for every integers j, k.

• x ℇⁱ y   iff   x = x₀ ϵ^i₁ x₁ ϵ^i₂ ⋯ ϵ^i_n x_n = y

• (ϵ¹) = (ϵ),   (ϵ⁰) = (≤),   and   (ϵ^-1)  =  (≤) ○ ((.ce)∪(.ɕɛ)) ○ (≤).   (See power membership.)

• if u ℇⁱ x then u.mli + i ≥ x.mli.

• x.d = sup {u.mli + i | u ℇⁱ x, i ∈ ℤ}.

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 ℇ⁰ x, the rank is at least so big as the metalevel index. Since (ϵⁱ) ⊆ (ℇⁱ) for every i > 0, the rank of every unbounded object x (such that x ϵⁱ 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:

• Unbounded objects are those with infinite rank.
• Bounded objects are those with finite rank.
• Terminal objects are those with zero rank.

Preliminaries

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

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.

• X.f = { y | there exists x ∈ X such that (x,y) ∈ f }.

Symbols → / ↷ / ↪ indicate total / partial / injective maps, respectively.

Ordinal numbers

• α + 1 = α ∪ {α}   (the successor of α),
• α ≤ β   iff   α ⊆ β,
• α < β   iff   α ∈ β   iff   α ≤ β and α ≠ β,
• α ∧ β = α ∩ β   (the minimum between α and β),   similarly, α ∨ β = α ∪ β,
• sup(X) = ∨X = ∪X.   (The supremum of X. We will mostly prefer the sup(X) expression.)

Cardinal numbers

Natural numbers

Integers

• i + ω = ω   for every integer i.

Well-foundedness

• … x₂ ϵ x₁ ϵ x₀ = x.

Rank

• r(x) = sup {r(a) + 1 | a ∊ x}.

• let the ∊-rank of a subset Y of X be sup {r(a) + 1 | a ∈ Y},
• let the rank of ∊ be the ∊-rank of X.

Limited rank

Fixing a limit ordinal ϖ

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

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

• allowing .ec and .ɛϲ to be incomplete,
• abstraction from ϵ, ϵ¯ and ϵ^-i for every natural i.

ϵ5-structure

• O is a set of objects,
• ϵ^⁽*⁾ and ϵ¯^⁽*⁾ are bi-infinite sequences of relations between objects such that (ϵⁱ) = (ϵ¯ⁱ) for i ≤ 0 and where
  • (ϵ) = (ϵ¹) is the (object) membership relation,
  • (ϵ¯) = (ϵ¯¹) is the power membership relation,
  • (≤) = (ϵ⁰) is the inheritance relation (with .↧ / .↥ used for preimages / images under ≤),
  • (ϵ^-1) is the anti-membership relation,
• r is the inheritance root, a distinguished object.

• .ec is the powerclass map   (objects from O.ec are powerclasses),
• .ɛɕ is the primary singleton map   (objects from O.ɛɕ are primary singletons).

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

• For every integer i,   ϶ⁱ (resp. ϶¯ⁱ) denotes the inverse of ϵⁱ (resp. of ϵ¯ⁱ).
• For a natural i,   let .ec(i) be the i-th composition of .ec with itself, with .ec(0) being the identity on O. Let .ec(-i) be the inverse of .ec(i).
• Let T = O ∖ O.ϵ.↧ be the set of terminal objects (or terminals).
• The metalevel index, x.mli, and rank, x.d, of an object x are defined by
  • x.mli = sup { i | x ϵ^1-i r, i ∈ ℕ },
  • x.d = sup {a.mli + i-j | a ∈ x.϶ⁱ.϶^-j, i,j ∈ ℕ},
  where the definition of .d only applies to the special case ϖ = ω and under additional assumptions which are consequences of (b~1)–(b~10). The general definition of .d is provided in the next section.

Basic structure

First observations:

1. The (b~2) condition has three important special cases:
   • For i = j = 0 the transitivity of ≤:   (≤) ○ (≤) ⊆ (≤).
   • For i = 0 and j = 1 the monotonicity of ϵ¯:   (≤) ○ (ϵ¯) ⊆ (ϵ¯).
   • For i = 1 and j = 0 the subsumption of ϵ¯:   (ϵ¯) ○ (≤) ⊆ (ϵ¯).
   Using (b~0) (b~1) and (b~3) it follows that (b~2) is equivalent to:  
   • (b~2)'   (a) (ϵ¯) ○ (≤) ⊆ (ϵ¯),   (b) (ϵ¯^-i) ○ (ϵ¯^1-j) ⊆ (ϵ¯^1-i-j) for every natural i, j.
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 (ⅱ):
   • (ϵ) ○ (ϵ^-i) ⊆ (ϵ^1-i)   for every natural i.
   • (ϵⁱ) ○ (ϵ^j) ⊆ (ϵ^i+j)   for every natural i > 0 and every integer j.
3. For i = 0 in (b~4) we obtain the antisymmetry and reflexivity of ≤:   (≤) ∩ (≥) = (O, =). It follows that
   • ≤ is a partial order on O.
   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,
   • O = T ⊎ r.↧.
   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:
   • O.϶ = O.϶¯ = O = r.϶¯ = r.϶.
   (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.ɛɕ,
   • x.϶¯^-i ⊆ x.ϵ¯ⁱ   for every natural i,
   • x.϶¯^-∗ ⊆ x.ϵ¯^∗   (where (ϵ¯^∗) = ∪{ϵⁱ | i ∈ ℕ} and (ϵ¯^-∗) = ∪{ϵ^-i | i ∈ ℕ}),
   • x.϶¯^-∗ = x.ec^∗   (where .ec^∗ is the reflexive transitive closure of .ec),
   • x.϶¯^∗-∗ = x.ec^∗-∗   (where (϶¯^∗-∗) = (϶¯^∗) ∪ (϶¯^-∗) and (.ec^∗-∗) = (.ec^∗) ∪ (.ce^∗)).
   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 (ⅰ)–(ⅲ):
   • (ⅰ) y.϶¯ = ∅,   (ⅱ) (x,y) ∉ (.ec),   (ⅲ) y ∉ O.ec,
   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,
    • .ec = .ɛɕ = ∅ = (ϵ¯ⁱ) for i < 0   and   (ϵ¯ⁱ) = (ϵ) = {(r, r)} for i ≥ 0.

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/ϵ¯ⁱ/ϵⁱ.
3. Corollary: In a powerclass complete (pre-)basic structure, powers of ϵ¯ are given by ≤ and .ec:
   • (ϵ¯ⁱ)   =   (≤) ○ .ec(i) ○ (≤)     for every integer i.
4. For every objects x, y and every integers i, j, k, if both x.ec(i) and y.ec(j) are defined then
   • x.ec(i) ϵ¯^k y.ec(j)   ↔   x ϵ¯^k+i-j y,
   • x.ec(i) ϵ^k y.ec(j)   →   x ϵ^k+i-j y,
   • .ec(i)x ϵ^k y.ec(j)   ↔   x ϵ^k-j y.
5. Corollary (the case i = j = 1, k = 0 in (ⅰ)):   The .ec map is an order embedding of (O.ce, ≤) into (O, ≤):
   • x ≤ y   ↔   x.ec ≤ y.ec     whenever both x.ec and y.ec are defined.
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:

2. (Apply:   (a) x.↧ = y.϶ⁱ ↔ y.϶ⁱ ⊆ x.↧ ⊆ y.϶ⁱ,   (b) x.ϵ¯ⁱ = y.↥ ↔ y.↥ ⊆ x.ϵ¯ⁱ ⊆ y.↥.) Assume that x.ec(i) = y, i ∈ ℤ. Then
   1. x.↧ = y.϶ⁱ follows from:   .ec(i) ○ (϶ⁱ) ⊆ (≥) and .ec(-i) ○ (≥) ⊆ (϶ⁱ).   (The same holds with ϶¯ⁱ instead of ϶ⁱ.)
   2. x.ϵ¯ⁱ = y.↥ follows from:   .ec(i) ○ (≤) ⊆ (ϵ¯ⁱ) and .ec(-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

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

Powerclass chains

• Let .ec^∗ be the reflexive transitive closure of .ec. For a positive natural i,
  • .ec(i) is the i-th composition of .ec with itself,
  • .ec(0) is the identity on O,
  • .ec(-i) is the inverse of .ec(i).
• Let .ce, .ce^∗, .ce(i) be the the inverse of .ec, .ec^∗, .ec(i), respectively.
• Let (.ec^∗-∗) = (.ec^∗) ∪ (.ce^∗).

• Let .pr be the map between objects such that:   x = y.pr   ↔   {x} = y.ce^∗ ∖ O.ec.
• For an object x, (in each case assume that the value is defined)
  • x.ec is the powerclass of x,
  • x.ec^∗ is the powerclass chain of x,
  • x.ce is the powerclass predecessor of x,
  • x.pr is the primary object of x,
  • x.eci is the powerclass index of x, defined by x.eci = sup {i | {x}.ce(i) ≠ ∅}.
    If x.pr exists then:   x.eci = i   ↔   x.pr.ec(i) = x.
• S is powerclass complete if .ec is a total map between objects, i.e. O = O.ce.

Object membership

• ϵ, the (object) membership, is the first constituent of an ϵ5-structure,
• ϵ¯, the power membership, equals ϵ¯¹ from the definitory sequence ϵ¯^⁽*⁾.
• ∊, the bounded membership, is defined by:   x ∊ y   ↔   x ϵ y and x.d < ϖ.
• ∊¯ denotes the intersection (∊) ∩ (ϵ¯) (the bounded power membership).

• (ϵ^∗) = ∪{ϵⁱ | i ∈ ℕ},   similarly for ϵ¯ / ∊ / ∊¯,   (note that due (b~0), ϵ^∗ is the transitive closure of (ϵ⁰) ∪ (ϵ¹)),
• (ϵ^-∗) = ∪{ϵ^-i | i ∈ ℕ},
• (ϵ¯^-∗) = (ϵ^-∗) and (ϵ¯^∗-∗) = (ϵ¯^∗) ∪ (ϵ¯^-∗).

• ϵ / ϵ¯ / ∊ / ∊¯   ⇢   ϶ / ϶¯ / ∍ / ∍¯.

• x.϶ is the set of members of x,
• x.϶¯ is the set of power members of x,
• x.∍ is the set of bounded members of x,
• x.ϵ is the set of containers of x,
• x.ϵ¯ is the set of power containers of x.

Inheritance

• (≤) = (ϵ⁰) = (ϵ¯⁰),

• x < y   ↔   x ≤ y and x ≠ y.

• x ∊⁰ y   ↔   x ≤ y and x.d < ϖ.

• x.↧ is the set of descendants of x,
• x.⋁ is the set of strict descendants of x,
• x.∍⁰ is the set of bounded descendants of x,   x.∍⁰ = x.↧ ∩ O.∍,   (assuming O = O.϶ for the equality)
• x.↥ is the set of ancestors of x,
• x.⋀ is the set of strict ancestors of x,   x.⋀ = x.↥ ∖ {x}.

Polars of ≤

• X ≤ Y   iff   x ≤ y for every x ∈ X and y ∈ Y,
• a ≤ X   iff   {a} ≤ X.

• X.▽ = { x | x ≤ X }, X.△ = { x | x ≥ X }   (.▽ and .△ are the polar maps of ≤),
• X.⋁ = { x | x < X }, X.⋀ = { x | x > X }   (.⋁ and .⋀ are the polar maps of <).

Anti-membership

• ϵ^-1 is the anti-membership relation.   (We might also consider ∊^-1 to be the bounded anti-membership.)

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

• The set O is the set of all objects.
• The set O.∍ is the set of bounded objects.   (Again, we assume O = O.϶ for this expression.)
• The set O.ec consists of powerclasses.
• The set O.pr = O ∖ O.ec is the set of primary objects.
• The set T of terminal objects (or terminals) is defined as O ∖ O.ϵ.↧.
• The set R = r.ec^∗ (the powerclass chain of r) is the reduced helix.
• The set H = r.ϵ^∗ is the set of helix objects.
• The set O.ɛɕ is the set of primary singletons.
• The set O.ɛϲ is the set of singletons.   (See below for the definition of .ɛϲ.)
• The set C of classes is defined as O ∖ (T ∪ O.ec ∪ O.ɛɕ).

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

• .ɛɕ is a partial map between objects, x.ɛɕ (if defined) is the primary singleton of x.

• x.ɛϲ = y   ↔   {x} = y.϶ and y is from (T.ec ∪ O.ɛɕ).ec^∗.

• .ɕɛ is the inverse of .ɛɕ,
• O.ɕɛ is the set of objects with a defined primary singleton,
• O.ɛɕ(0)   (= O.∍ ∖ (T ∪ O.ɛϲ))   is the potential domain of .ɛɕ.

Observations:

1. Condition (b~8)(a) is equivalent to (.ɛɕ) ⊆ (.ɛϲ).
2. Assume (b~1), (b~4) and (b~8)(a)(c). Then .ɛɕ is obtained from .ɛϲ :
   • (.ɛɕ) = (.ɛϲ) ∖ (.ec),
   • .ɛɕ equals the range-restriction of .ɛϲ to O.pr:
     • x.ɛɕ = y   ↔   x.ɛϲ = y and y is primary.
     In particular, a primary singleton is a singleton that is primary.
3. Assume all axioms of basic structures. Then the following are satisfied:
   • .ɛϲ.϶^-i = .ɛϲ.ec(i)   for every natural i.   (By (b~7)(a).)
   • .ɛϲ.ϵ = .ɛϲ.ϵ¯.   (By (b~7)(b).)
   • .ɛϲ.ɛɕ = ∅.   (By (b~8)(c) – A singleton has no primary singleton.)
   • .ɛϲ.ɛϲ = .ɛϲ.ec.   (Powerclasses of singletons are singletons.)
   • T ⊎ O.ɛϲ   =   (T ⊎ O.ɛɕ).ec^∗.   (An object x is terminal or a singleton  iff  x.pr is terminal or a singleton.)
4. Assume that S is a singleton complete basic struture. Then
   • .∊ = .ɛϲ.↥.   (That is, the bounded membership ∊ equals the composition (.ɛϲ) ○ (≤).)

Metalevels

• x.mli = sup {i | x ϵ^1-i r, i ∈ ℕ}.

• x.mli > i ↔ x ϵ^-i r    for every natural 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
   • t.϶ ∖ t.↧ is the i-th metalevel,   (with t.ce the top if i > 0)
   • t.↧ ∖ t.϶^-1 is the (i+1)-th metalevel with t as the top.
5. (Recall that i + ω = ω for every integer i.)
   If x ϵⁱ y for an integer i then i + x.mli ≥ y.mli.   (A consequence of r.϶^1-k.϶ⁱ ⊆ 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

• h = sup {i + 1 | r.ϵⁱ ≠ r.ϵ^i-1, i ∈ ℕ}.

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 ϵ:
   • ∅ = ⋯ = r.ϵ^-1 ⊂ {r} = r.ϵ⁰ ⊂ ⋯ ⊂ r.ϵ^-1+h = r.ϵ^h = ⋯ = H.   
   (Recal that H denotes the set r.ϵ^∗ of helix objects. Also recall that i + ω = ω for every integer i.)
2. For every natural i,  
   • i < h   ↔   r.ϵ^i-1 ≠ H   ↔   r.ϵⁱ ≠ r.ϵ^i-1.
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

• (a) z is well-founded in ϵ   and   (b) for every a from z.϶^∗.϶^-∗,   the metalevel index a.mli is finite.

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.)
   • {i-j + a.mli | a ∈ x.϶ⁱ.϶^-j, i,j ∈ ℕ},
   • {i+j + a.mli | a ∈ x.϶ⁱ.϶^j, i,j ∈ ℤ}.
2. For every object x satisfying x.϶^∗.϶^-∗.mli < ω the following set is identical to (ⅰ):
   1. (ⅰ') {i-j + a.mli | a ∈ x.϶ⁱ.϶^-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.϶ⁱ.϶^-j, i,j ∈ ℕ}.

Boundedness

• Objects x such that x.d < ϖ are bounded, the remaining objects x (such that x.d = ϖ) are unbounded.
• A set X of objects is bounded (resp. unbounded) if sup(X.d) < ϖ (resp. sup(X.d) = ϖ).
• The already introduced bounded membership relation, ∊, is therefore the domain restriction of ϵ to bounded objects. If O = O.϶ (as is asserted in basic structures) then O.∍ is the set of bounded objects.

Power instance-of and the .class map

• The .class map is the (partial) map between objects given by
  • x.class = y   iff   y is the (unique) bottom of x.ϵ¯ ∩ C,
  that is, x.class equals the least power-container of x that is a class (whenever such an object exists). If x.class = y then we say that y is the class of x. For an integer i we denote .class(i) the i-th power of .class defined in the usual way. That is,
  • for i > 0,   .class(i) is the i-th composition of .class with itself,
  • for i = 0,   .class(i) is the identity map between objects,
  • for i < 0,   .class(i) is the inverse of .class(-i).
• The power instance-of relation is the range-restriction of ϵ¯ to the set C of classes. That is, for every objects x, y,
  • x is a power instance of y   ↔   x ϵ¯ y ∈ C.
• As a subrelation of the power instance-of relation, .class is also called the direct power instance-of relation. For an object y,   {y}.class(-1) is the set of direct power instances of y.
• The instance-of relation is the range-restriction of ϵ to C.

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,
   • x ≤ y   →   x.class ≤ y.class.

Consistency and completeness

ϵ-rank and ∊-rank

• r_ϵ(x) be the ϵ-rank of x defined recursively by

  rϵ(x) = ϖ ∧ sup {rϵ(a) + 1 | a ϵ x }	if x is well-founded in ϵ,
  rϵ(x) = ϖ	otherwise,

• r_∊(x) be the ∊-rank of x defined recursively by
  • r_∊(x) = sup {r_∊(a) + 1 | a ∊ x }.

• r_∊(X) be the ∊-rank of X defined as sup {r_∊(a) + 1 | a ∈ X }.

Observations:

1. For every object x,
   • r_∊(x) ≤ r_ϵ(x) ≤ x.d.   (In particular, being ∊-ranked implies being ϵ-ranked.)
2. If r is ∊-ranked then r_∊(O) = ϖ+1.

Groundedness

• ϵ-grounded if x ∈ T.ϵ^∗, that is, u ϵⁱ x for some terminal u and natural i,
• ∊-grounded if x ∈ T.∊^∗, that is, u ∊ⁱ x for some terminal u and natural i.

Proposition A: Assume (a) (ϵ) = (∊) ∪ (ϵ¯), (b) (≤) ○ (ϵ¯) ⊆ (ϵ¯), and (c) T ⊆ O.∍.   (All of (a)–(c) are satisfied in basic structures.) Assume in addition that (d) (∊) = (∊) ○ (∊⁰).

1. For every natural i,   ∊ⁱ is the domain-restriction of ϵⁱ to bounded objects.
2. Corollary: If S is ϵ-grounded then S is ∊-grounded.
   (More specifically, if S is ϵ-grounded then T.ϵⁱ = T.∊ⁱ 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 ϵⁱ y ϵ z and x is bounded. We should prove that x ∊ⁱ⁺¹ z, that is, x.∊ⁱ ∩ z.∍ is non-empty. By induction assumption, x ∊ⁱ y, so that x ∊^i-1 a ∊ y for some a. By (c) there exist bounded b such that a ∊ b ≤ y.
   • If y is bounded then y ∈ x.∊ⁱ ∩ z.∍.
   • If y is unbounded then, by (a), y ϵ¯ z, therefore b ∊ z, and consequently, b ∈ x.∊ⁱ ∩ z.∍.

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,
   • x is ϵ-grounded and i < x.mli   →   ∅ ≠ x.϶ⁱ ≤ r.
   • x is ϵ-grounded and i ≤ x.mli   →   ∅ ≠ x.϶ⁱ.

Proof:

1. Let x be and object. We show that: x.mli = ω → x ∉ T.ϵ^∗. Observe that
   • x.mli = ω ↔ for every natural j, x ϵ^1-j r,
   • for every object u and every natural i, j:   i < j and u ϵⁱ x ϵ^1-j r   →   u ϵ^1+i-j r   →   u ≤ r.
   As a consequence, if x.mli = ω then x.϶ⁱ ≤ 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.϶ⁱ ≤ r (by (ϵⁱ) ○ (ϵ¯^-i) ⊆ (≤)). Since x.϶^∗ ≰ r by ϵ-groundedness of x it follows that x.϶ⁱ must be non-empty. The (b) statement follows from (a).

Extensional consistency

• x ≤ y ↔ x = y or ∅ ≠ x.∍ ⊆ y.∍.

∊-levelling

• x.mli = min { i | x ∈ T.∊ⁱ, i ∈ ℕ },

Observations:

1. In a basic structure,   an object x is ∊-levelled   ↔   x ∈ T.∊ⁱ   where i = x.mli.
2. For a basic structure S the following are equivalent:
   • S is ∊-levelled.
   • Every non-terminal object z has a bounded member u such that u.mli + 1 = z.mli.
     (That is, for every non-terminal z,   z.mli ≰ z.∍.mli.)
   • For every natural i,   the i-th metalevel equals T.∊ⁱ ∩ r.϶^1-i.

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,

• x.mli ≥ i+1 ↔ x ≤ r.ec(i).

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

• x.϶ = x.϶¯, and
• x.϶ ∩ Y.△ ≠ ∅ for every bounded subset Y of x.϶.

• x is powerclass-like → x is a powerclass.

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,   z_i.↧ (= z_i+1.϶ = z_i+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 ≤ z_i+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

• x is e+p consistent if it is both extensionally consistent and both powerclass consistent.

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 ϵ¯^ℓ z → y ϵ¯^ℓ-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,
   • y.mli > k-i   ↔   y ϵ¯^i-k r   ↔   x ϵ¯ⁱ r   ↔   i > 0.
   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
   • z is e+p consistent   (that is, z is both extensionally consistent and powerclass consistent).

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 .ԏ,
   • x.ϵ¯^k-1 = y.ϵ^-1 ⊎ {x}.ec(k-1)
   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
   • a.∊ = x.ϵ¯^k+n = y.ϵ¯ⁿ ⊎ {a}.ec = z.↥ ⊎ {a}.ec.
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,
   • z.∍ ⊆ u.∍ → {a,b} ⊆ u.∍ → z ≤ 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
   • X.△ = a.↥ ∩ b.↥ = z.ϵ^-1
   and thus X.△ ∩ z.϶¯ = z.ϵ^-1 ∩ z.϶¯ = ∅, i.e. X has no upper bound in z.϶ so that z is not powerclass-like.

Completeness

Pre-basic structure

Pre-basic structure

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:

3. For every terminal x,   x.϶ = ∅ and (as a consequence) x.϶^∗.϶^-∗ = x.϶^-∗ so that
   • x.d = sup {a.mli - i | a ∈ x.϶^-i }.
   Since by (ϐ~7), a ϵ^-i x → a.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:

• S is ϵ-ranked.   (I.e. x.d = r_ϵ(x) for every object x.)
• For every object x that is well-founded in ϵ,
  • x.mli < ω   (x has finite metalevel index), and
  • x ∈ T.ϵ^∗   (x is ϵ-grounded).

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

• r_ϵ(a) = 0 ↔ a.d = 0 ↔ a ∈ T   (the latter equality is by the observation made for pre-basic structures)

• (a') a.mli < ω for every a ∈ x.϶^∗.϶^-∗.

• (∗) there exists a pair (b,n) from O × ℕ such that (a) b ϵⁿ x and (b) n ≥ m.

• b ϵⁿ x   (since k ≥ j – a consequence of b ∈ T,   so that b.ϵ^k.ϵ^-j.ϵⁱ ⊆ b.ϵ^k-j.ϵⁱ ⊆ b.ϵ^k-j+i),
• n ≥ m   (since k ≥ a.mli   – use the observation about .mli, apply b.mli = 0).

Metaobject structure

• (ϵ¯ⁱ)   =   (≤) ○ .ec(i) ○ (≤),   (in particular, (ϵ¯) = (.ec) ○ (≤))

• (∊)   =   (.ɛϲ) ○ (≤).