Simultaneously vanishing higher derived limits
Jeffrey Bergfalk Chris Lambie-Hanson
math.LO math.AT 03E05, 03E75, 55N07, 55N40, 18E25, 03E55


  In 1988, Sibe Mardešić and Andrei Prasolov isolated an inverse system 𝐀
  with the property that the additivity of strong
  homology on any class of spaces which includes the closed subsets of
  Euclidean space would entail that lim^n𝐀 (the n^th derived limit of 𝐀) vanishes for every n >0. Since that time, the question of whether it is consistent with the 𝖹𝖥𝖢 axioms that lim^n 𝐀=0 for every n >0 has remained open. It remains possible as well that this condition in fact implies that strong homology is additive on the category of metric spaces.

   We show that, assuming the existence of a weakly compact cardinal, it is indeed consistent with the 𝖹𝖥𝖢 axioms that lim^n 𝐀=0 for all n >0. We show this via a finite support iteration of Hechler forcings which is of weakly compact length. More precisely, we show that in any forcing extension by this iteration a condition equivalent to lim^n𝐀=0 will hold for each n>0. This condition is of interest in its own right; namely, it is the triviality of every coherent n-dimensional family of certain specified sorts of partial functions ℕ^2→ℤ which are indexed in turn by n-tuples of functions f:ℕ→ℕ. The triviality and coherence in question here generalize the classical and well-studied case of n=1.



[2010]03E05, 03E75, 03E55, 55N07, 55N40, 18E25




𝒫,𝒯-odd Faraday rotation on atoms and molecules in intra-cavity absorption spectroscopy as an alternative way to search for the 𝒫,𝒯-odd effects in nature
    D. V. Chubukov^1,2, L. V. Skripnikov^1,2, L. Bougas^3, and L. N. Labzowsky^1,2
    
=========================================================================================================================================================





§ INTRODUCTION


A main and organizing theme in the study of infinitary combinatorics is the phenomenon of incompactness; broadly speaking, the term denotes settings in which the local and global behaviors of a structure sharply diverge. Nontrivial coherent families of functions on a variety of index-sets form one prominent class of  examples. These connect in turn to local-to-global questions in homology theory, wherein the nontrivial coherence relations of such set-theoretic interest figure as only the first in an infinite family of incompactness principles given by the derived functors lim^n of the inverse limit of various inverse systems. For one particular inverse system, denoted 𝐀 below, the question of whether these associated incompactness principles can simultaneously fail had been longstanding; the main result of this paper is that under the assumption of the existence of a weakly compact cardinal, they can. This result carries implications for the strong homology of metric spaces and, as we note below, possibly for other areas of mathematics as well.

We begin by reviewing the historical background to this result; it traces to Sibe Mardešić and Andrei Prasolov's 1988 paper “Strong homology is not additive" <cit.>. Their title references the following potential continuity property of a homology theory:
 A homology theory is additive on the class 𝒞 of topological spaces if for every natural number p and every family {X_α | α∈ A} with each X_α and ∐_A X_α in 𝒞, the map
 
    i_p:⊕_A H_p(X_α)→H_p(∐_A X_α)

 induced by the inclusion maps ι_α:X_α↪∐_A X_α is an isomorphism.
 

In <cit.>, Mardešić and Prasolov isolated an inverse system 𝐀 with the property that the additivity of strong homology on any class of topological spaces which includes the closed subsets of Euclidean space would entail that lim^n𝐀=0 for all n>0. They succeeded also in casting the vanishing of lim^1𝐀 in the following combinatorial terms: lim^1𝐀=0 if and only if for every family of functions

    Φ=⟨φ_f:{(k,m)| m≤ f(k)}→ℤ| f∈ ^ωω⟩
 whose elements agree pairwise modulo finite sets there exists some ψ:ω×ω→ℤ agreeing mod finite with each function in Φ. More succinctly, in a parlance that has since grown standard, lim^1𝐀=0 if and only if every coherent Φ as above is trivial. By way of this characterization, Mardešić and Prasolov showed that the continuum hypothesis implies that lim^1𝐀≠ 0. It follows that it is consistent with the 𝖹𝖥𝖢 axioms that strong homology is not additive, not even on the class of closed subspaces of ℝ^2.

The following year, Alan Dow, Petr Simon, and Jerry Vaughan showed that the Proper Forcing Axiom implies that lim^1𝐀=0, underscoring the possibility that the additivity of strong homology may also be consistent with the 𝖹𝖥𝖢 axioms <cit.>. Soon thereafter, Stevo Todorcevic showed that the Open Coloring Axiom implies that lim^1𝐀=0, while Martin's Axiom does not <cit.>. Around 2000, Andrei Prasolov produced a nonmetrizable 𝖹𝖥𝖢 counterexample to the additivity of strong homology <cit.>, but the additivity question on any “nicer” class — Polish or locally compact metric spaces, for example, or even metric spaces outright — remained entirely open (and for the aforementioned classes remains so; see, however, Remark <ref> for recent progress on this question).[Prasolov's example was, in essence, a geometric “realization” of an (ω_1,ω_1^*)-Hausdorff gap.] In short, in this sequence, the vanishing of lim^n𝐀 became a topic of set-theoretic study in its own right <cit.>, one closely linked to the study of forcing axioms and one, furthermore, rekindling older lines of research into relations between homological dimension and the cardinals {ℵ_n | n ∈ω} <cit.>.
It was therefore natural that the consistency of the additivity of strong homology would close out the list of  open questions in Justin Moore's 2010 ICM survey on the Proper Forcing Axiom <cit.>. Moore further observed therein that “it is entirely possible that it is a theorem of 𝖹𝖥𝖢 that either [lim^1𝐀≠ 0] or [lim^2𝐀≠ 0].” The first set-theoretic computation of lim^2𝐀 appeared some six years later in <cit.>; here framings of lim^n𝐀 (n>1) in terms of higher-dimensional coherence were given and applied to show that the Proper Forcing Axiom implies that lim^2𝐀≠ 0.
Here also Goblot's work <cit.> was applied to show that 𝔡≤ℵ_m implies that lim^n 𝐀 = 0 for all n > m. Still, Moore's speculation remained unanswered.

Against this background, we may state our main result:

 Let κ∈ V be a weakly compact cardinal and let ℙ denote a length-κ finite-support iteration of Hechler forcings. Then 
    V^ℙ“ lim^n𝐀=0 for all n>0.”



In addition to answering well-studied set-theoretic questions, the theorem is of interest for specifying a 𝖹𝖥𝖢 model — namely, V^ℙ — in which strong homology may well turn out to be additive on some “nice” class of spaces properly containing the class of homotopy types of CW-complexes. Moreover, although we have followed tradition in foregrounding the additivity question above, the nonvanishing of lim^n𝐀 for some n>0 is also the only known obstacle to strong homology having compact supports on some such “nice” class; hence this property of strong homology conceivably holds in V^ℙ as well.

 
  We have largely retained the text of this article's original incarnation, but a
  couple of recent developments should be noted.

  First, work of the first author together with Nathaniel Bannister and Justin Tatch
  Moore <cit.> vindicated the speculations of the previous paragraph by
  showing that, in V^ℙ, strong homology is indeed additive and has compact supports on
  the class of locally compact separable metric spaces. For the property of having compact supports,
  this class of spaces is at least close to optimal, by the results of <cit.> and <cit.>,
  but the question of whether strong homology is consistently additive on some broader class of
  spaces remains open, as we discuss at greater length in our conclusion below.

  Second, work of the authors together with Michael Hrušák <cit.>, building on the
  techniques of this paper, shows that the assumption of a weakly compact
  cardinal is not necessary to obtain the conclusion of our main theorem. More
  precisely, lim^n𝐀 = 0 for all n > 0 after adding ℶ_ω-many
  Cohen reals to any model of 𝖹𝖥𝖢.

  For interested readers, the most immediate point is probably the following: <cit.> and <cit.> each couple multiple new ideas to techniques which first appear, and, consequently, receive their fullest and most direct treatment, in the present work. Given the complexity of these techniques, there will be benefits to reading this work before either of the others, though ultimately, of course, readers may and should order their approach to these three texts most fundamentally according to their interests.


These limits also bear on questions seemingly remote from strong homology: within the context of Dustin Clausen and Peter Scholze's recently-developed condensed mathematics <cit.>, 𝐀 is the most basic system in a family of inverse systems 𝐀_κ,λ upon whose limits' simultaneous vanishing the full and faithful embedding of the derived category of pro-abelian groups into the associated derived condensed category depends <cit.>. More generally speaking, the above theorem reflects new levels of insight into the set-theoretic content of derived functors, and as such takes its place in a line of research beginning with Shelah's solution to Whitehead problem <cit.>. It bears comparison, lastly, with Boban Velickovic and Alessandro Vignati's recent result in the opposite direction:
\beginTHM”[<cit.>]
For all integers n≥ 0 it is consistent with the 𝖹𝖥𝖢 axioms that lim^n𝐀≠ 0.
\endTHM”

As in so much of the above-described research history, our argument of a fundamentally algebraic result will be predominantly set-theoretic in nature. Our Main
Theorem, in particular, can and will be recast as a purely set-theoretic statement that we
feel is of interest in its own right. For this reason we have divided
Section <ref>, in which we fix our notational conventions and record the definitions
and background facts most relevant to our main result, into two subsections.
One is more set-theoretic and one is more cohomological in character. Section <ref> contains the set-theoretic
reformulation of our Main Theorem and must be read in order to understand the
arguments of subsequent sections. Section <ref> records some of the original context of the problems
addressed in this paper together with the argument that our set-theoretic reformulation
of the Main Theorem is in fact equivalent to its statement above. Readers less familiar with
homological algebra may safely skip most of Section <ref> without sacrificing
any understanding of the remainder of the paper (we indicate at the end of
Section <ref> exactly which part of Section <ref>
is necessary for the rest of the paper). Of course, such readers are invited to return to this subsection after reading that remainder, in order to better contextualize its contents.

The paper thereafter is structured as follows.
In Section <ref> we describe a multidimensional
Δ-system lemma lying at the core of our subsequent arguments. We then
turn to the proof of our Main Theorem. Due to the technical
complexity of the full proof of the theorem, we begin by
presenting two cases in which our argument's core ideas more transparently appear. In Section <ref>, after recording the
requisite facts about finite-support iterations of Hechler forcing, we prove the
n=1 case of our main theorem. We prove the n=2 case in Section <ref>.
The full proof of the Main Theorem is contained in Section <ref>.
We conclude with a brief discussion of the import of this result and with
the questions following most immediately in its wake.



We close this introduction with a more general word on notations and conventions. For any X and cardinal λ we write [X]^λ to denote the collection of subsets of X of cardinality λ and [X]^<λ for ⋃_κ<λ[X]^κ. In particular we view [X]^0 as {∅}. When X is a collection of ordinals, it is frequently convenient to regard elements u of [X]^<ω as finite increasing sequences, and vice versa. For such u and i <|u| we let u(i) denote the unique α∈ u such that |u ∩α| = i. The notation u⃗ will always stand for an ordered tuple of the form ⟨ u_0,…,u_k ⟩, though we will occasionally begin our indexing with 1. Also, if u, v, and w are finite sets of ordinals, then the statement w = u ^⌢ v indicates both that w = u ∪ v and that u < v, i.e.,
that every ordinal in u is less than every ordinal in v, and the
statement u ⊑ v indicates that u is an initial segment of
v. We use angled brackets to emphasize the indexed or ordered character of a set; in all of this, though, the surest guide will simply be context.

We follow <cit.> and <cit.> in our approach to forcing. We remark
though that we view conditions in a κ-length finite support iteration
as finite partial functions p with domains contained in κ rather than as
total functions p such that p(α) is a name for the trivial condition
for all but finitely many α < κ. The difference between these views, of course, is cosmetic.



§ MAIN DEFINITIONS AND CONVENTIONS




 §.§ Set theoretic background
 

Our primary objects of study are families of functions from subsets of
ω^2 to Z. Let us begin by introducing some basic definitions and
notational conventions.

Given functions f,g : ω→ω, let f ≤ g if and only if
f(i) ≤ g(i) for all i ∈ω, let f ≤^* g if and only if
f(i) ≤ g(i) for all but finitely many i ∈ω, and let f =^* g
if and only if f(i) = g(i) for all but finitely many i ∈ω. We let
f ∧ g denote the greatest lower ≤-bound of f and g, i.e.,
(f ∧ g)(i) = min({f(i), g(i)}) for all i ∈ω. Similarly,
if f⃗ = ⟨ f_0, …, f_n ⟩ is a sequence of elements of ^ωω,
then ⋀f⃗ denotes the greatest lower ≤-bound of the functions
f_0, …, f_n. If f ∈^ωω, then I(f) denotes the set
{(i,j) ∈ω^2  |   j ≤ f(i)}; visually, this is the region
below the graph of f. Relatedly, U(f) denotes the set
{g ∈^ωω |   g ≤ f}. We note that, for
ease of readability, we will sometimes write ∧f⃗ in place of
the more formally correct ⋀f⃗ in expressions such as
φ: I(∧f⃗) →Z. The correct interpretation
will always be clear from context.

Our interest is in families of functions indexed by elements of
(^ωω)^n for some positive integer n. Before giving general definitions, we recall the better-known special case in which
n = 1.

 
  A family of functions Φ = ⟨φ_f : I(f) →Z |
    f ∈^ωω⟩ is coherent if
  
    φ_g  I(f ∧ g) - φ_f  I(f ∧ g)
        =^* 0

  for all f,g ∈^ωω.

  The family Φ is trivial if there exists a function ψ : ω^2
  →Z such that
  
    ψ I(f) - φ_f =^* 0

  for all f ∈^ωω. In this case, we say that ψ trivializes Φ.

  The notions of coherent and trivial also apply to families
  of functions indexed by some subset of ^ωω in the
  obvious way.


 
  In the following, as in Definition <ref>, sums involving functions with
  different domains will be common. In the interests of readability, we will tend to refrain from notating the restrictions of such functions to
  the intersection of their domains. An equation like
  
    φ_g  I(f ∧ g) - φ_f  I(f ∧ g)
        =^* 0,

  for example, will more typically appear as
  
    φ_g - φ_f =^* 0

  hereafter.


Clearly any trivial family of functions is coherent. More interesting are those families of functions which are coherent but not trivial; in these families there is a tension between local and global behaviors which is exemplary of the broader set-theoretic theme of incompactness. More precisely, observe that any coherent Φ = ⟨φ_f  |   f ∈^ωω⟩ is “locally” trivial: for any g ∈^ωω, the function φ_g trivializes the family
⟨φ_f  |   f ∈ U(g)⟩.  A nontrivial coherent Φ is simply one in which these local phenomena do not globalize. Such families are the subjects of the works <cit.>, <cit.>,
<cit.>, and <cit.>, among others.
As we will see in Section <ref>, their existence is equivalent to the statement lim^1 𝐀≠ 0.

For the more general definitions of n-coherence and n-triviality, we need some more notation.


  Suppose that n is a positive integer and f⃗ = ⟨ f_0, … f_n⟩ is a
  sequence of length n + 1. If i ≤ n, then f⃗^i denotes the
  sequence of length n obtained by removing the i^th entry of
  f⃗, i.e., f⃗^i = ⟨ f_0, …, f_i-1, f_i + 1, …, f_n⟩.

  If σ is a permutation of ⟨ 0, …, n ⟩, then sgn(σ) denotes the
  sign or parity of σ (so sgn(σ) is either 1 or -1).
  We will use the notation σ(f⃗) to denote the sequence
  ⟨ f_σ(0), …, f_σ(n)⟩.


 
  Let n be a positive integer, and let
  
    Φ = ⟨φ_f⃗ : I(∧f⃗) →Z |  f⃗∈ (^ωω)^n⟩

  be a family of functions.
  
    
  * Φ is alternating if
    
    φ_σ(f⃗) = sgn(σ) φ_f⃗

    for every f⃗∈ (^ωω)^n and every permutation σ of
    (0, …, n-1).
    
  * Φ is n-coherent if it is alternating and if
    
    ∑_i = 0^n (-1)^i φ_f⃗^i =^* 0

    for all f⃗∈ (^ωω)^n+1. (Note that, in accordance
    with Remark <ref>, for readability we have omitted the restrictions
    of the functions in the above expression to the intersection of their domains.
    Formally, each φ_f⃗^i should be φ_f⃗^i
    I(∧f⃗).)
    
  * For n > 1, Φ is n-trivial if there exists an alternating family
    
    Ψ = ⟨ψ_f⃗ : I(∧f⃗) →Z |  f⃗∈ (^ωω)^n-1⟩

    such that
    
    ∑_i = 0^n-1 (-1)^i ψ_f⃗^i =^* φ_f⃗

    for all f⃗∈ (^ωω)^n. We term such a family an
    n-trivialization of Φ.
  
  As in the case n = 1, the notions of alternating, n-coherent,
  and n-trivial apply in obvious ways to families
  indexed by F^n, where F is any subset of ^ωω.


Notice that if n = 1 then every family Φ as above is alternating, and
the definition of 1-coherence coincides with the that of coherence in
Definition <ref>. Similarly, we define 1-triviality to coincide with triviality as defined in Definition <ref>. If the value of n is clear from context then
it may be dropped from the expression n-trivial. Also we will sometimes
consider functions φ_f⃗ or ψ_f⃗ without explicitly
specifying their domains or codomains. It is in such cases implicit that
these functions have domain I(∧f⃗) and codomain Z.

Observe that if Φ is alternating then φ_f⃗ = 0 whenever f⃗∈ (^ωω)^n
has repeated entries, since if the permutation
σ induces a simple swapping of two repeated entries in f⃗ then sgn(σ) = -1 and σ(f⃗) = f⃗ and therefore φ_f⃗ = - φ_σ(f⃗)=-φ_f⃗.

Just as when n equals 1, any n-trivial family of functions is
n-coherent. Also just as before, nontrivial n-coherent families are exemplary cases of set-theoretic incompactness.
This is again because if Φ = ⟨φ_f⃗ |  f⃗∈
(^ωω)^n ⟩
is an n-coherent family then for each g in ^ωω the local family ⟨φ_f⃗ |  f⃗∈ U(g)^n ⟩ is
n-trivial, as witnessed by the collection

    ⟨(-1)^n+1φ_h⃗ ^⌢⟨ g ⟩ |  h⃗∈
      U(g)^n-1⟩

This fact will contrast with the global structure of any nontrivial such Φ.

We will see in Section <ref>
that for each positive integer n the nonexistence of nontrivial
n-coherent families of functions is equivalent to the statement lim^n 𝐀 = 0. Hence our Main Theorem may be rephrased as follows:

\beginTHM'
  Let κ be a weakly compact cardinal in V and let P denote a length-κ
  finite-support iteration of Hechler forcings. Then the following holds in V^P: for every
  positive integer n, every n-coherent family
  
    Φ = ⟨φ_f⃗ : I(∧f⃗) →Z |  f⃗∈ (^ωω)^n⟩

  is n-trivial.
\endTHM'

It is this version of the Main Theorem that we will prove.
To that end we give the following alternate characterization of the
n-triviality of an n-coherent family, one which is at least locally
more finitary in character than that of Definition <ref>. Our
aim is to facilitate the analysis of these phenomena as they arise in
forcing extensions. In what follows, and throughout the paper, if ψ:X
→Z is a function, then the support of ψ is the
set {x ∈ X |ψ(x) ≠ 0}. We say that ψ is finitely supported
if the support of ψ is finite.


  Suppose that F ⊆^ωω, and let Φ=⟨φ_f⃗ |  f⃗∈ F^n
  ⟩ be an n-coherent
  family. Then Φ is n-trivial if and only if there exists an alternating
  family of finitely supported functions Ψ=⟨ψ_f⃗ |  f⃗∈ F^n⟩ such that
  
    ∑_i=0^n(-1)^iφ_f⃗^i=∑_i=0^n(-1)^iψ_f⃗^i

  for all f⃗∈ F^n+1.



  See Lemma <ref> in Section <ref> for a cohomological approach to the above fact; the treatment there is notably cleaner and neatly complements the more computational perspective below.



  We first consider the case in which n = 1. Suppose that Φ is trivial
  and that τ : ω^2 →Z is a trivialization. For
  each f ∈ F, let
  
    ψ_f = φ_f - τ I(f).

  It is straightforward to verify that Ψ = ⟨ψ_f  |  f ∈
  F ⟩ is as desired.
  For the other direction, suppose that Ψ is as in the statement of
  the lemma. In particular, for all f,g ∈ F and all
  x ∈ I(f ∧ g), we have
  
    φ_f(x) - ψ_f(x) = φ_g(x) - ψ_g(x).

  We can therefore define τ : ω^2 →Z by setting,
  for all x ∈ω^2,
  
    τ(x) = φ_f(x) - ψ_f(x)

  for some (or, equivalently, all) f ∈ F such that x ∈ I(f) (if there is
  no f ∈ F such that x ∈ I(f), simply let τ(x) = 0). Since
  each ψ_f(x) is finitely supported, it follows that
  φ_f(x) =^* τ I(f) for all f ∈ F.

  We now consider the case in which n > 1.
  Suppose first that Φ is n-trivial, and let T = ⟨τ_f⃗ |  f⃗∈ F^n-1⟩ be an n-trivialization of
  Φ. For each f⃗∈ F^n, let
  
    ψ_f⃗ = φ_f⃗ - ∑_i=0^n-1 (-1)^i τ_f⃗^i.

  We claim that Ψ = ⟨ψ_f⃗ |  f⃗∈ F^n
⟩ is as desired.
  The following statements are straightforward but tedious to verify. This
  direction of the lemma being inessential to the proof of our main result, we
  leave them to the reader:
  
    
  * If T is an n-trivialization of Φ then
    each ψ_f⃗ is finitely supported.
    
  * If both T and Φ are alternating families then
    Ψ also is an alternating family.
    
  * For all f⃗∈ F^n
    
    ∑_i=0^n (-1)^i φ_f⃗^i = ∑_i=0^n (-1)^i ψ_f⃗^i

    as desired. This can be seen by writing
    
    ∑_i=0^n (-1)^i ψ_f⃗^i = ∑_i=0^n (-1)^i φ_f⃗^i
          - ∑_i=0^n ∑_j=0^n-1(-1)^i + jτ_(f⃗^i)^j

    and verifying that all of the terms in the double sum on the right-hand side
    of the above equation cancel out.
  

  For the implication in the other direction, suppose that Φ and Ψ are as in the statement of the
  lemma. For each x ∈ω^2, fix a function f_x ∈ F
  with x ∈ I(f_x) if there exists such a function in F (if not, then leave
  f_x undefined). We will define an n-trivialization
  T = ⟨τ_f⃗ |  f⃗∈ F^n-1⟩
  of Φ as follows. Given f⃗∈ F^n-1
  and x ∈ I(∧f⃗), note that f_x is defined, and let
  
    τ_f⃗(x) = (-1)^n(ψ_f⃗^⌢⟨ f_x
        ⟩(x) - φ_f⃗ ^⌢⟨ f_x ⟩(x) )

  The fact that T is an alternating family follows immediately from the
  fact that Φ and Ψ are alternating families. To see that
  T is an n-trivialization of Φ, fix f⃗∈ F^n
  and let x be an element of I(∧f⃗) outside of the support of
  ψ_f⃗. Then we have
  
    ∑_i=0^n-1(-1)^i τ_f⃗^i(x) = (-1)^n ∑_i=0^n-1
        (-1)^i (ψ_f⃗^i ^⌢⟨ f_x ⟩(x) -
        φ_f⃗^i ^⌢⟨ f_x ⟩(x) )

  Letting g⃗ = f⃗ ^⌢⟨ f_x ⟩, we have
  
    ∑_i=0^n(-1)^iφ_g⃗^i(x) =∑_i=0^n(-1)^iψ_g⃗^i(x)

  Rearranging the terms in this equation yields
  
    ∑_i=0^n-1
      (-1)^i (ψ_f⃗^i ^⌢⟨ f_x ⟩(x) -
      φ_f⃗^i ^⌢⟨ f_x ⟩(x) ) =
      (-1)^n ( φ_f⃗(x) - ψ_f⃗(x))

  Recall that we chose x so that ψ_f⃗(x) = 0. Hence, putting this all together,
  we obtain
  
    ∑_i=0^n-1(-1)^i τ_f⃗^i(x) = (-1)^2nφ_f⃗(x)
        = φ_f⃗(x)

  Since the support of ψ_f⃗ is finite, it follows that
  
    ∑_i=0^n-1(-1)^i τ_f⃗^i =^* φ_f⃗

  as required.


With the aid of one further lemma, we are now in a position to describe the basic strategy of the argument of our main theorem. When F is a subset of ^ωω
and Φ = ⟨φ_f⃗ | f⃗∈ (^ωω)^n⟩,
we will write Φ F for
⟨φ_f⃗ | f⃗∈ F^n⟩. Recall that a subset F ⊆^ωω
is said to be ≤^*-cofinal if, for all g ∈^ωω, there is
f ∈ F such that g ≤^* f.

 Let Φ=⟨φ_f⃗ | f⃗∈(^ωω)^n⟩ be an n-coherent family of functions. Then Φ is n-trivial if and only if Φ F is n-trivial for some ≤^*-cofinal F⊆ ^ωω.

 The rightwards implication is obvious. For the leftwards implication, the point is that any n-trivialization of any such Φ F extends to an n-trivialization of Φ. Suppose first that n = 1, F is ≤^*-cofinal in ^ωω, and
ψ:ω^2 →Z trivializes Φ F. We claim that ψ
trivializes the entire family Φ. Indeed, if g ∈^ωω, then
we can find f ∈ F such that g ≤^* f, i.e., I(f) contains I(g) modulo a
finite set. By the coherence of Φ, we have φ_f =^* φ_g. Since
ψ trivializes Φ F, we have ψ =^* φ_f, and hence
ψ =^* φ_g, as well.

We can therefore suppose that n>1. Let F be ≤^*-cofinal in ^ωω and let Υ=⟨υ_f⃗ | f⃗∈ F^n-1⟩ be an n-trivialization of Φ F. Fix a map a: ^ωω→ F such that g≤^* a(g) for each g∈ ^ωω. Write a(g⃗) for ⟨ a(g_0),…,a(g_n-1)⟩. The family Ψ=⟨ψ_g⃗ |  g⃗∈ (^ωω)^n-1⟩ is then an n-trivialization of Φ, where

    ψ_g⃗=υ_a(g⃗)-∑_i=0^n-1(-1)^iφ_⟨ g_0,…,g_i,a(g_i),…,a(g_n-1)⟩
 for each g⃗∈(^ωω)^n-1. The right-hand side of the equation is a sum of functions defined on all but finitely many elements of I(∧g⃗); the function ψ_g⃗ is defined more precisely as the extension of that sum to the domain I(∧g⃗) by letting ψ_g⃗(x)=0 on any otherwise undefined arguments x. The verification that this definition works takes the following shape: for any g⃗=⟨ g_0,…,g_n⟩∈ (^ωω)^n+1 the terms (-1)^iυ_a(g⃗^i) (i≤ n) in

    ∑_i=0^n(-1)^iψ_g⃗^i

together simplify (mod finite) to φ_a(g⃗). This together with (n-1) of the terms in the sum (<ref>) will simplify (mod finite) to φ_⟨ g_0,a(g_1),…,a(g_n-1)⟩. This process continues until (<ref>) has entirely simplified (mod finite) to the term φ_g⃗, thus completing the verification.

There are in fact a number of ways to argue Lemma <ref>. The above approach may be clearer in the following example.
 Let Φ be 2-coherent. Let F be as in the statement of Lemma <ref> and let Υ=⟨υ_f  |  f∈ F⟩ 2-trivialize Φ F. Let then a: ^ωω→ F be as in the proof of Lemma <ref> and let ψ_f=υ_a(f)-φ_⟨ f,a(f)⟩ for each f∈ ^ωω. Then for all f,g∈ ^ωω,

    ψ_g-ψ_f     =  υ_a(g)-υ_a(f)-(φ_⟨ g,a(g) ⟩-φ_⟨ f,a(f)⟩)
       =^* φ_⟨ a(f),a(g)⟩-φ_⟨ g,a(g)⟩+φ_⟨ f,a(f)⟩
       =^*φ_⟨ f,a(g)⟩-φ_⟨ g,a(g) ⟩
       =^*φ_⟨ f,g ⟩

as desired.

We may now describe the broad outlines of our proof of our main theorem. Fix n>0 and a weakly compact cardinal κ, and let ℙ be a length-κ finite-support iteration of Hechler forcings. To show that V^ℙ“ lim^n𝐀=0” we fix an arbitrary n-coherent Φ in V^P and show that it is n-trivial. This we accomplish by showing that Φ F is n-trivial, where F is a ≤^*-cofinal family of Hechler reals. This in turn we achieve by defining a family ⟨ψ_f⃗ | f⃗∈ F^n⟩ of finitely supported functions trivializing Φ F in the sense of Lemma <ref>. These ψ_f⃗ are formed out of the differences among particular functions φ_f⃗ in Φ. To select those functions we rely heavily on uniformities among the conditions in the ℙ-generic filter which derive from the weak compactness of κ by way of the multidimensional Δ-system Lemma of the following section. Our proof consists essentially in applying this procedure to each n>0. As indicated, however, expository considerations lead us to break this proof into three stages: that of n=1, that of n=2, and that of n>2.



 §.§ Homological background
 

We described above a historical sequence of investigations into the derived limits lim^n 𝐀, the point of departure for any of which is the following computation. For each positive integer n let X^n denote the one-point compactification of an infinite countable sum of copies of the n-dimensional open unit ball B^n={x⃗∈ℝ^n|‖x⃗‖<1}; more colloquially, X^n is an n-dimensional “Hawaiian earring.” Its strong homology groups are as follows:


    H_p(X^n)=
    ℤ    p= 0 
    ∏_i∈ωℤ    p=n 
    
          0    otherwise.

This is in marked contrast to the singular homology groups of X^n <cit.>, <cit.>, and essentially certifies H_* as a Steenrod homology theory <cit.>. For countably infinite sums of copies of X^n, on the other hand,

    H_p(∐_i∈ω X^n)=
    lim^n𝐀⊕(⊕_i∈ω ℤ)     p= 0 
    lim^n-p𝐀    0<p≤ n 
    
          0    otherwise.

We will define the inverse system 𝐀 and its higher derived limits momentarily; we will then leave all more direct references to strong homology behind until our conclusion. Interested readers are referred to <cit.> or to <cit.> more generally for details of the above computations. The significance of these computations, of course, is that they tell us that if strong homology is additive on closed subsets of Euclidean space then lim^n𝐀=0 for all n>0.

Let 𝒩 denote the partial order (^ωω,≤), and let 𝒩^op denote its order-reversal. Let τ(𝒩) denote the topology on ^ωω generated by the basis 𝖡(𝒩)={U(g)| g∈  ^ωω}, where we recall that U(g)={f∈ ^ωω| f≤ g}. Given a quotient B/A of groups, we write [b] for the coset of an element b of B.

Let 𝐀 denote the inverse system (A_f,p_fg,𝒩), where 
    A_f=⊕_i∈ I(f) ℤ
 and p_fg:A_g→ A_f is the projection map for each f≤ g in 𝒩. Similarly, let 𝐁=(B_f,q_fg,𝒩) and 𝐁/𝐀=(B_f/A_f,r_fg,𝒩), where 
    B_f=∏_i∈ I(f)ℤ
 and q_fg:B_g→ B_f and r_fg:B_g/A_g→ B_f/A_f are projection maps for each f≤ g in 𝒩.

𝐀

is an object, in other words, of the functor or presheaf category 𝖠𝖻^𝒩^op, and it is in this setting that its higher derived limits are most naturally defined. The inverse limit of 𝐀, for example, admits both a category-theoretic characterization via a universal property in 𝖠𝖻^𝒩^op and the following more concrete characterization:

    lim 𝐀={⟨φ_f | f∈ ^ωω⟩∈∏_f∈ ^ωωA_f  |   p_fg(φ_g)=φ_f for all f≤ g in  ^ωω}

More precisely, lim 𝐀 is the above family naturally viewed as a group.[Observe that in consequence lim^0𝐀, which equals lim𝐀 by definition, is isomorphic to ⊕_i∈ω∏_j∈ωℤ, as additivity in the degree n=p in equation (<ref>) would require.] Similarly, higher derived limits lim^n𝐀 admit abelian category theoretic description as the cohomology groups of the lim-image of an injective resolution of 𝐀. Standard resolutions convert this description to a more concrete general form, as above. The characterizations of lim^1𝐀 and of lim^n𝐀 (n≥ 1) in <cit.> and <cit.>, respectively, then each involved one further conversion, via the long exact sequence

    0⟶ lim 𝐀⟶lim 𝐁⟶lim 𝐁/𝐀lim^1 𝐀⟶lim^1 𝐁⟶⋯

associated to the natural short exact sequence

    0⟶ 𝐀⟶ 𝐁⟶ 𝐁/𝐀⟶ 0.

We will require for our work below two further reformulations.

First, for each U in τ(𝒩) let

    lim(𝐀 U)={⟨φ_f | f∈ U⟩∈∏_f∈ U
      A_f  |   p_fg(φ_g)=φ_f for all f≤ g in U}.

Observe that 
    lim(𝐀 U(g))≅ A_g  for any g∈ ^ωω.
 Similar definitions and observations apply for the systems 𝐁 and 𝐁/𝐀. By Jensen's observation in <cit.>,

    lim^n𝐀≅Ȟ^n((^ωω,τ(𝒩)),𝒜)

where 𝒜 is the sheaf on (^ωω,τ(𝒩)) given by U↦lim(𝐀 U) together with the natural restriction maps. Analogous definitions apply for the systems 𝐁 and 𝐁/𝐀; in particular, ℬ/𝒜 will denote the sheaf given by U↦lim(𝐁/𝐀 U). Since 𝖡(𝒩) is maximal in the refinement-ordering of open covers of 𝒩, equation (<ref>) now takes the following form:

    …→Ȟ^0(𝖡(𝒩),ℬ)→Ȟ^0(𝖡(𝒩),ℬ/𝒜)
    Ȟ^1(𝖡(𝒩),𝒜)→Ȟ^1(𝖡(𝒩),ℬ)→⋯

As observed in <cit.>, 
    lim^n 𝐁=0 for all n>0.

The same therefore holds for Ȟ^n(𝖡(𝒩),ℬ). In consequence,
    lim^1𝐀≅Ȟ^0(𝖡(𝒩),ℬ/𝒜)/im(Ȟ^0(𝖡(𝒩),ℬ)).

We will define these cohomology groups more explicitly below. It will then be clear that the natural rendering of the above quotient is as the coherent families of functions modulo the trivial families of functions in the sense of Definition <ref>.
The following is then immediate:
 lim^1𝐀=0 if and only if every coherent family of functions ⟨φ_f  |  f ∈^ωω⟩ is trivial.

By point (<ref>) above, the higher-n analogue of equation (<ref>) is simply

    lim^n𝐀≅Ȟ^n-1(𝖡(𝒩),ℬ/𝒜) for all n>1

The advantage of this formulation is that in computing Čech cohomology groups we have a choice among several indexing schema giving equivalent quotients <cit.>. As a generic real may fail to integrate nontrivially into the ordering (^ωω,≤) of its ground model, it is useful in contexts like ours to define higher coherence via indices as untethered to that order as possible. To that end we adopt the alternating cochains definition of the Čech complex.
 For n≥ 0, the group Ȟ^n(𝖡(𝒩),ℬ/𝒜) is the cohomology of the cochain complex

    ⋯ C_alt^n(𝖡(𝒩),ℬ/𝒜)C_alt^n+1(𝖡(𝒩),ℬ/𝒜)⋯

where C_alt^n(𝖡(𝒩),ℬ/𝒜) denotes the subgroup of

    ∏_f⃗∈(^ωω)^n+1lim(𝐁/𝐀 U(∧f⃗))=∏_f⃗∈(^ωω)^n+1B_⋀f⃗ /A_⋀f⃗

whose elements c satisfy 
    c(σ(f⃗))=sgn(σ)c(f⃗)

for all f⃗∈(^ωω)^n+1 and permutations σ of ⟨ 0,…,n⟩. The equality in  (<ref>) amounts simply to an application of the 𝐁/𝐀-variant of observation (<ref>).

The differentials d^n are defined as usual. Namely, for any i≤ n+1 and f⃗∈(^ωω)^n+2 recall that f⃗^i denotes the element of (^ωω)^n+1 formed via the omission of the coordinate f_i from f⃗. Then for any c∈ C_alt^n(𝖡(𝒩),ℬ/𝒜), define d^n c by the assignment

    d^n c(f⃗)=∑_i=0^n+1(-1)^i (c(f⃗^i) I(∧f⃗))

for each f⃗∈ (^ωω)^n+2.

Entirely analogous definitions hold for Ȟ^n(𝖡(𝒩),𝒜) and Ȟ^n(𝖡(𝒩),ℬ). Observe in particular that any c in C_alt^n(𝖡(𝒩),ℬ/𝒜) admits representatives ĉ in C_alt^n(𝖡(𝒩),ℬ), i.e., alternating cochains ĉ taking values in the groups B_⋀f⃗ and satisfying [ĉ(f⃗)]=c(f⃗) for all f⃗∈(^ωω)^n+1.

As in the cases of Section <ref>, the requisite function-restrictions will tend to be clear from context. Hence again for readability we will rarely notate them, writing,
for example, sums like that of equation (<ref>) as 
    ∑_i=0^n+1(-1)^i c(f⃗^i).


It is now clear that n-coherent and n-trivial families are, respectively,
representatives of the (n-1)-cocycles and (n-1)-coboundaries of the complex (<ref>) above.
Recall that every n-trivial Φ is n-coherent. We have just argued that
whether or not lim^n𝐀 vanishes is precisely the question of the converse;
we have in other words shown the following:
 Let n be a positive integer. Then lim^n 𝐀=0 if and only if every n-coherent family
Φ=⟨φ_f⃗ | f⃗∈(^ωω)^n⟩ is n-trivial.




We end this subsection by indicating how Lemma <ref> can be derived
from cohomological considerations in the special case F = ^ωω.
(The more general case of an arbitrary F ⊆^ωω can be obtained
via a routine modification of the arguments in this subsection, working with the
partial order 𝒩_F = (F, ≤) and inverse systems
𝐀 F = (A_f, p_fg, 𝒩_F), 𝐁 F,
and 𝐁 / 𝐀 F instead of 𝒩, 𝐀,
𝐁, and 𝐁/𝐀. All of the results of this subsection carry through with
no difficulty in this setting.)
We return to equation (<ref>), which had derived from the cohomological reformulation of equation (<ref>). Equation (<ref>) is more precisely stated as follows:
 Let n be greater than 1. Then Ȟ^n-1(𝖡(𝒩),ℬ/𝒜) is isomorphic to Ȟ^n(𝖡(𝒩),𝒜) via the connecting map ∂_n-1: [c]↦ [d^n-1ĉ], where ĉ is any representative of c in C_alt^n-1(𝖡(𝒩),ℬ).


Here the only new assertion is the characterization of the connecting map ∂_n-1. This, though, is simply the general form of the connecting maps of a long exact sequence; see for example <cit.>.

For n≥ 1 it follows that an n-coherent family Φ=⟨φ_f⃗ | f⃗∈(^ωω)^n⟩ represents a coboundary in C_alt^n(𝖡(𝒩),ℬ/𝒜) if and only if what we might write as d^nΦ is a coboundary in C_alt^n+1(𝖡(𝒩),𝒜).
Lemma <ref> is then immediate.



§ A MULTIDIMENSIONAL Δ-SYSTEM LEMMA


We turn now more towards the argument of our main theorem. We begin by proving a generalization of the two-dimensional Δ-system lemma appearing in <cit.> (see <cit.> for an earlier precedent). Structuring our generalization will be the following refinement of the relation holding between pairs of elements of a classical Δ-system.

  Sets u,v ∈ []^<ω are aligned if
  
    
  * |u| = |v|, and
    
  * |u ∩α| =
    |v ∩α| for all α∈ u ∩ v.
  



Let 0 < k < ℓ be natural numbers. A function t:ℓ→ 3
  is a type of width k and length ℓ if
  
    |t^-1[{0,2}]| = |t^-1[{1,2}]| = k.

  Given u,v ∈ []^k and an increasing enumeration ⟨α_i | i < ℓ⟩ of u ∪ v, we say that the type of u and v is the unique type t of width k and length ℓ such that
  
    
  * u ∖ v = {α_i | t(i)=0},
    
  * v ∖ u = {α_i | t(i)=1}, and
    
  * u ∩ v = {α_i | t(i)=2}.
  
 We denote this unique type t by
  (u,v). Observe that u and v are aligned if and only if t=(u,v) satisfies
  
    |t^-1[{0}] ∩ i| = |t^-1[{1}] ∩ i|

for all i in t^-1[{2}]. Any such type t is also called aligned.


Types as above admit natural representations as finite strings of 0s, 1s, and 2s. If α<β<γ, for example, then
  ({α,β},{β,γ}) is naturally rendered as 021.

We may now state our multidimensional Δ-system lemma. We first remind the reader
of the definition of a weakly compact cardinal.


  A cardinal κ is weakly compact if κ is uncountable and,
  for every positive integer n, every θ < κ, and every function
  c:[κ]^n →θ, there is a set H ∈ [κ]^κ
  such that c  [H]^n is constant.


There are many useful alternative characterizations of weakly compact cardinals;
for example, κ is weakly compact if and only if κ is strongly
inaccessible and has the tree property.
We refer the reader to <cit.> for more information on this and other
equivalent formulations of weak compactness.

Recall our notational convention that elements of [κ]^n are often thought
of as increasing n-tuples. So, for instance, when we write α⃗ =
⟨α_0, …, α_n-1⟩∈ [κ]^n, it is implicit
that α_0 < α_1 < … < α_n-1.

 
  Let n be a positive number and let κ be a weakly compact cardinal, and suppose that the family of n-tuples α⃗ = ⟨α_0, …, α_n-1⟩∈ [κ]^n indexes elements u_α⃗ of [κ]^<ω.
  Then there is a set A ∈ [κ]^κ and a collection
  ⟨ u_α⃗ |  α⃗∈ [A]^<n⟩
  of elements of [κ]^<ω such that
  
    
  * for all α⃗∈ [A]^<n,
    
      
  * if β∈ A and α⃗ < β, then
      u_α⃗ < β,
      
  * if β⃗∈ [A]^≤ n satisfies
      α⃗⊑β⃗, then u_α⃗⊑
      u_β⃗,
      
  * the set {u_α⃗
      ^⌢⟨β⟩ |  β∈ A\(max(α⃗)+1)
      } forms a Δ-system with root u_α⃗;
    
    
  * for all m ≤ n and all α⃗, β⃗∈ [A]^m,
    
    
  * |u_α⃗| = |u_β⃗|, and
    
  * if α⃗ and β⃗ are aligned, then u_α⃗
    and u_β⃗ are aligned.
    
  

To prove Lemma <ref>, we require one further technical lemma.
 
  Suppose that 0 < k < ℓ < ω and that t is an aligned type of width
  k and length ℓ. Then for some positive number m there exists a sequence
  ⟨ u_j | j ≤ 2m ⟩ of elements of []^k such that
  
    
  * (u_2j, u_2j+1) = (u_2j + 2, u_2j + 1) = t for all j < m, and
    
  * (u_0, u_2m) = t.
  



  The proof is by induction on k. We will also assume that t(ℓ - 1) ∈{1,2}.
  The case in which t(ℓ - 1) = 0
  is essentially the same as that in which t(ℓ - 1) = 1 and is left to the
  reader. If k = 1, then either t = 2 or t = 01. We may take m = 1 in either case. For if t=2 then for any ordinal α the sequence
  u_0 = u_1 = u_2 = {α} is as desired, while if t=01 then for any ordinals α < β < γ the sequence u_0 = {α}, u_1 = {γ}, u_2 = {β}  is as desired.

  Now assume that k > 1 and that we have established the lemma for all aligned
  types of width less than k.

  Case 1: t(ℓ - 1) = 2. In this case, t' = t  (ℓ - 1)
  is an aligned type of width k - 1, hence by our inductive hypothesis
  there exists some positive m and sequence ⟨ u_j | j ≤ 2m ⟩
  of elements of []^k-1 witnessing the conclusion of the lemma for t'.
  Now take any β>⋃_j ≤ 2mu_j, and
  let u_j^⋆ = u_j ∪{β} for all j. Then m and ⟨ u_j^⋆|
  j ≤ 2m ⟩ witness the conclusion of the lemma for t.

  Case 2: t(ℓ - 1) = 1. The idea in this case is to  form a type t' of
  width k - 1 and length ℓ-2 by deleting the last 0 and the last 1 from t. The induction hypothesis then furnishes a sequence ⟨ u_j | j≤ 2m⟩ as in the conclusion of the lemma for the type t'. It is then fairly straightforward (though notationally tedious) to modify ⟨ u_j | j≤ 2m⟩ to form a sequence as desired for the original type t.

  More formally, let ℓ_0 < ℓ be such that t(ℓ_0) = 0 and t(i) = 1 for all i with ℓ_0 < i < ℓ. Such an ℓ_0 must exist
  since t is aligned. Let k_0 = |t^-1[{1,2}] ∩ℓ_0|.
  This number k_0 has the following significance: if u,v∈[]^k are such that (u,v) = t, then k_0 is the number of elements of v that are smaller than
  the largest element of u. In other words, v(k_0) is the least element of v larger
  than every element of u. Now define t' : (ℓ - 2) → 3
  by letting
  
    t'(i) =
        
          t(i)    if  i < ℓ_0 
    
          1    if ℓ_0 ≤ i < ℓ - 2

This defines an aligned type t' of width k - 1. 
  
  Apply the induction hypothesis to obtain a positive m and a
  sequence ⟨ u_j | j ≤ 2m ⟩ of elements of []^k-1
  witnessing the conclusion of the lemma for t'. By “stretching" each u_j
  if necessary, we may assume that every element of every u_j is a limit of limit ordinals.

  We now augment the elements of the sequence ⟨ u_j | j ≤ 2m ⟩ to form a sequence ⟨ u^⋆_j | j ≤ 2n ⟩ for t. Two cases are straightforward: those in which k_0=0 and those in which k_0=k-1. In the latter case, for example, take {β_j | j≤ 2m}>⋃_j≤ 2mu_j such that
  
    
  * for all j, j' ≤ 2m, if j is even and j' is odd, then β_j < β_j';
    
  * β_0 < β_2m.
  
 Letting u_j^⋆=u_j∪{β_j} then defines a sequence as desired for t. The case of k_0=0 is similar. Therefore assume that 0<k_0<k-1. We will assume as well that u_j(k_0) > u_j'(k_0 - 1) for all odd j,j'<2m. We are free to assume this because if (u,v) = t' then v(k_0) is larger than every element of u, hence
  (u,w) = t' for any w with w k_0 = v k_0
  and w [k_0, k-1) consisting of arbitrarily large ordinals.

 We now define limit ordinals ⟨β_j | j ≤ 2m ⟩ so that u_j < β_j for
  each j ≤ 2m. We first do this for the even j ≤ 2m. First let β_0 be a limit ordinal such that u_1(k_0-1)<β_0<u_1(k_0), and let β_2m be a limit ordinal such that u_2m-1(k_0-1)<β_2m<u_2m-1(k_0). For any other even 0<j<2m let β_j>u_j be a limit ordinal satisfying
  
    max{u_j-1(k_0 - 1), u_j+1(k_0 - 1)}<β_j<min{u_j-1(k_0),
        u_j+1(k_0)}.

  This is all possible by the assumptions of the preceding paragraphs.

   Lastly, let β^⋆ be a limit ordinal larger than any ordinal so far considered, and for all odd j < 2m let β_j = β^⋆. (More precisely we require that β^⋆ > β_j for all even j ≤ 2m
  and β^⋆ > u_j for all odd j < 2m.) Now let u^⋆_j = u_j ∪{β_j} for each j ≤ 2m. By construction, (u^⋆_2j,
  u^⋆_2j+1) = (u^⋆_2j+2, u^⋆_2j + 1) = t for all j < m.
  However, (u^⋆_0, u^⋆_2m) = t may fail to hold: although (u_0, u_2m) indeed equals t', it may not be the case that u^⋆_2m(k_0 - 1)<u^⋆_0(k-1) < u^⋆_2m(k_0), as (u^⋆_0, u^⋆_2m) = t would require.

  We address this possibility by adding a u^⋆_2m + 1 and u^⋆_2m + 2 to our sequence and
  then “rotating” it two steps.  First, let u^⋆_2m + 2 be any element of []^k such that
  
    
  * (u^⋆_0, u^⋆_2m + 2) = t,
    
  * if k_0 > 0, then u^⋆_2m + 2(k_0 - 1) < u^⋆_2m(k_0)
    (this is possible since u^⋆_0(k-2) < u^⋆_2m(k_0) and the latter
    is a limit ordinal), and
    
  * u^⋆_2m + 2(k_0) > β^⋆.
  
  Now define u^⋆_2m + 1 by letting u^⋆_2m + 1 (k-1) =
  u^⋆_0  (k-1) and letting u^⋆_2m + 1(k-1) be any ordinal
  γ > u^⋆_0(k-2) such that
  
    max{u^⋆_2m + 2(k_0 -1), u^*_2m(k_0 - 1)}<γ < u^⋆_2m(k_0)

  (and hence γ < u^⋆_2m + 2(k_0)). Then
  
    (u^⋆_2m + 1, u^⋆_2m) = (u^⋆_2m + 1, u^*_2m + 2) =
        (u^⋆_0, u^⋆_2m + 2) = t.

  Therefore, if we define ⟨ v_j | j ≤ 2m + 2 ⟩
  by setting v_0 = u^⋆_2m + 1, setting v_1 = u^⋆_2m + 2 and, for 2 ≤ j < 2m + 2,
  setting v_j = u^⋆_j - 2, we see that ⟨ v_j | j ≤ 2m + 2 ⟩
  witnesses the conclusion of the theorem for t.

Readers may better appreciate the necessity of some argument like the above after constructing a cycle as in Lemma <ref> for the type 001011. For yet more on these matters, readers are referred to <cit.>.

We turn now to the proof of our main lemma:


  By the weak compactness of κ there exists a natural number ℓ and a B∈ [κ]^κ such that |u_α⃗| = ℓ for all α⃗∈ [B]^n.

  For any γ⃗ = ⟨γ_0, …, γ_2n-1⟩∈ [B]^2n and I ∈ [2n]^n let γ⃗[I] =
  ⟨γ_i | i ∈ I ⟩,  and let
  
    U_γ⃗ = {γ_0, …, γ_2n-1} ∪⋃_I ∈ [2n]^n
        u_γ⃗[I].

  Recall that H(ω) denotes the set of all hereditarily finite sets (in particular,
  H(ω) is itself a countable set). Define a coloring c:[B]^2n→ H(ω) by letting
  
    c(γ⃗) = ⟨(U_γ⃗),  ⟨ξ_i | i < 2n ⟩,  ⟨ v_I | I ∈ [2n]^n ⟩⟩,

  where the latter sequences record the images of the γ_i and u_γ⃗[I], respectively, under the order-isomorphism h:U_γ⃗→(U_γ⃗); more precisely,
  
    
  * ξ_i = h(γ_i) for each i < 2n,
    
  * v_I = h[u_γ⃗[I]] for each I ∈ [2n]^n.
  

  Again by the weak compactness of κ we may fix a set A ∈ [B]^κ such that
  c is constant on [A]^2n. 
  

  We now define u_α⃗ for α⃗ in [A]^≤ n
  by reverse induction on |α⃗|. The base case
  { u_α⃗ | α⃗∈ [A]^n} is given. In the induction step,
  
  
  * 0<m<n,
  
  * u_β⃗ is defined for all
  β⃗ in [A]^≤ n of length greater than m, and
  
  * the u_β⃗ with β⃗ in [A]^m+1 are all of the same size.

Now fix α⃗ in [A]^m.

   
    The set {u_α⃗ ^⌢⟨β⟩ |  β∈ A\( max(α⃗)+1)} forms a Δ-system
    with a root r such that r < β and r ⊑ u_α⃗ ^⌢β
    for every β∈ A with β > max(α⃗).
  

  
    First suppose that m=n-1. Consider any β_0 < β_1 < β_2
    in A\( max(α⃗)+1) together with any γ⃗_0, γ⃗_1, γ⃗_2 in [A]^2n
  such that
    
      
  * α⃗ ^⌢⟨β_1, β_2⟩⊑γ⃗_⃗0⃗,
      
  * α⃗ ^⌢⟨β_0, β_2⟩⊑γ⃗_⃗1⃗,
      
  * α⃗ ^⌢⟨β_0, β_1⟩⊑γ⃗_⃗2⃗.
    
   Let
    ε⃗(β_j) = α⃗ ^⌢⟨β_j⟩ for j < 3. Then c(γ⃗_⃗0⃗) = c(γ⃗_⃗1⃗) = c(γ⃗_⃗2⃗) implies that
    
    η∈ u_ε⃗(β_0)∩ u_ε⃗(β_1)⇔η∈ u_ε⃗(β_0)∩ u_ε⃗(β_2)⇔η∈ u_ε⃗(β_1)∩ u_ε⃗(β_2)

    for any η in κ. It follows immediately that {u_α⃗
    ^⌢⟨β⟩ |  β∈ A\( max(α⃗)+1)} forms a Δ-system. Let
    r be its root. Routine pigeonhole arguments together with the homogeneity of A then show that r < β and r ⊑ u_α⃗
    ^⌢⟨β⟩ for every β∈ A with β > max(α⃗).

    Now suppose that m<n-1. We argue again essentially as above, beginning instead with a sequence β_0 < β_1 < β_2<δ_0<…<δ_n-m-2
    in A\( max(α⃗)+1). Again take γ⃗_0⊒α⃗^⌢⟨β_1,β_2,δ_0,…,δ_n-m-2⟩; similarly for γ⃗_1 and γ⃗_2. Let
    ε⃗(β_j)=α⃗^⌢⟨β_j,δ_0,…,δ_n-m-2⟩ for each β_j. Then again the c-homogeneity of A implies that {u_ε⃗(β) |  β∈ (α_m-1,δ_0)∩ A}
    forms a Δ-system. Since u_α⃗ ^⌢⟨β⟩⊑ u_ε⃗(β) for each such β, and since the sets u_α⃗ ^⌢⟨β⟩ are all of the same size,
    {u_α⃗ ^⌢⟨β⟩ |  β∈ (α_m-1,δ_0)∩ A} forms a Δ-system as well. As δ_0 was arbitrary, {u_α⃗ ^⌢⟨β⟩ |  β∈ A\( max(α⃗)+1)} forms a Δ-system; pigeonhole and homogeneity arguments, as above, secure the remainder of the claim.
  

  Now let u_α⃗ equal the root of the Δ-system
  {u_α⃗ ^⌢⟨β⟩ |  β∈ A\( max(α⃗)+1)}. By Claim <ref>,
  the homogeneity of A, and a pigeonhole argument, we see that we have satisfied item (1) of Lemma <ref>. To see that we satisfy item (2a) as well (and hence that our third inductive assumption was justified), observe that we may calculate |u_α⃗| from the constant value of c[A]^2n, which we denote by ⟨ℓ^*,
  ⟨ξ^*_i | i < 2n ⟩, ⟨ v^*_I | I ∈ [2n]^n ⟩⟩; the point is that this computation depends only on the size, m, of α⃗. To this end, let ℐ_m={I∈ [2n]^n | I∩ m=m}. Consideration of c(γ⃗)
  for any γ⃗∈ [A]^2n end-extending α⃗ then shows that |u_α⃗| = |⋂_I∈ℐ_mv^*_I|.

  It remains to verify item (2b). To this end, fix m ≤ n and an aligned pair of m-tuples
  α⃗, β⃗⊆ A. Suppose for the sake of contradiction that
  u_α⃗ and u_β⃗ are not aligned and fix
  η∈ u_α⃗∩ u_β⃗ such that k_0 =
  |u_α⃗∩η| ≠ k_1 = |u_β⃗∩η|.
  Let t = (α⃗, β⃗).
  Observe that if (γ⃗, δ⃗) = t for some γ⃗,
  δ⃗∈ [A]^m
  then u_γ⃗(k_0) = u_δ⃗(k_1), by the homogeneity of A.

  By Lemma <ref> there exists an integer ℓ≥ 1 and
  a sequence ⟨γ⃗_j | j ≤ 2ℓ⟩ of elements of
  [A]^m such that (γ⃗_0, γ⃗_2ℓ) = t and (γ⃗_2j, γ⃗_2j+1) =
  (γ⃗_2j+2, γ⃗_2j+1) = t
  for all j < ℓ. Let
  ξ = u_γ⃗_0(k_0).

  
     u_γ⃗_2j(k_0) = ξ for all j < m.
  

  
    We proceed by induction on j. For j = 0, the claim is trivial. Suppose that
    0 < j < m and u_γ⃗_2j - 2(k_0) = ξ. Then, since
    (γ⃗_2j-2, γ⃗_2j-1) = t =  (γ⃗_2j,
    γ⃗_2j - 1), we have that ξ = u_γ⃗_2j-2(k_0) =
    u_γ⃗_2j-1(k_1) = u_γ⃗_2j(k_0), as desired.
  

It follows from the claim that u_γ⃗_2m(k_0) = ξ. However, since
  (γ⃗_0, γ⃗_2m) = t, we also have
  u_γ⃗_2m(k_1) = ξ, contradicting the fact that k_0 ≠ k_1.
  This completes the proof of the lemma.




§ HECHLER FORCING AND LIM^1 𝐀
 

We begin this section with a few useful observations about Hechler forcing and
finite-support iterations thereof. Recall that conditions in Hechler forcing are
pairs p = (s_p, f_p), where s_p ∈^<ωω and
f_p ∈^ωω. We will often call s_p the stem of p. If p and q
are conditions then q ≤ p if and only if 

  * s_q ⊇ s_p,

  * f_q ≥ f_p, and

  * s_q(i) > f_p(i) for all
i ∈(s_q) ∖(s_p).
Observe that any two conditions with the same stem are compatible.

If P is a finite-support iteration
of Hechler forcings, then the set of p ∈P such that, for all
α∈(p),

  
  * p α decides the value of ṡ_p(α), and
  
  * ḟ_p(α) is a nice P_α-name for an element of
  ^ωω

is dense in P. We will in general implicitly assume
that all of our conditions come from this dense set.

The following situation will frequently arise:

 
  Suppose that
  
    
  * P is a finite-support iteration of Hechler forcings,
    
  * 𝒜 is a finite collection of conditions in P such
    that s_p(α) = s_q(α) for all p,q ∈𝒜 and all α∈(p) ∩(q),
    
  * r ∈P and
    r ≤ p  (max((r)) + 1) for every p ∈𝒜.
  
  Then the set 𝒜∪{r} has a lower bound in P.



  We define such a lower bound q in P as follows. First, let (q) =
  (r) ∪⋃_p ∈𝒜(p). Next, let q
   (max((r)) + 1) = r. Finally, for all α∈(q)
  ∖ (max((r)) + 1), let s_q(α) = s_p(α) for
  any p ∈𝒜 with α∈(p) and let ḟ_q(α) be a nice
  P_α-name for the pointwise maximum of the set {ḟ_p(α)| p ∈𝒜,  α∈(p)}. It is now straightforward to verify that
  q is a condition in P and as desired.


We now turn to proving a lemma about uniformizing families of conditions in
finite support iterations of Hechler forcings. We first need the following
consequence of weak compactness.

 
  Suppose that κ is a weakly compact cardinal, n < ω, and that
  ⟨ X_α⃗ | α⃗∈ [κ]^≤ n⟩ is a family of
  sets such that |X_α⃗| < κ for every α⃗∈
  [κ]^≤ n. Suppose also that c is a function with domain
  [κ]^n+1 such that, for all β⃗∈ [κ]^n+1,
  we have c(β⃗) ∈∏_i ≤ n X_β⃗ i.
  Then there is an unbounded set A ⊆κ such that, for all
  i ≤ n, all α⃗∈ [A]^i, and all γ⃗, δ⃗∈ [A]^n+1 end-extending α⃗, we have c(γ⃗)(i) =
  c(δ⃗)(i).



  The proof is a relatively straightforward modification of the
  classical ramification argument used to prove that κ satisfies
  κ→ (κ)^n_θ for all n < ω and
  θ < κ. We provide some details for completeness.

  We proceed by induction on n. If n = 0, then the result follows simply
  from the fact that κ is regular and |X_∅| < κ.
  Thus, suppose n = m + 1 and we have established all instances of the
  result for m. By standard arguments (cf. <cit.>),
  using the strong inaccessibility of κ and the fact that
  |X_α⃗| < κ for all α⃗∈ [κ]^≤ n,
  we can define a tree ordering (κ, <_c) such that
  
    
  * for all α < β < κ, if α <_c β, then
    α < β;
    
  * for all α_0 <_c α_1 <_c … <_c α_m <_c
    γ <_c δ, we have c(⟨α_0, …, α_m,
    γ⟩) = c(⟨α_0, …, α_m, δ⟩);
    
  * (κ, <_c) is a κ-tree, i.e., it has height κ
    and every level has cardinality less than κ.
  
  Since κ is weakly compact and therefore has the tree property, we can
  fix an unbounded A_0 ⊆κ such that A_0 is linearly ordered by
  <_c. Now define a function d with domain [A_0]^n as follows.
  For every α⃗∈ [A_0]^n, let
  d(α⃗) = c(α⃗ ^⌢⟨γ⟩) 
  n for some γ∈ A_0 ∖ (α⃗(m) + 1). Note that,
  by property (2) of (κ, <_c) and the fact that A_0 is linearly ordered
  by c, the value of d(α⃗) is independent of our choice of
  γ.

  Apply the inductive hypothesis to find an unbounded A ⊆ A_0 such that,
  for all i ≤ m, all η⃗∈ [A]^i, and all α⃗,
  β⃗∈ [A]^n end-extending η⃗, we have d(α⃗)(i) =
  d(β⃗)(i). We claim that A is as desired. To this end, fix
  i ≤ n, α⃗∈ [A]^i, and γ⃗, δ⃗∈ [A]^n+1 end-extending α⃗. If i = n, then the fact that A
  is linearly ordered by <_c implies that
  c(γ⃗) = c(δ⃗), so, in particular, c(γ⃗)(i) =
  c(δ⃗)(i). If i < n, then, by our definition of d and our choice of A, we have
  
    c(γ⃗)(i) = d(γ⃗ n)(i) =
        d(δ⃗ n)(i) = c(δ⃗)(i),

  as required.


 
  Let n be a positive integer and let κ be a weakly compact cardinal.
  Let ⟨ p_α⃗ | α⃗∈ [κ]^n⟩ be a family of
  conditions in P, a length-κ finite-support
  iteration of Hechler forcings. Let u_α⃗ = (p_α⃗).
  Then there is an unbounded set A ⊆κ, a family
  ⟨ u_α⃗|α⃗∈ [A]^<n⟩, a natural number ℓ, and a set of stems ⟨ s_i | i < ℓ⟩
  such that
  
    
  * |u_α⃗| =
    ℓ for all α⃗∈ [A]^n, and if η is the i^th element of
    u_α⃗ then s_p_α⃗(η) = s_i,
    
  * A and ⟨ u_α⃗|α⃗∈ [A]^≤ n⟩
    satisfy the conclusions of Lemma <ref>,
    
  * p_β⃗ u_α⃗
    = p_γ⃗ u_α⃗ for all α⃗∈ [A]^<n and β⃗, γ⃗∈
    [A]^n such that α⃗⊑β⃗ and α⃗⊑γ⃗.
  



  First, apply the weak compactness of κ to the function on
  [κ]^n defined by
  
    α⃗↦⟨ s_p_α⃗(η)|η∈(p_α⃗) ⟩

  to find an unbounded set A_0 ⊆κ, a natural number
  ℓ < ω, and a sequence
  ⟨ s_i | i < ℓ⟩ of stems such that, for all α⃗∈ A_0, we have |(p_α⃗)| = ℓ and
  
    ⟨ s_p_α⃗(η)|η∈(p_α⃗) ⟩
        = ⟨ s_i | i < ℓ⟩.


  Next, apply Lemma <ref> to ⟨ u_α⃗|α⃗∈ [A_0]^n ⟩ to find an unbounded set
  A_1 ⊆ A_0 and sets ⟨ u_α⃗|α⃗∈ [A_1]^<n⟩ as in the conclusion of that lemma.

  For each α⃗∈ [A_1]^<n let X_α⃗ =
  {p ∈P|(p) = u_α⃗} and consider the function c
  on [A_1]^n defined as follows. For every β⃗∈ [A_1]^n,
  define c(β⃗) ∈∏_i < n X_β⃗ i
  by letting c(β⃗)(i) = p_β⃗ u_β⃗ i for all i < n.

  Apply Lemma <ref>
  to find an unbounded A ⊆ A_1 such that, for all
  i < n, all α⃗∈ [A]^i, and all β⃗, γ⃗∈ [A]^n end-extending α⃗, we have
  c(β⃗)(i) = c(γ⃗)(i), i.e., p_β⃗
  u_α⃗ = p_γ⃗ u_α⃗. Then
  A, ⟨ u_α⃗|α⃗∈ [A]^≤ n⟩,
  ℓ, and ⟨ s_i | i < ℓ⟩ are as desired.



  Suppose that A, ⟨ u_α⃗|α⃗∈ [A]^≤ n⟩, ℓ, and ⟨ s_i | i < ℓ⟩ are as in the conclusion of Lemma <ref>.
  Given α⃗∈ [A]^<n, define p_α⃗∈P by
  choosing any β⃗∈ [A]^n with α⃗⊑β⃗ and letting p_α⃗ = p_β⃗
  u_α⃗ (observe that this is independent of our choice of β⃗).
  The family ⟨ p_α⃗ | α⃗∈ [A]^≤ n⟩ then has the property that if m≤ n and α⃗, β⃗∈ [A]^m are aligned, then p_α⃗
  and p_β⃗ are compatible in P.


We turn now to the first of our results on the vanishing of lim^n𝐀. In
this case, the assumption of the existence of a weakly compact cardinal is
certainly more than we need.
For example, it is shown in <cit.> that lim^1 𝐀 = 0 in any forcing
extension by Add(ω, ω_2), the poset to add ℵ_2-many
Cohen reals. A similar argument shows that lim^1 𝐀 = 0 in any forcing
extension by a length-ω_2 finite support iteration of Hechler forcings, at
least as long as the ground model satisfies 𝖢𝖧.
This is to say that our main purpose in recording this theorem and proof is to foreground the essential logic of the more complicated arguments that will follow.

 
  Suppose that κ is a weakly compact cardinal, and let P be a
  finite-support iteration of Hechler forcings of length κ. Then
  V^P“lim^1 𝐀 = 0.”



  For α < κ, let ġ_α be a P-name for the
  α^th Hechler real added by P. In V^P,
  ⟨ġ_α|α < κ⟩ is a <^*-increasing,
  cofinal sequence in ^ωω, hence it suffices to show that, in V^P,
  every coherent family indexed by ⟨ġ_α|α < κ⟩
  is trivial. To this end, fix a condition p_0 ∈P and a sequence of
  P-names Φ̇ = ⟨φ̇_α : I(ġ_α) →Z |  α < κ⟩ forced by p_0 to be a coherent family.
  We will find a q ≤ p_0 forcing Φ̇ to be trivial.

  Let A_0 = κ∖ (max((p_0)) + 1). Observe that for any
  α < β in A_0 there exists a p ≤ p_0 such that
  p ⊩_P“ġ_̇α̇≤ġ_̇β̇". Namely, let p = p_0 ∪{⟨β, (∅, ġ_α) ⟩}.
  Hence for each α < β in A_0, since p_0 forces that
  Φ̇ is coherent, we may extend p_0 to a q_α, β≤ p_0 such that for some k_α, β <ω,
    
    q_α, β⊩_P“ġ_̇α̇≤ġ_̇β̇, and φ̇_α(k,m)
        = φ̇_β(k,m) for all  k ≥ k_α, β and  m ≤ġ_α(k)."

  Thin out A_0, if necessary, to an unbounded A_1 such that
  k_α, β equals some fixed k^* for all ⟨α, β⟩∈ [A_1]^2.
  Now apply Lemma <ref> to ⟨ q_α, β|⟨α, β⟩∈ [A_1]^2 ⟩ to find an unbounded
  A ⊆ A_1, u_∅, ⟨ u_⟨α⟩|α∈ A ⟩, ℓ, and ⟨ s_i | i < ℓ⟩ as
  in the statement of the lemma.

  Define conditions q_∅ and
  ⟨ q_α|α∈ A ⟩ as follows. First, let
  α < β be elements of A and let
  q_∅ = q_α, β u_∅. By Lemma <ref> item (3), this definition is independent of the choice of α and β.
  Next, for a fixed α∈ A, choose an arbitrary β∈ A
  with β > α and let q_α = q_α, β
  u_⟨α⟩. Here again the choice of β is immaterial.

  Let q = q_∅ and notice that, since q_α, β≤ p_0 for all
  α < β in A_0, we also have q ≤ p_0.
  We claim that q forces Φ̇ to be trivial. Let Ḃ
  be a P-name for the set of α∈ A such that q_α∈Ġ,
  where Ġ is the canonical P-name for the P-generic filter.

   
    q ⊩_P“Ḃ is unbounded in κ".
  

  
    Let r ≤ q and η < κ be arbitrary. It suffices to find an
    α∈ (A ∖η) such that q_α and r are compatible.
    By construction, the sequence ⟨ u_⟨α⟩∖ u_∅ |  α∈ A ⟩ consists of pairwise
    disjoint sets, so (u_⟨α⟩∖ u_∅)  ∩ (r) = ∅ for some α∈ (A ∖η).
    This implies that q_α is compatible with r, since q_α u_∅
    = q_∅ and r ≤ q_∅.
  

   
    q forces that, for all α < β in Ḃ, there is a
    γ∈ (A ∖β + 1) such that q_α, γ
    and q_β, γ are in Ġ.
  

  
    Fix r ≤ q and α < β such that r forces both α
    and β to be in Ḃ. By the definition of Ḃ, we may
    assume that r extends both q_α and q_β. It then suffices
    to find a γ∈ (A ∖β + 1) such that r, q_α, γ,
    and q_β, γ all have a common extension s. By construction, the
    families ⟨ u_⟨α, γ⟩∖
    u_⟨α⟩ |  γ∈ (A ∖β + 1) ⟩
    and ⟨ u_⟨β, γ⟩∖ u_⟨β⟩ |  γ∈ (A ∖β + 1) ⟩ each consist of pairwise
    disjoint sets. We can therefore find a γ∈ (A ∖β + 1)
    such that (u_⟨α, γ⟩∖
    u_⟨α⟩) ∩ (r) = ∅ and
    (u_⟨β, γ⟩∖
    u_⟨β⟩)  ∩ (r) = ∅.
    By item (2b) of Lemma <ref>, u_⟨α, γ⟩
    and u_⟨β, γ⟩ are aligned, hence by item (1) of Lemma <ref>, the stems in q_α,γ and q_β,γ match whenever their domains intersect. Now apply Lemma <ref> to r and
    {q_α, γ, q_β, γ}
    to find a single condition s extending all three conditions.
    This is the condition that we had sought.
  

   
    q forces that, for all α < β in Ḃ,
    
    φ̇_α(k,m) = φ̇_β(k,m)

    for every k ∈ω∖ k^* and m ≤min({ġ_α(k), ġ_β(k)}).
  

  
    Let G be P-generic with q ∈ G. Work in V[G]. Fix
    α < β in B. By Claim
    <ref>, we can find γ∈ (A ∖β + 1) such
    that q_α, γ and q_β, γ are in G. This implies that
    
      
  * g_α≤ g_γ,
      
  * g_β≤ g_γ, and
      
  * φ_α(k,m) = φ_γ(k,m) = φ_β(k,m) for all k ≥ k^* and m ≤min{g_α(k),
      g_β(k)}.
    
    The claim follows.
  
  Hence if G is P-generic with q ∈ G, then we may define a function
  ψ : ω×ω→ω trivializing Φ as follows.
  For all (k,m) ∈ω×ω, if there is an α∈ B with
  m ≤ g_α(k), then let ψ(k,m) =
  φ_α(k,m) for any such α. Note that, by Claim <ref>,
  if k ≥ k^*, then the value of ψ(k,m) is independent of our choice of
  α. If there is no such α∈ B, let ψ(k,m)=0 (or any other integer). It is then straightforward to verify that ψ does in fact
  trivialize Φ, thus completing the proof of the theorem.




§ HECHLER FORCING AND LIM^2 𝐀


In this section, we prove the n = 2 case of our Main Theorem, which contains
most of the key ideas of the general proof but is significantly less complex.
We begin with some preliminary observations.

Suppose that Φ = ⟨φ_fg : I(f ∧ g) →Z |   f,g ∈^ωω⟩ is a 2-coherent family of functions.
Recall that Φ determines a function ∂^1Φ taking each (f,g,h)∈ (^ωω)^3 to the function

    φ_gh - φ_fh + φ_fg : I(f ∧ g ∧ h)
      →Z





  


For simplicity, in what follows we write e for the difference-function ∂^nΦ whenever Φ and n are clear. Observe that when Φ is 2-coherent, every e(f,g,h) is finitely supported; in this case, we write 𝚎(f,g,h) for the restriction of e(f,g,h) to its support.

Recall also that, by the lemmas in Section <ref>, Φ is trivial
if and only if there exists a
≤^*-cofinal family F ⊆^ωω and an alternating family

    ⟨ψ_fg:I(f ∧ g) →Z |   f,g ∈ F ⟩

of finitely supported functions such that
for all f,g,h ∈ F

    e(f,g,h) = (ψ_gh - ψ_fh + ψ_fg) I(f∧ g∧ h).

When the functions in question are from an enumerated sequence ⟨ f_α|α < κ⟩ in ^ωω, we will often write e(α, β, γ) in place of e(f_α, f_β, f_γ), and
φ_αβ in place of φ_f_α f_β,
and so on. In such cases, due to the fact that all of our families of functions
will be alternating, it will suffice to deal only with functions
φ_αβ for α < β and e(α, β, γ)
for α < β < γ, since these determine the rest of the functions
in the relevant families. A similar statement will hold in the general case
in Section <ref>.

 
  Suppose that κ is a weakly compact cardinal, and let P be a
  finite-support iteration of Hechler forcing of length κ. Then V^P“lim^2 𝐀 = 0.”



  As in the proof of Theorem <ref>, for all α < κ, let
  ġ_α be a nice P-name for the Hechler real added at the α^th stage of ℙ. Much as before, it will suffice to consider 2-coherent families in V^P indexed
  by pairs of functions from ⟨ġ_α|α < κ⟩.
  Therefore fix a condition p_0 ∈P and a sequence of P-names
  Φ̇ = ⟨φ̇_αβ:I(ġ_α∧ġ_β) →Z |  α < β < κ⟩ forced
  by p_0 to be a 2-coherent family. We will find a q ≤ p_0 which forces
  Φ̇ to be trivial.

  Let A_0 = κ∖ (max((p_0)) + 1). Again, much as before, for all α < β < γ in A_0,
  there exists a condition q_α, β, γ≤ p_0 such that
  q_α, β, γ⊩_P“ġ_α≤ġ_β≤ġ_γ" and q_α, β, γ decides the value of
  𝚎̇(α, β, γ) to be  equal to some ϵ_α, β, γ∈ V.
  This condition exists because ė(α, β, γ) is forced by p_0 to
  be a finitely supported function. 
  
  
  Thin out A_0 to an unbounded A_1 such that
  ϵ_α, β, γ equals some fixed ϵ for all
  ⟨α, β, γ⟩∈ [A_1]^3.

  Now apply Lemma <ref> to ⟨ q_α, β, γ |  ⟨α, β, γ⟩∈ [A_1]^3 ⟩ to find
  an unbounded A ⊆ A_1
  together with sets u_∅, ⟨ u_⟨α⟩ |  α∈ A ⟩, and ⟨ u_⟨α, β⟩ |  α < β∈ A ⟩, a natural number ℓ, and stems
  ⟨ s_i | i < ℓ⟩ as in the statement of the lemma. Define
  conditions q_∅, ⟨ q_α|α∈ A ⟩, and
  ⟨ q_α, β|α < β∈ A ⟩ as follows.
  First, for any α < β < γ in A let
  q_∅ = q_α, β, γ u_∅. Next,
  for each fixed α∈ A, choose β < γ in A with
  β > α and let q_α = q_α, β, γ
  u_⟨α⟩. Finally, for fixed α < β in A,
  choose a  γ∈ A with γ > β and let
  q_α, β = q_α, β, γ
  u_⟨α, β⟩. By item (3) of Lemma <ref>, these definitions
  are independent of all of our choices.

  Let q = q_∅, and note that q ≤ p_0. We claim that q forces Φ̇ to be trivial.
  This we argue by first partitioning A into two disjoint and unbounded subsets, Γ_1 and
  Γ_2. Let Ḃ be a P-name for the set of
  α∈Γ_1 such that q_α∈Ġ, where Ġ is the canonical name for the ℙ-generic filter. The proofs of the
  next two claims follow those of Claims <ref>
  and <ref> almost verbatim, so we omit them.

   
    q ⊩_P“Ḃ is unbounded in κ."
  

   
    q forces that, for all α < β in Ḃ, there is a
    γ∈ (Γ_2 ∖β + 1) such that
    q_α, γ and q_β, γ are in Ġ.
  

   
    q forces the following to hold in V^P: Suppose that
    τ is in [Ḃ]^3 and ⟨α_σ|σ∈ [τ]^2 ⟩
    is such that, for all σ∈ [τ]^2 and all η∈σ,
    
      
  * α_σ∈Γ_2 ∖ (η + 1), and
      
  * q_η, α_σ∈Ġ.
    
    Then there is an α_τ in A ∖(max{α_σ|σ∈ [τ]^2} + 1)
    such that, for all σ∈ [τ]^2 and η∈σ,
    we have q_η, α_σ, α_τ∈Ġ.
  

  
    Fix τ∈ [Γ_1]^3, {α_σ|σ∈ [τ]^2},
    and r ≤ q such that r forces τ and {α_σ|σ∈ [τ]^2} to be as in the premise of the claim.
    Much as before, we may assume that r extends q_η, α_σ
    for all σ∈ [τ]^2 and η∈σ. By construction,
    for all such σ and η, the sequence ⟨ u_⟨η,
    α_σ, γ⟩∖ u_⟨η, α_σ⟩ |  γ∈ (A ∖α_σ
    + 1) ⟩ consists of pairwise disjoint sets. Hence there exists
    an α_τ∈ A ∖(max{α_σ|σ∈
    [τ]^2} + 1) such that
    
    (u_⟨η, α_σ, α_τ⟩∖
          u_⟨η, σ⟩) ∩(r) = ∅

    for all σ∈ [τ]^2 and η∈σ. Observe that,
    for any σ, ρ∈ [τ]^2, η∈σ, and ξ∈ρ,
    the sets {η, α_σ} and {ξ, α_ρ} are aligned
    (it was to ensure this alignment that we partitioned A into the
    disjoint sets Γ_1 and Γ_2). Therefore, by item (2b) of Lemma
    <ref>, the sets u_⟨η, α_σ,
    α_τ⟩ and u_⟨ξ, α_ρ, α_τ⟩ are aligned, hence by item (1) of Lemma <ref>
    the conditions q_η, α_σ, α_τ and
    q_ξ, α_ρ, α_τ are compatible, with identical stems
    wherever their domains intersect. Now apply Lemma <ref>
    to ⟨ q_η, α_σ, α_τ |  σ∈ [τ]^2,  η∈σ⟩ and r to find a single condition s ∈P simultaneously
    extending all of these conditions. This s forces α_τ to be as
    desired.
  

  We now turn more directly to the argument that q forces Φ̇ to be trivial.
  Let G be a P-generic filter with q ∈ G; work in V[G], and let
  B and Φ be the realizations of Ḃ and Φ̇. Since B is cofinal in κ, the family {g_η|η∈ B} is ≤^*-cofinal in ^ωω. Therefore it will suffice to find a family
  Ψ=⟨ψ_ηξ:I(g_η∧ g_ξ)
  →Z |  η < ξ∈ B ⟩ of finitely
  supported functions such that,
  for all η_0 < η_1 < η_2 in B,
  
    e(η_0, η_1, η_2) = (ψ_η_1 η_2
      - ψ_η_0 η_2 + ψ_η_1 η_2) I(g_η_0∧
      g_η_1∧ g_η_2).


  Using Claim <ref>, choose ordinals ⟨α_σ|σ∈ [B]^2 ⟩ such that α_σ∈ (Γ_2 ∖η + 1) and q_η, α_σ∈ G for all σ∈ [B]^2
  and all η∈σ. Then, using
  Claim <ref>, choose ordinals ⟨α_τ|τ∈ [B]^3 ⟩ such that α_τ∈ (A ∖α_σ + 1) and
  q_η, α_σ, α_τ∈ G for all τ∈ [B]^3, all
  σ∈ [τ]^2, and all η∈σ. Together these choices ensure that
  g_η≤ g_α_σ≤ q_α_τ
  and 𝚎(η, α_σ, α_τ) = ϵ for all τ∈ [B]^3 and σ∈ [τ]^2 and η∈σ.

  Now for arbitrary elements η < ξ in B let ψ_ηξ = e(η, ξ, α_{η,ξ}).
  Since g_η and  g_ξ are both less than or equal to g_α_{η,ξ}, the domain
  of ψ_ηξ is in fact I(g_η∧ g_ξ), as desired.
  We claim that the family Ψ so defined witnesses the triviality of Φ.

  To see this, let η_0 < η_1 < η_2 be arbitrary elements of B.
  To simplify notation, let α_i = η_i and α_ij =
  α_{η_i, η_j} for i < j < 3, and let α_012 =
  α_{η_0, η_1, η_2}. We then have the following series of equations, each of which follows immediately from an expansion of expressions followed by a cancellation of like terms:
  
    𝐚_012
        e(α_1, α_2, α_012)  - e(α_0, α_2, α_012)
        + e(α_0, α_1, α_012)  - e(α_0,α_1,α_2)     = 0,    
    𝐚_12
         e(α_2, α_12, α_012)  - e(α_1, α_12, α_012)
         + e(α_1, α_2, α_012)  - e(α_1,α_2,α_12)     = 0,    
    𝐚_02
        e(α_2, α_02, α_012) - e(α_0, α_02, α_012)
        + e(α_0, α_2, α_012) - e(α_0,α_2,α_02)     = 0,    
    𝐚_01
        e(α_1, α_01, α_012) - e(α_0, α_01, α_012)
        + e(α_0, α_1, α_012) - e(α_0,α_1,α_01)     = 0.

  The logic of the labeling is as follows: the operative indices in
  𝐚_012 are 0,1,2, and 012. The operative indices in
  𝐚_12 are 1,2,12, and 012; similarly for 𝐚_02
  and 𝐚_01. Here we have preferred readable equations to perfectly
  rigorous ones and have therefore omitted restriction-notations; the essential
  observation about the domains of the above functions is simply that
  I(g_α_0∧ g_α_1∧ g_α_2) is a subdomain of
  every one. This is because g_η≤ g_α_σ≤ g_α_τ for every
  τ∈ [B]^3, σ∈ [τ]^2, and η∈σ.

  By construction, the restriction of each of the first two terms of 𝐚_12, 𝐚_02,
  and 𝐚_01 to their support is equal to e.
  In consequence, these terms all cancel in the sum
  𝐚_12-𝐚_02+𝐚_01-𝐚_012, which reduces in turn,
  via cancellation of the third terms of 𝐚_12, 𝐚_02,
  and 𝐚_01 with the like terms in 𝐚_012, to
  
    e(α_0,α_1,α_2)- e(α_1,α_2,α_12)+
        e(α_0,α_2,α_02)-
        e(α_0,α_1,α_01) =0.

  We may rewrite this equation as
  
    e(α_0, α_1, α_2) = (ψ_α_1 α_2
      - ψ_α_0 α_2 + ψ_α_1 α_2) I(g_α_0∧
      g_α_1∧ g_α_2).

  This is the relation we had desired; this concludes our proof.




§ HECHLER FORCING AND LIM^N 𝐀





 







In this section, we prove our Main Theorem.
We prepare for the proof by first building up
some technical machinery, frequently referring back to the proof of Theorem
<ref> for motivation. For the following sequence of definitions, let κ be a fixed regular uncountable cardinal. Ultimately, of course, κ will denote the weakly compact cardinal of our main theorem, but that hypothesis is irrelevant to Definitions and Claims <ref> through <ref>.


  For any nonempty τ in [κ]^<ω, a subset-initial segment
  of τ is a sequence σ_1 ⊆⋯⊆σ_m ⊆τ
  such that
  
    
  * m ≤ |τ| and
    
  * |σ_i| = i for all i with 1 ≤ i ≤ m.
  
  We write σ⃗⊲τ to indicate that
  σ⃗ is a subset-initial segment of τ. If m = |τ|, then
  we call σ⃗ = ⟨σ_1, ⋯, σ_m ⟩⊲τ a long string or
  long string for τ.


Suppose now that ⟨ g_α|α
< κ⟩ is an injective sequence of elements of ^ωω.  Suppose that for each positive integer n the family

    Φ_n = ⟨φ_α⃗:I(α⃗)→ℤ |  α⃗∈ [κ]^n ⟩

is n-coherent, where I(α⃗) = I(⋀_i < n  g_α_i)
for each such n and α⃗∈ [κ]^n. Let
Φ⃗ denote the family ⟨φ_α⃗ |  α⃗∈ [κ]^<ω,  α⃗≠∅⟩.
Suppose also that B ⊆κ is unbounded and, to each nonempty τ∈ [B]^<ω we have assigned
an ordinal α_τ < κ in such a way that

  
  * if τ = {η}, then α_τ = η and
  
  * if ρ⊊τ, then α_ρ < α_τ.

Given a nonempty τ∈ [B]^<ω and a subset-initial segment
σ⃗⊲τ, write α⃗[σ⃗]
to denote the sequence ⟨α_σ_i| 1 ≤ i ≤
|σ⃗| ⟩; note that this sequence is increasing by assumption.

For α⃗∈ [κ]^<ω of length at least two, let

    e^Φ⃗(α⃗) = ∑_i < |α⃗| (-1)^i
      φ_α⃗^i

When the family Φ⃗ is clear from context, it will
be omitted from the superscript above. Similarly, we will continue to notationally suppress the restriction of sums of functions to the intersection of their domains.
Since each family Φ_n is n-coherent, the function e(α⃗) is finitely supported for
any α⃗∈ [κ]^<ω of length at least two. We write 𝚎(α⃗) for the restriction of e(α⃗) to its support.

We now record a series of formal equalities. First, for all α⃗∈ [κ]^<ω of length at least three, let

    𝖽 e(α⃗) = ∑_i<|α⃗|(-1)^i e(α⃗^i).

Observe that when the right-hand side of the above equation is fully expanded,
its terms will cancel; 𝖽 e is, after all, a composition of differentials.
Hence 𝖽 e(α⃗) is well-defined and equals 0 for all α⃗∈ [κ]^<ω of length at least three.
If L is some linear combination of the form

    ∑_i<ℓ a_i  e(α⃗_i)

with all α⃗_i of length at least three then let

    𝖽 L=∑_i<ℓ a_i 𝖽 e(α⃗_i).

Similarly, if j is less than |α⃗_i| for all i then let

    L^j=∑_i<ℓ a_i  e(α⃗^j_i).

Finally, here dropping the assumption that each α⃗_i has length at
least three, for any β⃗∈ [κ]^<ω with α⃗_i <
β⃗ for all i < ℓ, let

    L*β⃗=∑_i<ℓ a_i  e(α⃗_i, β⃗)

 where e(α⃗_i, β⃗) = e(α⃗_i
^⌢β⃗). If β⃗ = ⟨β⟩, then
we will abuse notation and write L*β and e(α⃗_i, β)
instead of L*⟨β⟩ and e(α⃗_i, ⟨β⟩).
Finally, if j is less than |α⃗_i| for all i then let

    L^j=∑_i<ℓ a_i  e(α⃗^j_i)


For integers n≥ 2 we now recursively define interrelated


  * expressions 𝒜^Φ⃗_n(ρ) parametrized by ρ∈ [B]^n,

  * expressions 𝒮^Φ⃗_n(τ) and
𝒞^Φ⃗_n(τ) parametrized by τ∈ [B]^n+1, and

  * statements 𝔲^Φ⃗_n(τ) parametrized by τ∈ [B]^n+1.

Again when the family Φ⃗ is clear from context it is omitted from superscripts. In fact the above expressions will depend also on the
collection ⟨α_τ|τ∈ [B]^<ω⟩ fixed earlier, but this dependence is always plain enough that we ignore it, notationally, entirely.

To begin, let

    𝒜_2(ρ) = e(ρ, α_ρ)

for each ρ∈ [B]^2. Recall that we interpret elements of [κ]^<ω
as finite increasing sequences, so, for example, if ρ = ⟨β_0, β_1 ⟩,
then e(ρ, α_ρ) denotes e(⟨β_0, β_1, α_ρ⟩).
Next, given n with 2 ≤ n < ω and τ∈ [B]^n+1, if
𝒜_n(τ^i) has been defined for all i ≤ n, let

    𝒮_n(τ)    = 𝖽 e(τ, α_τ) -
      ∑_i < n + 1 (-1)^i 𝖽[𝒜_n(τ^i) * α_τ], 
    𝒞_n(τ)    = e(τ) - ∑_i < n + 1
      (-1)^i 𝒜_n(τ^i),

and let 𝔲_n(τ) denote the conjunction of the following two
statements:

  
  * There exists an ϵ such that 𝚎(α⃗
  [σ⃗]) = ϵ for every long string σ⃗⊲τ.
  
  * For all nonempty ρ, σ with ρ⊊σ⊆τ, we have g_α_ρ≤ g_α_σ.

Lastly, let

    𝒜_n+1(τ) = (-1)^n+1𝒞_n(τ) * α_τ.


Let us pause to connect these definitions with the proof of
Theorem <ref>.  There B was an unbounded subset of κ. For ρ∈ [B]^2, we set ψ_ρ equal to 𝒜_2(ρ). Then by deducing equation
(<ref>) for an arbitrary τ∈ [B]^3, we showed that this assignment of values was as desired.
In the language just introduced, equation (<ref>) translates  to 𝒞_2(τ) = 0. Similarly, the expression 𝐚_12 - 𝐚_02 + 𝐚_01 -
𝐚_012 corresponds to -𝒮_2(τ). By the definition of B, the condition
𝔲_2(τ) holds for all τ∈ [B]^3; the relation
𝒞_2(τ) = -𝒮_2(τ) then followed immediately. The terms
in 𝒮_2(τ) are all of the form 𝖽 e(β⃗), hence 𝒮_2(τ) = 0. This, in essence, was the deduction that 𝒞_2(τ) = 0.

The following two lemmas are easily proven by induction, so their proofs are left
to the reader.

 
  For all n with 2 ≤ n < ω, all ρ∈ [B]^n, and all
  τ∈ [B]^n+1, the expressions 𝒜_n(ρ),
  𝒮_n(τ), and 𝒞_n(τ) are all of the form
  
    ∑_i < ℓ a_i e(α⃗_i),

  where, for all i < ℓ, we have
  
    
  * a_i ∈Z,
    
  * α⃗_i ∈ [κ]^n+1, and
    
  * α⃗_i is of the form σ_0
    ^⌢⟨α_σ_j| 1 ≤ j ≤ (n+1 - |σ_0|)
    ⟩,
    where
    
      
  * 0 < |σ_0| ≤ n + 1 and,
      if |σ_0| < n + 1, then 1 < |σ_1| ≤ n+1,
      
  * if |σ_0| < n + 1, then σ_0 ⊆σ_1,
      
  * σ_j ⊊σ_j+1 for all 1 ≤ j < (n+1 -
      |σ_0|), and
      
  * letting k = (n + 1 - |σ_0|), we have σ_k ⊆ρ,
      in the case of 𝒜_n(ρ), and σ_k ⊆τ,
      in the case of 𝒮_n(τ) or 𝒞_n(τ).
    
  


The point of this lemma is that, although the expressions defining
𝒜_n(ρ), 𝒮_n(τ), 𝒞_n(τ), and
𝔲_n(τ) are constructed via a recursion referencing Φ⃗, the values of
𝒜_n(ρ), 𝒮_n(τ), and 𝒞_n(τ), and
the truth values of 𝔲_n(τ) only ever depend on Φ_n
and not on Φ_m for any m ≠ n. Hence we may meaningfully employ these expressions to argue as we do that V^ℙ“lim^n 𝐀 = 0” while only referencing a single family Φ_n at a time. Similarly, since the values of 𝒜_n(ρ),
𝒮_n(τ), and 𝒞_n(τ) depend on the ordinals
⟨α_σ|σ∈ [B]^≤ n+1⟩ but not on α_σ for
|σ| > n+1, verifications via these expressions that
lim^n 𝐀 = 0 will never require that any ordinal α_σ of longer index (|σ|>n+1) has yet been defined.

We can say more of 𝒮_n(τ) than in
the previous lemma:

 
  For all n with 2 ≤ n < ω and all τ∈ [B]^n+1,
  the expression 𝒮_n(τ) is of the form
  
    ∑_i < ℓ b_i 𝖽 e(β⃗_i),

  where b_i ∈Z and β⃗_i ∈ [κ]^n+2 for all
  i < ℓ. Since 𝖽 e(β⃗) = 0 for all
  β⃗∈ [κ]^n+2, it follows that 𝒮_n(τ) = 0.


The following is the main technical lemma regarding these formal expressions.
Recall that we often interpret an element τ∈ [κ]^n+1 has an increasing
sequence, so, for example, the expression I(τ) denotes
I(⋀_α∈τ g_α).

 
  Suppose that 2 ≤ n < ω, τ∈ [B]^n+1, and
  𝔲_n(τ) holds. Then
  
    𝒮_n(τ)=(-1)^n+1𝒞_n(τ).




  We proceed by induction on n, in fact establishing the following
  strengthening of the lemma, which we maintain as an inductive hypothesis:
  
    𝔲_n(τ)     induces a reduction of 𝒮_n(τ)
         to  (-1)^n+1𝒞_n(τ)  via 
    (1)    the cancellation of identical terms appearing
        with opposite sign
        in the expansion of 𝒮_n(τ), 
    (2)    the cancellation of terms of the form  e(α⃗
        [σ⃗])  in which σ⃗⊲τ is 
        a long string, on the principle that, in the presence of 𝔲_n(τ),  
        these terms are
        all equal when restricted to the intersection
        of their domains.

  Such cancellations will be referred to as cancellations of type (1) and type (2),
  respectively.

  These cancellations could conceivably alter the domain of 𝒮_n(τ). We first show that they do not; we show in particular that when 𝔲_n(τ) holds, the domain of both 𝒮_n(τ)  and 𝒞_n(τ) is I(τ).
  By Lemma <ref>, every term in each of 𝒮_n(τ)
  and 𝒞_n(τ) is an integer multiple of e(α⃗),
  where α⃗ is of the form α⃗(σ_0) ^⌢⟨α_σ_1, ⋯, α_σ_k⟩, where
  the sequence ⟨σ_0, ⋯, σ_k ⟩ is as described therein.
  In particular, σ_0 ⊆σ_j ⊆τ for all
  j ≤ k. The condition 𝔲_n(τ) then ensures that g_η≤
  g_α_σ_j for all η∈σ_0 and j ≤ k.
  It follows that (e(α⃗)) = I(σ_0)
  ⊇ I(τ) and hence that the domains of
  𝒮_n(τ) and 𝒞_n(τ) both contain
  I(τ). Since both expressions explicitly include
  the term e(τ), whose domain is I(τ), the desired equalities hold.

  Now observe that the expression 𝒮_n(τ) can be rewritten as
  follows:
  
    𝒮_n(τ)
         =     𝖽 e(τ,α_τ) - ∑_i<n+1(-1)^i 𝖽 [𝒜_n(τ^i)*α_τ ] 
    
         =     𝖽 e(τ,α_τ)-∑_i<n+1(-1)^i ∑_j<n+2 (-1)^j [𝒜_n(τ^i)*α_τ]^j 
    
         =     𝖽 e(τ,α_τ)-∑_i<n+1(-1)^i ∑_j<n+1 (-1)^j [𝒜_n(τ^i)*α_τ]^j
         -∑_i<n+1(-1)^n+i+1𝒜_n(τ^i) 
    
         =     ∑_i<n+1(-1)^i e(τ^i,α_τ)-∑_i<n+1(-1)^i ∑_j<n+1 (-1)^j [𝒜_n(τ^i)*α_τ]^j
         +(-1)^n+1e(τ)-∑_i<n+1(-1)^n+i+1𝒜_n(τ^i) 
    ⋆   =     ∑_i<n+1(-1)^i e(τ^i,α_τ)-∑_i<n+1(-1)^i ∑_j<n+1 (-1)^j [𝒜_n(τ^i)*α_τ]^j
         +(-1)^n+1𝒞_n(τ)

  If type (1) and type (2) cancellations reduce the expression on the starred line to zero, then we will have shown
  𝒮_n(τ)=(-1)^n+1𝒞_n(τ) while maintaining our inductive hypothesis. This is our goal. We begin with the base case of n=2. This amounts simply to a more careful translation of the end of the proof of
  Theorem <ref> into our current terminology.

Since 𝒜_2(τ^i) * α_τ
  = e(τ^i, α_τ^i, α_τ) for any  fixed i < 3 and hence
  [𝒜_2(τ^i) * α_τ]^2 = e(τ^i, α_τ), the starred line in this case rearranges to
  
    ∑_i < 3 (-1)^i e(τ^i, α_τ) - ∑_i < 3
        (-1)^i e(τ^i, α_τ) -   ∑_i < 3 (-1)^i ∑_j < 2
        (-1)^j[𝒜_2(τ^i) * α_τ]^j 
    
        =    ∑_i < 3 (-1)^i+1∑_j < 2 (-1)^j[𝒜_2(τ^i) * α_τ]^j

 The only cancellation above is of type (1).

  Fix i < 3 and j < 2 and observe that [𝒜_2(τ^i)
  * α_τ]^j is of the form e(η, α_τ^i, α_τ),
  with η∈τ^i. But then σ⃗ = ⟨{η},
  τ^i, τ⟩ is a long string for τ and e(η, α_τ^i,
  α_τ) = e(α⃗[σ⃗]). Hence by
  𝔲_2(τ) there is a fixed ϵ such that the restriction of each such term to the common domain I(τ) is equal to ϵ.
  The starred line thus reduces further to
  
    ∑_i < 3 (-1)^i+1∑_j < 2 (-1)^j[𝒜_2(τ^i) * α_τ]^j
        = ∑_i < 3 (-1)^i + 1 (ϵ - ϵ) = 0,

  as desired. The reduction is evidently by way of cancellations of type (2).
  This completes the base case.

  Now assume that n > 2 and that the inductive hypothesis holds for
  n - 1. We need two claims.

  
    For all i < n+1,
    
    ∑_j<n+1 (-1)^j [𝒜_n(τ^i)*α_τ]^j=(-1)^n
          𝒮_n-1(τ^i)*α_τ.

  

  
    Rewrite the sum ∑_j<n+1 (-1)^j [𝒜_n(τ^i)*α_τ]^j
    in the following sequence of steps; each simply consists of an application
    of the definitions of the expressions under consideration:
    
    ∑_j<n+1 (-1)^j [(-1)^n𝒞_n-1
            (τ^i)*α_τ^i]^j*α_τ
    
            =     (-1)^n∑_j<n+1 (-1)^j[ [e(τ^i) -
            ∑_k<n(-1)^k𝒜_n-1
            ((τ^i)^k)]*α_τ^i]^j*α_τ
    
            =     (-1)^n[𝖽 e(τ^i,α_τ^i)-
            ∑_k<n(-1)^k 𝖽 [𝒜_n-1((τ^i)^k)*α_τ^i]
            ]*α_τ
    
            =     (-1)^n𝒮_n-1(τ^i)*α_τ

  

  
    For all i < n + 1, the condition 𝔲_n(τ) implies that
    
    (-1)^n𝒮_n-1(τ^i)*α_τ =
          𝒞_n-1(τ^i)*α_τ

    via cancellations of type (1) and of type (2).
  

  
    By the inductive hypothesis applied to 𝒮_n-1(τ^i), we know
    that the terms appearing in 𝒮_n-1(τ^i) but not in
    (-1)^n𝒞_n-1(τ^i) pair off in pairs either of type (1), meaning that the pair consists of identical terms
    with opposite signs, or of type (2), meaning that the pair is of the form
    (e(α⃗[σ⃗_0]), -e(α⃗[σ⃗_1])),
    where σ⃗_0 and σ⃗_1 are long strings for τ^i.

    If such a pair (t, -t) is of type (1), then t * α_τ and
    -t * α_τ also form a type (1) canceling pair in 𝒮_n-1(τ^i) * α_τ. Notice also that if σ⃗ is a long
    string for τ^i then σ⃗^* = σ⃗^⌢⟨τ⟩ is a long string for τ and α⃗[σ⃗^*]
    = α⃗[σ⃗] ^⌢⟨α_τ⟩.
    Therefore, if (e(α⃗[σ⃗_0]),
    -e(α⃗[σ⃗_1])) is a type (2) pair of terms from
    𝒮_n-1(τ^i) then
    e(α⃗[σ⃗_0]) * α_τ = e(α⃗[σ⃗_0^*])
    and -e(α⃗[σ⃗_1]) * α_τ = -e(α⃗
    [σ⃗_1^*]). The condition 𝔲_n(τ) then implies that these terms are
    equal to some ϵ and -ϵ, respectively, and thus cancel in
    𝒮_n-1(τ^i) * α_τ in a type (2) manner.

    The terms of 𝒮_n-1
    (τ^i) * α_τ that remain after these cancellations are precisely those of the form t * α_τ, where t
    appears in (-1)^n𝒞_n-1(τ^i). Hence
    𝒮_n-1(τ^i) * α_τ = (-1)^n 𝒞_n-1(τ^i)
    * α_τ. Hence (-1)^n 𝒮_n-1(τ^i) * α_τ
    = 𝒞_n-1(τ^i) via cancellations of type (1) and of type (2).
  

  By Claims <ref> and <ref> the starred line above now reduces to
  the following:
  
    ∑_i<n+1(-1)^i e(τ^i,α_τ)-∑_i<n+1(-1)^i
          [𝒞_n-1(τ^i)*α_τ ] 
    
          =     ∑_i<n+1(-1)^i e(τ^i,α_τ)-∑_i<n+1(-1)^i
          [ e(τ^i,α_τ)-∑_j<n(-1)^j𝒜_
          n-1((τ^i)^j)*α_τ]
    
          =     ∑_i<n+1∑_j<n(-1)^i+j𝒜_n-1((τ^i)^j)*α_τ

  Observe that the only cancellation above is of type (1).
  Now the key observation is that to each (τ^i)^j with i≤ j<n there
  corresponds a (τ^i')^j' with j'<i'<n+1, and vice versa. Namely, when
  i'=j+1 and j'=i then (τ^i)^j=(τ^i')^j'. In the above sum, these each
  associate to the signs (-1)^i+j and (-1)^i+j+1, respectively. We therefore
  conclude by  rewriting that sum as
  
    ∑_i≤ j<n(-1)^i+j𝒜_n-1((τ^i)^j)*α_τ+
        ∑_j<i<n+1(-1)^i+j𝒜_n-1((τ^i)^j)*α_τ=0,

  where again all cancellations are of type (1). This completes the induction step. It therefore completes the proof of Lemma <ref>.


We are now ready to prove our main result, which we restate here for convenience.


Let κ∈ V be a weakly compact cardinal, and let ℙ denote a length-κ finite-support iteration of Hechler forcings. Then 
    V^ℙ“ lim^n𝐀=0 for all n>0.”




  We will show that any n-coherent family of functions in V^ℙ is trivial.
  Since we have already done so for n = 1, we will assume in what follows that n > 1.
  For all α < κ, let
  ġ_α be a nice P-name for the Hechler real added at the α^th stage of ℙ. As in the n=1 and n=2 cases, it will suffice to consider n-coherent families in V^P indexed
  by n-tuples of functions from ⟨ġ_α|α < κ⟩.
  Therefore fix a condition p_0 ∈P and a family of P-names
  Φ̇_n = ⟨φ̇_α⃗:İ(α⃗) →Z |  α⃗∈ [κ]^n⟩ forced
  by p_0 to be an n-coherent family of functions. We will find a q ≤ p_0 which forces
  Φ̇_n to be trivial.

  Let A_0 = κ∖ (max((p_0)) + 1). Much as before, for all α⃗∈[A_0]^n+1
  there exists a condition q_α⃗≤ p_0 such that
  q_α⃗⊩_P“ġ_α_0≤…≤ġ_α_i≤…≤ġ_α_n" and
  q_α⃗ decides the value of
  𝚎̇(α⃗) to be  equal to some ϵ_α⃗∈ V.
  
  
  
  
  Thin out A_0 to an unbounded A_1 such that
  ϵ_α⃗ equals some fixed ϵ for all
  α⃗∈ [A_1]^n+1.

  Now apply Lemma <ref> to ⟨ q_α⃗ |  α⃗∈ [A_1]^n+1⟩ to find an unbounded A ⊆ A_1
  together with sets ⟨ u_α⃗ |  α⃗∈ [A]^≤ n⟩, a natural number ℓ, and stems ⟨ s_i | i < ℓ⟩
  as in the statement of the lemma.
  Next, define conditions ⟨ q_α⃗ |  α⃗∈ [A]^≤ n⟩
  as follows: for each α⃗ in [A]^≤ n let β⃗ be
  an element of [A]^n+1 such that α⃗⊑β⃗
  and let q_α⃗ = q_β⃗ u_α⃗.
  As usual, by item (3) of Lemma <ref>, these definitions
  are independent of all of our choices of (n+1)-tuples β⃗.
  We will sometimes abuse notation and write, for example, q_α instead of
  q_⟨α⟩. 
  
  
  
  

  Let q = q_∅, and note that q ≤ p_0. We claim that q forces Φ̇ to be trivial.
  This we argue by first partitioning A into n + 1 disjoint and unbounded subsets ⟨Γ_i| 1≤ i≤ n+1⟩. Let Ḃ be a P-name for the set of
  α∈Γ_1 such that q_α∈Ġ, where Ġ is the canonical name for the ℙ-generic filter. By exactly the same reasoning as in the proofs of Theorem <ref> and Theorem <ref>,
  
    q ⊩_P“Ḃ is unbounded in κ."


 
   Fix τ∈ [κ]^n+1. The condition q forces the following to hold
   in V^ℙ:

   Suppose that m and ⟨α_σ |  σ∈[τ]^<m
   and σ≠∅⟩ are such that
   
     
  * 1< m≤ n+1,
     
  * α_{η} = η for all η∈τ,
     
  * α_ρ<α_σ whenever ρ is a proper subset of σ,
     
  * α_σ∈Γ_|σ| for all nonempty
     σ∈[τ]^<m, and
     
  * for any 1≤ℓ< m and subset-initial segment σ⃗⊲τ of length ℓ, we have q_α⃗[σ⃗]∈Ġ. In particular, η∈Ḃ for all η∈τ.
   
   Then there exists a sequence ⟨α_σ |  σ∈[τ]^m⟩ of elements of Γ_m which
   together with ⟨α_σ |  σ∈([τ]^<m\{∅})⟩
   satisfies
   
     
  * α_ρ<α_σ whenever ρ is a proper subset of σ, and
     
  * for any subset-initial segment σ⃗⊲τ
     of length m, we have q_α⃗[σ⃗]∈Ġ.
   
 

 
   Fix an m and ⟨α_σ |  σ∈[τ]^<m\{∅}⟩
  and an r≤ q such that r forces m and ⟨α_σ |  σ∈[τ]^<m\{∅}⟩ to be as in the premise of
  the claim. In particular, r forces that q_α⃗[σ⃗] is in
  Ġ for every σ⃗⊲τ as in the premise of the claim.
  As before, we may assume that r extends all such q_α⃗[σ⃗].
  For each σ∈[τ]^m and σ⃗⊲σ of length m-1,
  observe that the sequence ⟨ u_α⃗[σ⃗]^⌢γ\ u_α⃗[σ⃗] |  γ∈Γ_m\
  (max(α⃗[σ⃗])+1)⟩ consists of pairwise disjoint sets.
  Therefore, we can choose an α_σ∈Γ_m
  so that (u_α⃗[σ⃗]^⌢α_σ\
  u_α⃗ [σ⃗])∩dom(r)=∅ for all
  σ⃗⊲σ of length m-1. This then defines a
  family of pairwise-aligned sequences ⟨α⃗[σ⃗]|σ⃗⊲τ is of length m⟩, since for any
  α∈Γ_k in the intersection of two such α⃗[σ⃗]
  and α⃗[ρ⃗],
  
    |α⃗[σ⃗]∩α|=|α⃗[ρ⃗]∩α|=k.

  As before, this implies that the family ⟨ q_α⃗[σ⃗] |  σ⃗⊲τ is of length m⟩ consists of
  pairwise compatible conditions, with identical stems wherever their domains intersect.
  Applying Lemma <ref> to this collection together with
  r then yields a lower bound s∈ℙ for all of these conditions,
  thereby witnessing the conclusion of the claim.
 

 As in the proof of Theorem <ref>, we will conclude our argument
 in V[G], where G is a P-generic filter containing q. Let B
 be the realization of Ḃ and Φ_n the realization of
 Φ̇_n in V[G]. For each nonempty σ∈
 [B]^≤ n+1, we will specify an ordinal α_σ < κ in such a way
 that the collection ⟨α_σ |  σ∈ [B]^≤ n+1⟩ satisfies
 the following:
 
   
  * α_{η} = η for all η∈ B,
   
  * α_ρ < α_σ whenever ρ is a proper subset of
   σ,
   
  * α_σ∈Γ_|σ| for all nonempty σ∈
   [B]^≤ n + 1, and
   
  * for every τ∈ [B]^n+1 and every subset-initial segment
   σ⃗⊲τ, we have q_α⃗[σ⃗]∈ G.
 

 The construction of ⟨α_σ |  σ∈ [B]^≤ n+1⟩
 proceeds via a straightforward recursion on |σ|, invoking
 Claim <ref>.

 The n-coherent family Φ_n and collection ⟨α_σ |  σ∈ [B]^≤ n + 1\{∅}⟩ determine
 expressions 𝒜_n(ρ) for all ρ∈ [B]^n and
 expressions 𝒮_n(τ) and 𝒞_n(τ) and statements
 𝔲_n(τ) for all τ∈ [B]^n+1. Note that our choices of
  q, B, and the sequence ⟨α_σ |  σ∈ [B]^≤ n + 1⟩
 ensure that 𝔲_n(τ) holds for all τ∈ [B]^n+1.

 For each ρ∈ [B]^n, let ψ_ρ = 𝒜_n(ρ).
 It follows from the definition of 𝒜_n(ρ) and the fact that 𝔲_n(τ)
 holds for all τ∈ [B]^n+1 that 𝒜_n(ρ)
 is a finitely-supported function with domain
 I(ρ). To
 show that Φ_n is trivial, it will suffice to show that
 
    e(τ) = ∑_i < n+1 (-1)^i ψ_τ^i

 for all
 τ∈ [B]^n+1. Fix such a τ. The above equation is easily seen to be equivalent to the assertion that 𝒞_n(τ) = 0.
 By Lemma <ref> and the fact that 𝔲_n(τ) holds, 𝒮_n(τ) = (-1)^n+1𝒞_n(τ).
 By Lemma <ref>, 𝒮_n(τ) = 0. In consequence, 𝒞_n(τ) = 0. This shows equation (<ref>) for an arbitrary τ hence Φ_n is trivial.




§ CONCLUSION


Several natural questions follow immediately from the above results. The first of these is whether the assumption of a weakly compact cardinal is necessary for
the conclusion of the Main Theorem. As noted in Remark <ref> above,
this was answered in the negative by the authors together with Michael Hrušák in <cit.>,
where they showed that lim^n 𝐀 = 0 for all n > 0 after the addition of ℶ_ω-many Cohen reals.
Closely related is the question of whether a large continuum is necessary for the conclusion of the Main Theorem.
 
What is the minimum value of the continuum compatible with the statement “lim^n𝐀=0  for all n>0"?

By the results of <cit.>, that minimum value is at least ℵ_2. By the
aforementioned result in <cit.>, ℵ_ω+1 is an upper bound
for the answer to Question <ref>.

Our Main Theorem also lends the original, motivating questions a certain renewed charge:
 Is it consistent with the 𝖹𝖥𝖢 axioms (possibly modulo large cardinal assumptions) that strong homology is additive


  * on Polish spaces?

  * on locally compact metric spaces?

  * on metric spaces?


The extension V^ℙ of the Main Theorem is, of course, a candidate model for an affirmative answer to any of these questions, and indeed, as noted in Remark <ref>,
Bannister, Bergfalk, and Moore recently showed in <cit.> that strong homology is additive
on the class of locally compact Polish spaces in V^P. A word is in order here about the machinery of strong homology, which consists first in an assignment of a system of approximations to a given topological space X and second in an assignment of a homology group to X by way of the system of homology groups of its approximations <cit.>. Compact metric spaces figure within this framework as particularly tractable: they admit sequential systems of approximations. Indeed, the index-set ^ωω so central to all our considerations above arose as a countable product (induced by a countable topological sum) of just such a family of height-ω systems of approximations to n-dimensional Hawaiian earrings; the argument of <cit.> consists largely in correlating a broader class of ^ωω-indexed inverse systems to strong homology computations for locally compact Polish spaces, and in then showing that the present work's arguments apply to that broader class. In short, strong homology computations translate the ways that each of the bulleted classes above relate to “simpler” spaces to an associated family of index-sets; Question <ref> is perhaps largely one of what sorts of combinatorics these index-sets may or may not simultaneously support. Accordingly, the combinatorics of the interrelations among various partial orders may well play some role in its further solution (see, e.g., <cit.>). Through these interrelations, the vanishing of one system's higher derived limits may entail the vanishing of others'; Theorem 5.1 of <cit.> is an example of such a result.

At some broader level, Question <ref> is asking what sorts of continuities we may compatibly expect of homology functors on categories of topological spaces properly extending 𝖧𝖢𝖶, i.e., properly including the category of spaces homotopy equivalent to a CW-complex. For the question on what class of spaces may a homology theory be both strong shape invariant and additive? is at heart a question about the interactions of the inverse and direct limits associated to the first prospective property and the second, respectively. As mentioned, closely related is the question of whether the strong homology groups of a space are the direct limits of the strong homology groups of its compact subspaces; a highly canonical extension of Steenrod homology exists on any class for which the answer is yes. This is the case in <cit.>; see its introduction and <cit.> and <cit.> for further discussion.

Lastly, one of this paper's referees asked what happens if we replace our iteration P of
Hechler forcing with the standard length-κ finite support iteration
Q for forcing Martin's Axiom (𝖬𝖠) together with 2^ℵ_0 = κ.
We conjecture that, for all n > 0, lim^n 𝐀 = 0 will hold in V^Q as well, but our argument does not
directly generalize to prove this, since it makes essential use of the fact
that Hechler forcing is σ-centered (in particular, any finitely many
conditions with the same stem have a common lower bound). This is evident in
Lemmas <ref> and <ref>(1), which are
then used in the proof of Claim <ref>. There are straightforward
generalizations of Lemmas <ref> and <ref>
to arbitrary length-κ finite support iterations of σ-centered
forcings of size <κ. (In this more general context, if
S is a σ-centered poset and p ∈S, then s_p,
the stem of p, is interpreted as the unique j < ω such that
p ∈ S_j, where ⟨ S_j | j < ω⟩ is a fixed partition
of the underlying set of S into centered subsets.) With this in mind,
our proof adapts to show that, if κ is weakly compact and Q^* is the standard
length-κ finite support iteration for forcing 𝖬𝖠(σ-𝖼𝖾𝗇𝗍𝖾𝗋𝖾𝖽) +
2^ℵ_0 = κ, then lim^n 𝐀 = 0 for all n > 0.
The proof proceeds by considering n-coherent families indexed by n-tuples of
the generic reals ⟨ġ_α|α∈ B ⟩,
where B ∈ V is an unbounded subset of κ such that, for each
α∈ B, the α^th iterand of Q^* is a
Q^*_α-name for Hechler forcing and ġ_α is a name
for the corresponding Hechler real. We therefore close with the question of the full form of Martin's Axiom, and with thanks to the referee for asking it:


  Suppose that κ is a weakly compact cardinal and that Q is the standard
  length-κ finite support iteration for forcing 𝖬𝖠 + 2^ℵ_0 = κ.
  Is it the case that, in V^Q, lim^n 𝐀 = 0 for all n > 0?



Acknowledgements. This work began with a visit by Chris Lambie-Hanson to UNAM Morelia. The authors would like to thank both the institutions VCU and UNAM for their support for this visit. More particularly, many of this paper's most fundamental impulses are due to Michael Hrušák and grew out of conversations with him both before and during Chris's visit; the authors would like to thank him very especially. Jeffrey Bergfalk would like to thank Justin Moore and Jim West as well for much patient and formative instruction in the subject-matter of this paper. The authors would also like to thank Stevo Todorcevic for encouraging them to reduce their large-cardinal assumption from a measurable to a weakly compact, and for his several suggestions for how to do so. Finally, they would like to thank both referees for their extremely thorough and thoughtful readings, comments, and questions.

amsplain


