Dmytro Taranovsky March 10, 2015 Modified: October 31, 2016 Small change: December 14, 2016

# Set Theory with Reflective Sequences

Abstract: We extend the language of set theory through reflective sequences of ordinals, develop a hierarchy of reflective sequences, obtain limits on infinitary indiscernibles, and propose axioms for reflective sequences.

Note: For reader's convenience, the text now is also incorporated into Reflective Cardinals paper.

## Introduction

Within the language of set theory, one reaches higher and higher expressive power by climbing higher in the cumulative hierarchy of V. But how can we go further once the language allows quantification over the whole V? Intuitively, we would want to continue the hierarchy above V, except that all sets are already in V. The solution is to label a cardinal κ such that Vκ is sufficiently close to V, and continue the hierarchy above Vκ. Vκ represents V, and with κ labeled in an extended language, hierarchy above Vκ corresponds to higher order set theory.

To go further, we can iterate higher order set theory by picking λ>κ with Vλ representing V, and then μ>λ, and continuing to longer sequences of ordinals. Thus, continuing the cumulative hierarchy above V corresponds to labeling certain ordinals that are sufficiently similar to Ord — in other words, certain ordinals with sufficiently strong reflection properties — while staying within V.

How do we choose the right κ? The answer is that we postulate a certain degree of symmetry and reflection in V. Convergence Hypothesis (general form): For an appropriate type of objects, all objects of that type with sufficient reflection properties are, to a certain degree, indistinguishable from each other. Convergence Hypothesis (ordinals): If α and β are ordinals with sufficiently strong reflection properties, then φ(S, α) ⇔ φ(S, β) whenever rank(S) < min(α, β) and φ is a first order formula of set theory with two free variables. Definition: κ is a reflective cardinal, denoted by R(κ), iff (V,∈,κ) has the same theory with parameters in Vκ as (V,∈,λ) for every cardinal λ>κ with sufficiently strong reflection properties. Example: In L (assuming 0#), every Silver indiscernible has sufficient reflection properties, which allows us to define RL in V. Note: A formalist can treat the Convergence Hypothesis as a guiding principle to get good systems of axioms. A formalist can ask, for example, whether we want the Convergence Hypothesis to hold in V, and if yes (or maybe), investigate how far it can hold and how to axiomatize it. A counterexample to the Convergence Hypothesis would be a property that 'toggles', with an explanation of why it toggles.

To the extent that it holds, the Convergence Hypothesis allows us to define new reflective notions without ambiguity. We specify a notion by stating its type (example: a pair of ordinals) along with the class of predicates for which it agrees with all objects (of the same type) with sufficient reflection properties. See my Reflective Cardinals paper for analysis, axiomatization, and theory of reflective cardinals. Here, I will develop a theory of infinite reflective sequences. Definition: Given a length condition P (such as having length ω), an increasing sequence of ordinals S satisfying P is reflective (denoted by RP(S) or simply R(S)) iff   (1) the theory of (V,∈,S) with parameters in Vmin(S) is correct, that is it agrees with (V,∈,T) for every T satisfying P and having sufficient reflection properties and min(T)>min(S), and   (2) for every α<sup(S) S\α is reflective under the above criterion (where the length condition is modified to correspond to S\α if S\α is "shorter" than S). A variation on the notion is to omit the second condition.

Notes about R: • We use R rather a single element of R for two reasons:   - We want to be able to express predicates, such as the satisfaction relation of (V,∈), and not just statements.   - For infinite reflective sequences, it is unclear if (or how) an example is definable, and we want the intended semantics of the language to be unambiguous. • There is a hierarchy notions related to R based on the degree of "correctness" required (one example is to allow just ΣV2 φ in the definition as opposed to ΣV φ). Essentially, our choice for R(x) is to require just enough correctness to maximize expressiveness of (V,∈,x) for predicates that do not depend on x. • In every extension here, R will correspond to a single type of objects (for example, sequences of ordinals of length ω). However, these notions form a hierarchy, and an alternative, which we will use informally, is to use R(x) in place of Rtype(x)(x), thus having just a single symbol R.

## Reflective Sequences

To understand the hierarchy of reflective sequences, imagine a process of picking ordinals with sufficient reflection properties, and with the process itself having sufficient reflection properties. Let S be a resulting sequence. Here are some stages in the process: 1. n ordinals for finite n. This is well-understood (see "Reflective Cardinals" reference for theory). 2. ω ordinals. See "Reflective Cardinals" for some results. There is a refined hierarchy based on the degree of correctness we require. We have good axiomatization (specifically, through iterations of reflective cardinals) up to about correctness in Lsup(S)(Vsup(S)), and through an analogue of Prikry forcing, we may be able get up to M(Vsup(S)) (where M is a mouse operator and assuming sufficient structure above M). However, under reasonable assumptions, full correctness in V contradicts V=HOD, which makes analysis and finding of canonical models difficult. A reasonable conjecture is that the Σ2 truth predicate of (Vsup(S), ∈, S) corresponds to enumeration of all ordinal definable reals. 3. α ordinals for countable α. We expect R to be closed under subsequences that preserve order type. 4. ω1 ordinals. Assuming the Continuum Hypothesis (CH), we cannot require closure of R under all subsequences of the same length. Even without CH, this limitation holds at ω2. 5. α ordinals for a fixed ordinal α >ω1 (min(S)>α). 6. More complicated conditions about the length of S, such as |S|=min(S). S excludes its limit points. 7. Length of S has sufficiently strong reflection properties relative to S. S excludes its limit points. 8. To go beyond (7), we assume that S includes its limit points at places with sufficient (relative to S) degree of reflectiveness. One may then state conditions on the length of S such as "S includes exactly ω limit points, and they are cofinal in S" or "S has maximum element and it is the only element such that S below it is stationary". 9. Length of S has sufficiently strong reflection properties relative to S. This notion is axiomatized in "Axiomatization of Long Reflective Sequences" below.

To go beyond what is expressible with S, we mark some points on S that have sufficient (relative to S) degree of reflectiveness, analogously to how S is obtained by marking some ordinals with sufficient reflectiveness in V. To go further, we then add a third type of marking, and in general, for each ordinal in S, we can assign a degree of reflectiveness through a function f:S→Ord\{∅}. For a limit α, f(x)=α corresponds to x receiving all markings <α. In the definition of reflectiveness, use f in place of S, min(dom(f)) in place of min(S) (and min(dom(T)) in place of min(T)), sup(dom(f)) in place of sup(S), and in place of S\α, use f↾(Ord\α) modified to make f(min(dom(f)\α)) equal 1. Here are some notions. (Here S=dom(f).)

10. For a fixed ordinal α, f(sup(S))=α (and hence sup(S)∈S), and sup(S) is the only ordinal κ with f(κ)=α (and min(dom(f))>α). 11. f(sup(S))=sup(S), and sup(S) is the only ordinal κ with f(κ)=κ. 12. To go beyond f(κ)=κ, we modify the condition — that f(κ)=α+1 implies that κ has sufficiently strong reflection properties relative to f that is clipped to α — by invoking an ordinal notation system (for ordinals ≥κ) or just a comparison method between f(λ) and f(κ), and considering f clipped below f(κ) as defined through the comparison method. Below (in "Extension to Reflective Functions") we axiomatize the following: There is only one ordinal κ with f(κ)=(κ+)HOD, and it equals sup(dom(f)).

For reflective cardinals, an axiomatization essentially states the degree of correctness (relative to other reflective cardinals) and existence of enough reflective cardinals, and it can be extended with large cardinal axioms applied to reflective cardinals. For reflective sequences, we also need to state enough axioms for the sequence as a whole, or the axiomatization would be too incomplete. Just like large cardinal axioms for cardinals, there are various axioms for reflective sequences.

The type of f and many of its basic properties can be formalized using inner models. For example, for notion 11 we can require that there is an inner model M of ZFC such that  - dom(f) is the set of measurable cardinals in M  - for every κ in the domain of f, f(κ) is the Mitchell order of κ in M  - M has only one cardinal κ such that o(κ)M=κ and it is the largest measurable cardinal in M. From inner model theory, it appears that without restricting the class of f that satisfy the requirement, M can be taken to be an iterate of the minimal inner model with these cardinals. The possibilities for M and iteration are sufficiently rich to get any reasonable f corresponding to this notion (notion 11 in this case). One can also similarly state requirements on M for other notions.

If f satisfies the condition above (with M an iterate of the minimal model), then the theory of (L(f),∈,f) is independent of f, which is one example of the Convergence Hypothesis, and moreover, we can study this theory to get a better understanding of f.

Our axiomatization involves a strengthening of the above condition by asserting that elements of a reflective sequence are, in a sense, infinitary indiscernibles. To do that, we need to know how much infinitary indiscernibility is possible in V.

## Limits on Infinitary Indiscernibility

The axiom of choice sharply limits the amount of infinitary indiscernibility.

Theorem: For every uncountable sequence of distinct reals X, there is X-definable f:V→ω such that for every S⊂Ord of order type ω1 there is X,S-definable T⊂S of order type ω1 with f(T)≠f(S). Notes: • This implies that for every κ≥ω1, the partition relation κ → ω1ω1ω fails for a function f definable from X. • For definability, ΔV2 definability more than suffices. • If T could be made S-definable, the axioms below would be inconsistent, but a weakening to (essentially) lightface version would be unaffected. • Acknowledgment: I would like to thank Hugh Woodin for outlining a proof of a weaker version of the theorem with exponent ω2. Proof: Using X, we can define a sequence X′ of subsets of ω of length ω1 that does not have a perfect subset. Thus, the following game (this is the standard game for the perfect subset property) is undetermined: Player I: Each move consists of zero or more zeroes and ones. Player II: Each move is 0 or 1. Player I wins iff if the concatenation of the moves belongs to the set (X′). However, analogously to the standard proof of analytic determinacy from sharps (which can be found in, for example, Wikipedia Determinacy article (accessed October 30, 2016)), the partition relation would make the game determined as follows. The tree TX′ corresponding to the game will have ω1 branches at the root, each corresponding to an element of X′, and no further branches. The open auxiliary game requires player II to play the subtree of TX′ corresponding to the play so far (including all initial segments of the play), and a mapping of the subtree into ordinals, such that the mappings are consistent with each other and agree with the Kleene-Brouwer order. Player I wins the auxiliary game and has a definable strategy: For example, pick the least move that gives maximum reduction of the rank of the remaining game. Let g(S) return move given position where S is the set of ordinals used in the tree. If we attempt to use S to convert the strategy into a strategy for the original game, the failure will give us the required T. While g returns elements of 2ω, it can be converted into f:V→ω as follows: f(S)=2n+(g(S))n where n = min(m: ∃T⊂S T∈Def(X′,S) ∧ |T|=ω1 ∧ (g(S))m≠(g(T))m)) where Def(X′,S) can be for example definability from X′,S in Vsup(S)+1.

Corollary: There is a definable predicate P such that for every set of ordinals S of order type at least (22ω1)+ there are subsets T1 and T2 of order type ω1*2 such that such that P(T1)≠P(T2). Proof Sketch: Here is one such P: P(S) iff {Si:i<ω1} agrees with {Si1≤i<ω1*2} with respect to all predicates that are definable in Vsup(S) using parameters that are subsets of ω1.

In the absence of a convincing theory, lack of closure under subsets would cast doubt on whether the notions of reflective sequences are well-defined. However, we can weaken closure under subsets by requiring the subsets to be definable, and that may give us what we need to axiomatize R. Note: It is also possible that the convergence hypothesis holds for statements but not for statements with arbitrary sets as parameters. In that case, R would be ill-defined in V but might have a preferred well-defined theory, and its lightface version (requiring correctness only for statements without parameters) would be well defined. If the 'boldface' version is ill-defined or otherwise undesirable, the systems of axioms below can be modified for the lightface version by requiring the relevant theories to agree without parameters (as opposed to with parameters), and analogously for a strengthening of the lightface version that allows countable sequences of ordinals as parameters.

Assuming determinacy of games on ordinals of length ω1 and ordinal definable payoff, κ → κω12λ holds for every regular countably closed κ and λ<κ for functions definable from a countable sequence of ordinals. See my "Reflective Cardinals" paper for a proof sketch of a more general proposition using Extended Determinacy Maximum. Question: Can similar relations can be obtained from much weaker assumptions?

Partition relations with exponents >ω1 might be consistent by restricting to definable subsets. A strengthening of the strong partition relation (restricted to definable partitions and subsets) is to also require the homogeneous set to have enough limit points and require the same of the subset, and this can be strengthened further by requiring the sets to be in an appropriate filter. Here is a key proposition to investigate: Conjecture: There is an ordinal κ, a normal nonprincipal κ-complete ultrafilter U on κ, and S∈U such that for every T⊂S with T∈U and T ordinal definable from S and a countable set of ordinals, (V, ∈, T) and (V, ∈, S) have the same ΣV2 theory with parameters in Vmin(S). Question: Is this conjecture consistent? If consistent and nonrestrictive, this property can be used in axiomatization of long reflective sequences of ordinals as follows.

## Axiomatization of Long Reflective Sequences

Here is an axiomatization corresponding to notion 9 above. Its consistency and truthfulness are unclear.

Language: ∈, R (unary predicate) Definition: Theory(M, ∈, S; W) (where M is transitive, S⊂M and W⊂M) is {"φ",w: w∈W ∧ (M,∈,S)⊨φ(w)} where φ has 1 free variable and may use relational symbols '∈' and 'S' (unary predicate). Definition: ODS(C) is the class of sets ordinal definable (without using R) from S and elements of C. Definition: R1(κ) ⇔ ∃S∈R κ∈S Note: sup stands for supremum. Axioms: 1. ZFC 2. ∀x∃y∀z(z∈y⇔z∈x∧R(z)) 3. R(S) ⇔ Raux(S) ∧ ∀α<sup(S) Raux(S\α)     where Raux(S) ⇔ S≠∅ ∧ S⊂Ord ∧ ∀T∈R ∀κ∈R1\(sup(S∪T)+1) Theory(Vκ, ∈, S; Vmin(S∪T)) = Theory(Vκ, ∈, T; Vmin(S∪T)) 4. (schema; n is a natural number) ∃κ∈R1 ∃S∈R κ=sup(S) ∧ VκΣRn V 5. ∃S∈R ∃U∋S (a normal nonprincipal κ-complete ultrafilter on κ=sup(S)) ∀T∈ODS(Ordω) (T⊂S ∧ T∈U ⇒ R(T)).

Notes:

• (3) specifies the type of R and the degree of correctness required. The intended semantics is that members of R have sufficiently strong reflection properties so as to (if possible) render R unambiguous in V. As mentioned above, the general underlying hypothesis is that for an appropriate type, all objects of that type with sufficiently strong reflection properties are sufficiently indistinguishable from each other.
• Raux and R have the same expressive power (the definition of Raux in (3) could just as well have used Raux; R1 is {min(S):S∈Raux}), but R is more natural (and is different from Raux). Other than that, (1)-(4) are essentially standard, and the combinatorial properties are obtained from (5).
• (4) is a strengthening of replacement for formulas with R, and it also ensures that sup(S) has essentially the same properties as members of S.
• A weakening of (5) (if one objects to requiring measurable cardinals in V) is to require U to be an ultrafilter on a smaller model ZFC, as long as it contains HOD(Vκ, S).
• It is unclear whether the property in (5) holds for all members of R. Its weakening to ΣVn predicates holds, but it is unclear whether U can be chosen independent of n.
• In (5), it is unclear whether the ultrafilter itself can be chosen to have a canonical theory with parameters in Vκ.
• A strengthening of 5 is to also require S∈iU(R) to hold (where iU is the embedding corresponding to U).
• These notes also apply to the extension to reflective functions below (except the part about S∈iU(R)).

Using the theorem above, the axioms imply that there is no OD(Ordω) uncountable sequence of distinct reals.

Question: Is it consistent/provable/true that ∃κ>0 ∀f:κ→κ ∃T∈R∩P(κ) ∀α<κ Tα+1>f(Tα)? If yes, what about the stronger ∀S∈U ∃T⊂S T∈R∩U (where U is as in axiom 5 above)? Notes: * The same question can be asked about extensions to reflective functions using the domain of the function in place of T. * The statement (either weaker or stronger form) is natural and appears to fill in the gap created by the lack of closure of R under subsequences. However, we do not know whether there are 'pathological' counterexamples to the statement. * If true but unprovable, the statement is a good addition to the axioms.

Here are possible outcomes for the axioms: a. The axioms are inconsistent. One would then search for a suitable replacement, and if it is found, try again. b. The axioms are consistent but restrictive (for example, they contradict a true large cardinal axiom). One would then also look for replacement (though models for the axioms may also be interesting). c. The axioms are consistent but too incomplete because the underlying notion is ill-defined. One can still study models with the axioms, and appreciate the underlying symmetry and beauty. d. The axioms are consistent but too incomplete. One would then search for additional axioms. Good axiomatization is key evidence that the underlying notion is well-defined. e. The axioms form the core of the theory, but it can still be extended, analogously to ZFC forming basic axioms for set theory.

## Extension to Reflective Functions

We can go beyond notion 9 by having a coherent system of measures instead of a single measure. For an ordinal κ, measure U(κ,α) (note that its Mitchell rank need not be α) will witness that there are enough ordinals λ<κ with f(λ)=α (or if α≥κ that f(λ) corresponds to α). For transformations of f, besides reducing its domain, we can downgrade some of the labels. A complication is that in the transformed f, we may have, for example, an ordinal with label 2 without enough label 1 ordinals below it. We resolve it by recursively relabeling ordinals, each time keeping as much structure as is compatible with the labels for lower ordinals. The proposed axiomatization for notion 12 is as follows.

Language: ∈, R (unary predicate) Definition: κ∈R1 ⇔ ∃f∈R "f is a nonempty function with dom(f)⊂Ord" ∧ κ=min(dom(f)). Note: See above for definitions of Theory(M, ∈, S; W) and OD. Axioms: 1. ZFC 2. ∀x∃y∀z(z∈y⇔z∈x∧R(z)) 3. R(f) ⇔ Raux(f) ∧ ∀α<sup(dom(f)) ∃β>α Raux(f↾(Ord\β))     where Raux(f) ⇔ f≠∅ ∧ (f is a function) ∧ dom(f)⊂Ord ∧ ran(f)⊂Ord ∧ ∀g∈R ∀κ∈R1\(sup(dom(f)∪dom(g))+1) Theory(Vκ, ∈, f; Vmin(dom(f)∪dom(g))) = Theory(Vκ, ∈, g; Vmin(dom(f)∪dom(g))). 4. (length condition) ∀f∈R {κ∈dom(f): f(κ)=(κ+)HOD} = {sup(dom(f))} 5. (schema; n is a natural number) ∃κ∈R1 ∃f∈R κ=sup(dom(f)) ∧ VκΣRn V 6. (key combinatorial principle) There is f ∈ R and a sequence of ultrafilters U such that:      i. dom(U) = {(κ,α): κ∈dom(f) ∧ α<f(κ)}     ii. U(κ,α) is a κ-complete normal nonprincipal ultrafilter on κ    iii. ∀(κ,α)∈dom(U) (κ,α)∉dom(iU(κ,α)(U)) ∧ ∀β<α iU(κ,α)(U)(κ,β) = U(κ,β) (coherence condition; i is the embedding corresponding to the ultrafilter)    iv. Given a function g:Ord→Ord\{∅} with dom(g)⊂dom(f), define g′ (with dom(g′)=dom(g)) as follows: g′(κ)=min(g(κ), sup(α+1: α=0 ∨ ∃β>0 iU(κ,β)(g′)(κ) = α)).  Key Condition: ∀g∈ODf(Ordω) g′(sup(dom(f))) = f(sup(dom(f))) ⇒ R(g′).

## Further Extensions

### General

To extend the language further, some of the possibilities are:

1. Extend the length condition to a higher ordinal.
2. Extend R to a different type of objects.
3. Find a different property in the set-theoretical universe.
4. Find something other than sets that is not reducible to sets.

The axioms above are essentially independent of the length condition, and by using (non-overlapping) extenders in place of ultrafilters, we can go up to a strong cardinal (though the resulting system might well be inconsistent or otherwise false). On the other hand, our semantic development depends on being able to compare f(κ) with f(λ). We can likely go beyond (κ+)HOD by, for example, using R to define a higher ordinal and requiring correctness relative to R in the axioms to define R'. To potentially go much further, note that we depend only on the correctness of theory with appropriate parameters rather being able to compare all f(κ) and f(λ), and it is possible that there is unique privileged theory here.

Question: Does the convergence hypothesis apply to the class of iterates of the minimal inner model with a strong cardinal?

If yes, then we have a corresponding extension to the language of set theory, essentially corresponding to maximal canonical non-overlapping f.

### Overlapping Extenders

We can try to go even further by allowing f to overlap, that is by letting f(κ)≥λ for λ>κ and λ∈dom(f). This may be analogous to overlapping extenders in the models beyond a strong cardinal — for example two cardinals strong up to the same measurable cardinal may correspond with f(κ) = f(λ) = min(dom(f)\(λ+1)) (with κ<λ) — but there are other possibilities as well, and the right framework is unclear.

For overlapping f, we must impose a restriction on the type of overlap. Otherwise, let x0<x1<x2<... be an infinite sequence of ordinals such that ∀i<ω f(xi) ≥ sup(xi:i<ω). Let yi=min(α: f(α)≥xi). Without restrictions on overlapping, we would have y0<y1<...<x0, and repeating the process with y in place of x, we get z0<z1<...y0, and so on, leading to infinite regress. One restriction is to prohibit infinite overlap — that is to prohibit x0<x1<... with ∀i<ω f(xi)≥xi+1. However, this restriction is too limiting, and there is a better alternative. Note that if κ < λ < μ and κ is <λ-strong and λ is <μ strong, then κ is <μ strong. Analogously, we require that ∀κ∈dom(f)∀λ∈dom(f) (κ<λ ∧ f(κ)≥λ ⇒ f(κ)≥f(λ)).

The right general framework is to have a rich system of embeddings to witness f, perhaps using iteration trees. For an example, suppose f(κ)=λ+1 where λ=min(dom(f)\(κ+1)) and μ>λ and μ∈dom(f). If we remove all ordinals strictly between κ and μ from dom(f), then we should be able to arrange f(κ)=μ+1, and the system should have an embedding to witness that. However, we do not yet know how to axiomatize such systems. Below, we attempt an axiomatization for limited degree of overlap and without the ability to move f(κ) upward. The later restriction might make the system too incomplete, but (if consistent) it should still show important structure.

Language: ∈, R (unary predicate) Note: See "Axiomatization of Long Reflective Sequences" above for definitions of Theory(M, ∈, S; W) and OD. Axioms: 1,2,3 as above ("Extension to Reflective Functions"). 4. (schema; n is a natural number) There is f ∈ R, κmax=sup(dom(f)), a sequence of extenders E, and an ultrafilter U such that:      i. dom(E) = {(κ,α): κ∈dom(f) ∧ α<f(κ)}     ii. E(κ,α) is a normal short extender such that the corresponding embedding iE(κ,α) is α-dom(E)-S strong and has critical point κ. Here S is the satisfaction relation for ΣR,Vn formulas.    iii. ∀(κ,α)∈dom(E) (κ,α)∉dom(iE(κ,α)(E)) ∧ ∀β<α iE(κ,α)(E)(κ,β) = E(κ,β) (coherence condition)    iv. U is a κmax-complete normal nonprincipal ultrafilter on κmax.     v. VκmaxΣRn V and Theory(V,∈,R,f;Vκmax) = Theory(iU(V),∈,iU(R),f;Vκmax), where Theory is restricted to φ with n unbounded quantifiers.    vi. Given a function g:κmax→Ord, define g′:κmax→Ord as follows: g′(κ) = min({g(κ), sup(α+1: ∃β iE(κ,β)(g′)(κ) = α)} ∪ {sup(α+1: α<g′(λ) ∧ ∀γ<g′(λ)∃β iE(λ,β)(g′)(λ)≥γ ∧ iE(λ,β)(g′)(κ)≥α): λ<κ ∧ g′(λ)≥κ}}.  Let g′′ = g′↾{κ:g′(κ)>0}.  Key Condition: ∀g∈ODf,R(Ordω) ({λ∈dom(g′′): g′′(λ)=κmax}∈U ⇒ Theory(V,∈,R,g′′;Vκmax) = Theory(V,∈,R,f;Vκmax)), where Theory is restricted to φ with n unbounded quantifiers. Furthermore, if g↾dom(f) = f, then g′′ is f.

Notes:

• If the system is inconsistent, it may still be useful as an outline of how the axioms can look like.
• A schema was used to get the most natural stopping point at the price of some syntactic complexity. However, expressiveness using R goes only slightly beyond what is expressible with a single f∈R (assuming the relevant objects are in Vmin(dom(f))), and there is a natural mild weakening of 4 that avoids the schema and goes just beyond what is expressible about f without using R:
4.ii - let S be the satisfaction relation for (V,∈,f) formulas (which is definable using R and f). It is unclear whether omitting S entirely would cause much harm.
4.v - simply require that iU(R)(f) holds, and as a partial substitute for the remainder, add axiom 5 (from "Extension to Reflective Functions") to the axioms (or a related statement/schema).
4.vi - instead of using Theory, just require that g′′∈R; also, prohibit use of R in defining g.
• α-dom(E) strongness ensures that the embeddings witness not only the absolute largeness of f(κ) but also the structure of f between κ and f(κ).
• In 4.vi, note that if κ∉dom(f), then there is no E(κ,β), and sup(∅)=∅.
• In 4.vi, "g′′ is f" is used to avoid having to write out some properties twice (once for f and once for g′′).
• The difference of 4.vi from Extension to Reflective Functions 6.v is the treatment of overlapping f. If f(λ)>λ, then the structure of f between λ and f(λ) must be witnessed using E(λ,α) and hence by f below λ, and we apply the same requirement to g′. Thus, if the necessary structure below λ is erased, we correspondingly reduce g′ in the region between λ and f(λ).

For a model M with overlapping extenders, there may be multiple reasonable ways to represent M by f, and there is additional structure and complexity once M has a cardinal κ with a measure that concentrates on <κ-strong cardinals. One option is to let R apply to models directly (and for now, dropping the analogue of the second condition in the definition of R). Here is an example: R = {code(M): M0 elementarily embeds into M and (V,∈,code(M)) has the correct theory with parameters in Vκ where κ is the least measurable cardinal in M}, where M0 is (for example) the minimal inner model with a measurable limit λ of <λ-S-strong cardinals where S is the set of <λ strong cardinals, and code(M)=VδM for the least δ such that M=L(VδM).

The study of reflective constructs has only just begun.

REFERENCE