{'fraction_non_alphanumeric': 0.05623923726321979, 'fraction_numerical': 0.01228527027594607, 'mean_word_length': 3.723638527923817, 'pattern_counts': {'":': 0, '<': 19, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 1, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 11, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Characterization of Non-Iterative Normal Modal Logics

Non-iterative normal modal logics are defined by axioms of modal degree 1. In this paper we use calculations with normal forms to determine the set of all possible non-iterative normal modal logics, unimodal propositional extensions of K. To characterize them, we construct the complete set (lattice) of such logics and we provide the generic specification of their axioms and their semantics.


Introduction
Scope. The normal modal logic K and its extensions are defined in classical text books such as [1] and [3]. We use the terms modal logic, modal logic system, or simply logic or system interchangeably. Note that, as a general rule, in this paper by "system" we mean a finitely-axiomatizable unimodal propositional extension of K; exceptions shall be pointed out explicitly.
A non-iterative system is one that can be axiomatized by formulas with no iterated (i.e. no nested) modalities. These systems have been studied before and several of their attributes (e.g. having the finite model property or being canonical) have been proven in papers like [4] and [6]. However, noniterative systems are not determined solely from these properties, because other systems may have them too.
So in this paper we attempt to provide a comprehensive characterization of all non-iterative systems. We basically ask the following question: (Q): What are all the possible non-iterative systems, i.e. how can we define every single instance from this set explicitly?
To answer, we apply some of the methods described in [5]. We use normal forms, specifically the disjunctive normal forms (DNF) described in [2], which are a special case of the canonical forms defined in [5]. The results that we provide consist of: • A method to define/construct the lattice of non-iterative systems (partially ordered by inclusion), showing the relationships between systems. • For each such system, the explicit formula for a defining axiom, as well as the characterizing class of Kripke frames.
Methodology. To begin with, in Sections 2 and 3 we introduce some prerequisite concepts and basic properties. Then the main results are in Sections 4-6. The following is an outline of our strategy for answering (Q): (1) First, in Section 4, using the Lindenbaum-Tarski algebra, we partition all (classes of equiprovable) non-iterative modal formulas into a countable set of modal contexts, where each context includes only a finite number of formulas. Any such formula can be used as an axiom for a non-iterative system. But a number of different axioms may end up generating the same system. So we prune the formulas to a minimal set of candidate axioms that tentatively yield all the non-iterative systems. We show that in each context there is only a finite number of systems determined by our axioms, and that they form a lattice. This lattice is remarkably regular, such that by using some ad-hoc coordinates we can conveniently label each system by its unique position in the lattice.
(2) Next, in Section 5, we assemble the finite lattices from all contexts into a single candidate lattice that should include all the non-iterative systems. Here, each system is again determined by its axiom and its unique position in the assembled, infinite lattice. Still at this point we don't know yet whether or not the systems in the lattice are all distinct.
(3) Finally, in Section 6, for each system in the candidate lattice we explicitly determine the corresponding Kripke semantics, i.e. its characterizing class of Kripke frames. And since we are able to prove that each system is characterized by a different class of frames, we conclude that all the non-iterative systems in our candidate lattice are distinct.
We achieve all this by identifying the DNF patterns that yield suitable axioms. The relevant patterns turn out to be what we call prime orbits of normal forms, which are like building blocks for the systems axioms.

Modal Contexts and their Systems
Notations. The notations to use in this paper have been a significant challenge and are thus the result of an extensive consideration. The problem is that in our case the traditional notations often result in very long formulas. Since our paper consists mainly of algebraic calculations with normal forms, which are essentially sums of products, we opted for a shorter representation, in the style of Boolean algebra. For example we write pq+!rs instead of (p ∧ q) ∨ (∼ r ∧ s). So we kindly ask the reader to bear with us in terms of the notations introduced further on, because we believe that in the end it is worth it, for the sake of compactness and readability of the proofs.
For formulas we use the Greek letters ϕ, ψ . . . as well as specific notations detailed further on. Propositional variables are {p, q, r . . .} or {p i } and the logical constants are 0 and 1 (note the italics). The operators are listed in the table below, in descending order of precedence: , ♦ and ! necessity, possibility and negation • uniform substitution (US) application (see further on) · conjunction, as well as US composition (but the symbol is typically omitted) + disjunction → and ↔ logical implication and logical equivalence = and ≈ S identity and equivalence (equiprovability) in S of formulas; S omitted when K Whenever necessary, parentheses are used for disambiguation. Examples of well-formed formulas (wff) are p!q + qr → !qr and ( p ↔ ♦p) → ♦ p.
The modal degree of a formula is the largest number of nested modal operators found in any sub-formula of the given formula. We also refer to it as the level of the formula. In the above examples, the modal degrees (levels) are 0 and 2 respectively.
Modal contexts. We denote systems by boldface and axioms by Roman letters. F is reserved for the inconsistent system (consisting of all formulas).
Let F(v, d) be the set of all unimodal wff in a number of variables not exceeding v and of modal degree not exceeding d. Consider a modal logic system B as a basis for the discussion. In this paper B is typically K, the weakest normal modal logic. We define a modal context B [v, d] as the quotient F(v, d)/ ≈ B , the Lindenbaum-Tarski algebra of classes of formulas equiprovable in B. But we tacitly equate a class with a representative from it, so that we can still refer to these classes as formulas. This is similar to writing 1+1=0 instead of1 +1 =2 =0 in Z 2 , which is often done and has the advantage of avoiding hats over large formulas.
The reason for this countable-contextualization of formulas is as follows. Let S be the system that extends K by a finite set of axioms {α i }. Then there is an equivalent axiomatization for S using a single axiom α = α i , with α ∈ K [v, d], where v and d are the largest among all α i . But as we shall see, K[v, d] is a finite set of (classes of equiprovable) formulas. So for (Q) we ask what are all α ∈ K[v, d] that yield distinct extensions of K. It turns out that for non-iterative contexts this question can be answered, and we shall provide a constructive way to determine all the corresponding systems, axioms and semantics.
Boolean contexts. A level 0 context K[v, 0] consists of non-modal formulas with up to v variables. These can also be written in the well-known, equivalent disjunctive normal form (DNF). For DNF, the factors (conjuncts) in every term (disjunct) must consist of all v variables, where each variable is either complemented or not. Such terms are usually referred to as full normal forms, but we call them minterms, as by "normal form" we typically mean the DNF representation of formulas in general. Note , since prior to (re)normalization in K[v , 0] any missing variable p i can be reintroduced in the formula by conjunction with (p i + !p i ).
The following example shows a K[v, 0] formula ϕ and its DNF equivalent: The above DNF formula can be displayed in matrix form as follows: We call this the minterms-matrix (short minmatrix ) representation of the formula. The labels on the left denote the DNF factors, which in this case are all the propositional variables. There is one column per minterm and the minmatrix entries represent the state of the row's factor in the corresponding minterm: 0 if the factor is complemented, otherwise 1.
Barring the reordering of rows and columns the minmatrix representation of a formula is unique. However, we prefer to use a standard order for rows and columns, with the variables ordered alphabetically or by some index and the minterms left-to-right in descending order of their state-tuples, as shown in the example above.
For v propositional variables p 0 , . . . , p v−1 there are n = 2 v Boolean minterms denoted as m 0 , . . . m n−1 . Then K[v, 0] is the set of 2 n distinct formulas (including 0 and 1 ) obtained by adding the minterms from any subset of {m i }. A formula is called positive if its DNF includes m n−1 ; otherwise it is called a negative formula. (The reason is that any positive formula has a non-DNF equivalent formula that does not use the negation operator or the constant 0 ; but we do not need to detail this property here.) A notation that we shall use further on is E v (k) for the set of K[v, 0] formulas whose DNF contains precisely k minterms. Also, E + v (k) and E − v (k) denote the subsets of positive and negative formulas from Modal disjunctive normal form. In [2], the DNF for K [v, d] formulas with d ≥ 1 is defined recursively. The corresponding minmatrices include: • Non-modal factors consisting of all the v propositional variables p i (the same as in non-modal minmatrices).
• Modal factors of the form ♦µ i , where µ i is every DNF minterm from the For example, in K [1,1] the factors are p, ♦p and ♦!p. In K [2,1] the factors are p, q, ♦(pq), ♦(p!q), ♦(!pq) and ♦(!p!q), etc. The following is an example minmatrix from K [2,1]: 1 1 0 1 1 1 1 1 1 1 0 The horizontal line that separates the modal and non-modal factors is optional, for convenience only. The dashed vertical lines are also optional, separating minmatrix sections, which are subsets of minterms whose nonmodal factors have the same states. The product of non-modal factors in their respective states is called the (non-modal) prefix of the minterm. The minmatrix section corresponding to minterms with prefix m n−1 = n−1 i=0 p i is called its positive section. Observe that a standard order also applies to the modal factors, which we denote by ν i , 0 ≤ i < n; namely ν i = ♦µ i .
We wish to point out that the above "matrix" is only a schematic representation of a normalized formula. This is useful to quickly show what is relevant for its DNF, namely the states of the minterm factors. But this representation can be equivalently replaced at any time by the full algebraic formula. Other than that, a minmatrix is, in fact, a normalized formula.
Our notation for the minmatrix of a formula ϕ is [ϕ], or d v [ϕ] to emphasize the context. This is still the same formula in DNF, therefore ϕ ≈ [ϕ]. The formula 0 is represented by the empty minmatrix [ ] = [0 ] and the formula d v [ i µ i ] containing all the minterms from the context by [1 ] (notation not to be confused with the reference [1]).
Per our convention to freely refer to K[v, d] classes as formulas, K[v, d] is the (obviously finite) set of all minmatrices from the context. Then the Boolean operations on formulas can be performed as set operations on the corresponding minmatrix minterms: union for disjunction, intersection for conjunction, complementation (with respect to [1 ]) for negation, etc.
For this reason we may also interpret [ϕ] as a set (rather than a sum) of minterms. This notation overloading allows us to avoid the constant use of back-and-forth conversion operators between DCF formulas and their sets of minterms, while all can still be disambiguated from the surrounding text (as in, for example, f : [1 ] → [1 ]). And this also allows us to be brief by writing "minmatrix intersection" instead of "the minmatrix that is the sum of the minterms from the intersection of the sets of minterms from ..." With this notation we can also write, for example, (1) Let S ∈ NExtK. The characteristic minmatrix (CMM) of S for a context , is defined as the conjunction (i.e. intersection of the minmatrices) of all the S-theorems from the context. This definition is sound, since under equivalence there is only a finite number of S-theorems per context. Note that the minmatrices used in the intersection must belong to the context, but the formal proof of the corresponding S-theorems may involve formulas from other contexts (and in fact this is often necessary).
The definition of a CMM combined with (1) . When this is the case, one can construct a formal proof for ϕ from [[S]] using mainly the rule of substitution of equivalents (EQ), defined for example in [3], as well as the propositional calculus (PC) monotony rule: from p infer p + q. In this sense the CMM is the "strongest" theorem that a system can prove within a context. As an example, below are the axiom of the well-known normal system T and its axiom T, where in K [1,1]

we have [[T]] = [[T]] yet [[T]] [T]
: It turns out, as we shall prove further on, that for non-iterative contexts b) is also an equality. But when d > 1 the inclusion can actually be strict. See an example in Section 3 of [5] [1,2].
As defined, a K[v, d] system is finitely-axiomatizable, and it is also the weakest extension of K that has that CMM in the given context. Obviously, every finitely-axiomatizable system is a K[v, d]-system in some context, as well as in all successor contexts thereafter. A system that is not finitelyaxiomatizable is not a K[v, d]-system in any context, but it still has a CMM in every context.  First, in Ksys[[v, d]] the systems are "upside-down" with respect to NextK, since the partial order between CMMs is the reverse of the order that results from defining the systems as sets of theorems. Then the lattice operations from NextK, denoted as ⊕ and , are not the same as ∨ and ∧ from Ksys [[v, d]]. In this paper we do not need to work with sublattices of NextK, but the reader can verify that for S , S ∈ Ksys [[v, d]

Prime Orbits of Minterms
In this section we derive an initial necessary condition for a minmatrix to be the CMM of some system.
Uniform substitutions. In the following we shall assume that the working context K [v, d] can accommodate all the formulas involved. We write α i as a shorthand for (α 0 , . . . , α v−1 ), for example ϕ(p 0 , . . . , p v−1 ) = ϕ p i and (σ 0 p j , . . . , σ v−1 p j ) = σ i p j , even though not all these formulas may effectively reference all the propositional variables p i , 0 ≤ i < v. (But when they don't, if needed, we can always promote them to equiprovables that do reference all the v variables.) Let σ be the uniform substitution p i → σ i p j , where σ i are formulas, 0 ≤ i < v. The result, denoted as ϕ • σ, of applying the substitution σ to a formula ϕ = ϕ p i is the formula (ϕ • σ) p i obtained by consistently replacing every occurrence of every propositional variable p i in ϕ by the corresponding σ i p j . We write this as ϕ Formally, this operation is defined by the following rules, applied recursively to the sub-formulas ψ, θ, . . . that occur in ϕ: Then the following are immediate consequences: Also, using US-1 to US-10 above and the fact that ϕ ≈ ψ is defined as K ϕ ↔ ψ, one can easily prove the following additional properties: Our immediate interest is in level 0 substitutions, i.e. substitutions where all σ i are level 0 formulas. We also call them context-preserving substitutions, because by applying them to any formula neither the number of variables nor the modal degree increase. If v or d actually decrease for a sub-formula, it can always be promoted back to K[v, d].
There are 2 2 v formulas in K[v, 0], therefore 2 v·2 v context-preserving substitutions σ that can be applied to any ϕ ∈ K [v, d]. These substitutions are defined independently of the formulas ϕ and their modal degree. Denote by S(v, 0) the set of all level 0 substitutions σ in v variables. The composition σσ of substitutions σ = σ i p j ∈ S(v, 0) and σ = σ i p j ∈ S(v, 0) is defined as follows: The composition of level 0 substitutions is obviously well-defined (i.e. the result is context-preserving) and its associativity is straightforward to verify. With this operation S(v, 0) is a monoid, whose unit is the identical As we have seen, if [S] collapses under σ then it can not be a CMM, since this would imply [S] ⊆ [S ϕ]. Thus, a candidate CMM must first of all be immune to all the context-preserving substitutions. This is a necessary, although not sufficient condition for a minmatrix to be a CMM.
We therefore analyze which minmatrices are immune to level 0 substitutions. We begin by considering a subset of level 0 substitutions that we call prime substitutions. They are defined as the invertible elements of the monoid S(v, 0), hence they form a group that we denote by S p (v, 0).
It turns out that prime substitutions are precisely those level 0 substitutions ς that always transform a minterm into a single minterm. As such, they generate automorphisms of the lattice K[v, d]. The following theorems establish the result.

Theorem 3
For any given v , the group However, from lattice theory any automorphism of a finite Boolean lattice is determined by its values on the atoms of the lattice, and that these automorphisms correspond to the permutations of the atoms. In our case the atoms are the 2 v minterms of K[v, 0], which proves our claim.

Theorem 4
Let ς ∈ S p (v, 0). Then for every K[v, d] context: a) The function f ς : ) when minmatrices are viewed as sets, b) is a corollary of a). We prove a) by induction on the modal level d.
For d = 0 the result follows directly from Theorem 3. Assume a) holds up to some level d. Let µ = m π be a level d + 1 minterm, where: • m, the non-modal prefix of µ, is a level 0 minterm, hence so is m • ς. • π is a product of all the level d + 1 modal factors from the set {♦µ k } in their respective states, with µ k being all the level d minterms. But by the induction hypotheses, ς permutes the level d minterms, therefore Then π • ς is again a product of all the level d + 1 modal factors from {♦µ k } in correspondingly permuted states.
We apply property US-6 to conclude that µ , hence it is a bijection.
Theorem 4 implies that for every context K[v, d], S p (v, 0) determines a group action on the set d v [1 ] of minterms. We then define the (contextdependent) prime orbits of minterms as the orbits of this group action.
The order (or count) of a prime orbit is the number of its minterms. Applying all the prime substitutions to a minterm µ does not necessarily yield only distinct minterms. However, as we shall see shortly, this yields an equal number of minterms per level 0 prefix. Thus, in general, the prime orbits from a K[v, d] context do not all have the same order. But the order is always a multiple of 2 v , its smallest value being 2 v . (The largest possible value would be (2 v )!, but this is typically not reached for K.)

Theorem 5
If a minmatrix ϕ includes some, but not all, the minterms of a prime orbit ω, then it collapses under some prime substitution ς.

Corollary 6
Any CMM must consist only of complete prime orbits.
Obviously, Ω(K) = Ω( [1 ]) in all contexts. The reader may note that prime orbits from K [v, d] contexts are a special case of the prime orbits from E[v, d] contexts that we defined in [5] using canonical forms, and that results 3-6 are quite similar for both bases.
The results we have proved so far are general, as they apply to all K[v, d] contexts. In the next sections we shall focus on non-iterative contexts.

The K[[v, 1]] Lattices
We now determine all the CMMs from a level 1 context. To avoid collapses under prime substitutions, we already know that they must be sums of complete prime orbits. But we are able to impose stricter conditions by requiring that they do not collapse under non-prime substitutions either.
Note that there are other methods to collapse a candidate CMM, for example using theorems from other contexts. But our findings imply that for level 1 systems other methods yield nothing new, i.e. if a level 1 minmatrix does not collapse under any level 0 substitution then it is indeed a CMM.
Definitions Consider the formulas n−1 i=0 ϕ i and n−1 i=0 ϕ i . We will need to work with variations of them, specifically some in which a fixed number of the ϕ i are complemented, or are absent.
For any subformula ϕ i that may occur in a certain state (complemented or not) in a sum or product, we define a pseudo-coefficient ε i to reflect its state: ε i = 1 for ϕ i and ε i = 0 for !ϕ i . Then we can write sums and products of mixed complementation uniformly as n−1 i=0 ε i ϕ i or n−1 i=0 ε i ϕ i . When we need several ε-tuples in nested sums or products we write ε i = ε i,j or ε i,j = ε i,j,k , with indices in the nesting order.
Let K[v, 1] be a non-iterative context and n = 2 v . We assume v ≥ 1, as the degenerate context K[0, 1] can be analyzed separately. Recall that for the given context: • n is the number of level 0 (Boolean) minterms m i , 0 ≤ i < n, • n is also the number of sections s in a minmatrix, 0 ≤ s < n, • n is also the number of level 1 modal DNF factors ν i = ♦m i , 0 ≤ i < n.
With the above notations, an arbitrary minterm µ j ∈ K[v, 1] is: where m s is the Boolean prefix of µ, s is the minmatrix section containing µ, ν i is the i-th modal factor from K[v, 1], namely ν i = ♦m i , and ε j = ε j,i is a suitable tuple of pseudo-coefficients.
Determining K [[v, 1]] The next lemma shows that the minterms of a prime orbit follow a certain pattern: in every minterm from a given section s: • the modal factor ν s has the same state (0 or 1), and • of the other modal factors, precisely k (0 ≤ k ≤ n − 1) have state 1.
Note that this also implies that prime orbits have an equal number n−1 k of minterms per section, where k depends on the prime orbit.

Proof.
Since prime orbits are group orbits, by applying all ς ∈ S p (v, 0) to µ we must get all the minterms from ω. Fix ς ∈ S p (v, 0). By Theorem 4, ς permutes the atoms of the lattice K[v, 0], which are all the m i , therefore: where s is the new section of the transformed minterm and ε i are all the ε i permuted, hence χ(ε ) = χ(ε). Furthermore, since this permutation maps m s to m s we have ν s • ς ≈ ♦(m s • ς) ≈ ♦m s ≈ ν s and so ε s = ε s .
Next, by Theorem 3, prime substitutions correspond to all permutations of the atoms of the lattice K [v, 0]. Then conversely, if µ is any minterm for which χ(ε ) = χ(ε) and ε s = ε s , we can choose a ς ∈ S p (v, 0) that corresponds to a permutation mapping m s to m s and any m j = m s for which ε j = 0 in µ to an m i = m s for which ε i = 0 in µ. This is possible since χ(ε ) = χ(ε), and then similar calculations yield µ • ς ≈ µ, hence all the minterms µ satisfying the stated conditions belong to ω.
With the above property we can now determine all the prime orbits from K [v, 1]. This will help us to find all the CMMs in the following way: Suppose any ϕ ∈ K[v, 1] could be a CMM. Then, since there are 2 v+n minterms in the context, we would need to check 2 2 v+n candidate CMMs to see whether or not they collapse. And most of them will indeed collapse. But from Corollary 6, any CMM is a sum of (complete) prime orbits. As we now show there are only 2n prime orbits in K[v, 1], we will have only 2 2n candidate CMMs to check.

Proof.
This is a consequence of the restrictions imposed on the prime orbits by Lemma 7. For simplicity, we can look only at the minterms from a single section s. Minterms from the other sections then follow suit, and for each prime orbit we add the minterms from all sections, 0 to n − 1.
Write a section s minterm as µ j = m s n−1 i=0 ε j,i ν i . The choices for χ(ε j ) are 0, 1, . . . , n. But the state of modal factor ν s must be the same across all section s minterms. When χ(ε j ) = 0 (all ν i complemented) we obtain Vv 0 . When χ(ε j ) = 1 we can have either ε j,s = 1, which yields Dd 0 , or ε j,s = 0, in which case χ(ε j ) = 1 over the other ε j,i and the matching minterms yield Dc 1 . Similar reasoning shows that when χ(ε j ) = k, with 2 ≤ k ≤ n − 1, the resulting prime orbits are either Dw k−1 (if ε j,s = 1) or Dc k (if ε j,s = 0). Finally, when χ(ε j ) = n we can only obtain Dw n−1 . Since these choices exhaust all possibilities for µ j , there are no other K[v, 1] prime orbits.
The reader may note that Vv 0 and Dd 0 are quite similar to Dc k and Dw k and we could have labeled them Dc 0 and Dw 0 , for k = χ(ε s,j ) = 0. However, Vv 0 and Dd 0 are special, since they are associated with systems Ver and Triv respectively, so we prefer to distinguish them in this way.
As per Corollary 6, a minmatrix that includes only complete prime orbits is immune to prime substitutions. Yet it may still collapse under non-prime substitutions. In the worst case it may collapse to [[F] We now show that, starting from minmatrix [0 ], in order to construct (non-collapsing) level 1 CMMs, prime orbits must be added in a particular order, determined by certain dependencies between prime orbits.
To state these dependencies we introduce the concept of prime orbit coverage under a (typically non-prime) substitution σ. To begin with, where and since all ω i are pairwise disjoint, by US-6 and US-12 all ω i • σ are also pairwise disjoint. Comparing each ω i • σ with the corresponding ω i we observe that under σ some of these minmatrices lose (potentially all) their minterms, while others gain minterms, yet overall we still find all the minterms from the context redistributed among several ω i • σ. Any minterm µ ∈ ω i • σ is said to be covered by ω i under σ. Whenever (ω i • σ) ∩ ω j = ∅ and (ω i • σ) ∩ ω j ω j we say that ω i partially covers ω j under σ. And when ω j ⊆ (ω i • σ) we say that ω i fully covers ω j under σ. Note that self-coverage (when i = j) is included here.

Claim 9
For level 1 prime orbits, if ω i covers ω j (partially or fully), then a CMM can include ω j only if it also includes ω i .

Proof.
Since all ω j • σ are pairwise disjoint, for any minterm µ ∈ ω j not covered by ω j under σ there must be precisely one other ω i that covers µ under that σ. So if a candidate CMM ξ includes ω j but not ω i , then ξ • σ includes at best the incomplete prime orbit ω j , i.e. ξ collapses under σ to a minmatrix that does not include ω j , therefore it cannot be a CMM.
Using this argument, we can infer some necessary dependencies between prime orbits in our CMMs. The calculations below may seem a little complex, but in fact they are just basic Boolean algebra with DNF formulas, where we need to keep track of the prime orbits minterms based on their definition from Theorem 8. (DR3): ξ includes Dc k , 1 ≤ k < n, only if it includes Dd 0 as well as all Dw l , 1 ≤ l < k, and all Dc l , 1 ≤ l < k.

Proof.
Let σ be the non-prime substitution where p 0 → p 0 !m n−1 !m n−2 and p 1 , p 2 , . . . , p v−1 are unchanged. This is the same as p 0 → p 0 n−3 i=0 m i , or p 0 → 0 if v = 1 and the context has only n = 2 v = 2 minterms. Then: and for the other m j (if any, i.e if v > 1) we have m j • σ ≈ m j . Indeed, when j is even, j + 1 < n − 2 and the state of p 0 in m j is 0, therefore: and when j is odd, j < n − 2 and the state of p 0 in m j is 1, therefore: On level 1, for all µ in section s = n − 1, µ • σ ≈ 0 ; and for s < n − 1: (Note that when n = 2 v = 2, the last product is 1 ; otherwise n ≥ 4.) For Vv 0 , there is one minterm per section, and if µ is in section n − 2: which covers µ and the vanished section n − 1 minterm µ v . Minterms from remaining sections, if any, are unchanged by σ, as for s < n − 2 we have: so overall Vv 0 covers only itself, fully. Thus Vv 0 does not depend on other prime orbits and it may be added to any CMM without causing a collapse.
For Dd 0 , also with one minterm per section, and for µ in section n − 2: Here, prefix m n−1 covers the vanished Dd 0 minterm from section n − 1 and also a Dw 1 and a Dc 1 minterm, while prefix m n−2 covers µ and more. Dd 0 minterms from remaining sections, if any, are unchanged by σ, so overall Dd 0 covers itself fully and covers Dw 1 and Dc 1 partially. Thus, Dd 0 does not depend on any other prime orbit, but both Dw 1 and Dc 1 depend on Dd 0 .
For Dw k , we just saw that Dw 1 depends on Dd 0 . If n = 2 there is no other Dw k . Otherwise we pick a Dw k minterm µ from section n − 2 with ε n−1 = 0 and χ(ε) = k (excluding ε n−2 = 1), 1 ≤ k ≤ n − 2. Then: Here, because of ♦m n−1 instead of !♦m n−1 , prefix m n−2 adds 1 to χ(ε) and it includes both states for ♦m n−2 , so it covers Dw k+1 as well as Dc k+1 minterms. Therefore Dw k+1 and Dc k+1 depend on Dw k , thus transitively on all previous Dw i , 1 ≤ i ≤ k, as well as on Dd 0 .
For Dc k we saw that Dc 1 depends on both Dd 0 and Dw 1 . If n = 2 there is no other Dc k . Otherwise we pick a Dc k minterm µ from section n − 3 with ε n−1 = 0, ε n−2 = 1, ε n−3 = 0 and χ(ε) = k (overall), 1 ≤ k ≤ n − 2. Then: Here, because of ♦m n−1 ♦m n−2 instead of !♦m n−1 ♦m n−2 , prefix m n−3 adds 1 to χ(ε), so it covers a Dc k+1 minterm plus more. Therefore Dc k+1 , which already depends on all Dw i , 1 ≤ i ≤ k and on Dd 0 , also depends on Dc k , thus transitively on all previous Dc i , 1 ≤ i ≤ k.
Finally, by aggregating all the dependencies that we found above, we get precisely the rules stated by this theorem.
The choice for σ in the above proof is due to a result that we don't actually need to prove here. In fact, every non-prime substitution reveals a set of dependencies between prime orbits. But many substitutions yield the same set of dependencies, so we can partition all of them into equivalence classes. One particular class of critical substitutions happens to determine the strongest set of dependencies between prime orbits. The σ from Theorem 10 is just a simple and convenient substitution from this class.
From rules DR1-DR3 we build a candidate lattice K[[v, 1]], which is as shown in Figure 1. In the diagram the CMMs are represented by dots. Prime orbits are marked along the edges such that one can determine what sets are included in any particular CMM. A simple calculation shows that the total number of CMMs from K[ [v, 1]] is n(n + 3).  1]], since any other minmatrix from the context collapses under a critical substitution. Yet in principle, any of these candidate CMMs may still collapse by other methods. But note that adjacent K [[v, 1]] CMMs are a single prime orbit apart. So if we can show that they all correspond to distinct systems, then they are indeed all CMMs, as there are no other suitable minmatrices to collapse to. This would also imply that level 0 prime substitutions plus a single critical substitution suffice to determine the CMM of a level 1 system.
We observe that a number of K [[v, 1]] CMMs include prime orbit Vv 0 and an equal number do not. These are referred to as K-plane and D-plane CMMs respectively and the corresponding Ksys [[v, 1]] systems as K-plane and D-plane systems respectively. The diagram does not provide names for them, except in a few cases where we anticipate the position of some wellknown systems. But due to the regularity of this lattice we can denote the CMMs by the x and y coordinates defined as illustrated. Figure 2 shows the lattices for the first two contexts. Note that we chose generic names for the K[v, 1] prime orbits, but in fact they are contextdependent; so in principle they must be renamed in each particular context.

The Candidate Lattice Ksys[[ * , 1]]
Having all the K[ [v, 1]] lattices, we note that it doesn't make sense to assemble them into a single lattice, since a system has different CMMs in different contexts. However, it does make sense to assemble all the corresponding (as per Claim 2) lattices Ksys [[v, 1]] into a single one.
We denote the assembled lattice by Ksys [[ * , 1]]. For now, it is a candidate lattice, as we still need to prove that all the systems in it are distinct. And we recall from Section 2 that this is not meant to be a sublattice of NextK. It is just our way to present all the finitely-axiomatizable, non-iterative systems.
We  1]]. This will become clear when we determine the semantics for these systems, i.e. their characterizing classes of Kripke frames.  1]] lattice is embedded in it, therefore we can add up the prime orbits to get an axiom for each system. Also note how for every successor context, new systems will appear in the shaded area only. From Section 4, we know that all non-iterative system must be in this lattice, as the minmatrix of any other axiom would collapse in some context. Next, by showing that every (x, y) position from Ksys[[ * , 1]] is associated with a distinct semantics will prove that the corresponding systems are also distinct, i.e. that Ksys[[ * , 1]] contains all the systems we are looking for. Instead, however, we shall build some equivalent, more suitable axioms. These are constructed using the following trick: Consider any system S with axiom [[S]] ≈ ω j ∈Ω(S) ω j . If we add any minterms to this minmatrix, then, as long as we do not end up with new, complete prime orbits, these extra minterms will be "trimmed" by prime substitutions. Hence, if we define:

Construction of Ksys
ω j then section n − 1 (the positive section) of this minmatrix includes all the minterms from the selected prime orbits, and only those minterms, while the remaining sections include all the minterms. Consequently, α S will collapse to [[S]] under prime substitutions, so it is an equivalent axiom for S. Using this trick and Theorem 10, we construct a similar minmatrix α ω for each prime orbit ω, where the positive section of α ω includes only the minterms from ω, while the other sections include all their minterms. Then with our notation for a generic minterm µ j = m s n−1 i=0 ε j,i ν i , we get: µ j and for 1 ≤ k < n: where all the µ j above belong to section n − 1.
(Note that in α Dw k , χ(µ j ) = k + 1 because it now includes ε j,n−1 = 1.) Proceeding to S K (x, y), we add according to its CMM from Figure 1, to obtain the following axiom: α Dw k and this minmatrix, as per the trick above, collapses to [[S K (x, y)]]. Then, after replacing the α ω of the level 1 prime orbits ω, we combine the resulting formulas using the simple Boolean equivalence: and we immediately obtain: where again, all the µ j are from section n − 1. This is the formula that we shall use in the next section to determine the semantics of S K (x, y). As a caveat, when y = n − 1 we call this α S K (x, * ) , unless x = y = n − 1 when it is called α S K ( * , * ) .
Finally, for S D (x, y) we can immediately write the axiom: since ♦1 ≈ !Vv 0 and conjunction with it eliminates precisely the prime orbit Vv 0 . Then this conjunction, together with trimming the minmatrix to complete prime orbits, turns Additional axioms After further calculations, it is possible to show that: also works as an axiom for S K (x, y). Although we do not need to use this last formula in our paper, we mentioned it here because it is a nice axiom with only positive subformulas. The sums e i can often be optimized, for example they may reduce to sums that include only a subset of the e i generated by cyclic permutations of their p j .

Semantics for Ksys[[ * , 1]] systems
In the following we assume that the reader is familiar with Kripke frames and the semantics of normal modal logics. Let F = (W, R) be a Kripke frame and w, w ∈ W . If wR w we say that w sees w . Let "self" be the condition that a world w is reflexive, i.e. it sees itself. Let "others" denote the number of w = w seen by w, with "others ≤ * " meaning w sees any number of w = w. We define the following frame conditions on any w (and since these are not modal logic formulas, we use the classical notations):

Theorem 11
For the Ksys[[ * , 1]] systems defined in Section 5: a) The class of frames F for which F K (x, y) holds at every world w ∈ W corresponds to S K (x, y). b) The class of frames F for which F D (x, y) holds at every world w ∈ W corresponds to S D (x, y).
1} be a valuation on F , the other notations being as before. To understand the significance of F K (x, y) and F D (x, y), the following observations are critical: • At any w, the values V (w, p k ), 0 ≤ k < v, determine a unique level 0 minterm m i , 0 ≤ i < n, with V (w, m i ) = 1. But all other level 0 mintems m are disjoint with m i , so V (w, m ) = 0. Conversely, when V (w, m i ) = 1 for some m i , this uniquely determines all V (w, p k ). Overall, choosing V at w is the same as choosing an m i for which V (w, m i ) = 1, so we can say that this m i represents the valuation at w.
• If w sees up to z other w i , 0 ≤ i < z ≤ n, then there are up to z such w i where valuations are pairwise distinct, i.e. where V (w i , m i ) = 1 for all m i distinct. Consequently, V (w, ν i ) = 1 for up to z modal factors ν i . In this case, to have V (w, µ j ) = 1 for a minterm µ j , we need χ(µ j ) ≤ z.
Step 2: Proof of a). Let F be an arbitrary frame. It is well known (see for example [3]) that what we need to show here is the following: the axiom α S K (x,y) is valid on F iff F K (x, y) holds at all worlds of F . Let us rewrite: where β and γ are the corresponding sums of minterms from section n − 1.
Sufficiency: Assume F K (x, y) holds for F . Fixing an arbitrary valuation function V on F , we show that α S K (x,y) is valid in the model (W, R, V ).
If V (w, m n−1 ) = 0 then α S K (x,y) is immediately valid at w. Thus, we can assume that V (w, m n−1 ) = 1, and it will be enough to find V (w, µ j ) = 1 for a single minterm µ j from either β or γ. Such a minterm always has the right prefix m n−1 , so it all depends on the states of its modal factors.
If W K (y) holds, V (w, ν i ) = 1 for at most y + 1 modal factors ν i in total, one of them certainly being ν n−1 (because w is reflexive), plus up to y others. Then V (w, µ j ) = 1 for a suitable minterm from γ, where all χ(µ j ) ≤ y + 1.
If C K (x) holds, the argument is the same as above. If W K (y) = W K ( * ) holds, then V (w, ν n−1 ) = 1 (because w is reflexive), and γ minterms now have up to the maximum n = y + 1 modal factors ν i in state 1, so regardless of how many distinct valuations w actually sees, one can always find a suitable minterm in γ for which V (w, µ j ) = 1.
Necessity: Assume F K (x, y) does not hold for F , i.e. assume that there is a world w ∈ W for whichF K (x, y) ¬F K (x, y) holds, where: For such a frame we choose V (w, m n−1 ) = 1 to make the antecedent in α S K (x,y) true, and we show that, in all cases, we can find suitable valuations at the other worlds such that the consequent in α S K (x,y) is false.
IfC K (x) holds, w sees at least x + 1 other w i . For 0 ≤ i ≤ x we choose V (w i , m i ) = 1 (all distinct) and for i > x, V (w i , m 0 ) = 1 (no new valuation). Since x < n−1, V (w, ν n−1 ) = 0, so V (w, µ j ) could be 1 only for a β minterm with χ(µ j ) = x + 1, which is not the case, since our β has only χ(µ j ) ≤ x.
IfW K (y) holds, w sees itself and at least y+1 other w i . But y+1 ≤ n−1, so w always sees at least y+2 total w i . For 0 ≤ i ≤ y we choose V (w i , m i ) = 1 (y + 1 distinct valuations) and for i > y, V (w i , m n−1 ) = 1 (valuation y + 2). Then V (w, µ j ) could be 1 only for a γ minterm with χ(µ j ) = y + 2, which again is not the case, since our γ has only χ(µ j ) ≤ y + 1.
Necessity case 2: When x = n − 1 or y = n − 1 (but not both). For x = n − 1,C K (x) =C K ( * ) is false. For y = n − 1,W K (x) =W K ( * ) is false. Either way, if the other condition holds, the argument is as above.
This completes the proof of a).
Step 3: Proof of b). For the D-plane systems, α S D (x,y) = D α S K (x,y) , where axiom D ♦1 eliminates prime orbit Vv 0 from any minmatrix. But Vv 0 minterms are precisely those that make a formula valid at blind worlds. Thus, conjunction with D makes the subtle difference between C K (y) and C D (y) that precludes frames with blind worlds, and Theorem 11 holds for D-plane systems too.
Recall that n = 2 v . Consider v-bit binary registers, which can only hold unsigned numbers from 0 to 2 v − 1; larger numbers cause a condition called overflow, in which the register represents an unknown number. In this sense, worlds of Ksys [[v, 1]] frames can be said to be able to "count" up to 2 v − 1 worlds total, themselves included; beyond that, it is "any number" for them. Together with the fact that they can only count the worlds that they see directly, this could be interpreted as the descriptive limitation of the semantics of non-iterative modal logics.
We end with a result on non-finitely-axiomatizable systems that proves that we have found all non-iterative normal logics.

Corollary 12
Let S be a non-finitely-axiomatizable unimodal normal modal logic system. Then S cannot be axiomatized by a (countable) set of non-iterative formulas.
Proof. Let S be defined by an infinite (but necessarily countable) set of axioms {α i }, all non-iterative. Every minmatrix α i is in some K[v, 1], so it equals or collapses to some CMM that has coordinates (x i , y i ) in ] for all v > v). By construction S proves α. But by CMM inclusion α proves any α i , making all the latter redundant. So S is really S and is finitely-axiomatizable.
In fact, we conjecture that, for any fixed positive integer d, if a system S is not finitely-axiomatizable, then it cannot have only axioms of modal degree ≤ d. Which is to claim that any non-finitely-axiomatizable system must have non-redundant axioms of arbitrarily large modal degree.

Appendix A
In this appendix we show the first few non-iterative modal contexts, lattices and systems. These concrete examples are intended to help the reader follow the generic calculations from the main sections of our paper. For the systems presented below, we have already shown a method to derive defining axioms. But axioms that are sums of minterms, or even α SK(x,y) or α SD(x,y) , produce formulas that are far from minimal. In this appendix we also show axiomatizations using a number of optimized formulas that are more practical for inferences.
We recall some facts established in [5]. Normal minterms are a special case of canonical minterms, namely those that satisfy the axioms of K: ♦(p + q) ↔ ♦p + ♦q and !♦0 . Thus, in a normal E[v, d] minterm, the states of all ν i = ♦µ i factors uniquely determine the state of any other ν j = ♦φ j , where µ i and φ i are the minterms and formulas from E[v, d − 1] respectively. In E, we assigned labels to minterms based on the state tuple (♦1 , ♦0 ), namely label V for (0,0), C for (0,1), D for (1,0) and W for (1,1). Prime orbits are invariant under prime substitutions, which also preserve labels. So prime orbits of E[v, d] contexts inherit labels from their minterms. It turns out that only some D-orbits and precisely one V-orbit have normal minterms, which explains our notations. And of course, prime orbits are context-dependent, so we have to rename them per context.
This is a limit context, because it misses the Dc and Dw prime orbits, yet it still fits the generic pattern, e.g. S D (0, 0) = S D ( * , * ).
Context K [1,1] Here, v = 1 and n = 2. This context has 3 DNF factors (1 Boolean plus 2 modal) and 8 minterms. There are 2 prime substitutions, namely p → p and p →!p, which generate 4 prime orbits as follows: The lattice Ksys[ [1,1]] is shown in Figure 5. The K[1, 1]-systems CMMs and possible axiomatizations are as follows: This is one of the few contexts where calculations can be done easily by hand. For example, one can check that other candidate CMMs (like [Dc + Dw]) collapse, using the non-prime substitution p → 0 .
Starting with this context, calculations by hand become quite tedious, so we developed a software workbench to assist. This is straightforward since, after parsing formulas and converting them to minmatrices, calculations become plain Boolean operations with bitsets.
The prime substitutions generate 8 prime orbits, namely: Vvv, Ddd, Dcc1, Dcc2, Dcc3, Dww1, Dww2, Dww3 It is worth noting that promoting K [1,1] prime orbits does not result in K [2,1] prime orbits. Indeed the 4 promoted prime orbits from K [1,1] are disjoint minmatrices and they still need to cover all K [2,1]  − Pick any unassigned minterm, assign to a new prime orbit. − Perform all prime substitutions, assign the results to the same orbit. − Repeat as long as there are minterms unassigned to orbits.
In the K [2,1] prime orbits shown below, one can relate the highlighted bit patterns of the minterms to the rules from Lemma 7 and Theorem 8: Ksys[ [2,1]] has 28 systems total: the 10 from Ksys[ [1,1]] plus 18 new ones. Here, one can already see how the systems from predecessor contexts (larger dots) will preserve their position in the aggregate Ksys [[ * , 1]]. The proposed axioms for K [2,1]-systems were found using our software workbench. Although not necessarily minimal/optimal formulas, they are often shorter than α SK(x,y) and α SD(x,y) . Note that, except for Ver and F, the remaining systems can be axiomatized using positive formulas.
The exact patterns that determine which substitutions are in which class are for further study. Nevertheless, SC 00 (3, 0) and SC 21 (3, 0) are the most important classes. The labeling of the others is not very relevant, because (see Section 4) they determine prime orbit dependencies that are weaker than those revealed by the critical substitutions.
The prime substitutions determine 16 prime orbits, which conform to the patterns from Lemma 7 and Theorem 8, namely: Vvvv and Dddd have 8 minterms each, and Dccc i and Dwww i have 8 n−1 i minterms each, 1 ≤ i ≤ 7.
The lattice Ksys[ [3,1]] is shown in Figure 7. It has 88 systems total: the 28 from Ksys[ [2,1]] plus 60 new ones. Larger dots are systems from predecessor contexts. Note that, as for the other contexts, we present the Hasse diagram by CMM rank (i.e. number of prime orbits) rather than by CMM count (i.e. number of minterms). The K [3,1]-systems are similar to those in the predecessors contexts. We present them here for completness, but only the new K-plane systems. For the corresponding D-plane system one just needs to add axiom D.
(Note: This is in fact an E[2, 1]-system that we called R cw in [5], as it only sinks into another, "genuine" system R that we defined as an E[0, 1]-system. But here we continue to refer to this system R by its popular name.) We call R pre-normal because it is similar to K except that it lacks the normality axiom N = 1 . But axiom R still allows us to use the previouslydefined ν j = ♦µ j , 0 ≤ j < n to determine the state of all other ♦e i , except for the modal factor ν ∅ = ♦0 , which can be in any state, so we need to add it to every R-minmatrix. Thus, in R[1, 1] for example: and we observe that, in addition to the normal minterms, some pre-normal minterms show up, where the state of ♦0 is 1. Then, by axiom R, these pre-normal minterms must have all modal factors in state 1, so they end up in the same prime orbit, which we label Ww 0 .
We note that R is not a perfect base, since 1 1 [[R]] does not have the full 2 4 = 16 minterms. Nevertheless, the theory from this paper holds with only minor adjustments. Then it turns out that prime orbit Ww 0 is similar to Vv 0 , in the sense that it covers only itself under substitutions and therefore can be added to any S D (x, y) and S K (x, y) CMM without collapsing it. So Rsys [[ * , 1]] is similar to Ksys[[ * , 1]], but adds a J-plane and an R-plane: