
\section{Introduction}

\subsection*{A} An \emph{almost disjoint family} is subset $\mathcal A$ of $[\nat]^\infty$, the infinite subsets of $\nat$, such that
any two elements $A, B$ of $\mathcal A$ are almost disjoint, i.e., $A\cap B$ is finite. A \emph{maximal almost disjoint} (short, mad) family is an almost disjoint family which is maximal among such families under $\subseteq$.
For instance, any partition of $\nat$ is a (trivial) mad family.

\medskip

Infinite mad families are usually constructed using the Axiom of Choice ($\ensuremath{\mathsf{AC}}$).\footnote{One can also obtain such families by forcing.}
Therefore, on the basis of the standard axioms of set theory ($\ZFC$) we can not say much about their possible definability. 
In 1969, not long after Cohen invented forcing, A.\ R.\ D.\ Mathias used a large cardinal axiom and forcing to construct a model of $\ZF$ where there are no mad families.
Shortly before, in 1968, he had shown that in Solovay's model (from \cite{solovay}) every set has the Ramsey property.
He then asked the question whether these two statements are related, specifically: Does `every set has the Ramsey property' imply `there are no infinite mad families'? 


In the same work (his unpublished thesis, see \cite{mathias-thesis}; he published somewhat different proofs later in \cite{mathias}) Mathias also showed that there are no analytic mad families (a subset of $[\nat]^\infty$ or more generally, a subset of a Polish space, is analytic if it is a continuous image of Baire space, $\nat^\nat$).
This is the best one can do in $\ZFC$ since in Gödel's constructible universe, there is a co-analytic mad family (this was shown by Miller \cite{miller2012}).

\medskip

In recent years, results about mad families have seen in a kind of renaissance.
The second author showed that there are no infinite mad families in Solovay's model \cite{solovay}.
Horowitz and Shelah showed that a model of $\ZF$ where no infinite mad families exist, just assuming that $\ZF$ is consistent, without using any large cardinal assumption \cite{horowitz-shelah}.

Neeman and Norwood \cite{neeman-norwood} and independently, Karen Bakke Haga and the present authors \cite{haga-schrittesser-toernquist} showed that under the Axiom of Determinacy ($\AD$, a natural alternative to $\ensuremath{\mathsf{AC}}$) there are no infinite mad families in $\mathbf{L}(\reals)$, and that under the Axiom of projective determinacy ($\PD$) there are no projective infinite mad families.
These results align with the overall tendency that sets in $\mathbf{L}(\reals)$ have similar properties under $\ZF$ plus $\AD$ as do analytic sets under just $\ZF$, or under $\ZFC$ if you prefer.

\medskip

\subsection*{B}
Mad families are venerable objects in mathematics,  relevant in set theory, topology, and theory of Banach spaces.
Over the years, it was suggested again and again to study variants where in the definition of a mad family, `finiteness' is replaced by some other notion of smallness,
i.e., by some \emph{ideal} $\mathcal I$ (in the set theoretical, not algebraic sense).
One thus arrives at the notion of an $\mathcal I$-mad family (see~\S\ref{s.prelim} for the precise definition).
When $\mathcal I = \fin$, the ideal of finite sets, the notion of an $\mathcal I$-mad family coincides with the classical notion of a mad family. 

What are the possible sizes of $\mathcal I$-mad families? Can an infinite (or for some ideals, uncountable) $\mathcal I$-mad family be analytic? 
Such questions were asked, for instance, for the ideal $\fin\times\fin$, the Fubini product of the finite ideal with itself.
Another natural choice for $\mathcal I$ is the finite part of a submeasure; 
any ideal which is $F_\sigma$ (viewed as a subset of $\powerset(\omega)\cong 2^\omega$) is of this form.
Several questions related to definability and existence of $\mathcal I$-mad families in various settings were answered in  \cite{haga-schrittesser-toernquist}.









\medskip

In the present paper we shall supply proofs to the theorems which were announced in \cite{pnas}: 

We establish a link between the ideals in a large class $\mathfrak F$ (defined below)  
and principles of universal Ramsey regularity.
We shall use the following weak choice principle.

\begin{dfn}[Ramsey positive uniformisation, \text{\textsf{R-Unif}}]~\label{d.Runif} 
\begin{enumerate}
\item Let $R$ be a binary relation. We say that $f$ uniformises $R$ on $X$ if $f$ is a function with $\dom(f)=X$, $X\subseteq\dom(R)$ and 
for each $x \in X$, $(x,f(x))\in R$.
\item
The \emph{Principle of Ramsey positive uniformisation} (short: \text{\textsf{R-Unif}}) is following statement:
For every $R\subseteq [\nat]^\infty \times [\nat]^\infty$ such that $\dom(R)=[\nat]^\infty$
there is $A\in [\nat]^\infty$ and a function $f$ which uniformises $R$ on $[A]^\infty$.
\end{enumerate}
\end{dfn}

\begin{thm}[\ZF]\label{t.intro.main}
Let $\mathfrak F$ be the least class of ideals such that $\fin \in \mathfrak F$ which is closed under Fubini sums over $\fin$. 
Suppose
\begin{itemize}
\item $\DC_{\reals}$, i.e, the Principle of Dependent Choice restricted to $\powerset(\nat)$,
\item The Principle of Ramsey positive uniformisation (from above), and
\item Every subset of $[\nat]^\infty$ has the Ramsey property.
\end{itemize}
Then there are no infinite $\mathcal I$-mad families, for any ideal $\mathcal I \in \mathfrak F$.
\end{thm}

This shows that all these ideals are in fact much closer to $\fin$ than could possibly have been anticipated.
As a special case, one can derive a positive answer to Mathias question mentioned above, as was quickly sketched in \cite{pnas}.
It also shows that some of the conclusions of our earlier paper \cite{haga-schrittesser-toernquist} can be drawn from much, much weaker assumptions (see Corollary~\ref{c.intro.con} below).



\medskip

\subsection*{C} The proof of Theorem~\ref{t.intro.main} localizes to a pointclass. By a pointclass we mean any class of subsets of Polish spaces which is closed under intersections, continuous preimages, and contains the Borel sets (of each Polish space).
\begin{thm}[\ZF]
Let $\Gamma$ be a pointclass and suppose
that for every relation $R\subseteq [\nat]^\infty\times [\nat]^\infty$ such that $R\in \Gamma$ and $\dom(R)=[\nat]^\infty$ there is  $A\in [\nat]^\infty$ and a Ramsey-measurable function $f$ which uniformises $R$ on $[A]^\infty$.
Then there are no Dedekind infinite $\mathcal I$-mad families, for any ideal $\mathcal I \in \mathfrak F$.
\end{thm}
Here, when we say that a function from $[\nat]^\infty$ into any topological space is called Ramsey measurable, we mean that the preimage of every open set has the Ramsey property. Recall also that a set $X$ is Dedekind infinite if and only if there is no injection from $\nat$ to $X$. 

\medskip

As a consequence of this local formulation, we obtain many previous results as corollaries:
\begin{cor}[\ZF]\label{c.intro} 
Let $\mathcal I$ be an ideal from $\mathfrak F$, smallest class of ideals on $\nat$ closed under taking Fubini sums over $\fin$ and containing $\fin$ as an element.
\begin{enumerate}
\item There is no infinite analytic $\mathcal I$-mad family (see also \cite{haga-schrittesser-toernquist}).
\item There is no infinite $\mathcal I$-mad family in Solovay's model \cite{asger}.
\item Under $\PD$ and $\DC_{\reals}$, there is no infinite projective $\mathcal I$-mad family (this was shown in \cite{neeman-norwood} for classical mad families, and in \cite{haga-schrittesser-toernquist} for ideals in $\mathfrak F$).
\item Under $\AD$ there is no infinite $\mathcal I$-mad family which is an element of $\mathbf{L}(\reals)$ (same as above).
\end{enumerate}
\end{cor}



It is interesting that the ideals in $\mathfrak F$ lie cofinally in the Borel hierarchy in terms of their complexity.
This points to a general question: 
For which analytic (or just, Borel) ideals $\mathcal I$ do the items in the above corollary hold?

\medskip

Note that we also obtain the following corollary:
\begin{cor}\label{c.intro.con} 
If $\ZF + $`there is an inaccessible cardinal' is consistent, so is the theory $\ZF + $`there are no infinite $\mathcal I$-mad families, for any ideal $\mathcal I \in \mathfrak F$'. 
\end{cor}
This is conjectured to be not optimal; in all likelihood, the theory in question is equiconsistent with just \ZF, without any large cardinal assumption.

\medskip

\subsection*{D} The proofs given in the present paper of the above theorems may leave the reader with the impression that the main reasons they work are: (1) Mathias reals grow very fast (2) Mathias forcing has pure decision, (3) the assumption of Ramsey uniformization. 

The following theorem shows that this impression may not be entirely well-founded:

\begin{thm}\label{t.laver}
There is an infinite $\Pi^1_1$ (lightface) mad family in the Laver extension of $L$.
\end{thm}

Note that (1) Laver reals grow very fast, (2) Laver forcing has pure decision, and (3) the pointclass $\Pi^1_1$ has the uniformization property.


\medskip


\subsection*{Organization of the paper}
To give the reader a sense of orientation, we shall first prove our main theorem for the case $\mathcal I=\fin\times\fin$.
This is carried out in~\S\ref{s.2D}.
After that, we tackle the general case in~\S\ref{s.alphaD}. If the reader is brave enough, she can also skip~\S\ref{s.2D} and begin with this section, as it is completely self-contained.
We show Corollary~\ref{c.intro} in the short~\S\ref{s.corollaries}.
Finally, in Section~\ref{laver} we construct a co-analytic infinite mad family in the Laver extension of $L$, showing Theorem~\ref{t.laver}.

\subsection*{Acknowledgments} The first author thanks the FWF for support through Ben Miller's project P29999 and Vera Fischer's START Prize Y1012. 
The second author thanks



\section{Preliminaries and Notation}\label{s.prelim}



Let $\mathcal I$ be an ideal, in the set-theoretical sense, on a countable set $S$:
That is, $\mathcal I$ is a subset of 
$\powerset(S)$ such that for all $I,J\in\powerset(\mathcal \nat)$ it holds that $I,J \in \mathcal I \Rightarrow I\cup J \in \mathcal I$ and if $I\subset J$ and $J\in \mathcal I$, then also $I\in\mathcal I$.
An $\mathcal I$-almost disjoint family is a set $\mathcal A \subseteq \powerset(S)\setminus \mathcal I$ 
such that any two distinct $A,B \in \mathcal A$ are $\mathcal I$-almost disjoint, 
i.e., $A\cap B \in \mathcal I$.
Such a family is called maximal if it is not a proper subset of an almost disjoint family. 
We abbreviate maximal $\mathcal I$-almost disjoint family by $\mathcal I$-mad family.
If we take $S=\nat$ and $\mathcal I$ to be $\fin$, i.e., the ideal of finite subsets of $\nat$, we speak simply of an almost disjoint, resp.\ mad family.

For this entire paper, our background theory is $\ZF$.





\section{The two-dimensional case}\label{s.2D}

We start by proving a special case of Theorem~\ref{t.intro.main}.

\begin{thm}\label{t.2D}
Let $\Gamma$ denote either $\pset(\pset(\omega))$ or the collection of all projective subsets of $\pset(\omega)$.
Suppose the following:
\begin{itemize}
\item The principle of Dependent Choice \textup{(\DC)} holds;
\item \textup{$\text{\textsf{R-Unif}}$} from Definition~\ref{d.Runif} holds, i.e., Ramsey positive uniformisation holds for total relations in $\Gamma$;
\item All sets in $\Gamma$
have the Ramsey property. 
\end{itemize}
Then there is no infinite  $\fin[2]$-\emph{mad} family 
in $\Gamma$.
\end{thm}
In fact here is a slightly more precise version of the theorem.
By a \emph{pointclass} we mean a class of subsets of Polish spaces which is closed under continuous preimages, intersections, and contains the Borel subsets (of each Polish space).
\begin{thm}\label{t.2D.precise}
Suppose every total binary relation on $[\nat]^\infty$ in a point-class $\Gamma$ can be uniformized on some set of the form $[A]^\infty$ (where $A\in[\nat]^\infty$) by a function such that for some point-class $\Gamma'$, $f$ is $\Gamma'$-measurable and every set in $\Gamma'$ is Ramsey.
Then there is no Dedekind infinite $\fin[2]$-\emph{mad} family in $\Gamma$.
\end{thm}
We point out that an immediate corollary is our earlier result from \cite{haga-schrittesser-toernquist}:
\begin{cor}\label{c.2D.no.analytic}
There are no analytic $\fin[2]$-\emph{mad} families.
\end{cor}




We begin the proof of Theorem~\ref{t.2D.precise} by showing a more technical result (Theorem~\ref{t.2D.analytic}) which already implies this corollary.
Theorem~\ref{t.2D.analytic} will be shown in $\ZF$, without using any of the additional assumptions of Theorem~\ref{t.2D.precise}.
For this we need a crucial definition.



\subsection{The two-dimensional tilde operator}

\medskip
Suppose $\mathcal A$ is a $\fin[2]$-a.d.\  family and $\langle {\bar A}^l\setdef l\in\nat\rangle$ is a sequence of distinct elements of $\mathcal A$.
\begin{rem}\label{r.sequence}
Note that if $\mathcal A$ is analytic, such a sequence may be chosen in the absence of $\DC$ by taking left-most branches, i.e., using Jankov-von Neumann, or $\sigma(\Sigma^1_1)$ uniformization for analytic relations (see~\cite[18.1]{kechris}).
\end{rem}
\begin{fct}\label{x.sequence}
There is a pairwise disjoint sequence $\vec x=\langle x^l\setdef l\in\nat\rangle$ such that for each $l\in\nat$
\begin{itemize}
\item $x^l \subseteq \bar{A}$ for some $\bar A \in \mathcal A$,
\item each non-empty vertical of $x^l$ is infinite.
\end{itemize}
\end{fct}
\begin{proof}
Simply let $x^l = (\bar A^l \setminus \bigcup_{l'<l} \bar A^{l'})^{++}$.
\end{proof}

\begin{dfn}[The two-dimensional $\sim$-operator]
We define a map
\begin{align*}
[\nat]^{\infty} &\to {\fin[2]}^{+},\\
A &\mapsto \from[A]
\end{align*}
Let 
 $x^l_m \subseteq \nat^2$
be the $m$th infinite column of $x^l$.
Further write $\hat x^l_m$ for the 
function which enumerates the pairs in $x^l_m$ in increasing order of their second component (i.e., in lexicographic order).


\medskip
Given $A \in [\nat]^{\infty}$, we write $l \consec[A] m$ to mean that $l$ and $m$ are consecutive elements of $A$, i.e.,
\[
l \in A \text{ and } m = \min A\setminus l+1
\]
and define $\from[A] \in {\fin[2]}^{+}$ as follows:
\[
\from[A] = \{ \hat x^l_m(n) \setdef l \consec m < n \in A\}.
\]
When we want to make explicit the dependence on $\vec x$ we write $\fromx[\vec x]{A}$.
\end{dfn}



We collect some of the crucial properties of this map:
\begin{facts}~\label{f.from}
\begin{enumerate}
\item\label{i.from.invariant} \emph{Invariance:} If $z \mathbin{E_0} z'$, i.e., if $z \Delta z'\in \fin$, then also $\tilde z \Delta \tilde z' \in \fin[2]$.

\item\label{i.from.pigeonhole} \emph{The Pigeonhole Principle, first level:} For any $\bar X \in \powerset(\nat^2)$,  $A \in [\nat]^{\infty}$ and any $k\in\nat$ there is $B \in [A\cap k, A\setminus k]^{\infty}$ such that $\from[B]\subseteq_{\fin[2]} \bar X$ or $\from[B]\subseteq_{\fin[2]} \powerset(\nat^2)\setminus\bar X$.

\item\label{i.from.pigeonhole.vertical} \emph{The Pigeonhole Principle, second level:} Suppose $m\in\nat$ and $X \subseteq \nat \times \{m\}$.
For every $A \in [\nat]^{\infty}$ and any $k\in\nat$ there is $B \in [A\cap k, A\setminus k]^{\infty}$ such that $\from[B](m) \subseteq_{\fin}X$ or $\from[B](m)\subseteq_{\fin} \powerset(\nat)\setminus X$.


\item\label{i.from.avoid.single} \emph{The Almost Disjointness Principle:} For $\bar A \in \mathcal A$ and any $A \in [\nat]^{\infty}$ there is $B \in [A]^{\infty}$ such that
$\from[B] \cap \bar A \in \fin[2]$.
\end{enumerate}
\end{facts}
\begin{proof}
(\ref{i.from.invariant}) This is because only finitely many verticals are affected when replacing $z$ with $z'$. 

\medskip
(\ref{i.from.pigeonhole})
Given $\bar X$, $k\in\nat$, and $A\in[\nat]^{\infty}$ define a coloring
\[
c\colon [A\setminus k]^3 \to 2
\]
as follows: For $\{l,m,n\} \in [A\setminus k]^3$ such that $l<m<n$ let
\[
c(l,m,n)=\begin{cases}
0 &\text{ if $\hat x^l_{m}(n) \in \bar X$, }\\
1 &\text{ if $\hat x^l_{m}(n) \notin \bar X$.}\\
\end{cases}
\]
By the Infinite Ramsey's Theorem find $H\in[A\setminus k]^{\infty}$ such that $c$ takes only one colour on $[H]^2$.
Letting $B=(A\cap k)\cup H$, clearly $B$ is as desired.

\medskip
(\ref{i.from.pigeonhole.vertical})
Suppose we are given $X \subseteq \nat \times \{m\}$, $k\in\nat$ and $A \in [\nat]^{\infty}$.
We are done if $m \notin \dom(\from[A])$; so pick $l_0,m_0$ such that $\dom(\hat x^{l_0}_{m_0})=\{m\}$.
We may assume that $k > m_0$ (otherwise increase $k$). 
One of the two sets
\begin{align}
B_0&=\{n\in A\setminus k\setdef \hat x^{l_0}(m_0,n)\in X\},\\
B_1&=\{n\in A\setminus k\setdef \hat x^{l_0}(m_0,n)\notin X\}
\end{align}
has to be infinite, so letting $B=(A\cap k)\cup B_i$ where $i$ is chosen so that $B_i$ is infinite, $B$ is the desired set. 

\medskip
(\ref{i.from.avoid.single}) If for some $l\in\nat$, $\bar A \subseteq x^l$, it suffices to take $B= A$, since $\from[A]$ meets $\bar A$ in at most one vertical.  
Otherwise, as $\bar A \in \mathcal A$, for each $l\in\nat$, $\bar A \cap x^l \in \fin[2]$.
In particular we may choose $m_l$ such that for every $m > m_l$,
$x^l_m\cap \bar A$ is finite.

Define a sequence
$n_0, n_1, \hdots\in \nat$ as follows. 
Let $n_0 = 0$.
Given $n_0, \hdots, n_{k}$ let 
$n_{k+1}$ be the least number $b$ such that $b > \max(n_{k}, m_{n_{k}})$.
Finally let  
$B=\{n_{k}\setdef k\in\nat\}$.
Then $\from[B] \cap \bar A \cap x^i_j$ is finite for each $i,j \in \nat$,  so $\from[B]\cap \bar A \in \fin[2]$.
\end{proof}
\medskip
Now we can state the theorem.
\begin{thm}[$\ZF$]\label{t.2D.analytic}
 Suppose $\mathcal A$ is an analytic $\fin[2]$-a.d.\  family  and $\vec x = \langle x^l\setdef l\in\nat\rangle$ is a sequence of pairwise disjoint sets from ${\fin[2]}^{++}$ each of which is a subset of an element of $\mathcal A$ (as in Fact~\ref{x.sequence}).
For any $W \in [\nat]^{\infty}$ there is $W_0 \in [W]^{\infty}$ such that  $\fromx[\vec x]{W_0}$ is $\fin[2]$-a.d.\  from each element of $\mathcal A$.
\end{thm}
It is obvious that Theorem~\ref{t.2D.analytic} already implies Corollary~\ref{c.2D.no.analytic}, that there are no analytic $\fin[2]$-mad families (since a sequence $\vec x$ as above can be found using just $\ZF$ when $\mathcal A$ is analytic, see Remark~\ref{r.sequence}). 
For the proof of Theorem~\ref{t.2D.analytic} we shall need to make some definitions.
We first introduce a collection of trees with an interesting invariance property.

\subsection{An invariant family of trees in two dimensions}

Let $\mathcal A$ be an analytic almost disjoint family, and fix a tree $T$ on $2\times\omega$ such that $\mathcal A=\pi[T]$.
For the proof of Theorem~\ref{t.2D.analytic} we import the following crucial definition from \cite{haga-schrittesser-toernquist}.

\begin{dfn}
Given $z \subseteq \nat^2$, define $T^z$ as follows:
\[
T^z = \{t \in T \setdef (\exists \bar A \in \pi[T_t]) \; \bar A \cap z \notin \fin[2]\}.
\]
\end{dfn}

It is easy to see that $T^z$ has the following properties:
\begin{facts}~\label{f.T^z}
\begin{enumerate}
\item\label{i.T^z.pruned} $T^z$ is pruned, i.e., for any $t \in T^z$ it holds that $[T^z_t]\neq \emptyset$.
\item\label{i.T^z.non-empty} $(\exists \bar A \in \mathcal A)\;\bar A \cap \from[z]\notin \fin[2]$ if and only if $[T^z]\neq \emptyset$.
\item\label{i.T^z.invariant} \emph{Invariance:} $z \Delta z' \in \fin[2] \Rightarrow T^z = T^{z'}$.
\end{enumerate}
\end{facts}


To deal with $\fin[2]$ we refine this definition by introducing a family of trees which also take into account some information about which verticals of the intersection are infinite:
For $\bar X \subseteq \nat^2$ and $d \in [\nat]^{<\infty}$ define
\begin{equation*}
T^{\bar X,d}=\{s \in T\setdef (\exists \bar A \in \pi[T_s])\; \bar A \cap \bar X \in{\fin[2]}^{+} \land
 (\forall n\in d)\; \bar A(n) \cap \bar X(n) \in \finp\} 
\end{equation*}
It is again easy to see that for any $\bar X,\bar Y \subseteq \nat^2$ and $d \in [\nat]^{<\infty}$ the following hold:
\begin{facts}~\label{f.T^z,d}
\begin{enumerate}


\item $T^{\bar X,d}$ is a sub-tree of $T^{\bar X}$,

\item $T^{\bar X,d}$ is pruned, i.e., $t \in T^{\bar X,d} \iff [T^{\bar X,d}]\neq \emptyset$,

\item $T^{\bar X,\emptyset} = T^{\bar X}$,

\item\label{f.T^z,d.invariant} \emph{Conditional Invariance:} $[(\forall n\in d)\; \bar X(n) \Delta \bar Y(n) \in \fin \land \bar X \Delta \bar Y \in\fin[2] ]\Rightarrow T^{\bar X,d} = T^{\bar Y,d}$.

\end{enumerate}
\end{facts}
The most crucial fact about these trees is expressed by the following lemma:
\begin{lem}[Branch Lemma]\label{l.2D.branch}
Suppose $\bar X \subseteq \nat^2$ and $t_0, t_1 \in T^{\bar X}$ with $\lh(t_0) = \lh(t_1)$ but $\pi(t_0)\neq \pi(t_1)$.
There are $d \in [\nat]^{<\infty}$ and 
$t'_i \in  T^{\bar X,d}_{t_i}$ for each $i\in \{0,1\}$ such that one of the following holds:
\begin{enumerate}[label=(\Roman*),ref=\Roman*]
\item\label{i.2D.branch.I} For all $n\in\nat\setminus\big(\max(d)+1\big)$ and all pairs $(w_0,w_1) \in [T^{\bar X,d}_{t'_0}] \times [T^{\bar X,d}_{t'_1}]$,
\[
n \notin \dom_\infty\big(\pi(w_0)\cap \bar X\big) \cap \dom_\infty\big(\pi(w_1)\cap \bar X\big);
\]
Or
\item\label{i.2D.branch.II} There is $n\in d$ and $m\in\nat$ such that for all $(w_0,w_1) \in [T^{\bar X,d}_{t'_0}] \times [T^{\bar X,d}_{t'_1}]$,
\[
\big(\pi(w_0)\cap \pi(w_1)\big) (n) \subseteq m.
\]
\end{enumerate}
\end{lem}
Note that in this lemma, $\bar X$ is merely a parameter---it may help the reader to first set $\bar X=\nat^2$ mentally and then convice herself that the proof goes through in the general case (the case $\bar X\in \fin[2]$ is entirely uninteresting, but even then the lemma holds vacuously).
The proof idea is that the failure of the lemma would give a recipe for building two branches though $T$ whose projections have a $\fin[2]$-large intersection.
Here, another definition is convenient.
\begin{dfn}
Given $b, b' \in [\nat^2]^{<\infty}$, write $b \sqsubset_2 b'$ to mean that
$\dom(b)\sqsubsetneq \dom(b')$ and for each $n\in \dom(b)$,
$b(n)\sqsubsetneq b'(n)$ (where of course for $a,a'\in[\nat]^{<\infty}$,  $a \sqsubsetneq a'$
 means that
$a$ is proper initial segment of $a'$).
 \end{dfn}
 We point out the following fact, which we leave to the reader to prove:
 \begin{fct}
 If $\langle b_k\setdef k\in \nat\rangle$ is a sequence such that $b_k \sqsubset_2 b_{k+1}$ for each $k\in\nat$, 
 then $\bigcup_{k\in\nat} b_k \in {\fin[2]}^{++}$.
 \end{fct}
 With this we can prove Lemma~\ref{l.2D.branch}, i.e, the two-dimensional Branch Lemma.
\begin{proof}[Proof of Lemma~\ref{l.2D.branch}]
We naturally assume $\bar X \in {\fin[2]}^{+}$.
Fix $t_0, t_1 \in T^{\bar X}$ such that $\lh(t_0) = \lh(t_1)$ but $\pi(t_0)\neq \pi(t_1)$.
Towards a contradiction, suppose the lemma fails. 
We build sequences
\begin{itemize}
\item $b^0, b^1, b^2, \hdots$ from $[\nat^2]^{<\infty}$,
\item $t^0_i, t^1_i, t^2_i \hdots$ from $T_{t_i}$ for each $i\in\{0,1\}$ 
\end{itemize}
such that
for each $k\in \nat$
\begin{enumerate}[label=(\Alph*)]
\item\label{IH.grow}\label{IH.first}  $b^k \sqsubset_2 b^{k+1}$,
\item\label{IH.subseteq} $b_{k+1} \subseteq \pi(t^k_0)\cap \pi(t^k_1)$,
\item\label{IH.keep.going}\label{IH.last} $t^{k+1}_i \in T^{\bar X,\dom(b^k_i)}_{t^k_i}$.
\end{enumerate}
For $k=0$ let $b^0=\emptyset$ and $t^0_i = t_i$ for each $i\in\{0,1\}$.
Now suppose we have constructed $b^k$, $t^k_0$, and $t^1_k$.

Since (\ref{i.2D.branch.I}) in the the lemma fails with $d=\dom(b^k)$ and $t'_i=t^k_i$ for each $i\in\{0,1\}$ we can find 
$n> \max(d)$
so that letting $d'= \dom(b^k)\cup\{n\}$, 
we have
\[
(t'_0, t'_1) \in  T^{\bar X,d'} \times T^{\bar X,d'}.
\] 
Now use the failure of (\ref{i.2D.branch.II}) with $d'$ substituted for $d$, finitely many (namely, $|d'|$) 
times to extend $t'_i$ to $t^{k+1}_i \in T^{\bar X,d'}$ for each $i\in\{0,1\}$ 
so that there is $b^{k+1} \subseteq \pi(t^{k+1}_0)\cap \pi(t^{k+1}_0)$ with $n\in \dom(b^{k+1})$ and $b^k\sqsubset_2 b^{k+1}$.

Thus by our assumption that the lemma fails, we can build infinite sequences $b^k, t^k$ for $k\in \nat$ as above;
but this contradicts that $\mathcal A$ is $\fin[2]$-almost disjoint since $ \bigcup_{k\in\nat}b^k \in {\fin[2]}^{+}$ and $\bigcup_{k\in\nat} t^k_i\in [T]$ for each $i\in\{0,1\}$ while also
\[
 \bigcup_{k\in\nat}b^k\subseteq \pi\left(\bigcup_{k\in\nat} t^k_0\right) \cap \pi\left(\bigcup_{k\in\nat} t^k_1\right) \qedhere
\]
\end{proof}

\medskip

With the previous lemma we can prove Theorem~\ref{t.2D.analytic}.
\begin{proof}[Proof of Theorem~\ref{t.2D.analytic}]
Let $\mathcal A$ and $\vec x$ as in the lemma be given.
Fix a tree $T$ on $2\times\nat$ such that $\pi[T]=\mathcal A$.

First we shall make, for each $d \in [\nat]^{<\infty}$, the function 
\[
(B,d) \mapsto T^{\from[B],d}
\] 
constant,
using the fact that analytic sets are completely Ramsey and ``invariance'' of each of the trees.
\begin{claim}\label{c.2D.constant}
For every $W \in [\nat]^{\infty}$ there is $W_0 \in [W]^{\infty}$ such that 
\[
(\forall W' \in [W_0]^{\infty})(\forall d \in [\dom(\from[W'])]^{<\infty})\; T^{\from[W'],d}=T^{\from[W_0],d}
\]
\end{claim}
\begin{proof}[Proof of Claim~\ref{c.2D.constant}]
The proof is by a fusion argument.
Let $\langle(d_k, t_k)\setdef k\in\nat\rangle$ enumerate $[\nat]^{<\infty}\times T$ so that each element of $[\nat]^{<\infty}\times T$ occurs infinitely many times in the enumeration.
Let for each $k\in \nat$
\[
D_k=\{B \in {\fin[2]}^{++}\setdef t_k \in T^{\from[B],d_k}\}
\]
and note that this set is analytic and hence, completely Ramsey.

We inductively build a sequence $(b_k,C_k) \in [\nat]^{<\infty}\times[\nat]^{\infty}$ for $k\in \nat$.
Let $(b_0, C_0)=(\emptyset, W)$. Suppose now we have constructed $(b_k,C_k)$.
Find $C_{k+1} \in [C_k\setminus b_k]^{\infty}$ such that
\begin{equation}\label{e.make.constant.one.step}
[b_k, C_{k+1}]^{\infty}\subseteq D_k \text{ or } [b_k, C_{k+1}]^{\infty}\subseteq [\nat]^{\infty} \setminus D_k,
\end{equation}
and let $b_{k+1}=b_k\cup\{\min C_{k+1}\}$.
Finally let $W_0 = \bigcup_{k\in\nat} b_k$. 

To see that $W_0$ is as desired, let an arbitrary $W'\in[W_0]^{\infty}$ and a finite set $d \subseteq \dom(\from[W'])$ be given.
To show $T^{\from[W'],d}=T^{\from[W_0],d}$, consider an arbitrary $t \in T$.
Find $k\in\nat$ such that $(d_k,t_k)=(d,t)$ and $d \subseteq \dom(\from[b_k])$.
Since $W' \subseteq_{\fin} C_{k+1}$ we may choose $W''$ such that $W'' \mathbin{E_0} W'$ and $W'' \in [b_k, C_{k+1}]^{\infty}$.
Thus by Equation~\eqref{e.make.constant.one.step},
\[
t \in T^{\from[W''],d} \iff t \in T^{\from[C_{k+1}],d}, 
\]
and by the conditional invariance of this tree expressed in Fact\ref{f.T^z,d}\eqref{f.T^z,d.invariant} and since
$\from[W''] \Delta \from[W'] \in \fin[2]$ and $d \subseteq \dom^\infty \from[W'']$ and so also $\from[W''](n) \Delta \from[W'](n) \in \fin$ for each $n\in d$, 
we also have 
\begin{equation}\label{e.fusion}
t \in T^{\from[W'],d} \iff t \in T^{\from[C_{k+1}],d}.
\end{equation}
Since in particular, \eqref{e.fusion} also holds with $W'$ replaced $W_0$, and since $t\in T$ was arbitrary, we conclude $T^{\from[W_0],d}=T^{\from[W'],d}$.
\renewcommand{\qedsymbol}{{\tiny  Claim~\ref{c.2D.constant}~}$\Box$}
\end{proof}
As we shall presently see, $W_0$ is ``generic enough'' so that $\from[W_0]$ will be disjoint from every set from $\mathcal A$. 
The following two claims each use this ``weak genericity''; the first does so in a particularly simple manner.
\begin{claim}\label{c.2D.not1branch}
$\lvert \pi[T^{*,\emptyset}]\rvert \neq 1$.
\end{claim}
\begin{proof}[Proof of Claim~\ref{c.2D.not1branch}]
Towards a contradiction suppose $\{\bar A\} = \pi[T^{*,\emptyset}]$.
Find $W_1 \in [W_0]^{\infty}$ such that $\from[W_1] \cap \bar A \in \fin[2]$, using Fact~\ref{f.from}(\ref{i.from.avoid.single}).
By weak genericity (i.e., because $T^{\from[W_1]} = T^{*,\emptyset}$) we have  $\{\bar A\} = \pi[T^{\from[W_1]}]$. 
But by the definition of this tree 
it should hold that $\from[W_1] \cap \bar A \in {\fin[2]}^{+}$ contradicting the choice of $W_1$.

For the readers convenience we show this in detail: 
Since $\pi[T^{\from[W_1]}]\neq \emptyset$ in particular $\emptyset \in T^{\from[W_1]}$, so there is $w \in [T]$ with $\pi(w) \cap \from[W_1] \in {\fin[2]}^{+}$.
But clearly also $w \in [T^{\from[W_1]}]$ and so $\pi(w) = \bar A$.
We have shown $\bar A \cap \from[W_1] \in {\fin[2]}^{+}$, contradiction.
\renewcommand{\qedsymbol}{{\tiny  Claim~\ref{c.2D.not1branch}~}$\Box$}
\end{proof}
We continue exploring the ``weak genericity'' of $W_0$, this time using the pigeonhole principles proved in Fact~\ref{f.from} as well as Lemma~\ref{l.2D.branch}.
\begin{claim}\label{c.2D.one.branch}
$\pi[T^{*,\emptyset}]=\emptyset$.
\end{claim}
\begin{proof}[Proof of Claim~\ref{c.2D.one.branch}]
Otherwise by the last claim, $\lvert \pi[T^{*,\emptyset}]\rvert\geq 2$.
Then we can choose $t_0, t_1 \in T^{*,\emptyset}$ with $\lh(t_0) = \lh(t_1)$ and $\pi(t_0)\neq \pi(t_1)$.
Use Lemma~\ref{l.2D.branch} to find $d \in [\nat]^{<\infty}$ and 
$t'_i \in  T^{*,d}_{t_i}$ for each $i\in \{0,1\}$ satisfying Clause
(\ref{i.2D.branch.I}) or (\ref{i.2D.branch.II}) of said lemma.
We now argue by cases.

\medskip
\textit{Clause (\ref{i.2D.branch.I}) of Lemma~\ref{l.2D.branch} holds.} 
For each $i\in\{0,1\}$ let
\[
\bar X_i = \Big(\bigcup\{\dom_\infty\big(\pi(w)\cap\from[W_0]\big) \setdef w \in [T^{*,d}_{t'_i}] \Big) \times \nat.
\]
Clearly $\bar X_0 \cap \bar X_1 \in \fin[2]$.
Use Facts~\ref{f.from}(\ref{i.from.pigeonhole}) to find $W_1 \in [W_0]^{\infty}$ such that $d \subseteq \dom(\from[W_1])$ and such that
$\from[W_1]\subseteq_{\fin[2]} \bar X_0$ or $\from[W_1]\subseteq_{\fin[2]} \powerset(\nat^2) \setminus \bar X_0$.
Thus, we may fix $i\in\{0,1\}$ so that 
\begin{equation}\label{e.2D.small}
\from[W_1]\cap \bar X_i \in \fin[2].
\end{equation}

But by the definition of the invariant tree, this contradicts that  $t'_i \in T^{*,d}$ as we now show in detail for the readers convenience:
Since $T^{*,d} = T^{\from[W_1],d}$, $t'_i  \in T^{\from[W_1],d}$ and so by definition of the tree there is $w \in [T_{t'_i}]$ such that 
\begin{equation}\label{e.2D.big}
\pi(w) \cap \from[W_1] \in {\fin[2]}^{+}.
\end{equation} 
and
$d \subseteq \dom^\infty(\pi(w) \cap \from[W_1])$. 
Also by definition of the tree $w$  is a branch through $T^{W_1,d}_{t'_i}$ and hence through $T^{*,d}_{t'_i}$. 
But this entails $\pi(w) \subseteq \bar X_i$ which is an absurdity by Equations \eqref{e.2D.small} and \eqref{e.2D.big}.

\medskip
\textit{Clause (\ref{i.2D.branch.II}) of Lemma~\ref{l.2D.branch} holds.}
Fix $m\in d$ as in Clause (\ref{i.2D.branch.II}). For each $i\in\{0,1\}$ let
\[
\bar X_i = \bigcup\big\{\pi(w)(m) \setdef w \in [T^{*,d}_{t'_i}]\big\}.
\]
By assumption $\bar X_0 \cap \bar X_1 \in \fin$.
Argue as above, this time using Facts~\ref{f.from}(\ref{i.from.pigeonhole.vertical}) to find $W_1 \in [W_0]^{\infty}$ such that $d \subseteq \dom(\from[W_1])$ and such that we may find $i\in\{0,1\}$ with
\begin{equation}\label{1D.case.B.W_1.smallintersection}
\from[W_1](m)\cap \bar X_i(m) \in \fin.
\end{equation} 
Then similarly to the previous case, this contradicts that $n\in d$ and
$t'_i \in T^{\tilde W_1,d}$.
Having reached a contradiction in each case, this proves the claim.
\renewcommand{\qedsymbol}{{\tiny  Claim~\ref{c.2D.one.branch}~}$\Box$}
\end{proof}

By the last two Claims it has to be the case that 
$[T^{\from[W_0]}]=\emptyset$. 
By Facts~\ref{f.T^z}(\ref{i.T^z.pruned}) this means that $\emptyset \notin T^{\from[W_0]}$ and so by Facts~\ref{f.T^z}(\ref{i.T^z.non-empty}) we conclude that $\mathcal A$ is not maximal.
\renewcommand{\qedsymbol}{{\tiny  Theorem~\ref{t.2D.analytic}~}$\Box$}
\end{proof}


\subsection{Proof of the main theorem in two dimensions}\label{proof.t.2D.precise}

Now we can easily prove Theorem~\ref{t.2D}. In fact, the proof shows Theorem~\ref{t.2D.precise}.
\begin{proof}[Proof of the main theorems~\ref{t.2D} and \ref{t.2D.precise}]
Suppose to the contrary $\mathcal A$ is an infinite $\fin[2]$-\emph{mad} family in $\Gamma$
and for Theorem~\ref{t.2D}, choose infinite sequence $\vec x=\langle x^l\setdef l\in\nat\rangle$ as in Fact~\ref{x.sequence} using Dependent Choice.
We reduce the proof to the case that $\mathcal A$ is analytic:
\begin{claim}\label{c.make.analytic}
There is $W_1\in [\nat]^{\infty}$ and an analytic set $\mathcal A'$ such that 
for any $z \in [W_1]^{\infty}$ there is $\bar A \in \mathcal A'$ with 
$\fromx[\vec x]{z} \cap A \notin \fin[2]$.
\end{claim} 
\begin{proof}[Proof of Claim~\ref{c.make.analytic}]
Let $R(z,y)$ be the relation defined by
\[
R(z,y) \iff z \in [\nat]^{\infty} \land y \in \mathcal A \land \fromx[\vec x]{z}\cap y \notin \fin[2].
\]
By our assumptions on $\Gamma$, $R$ is in $\Gamma$.
So we may find $W_0 \in [\nat]^{\infty}$ and $f$ in $\Gamma'$ such that
for all $A\in [W_0]^{\infty}$, $R(A, f(A))$.

Identifying $\powerset(\nat^2)$ with $2^\nat$, and denoting by $N_s$ the basic open neighborhood in $2^\nat$ given by $s\in 2^{<\nat}$, for each $s\in2^{<\nat}$
\[
\{A\in [W_0]^{\infty} \setdef f(A) \in N_s\}
\]
is in $\exists\Gamma\cap\neg(\exists\Gamma)$.
An easy diagonalization shows that we may thin out $W_0$ to $W_1 \in [W_0]^{\infty}$ so that $f$ restricted to $[W_1]^{\infty}$ is continuous. 
Letting $\mathcal A' = \ran(f)$ this proves the claim.
\renewcommand{\qedsymbol}{{\tiny  Claim~\ref{c.make.analytic}~}$\Box$}
\end{proof}
This finishes the proof, for by Theorem~\ref{t.2D.analytic} no such $\mathcal A'$ can exist.
\renewcommand{\qedsymbol}{{\tiny  Theorem~\ref{t.2D}~}$\Box$}
\end{proof}











\section{The general case}\label{s.alphaD}


The following is provable in $\ZF$.
\begin{thm}\label{t.Finalph}
Suppose $\Gamma$ is a reasonable pointclass, relations in $\Gamma$ can be uniformized by functions in a point-class $\Gamma'$, on an Ellentuck-basic open set, where all sets in $\Gamma'$ are completely Ramsey. Then there is no Dedekind infinite $\fin[\alpha]$-\emph{mad} family in $\Gamma$.
\end{thm}

\subsection{The ideal}
We need a convenient representation of $\fin[\alpha]$ for $\alpha < \aleph_1$.
It is (we feel) most easily described as an ideal on the following set $S_\alpha \subseteq {}^{<\nat}\nat$ (of course $S_\alpha$ is in bijection with $\nat$).
To every ordinal $\alpha$ such that $0<\alpha<\aleph_1$, associate a  non-decreasing sequence $\langle \gamma^\alpha_n\setdef n\in\nat\rangle$  such that
\[
\bigcup \{\gamma^\alpha_n +1\setdef n\in\nat\} = \alpha.
\]
For successor ordinals $\alpha = \beta+1$, we can let this be the constant sequence with value $\beta$.
If $\alpha$ is a limit, we can assume this sequence is strictly increasing.

Define $S_1 = {}^{1}\nat$, the set of sequences from $\nat$ of length $1$, which can and shall be identified with $\nat$ in the obvious way.
For $\alpha>1$ let 
\[
S_\alpha = \{n\conc s \setdef n\in\nat\wedge s\in S_{\gamma^\alpha_n}\}.
\] 
It will be convenient to let $S_0=\{\emptyset\}$.

\medskip

It is now easy to define $\fin[\alpha]$ as a subset of $\powerset(S_\alpha)$ by induction on $\alpha$:
Let $\fin[1]=\fin$, and for $\alpha >1$ define $X \subseteq S_\alpha$ to be an element of $\fin[\alpha]$ if and only if
\[
\{n\in\nat\setdef X(\langle n\rangle) \notin \fin[\gamma^\alpha_n]\} \in \fin.
\]
We also write $[S_\alpha]^{+}_{\fin[\alpha]}$ or ${\finalph}^+$ for the co-ideal $\powerset(S_\alpha)\setminus\fin[\alpha]$.

\medskip

For any $\alpha < \aleph_1$, $X \subseteq S_\alpha$, and $s \in {}^{<\nat}\nat$, define
\[
X(s) = \{s'\in{}^{<\nat}\nat\setdef s \conc s' \in X\}.
\]
We also need a notion of `higher dimensional domain' (in analogy to the role of the ordinary operation of taking domains in the two-dimensional case).
We define
\[
\higherdom(X)=\{s\res k \setdef s \in X, k < \lh(s)\}.
\]



\medskip

Further, we define a partial function $\gamma^\alpha\colon{}^{<\nat}\nat\rightharpoonup \aleph_1$ as follows:
Let $\gamma^\alpha(s)$ be the unique $\gamma<\aleph_1$ such that
$S_\alpha(s) = S_\gamma$ whenever such $\gamma$ exists; otherwise, $\gamma^\alpha(s)$ is undefined, i.e, $s \notin \dom(\gamma^\alpha)$.
In fact, it follows that $\dom(\gamma^\alpha) = \{s \res n \setdef n \leq \lh(s), s \in S_\alpha\}$.
We may drop the superscript $\alpha$ if it is clear from the context.

Note that since $S_0=\{\emptyset\}$ we have $s \in S_\alpha$ if and only if $\gamma^\alpha(s) = 0$.
Moreover, for example, $\gamma^\alpha(\emptyset) = \alpha$ and $\gamma^\alpha\big(s\res (\lh(s)-1)\big) = 1$ for each $s \in S_\alpha$.

\iffalse
For the readers convenience, we discuss some alternative ways of viewing the partial function $\gamma^\alpha$:
Given $s\in {}^{<\nat}\nat$, 
\[
\gamma^\alpha(s)= \sup\{\gamma \in \alpha+1 \setdef (\exists s' \in S_\gamma) \; s\conc s' \in S_\alpha\},
\]
if the set on the right-hand side is non-empty.

We can also define $\gamma^\alpha$ as follows. 
First define an axillary sequence: 
By finite induction for each $k$ such that $ k+1 < \lh(s)$, write
\begin{align*}
\gamma^\alpha_0(\emptyset) &= \alpha\\
\gamma^\alpha_{k+1}(s) &= \gamma^{\gamma^\alpha_k}_{s(k)}
\end{align*}
provided these expressions are defined (recall that $\gamma^\alpha$ is merely a partial function on ${}^{<\nat}\nat$).
Now $\gamma^\alpha(s) = \gamma^\alpha_{\lh(s)}(s)$, if the expression is defined. 
\fi

\medskip

We will mostly be concerned with the following subset of ${\finalph}^+$.
Define ${\finalph}^{++}$, also denoted by $[S_\alpha]^{++}_{\fin[\alpha]}$, to be the set of all $X \in {\finalph}^+$ such that
for any $s\in\higherdom(X)$ 
the set
\[
\{n\in\nat\setdef s\conc n \in \higherdom(X)\cup X\}
\]
is infinite. 
In other words, $\bar X \in {\finalph}^{++}$ if and only if the above set is infinite or empty for each $s\in {}^{<\nat}\nat$.




It is straightforward to check that for $X \subseteq S_\alpha$, $X \in [S_\alpha]^{+}_{\fin[\alpha]}$ if and only if there is $X' \subseteq X$ such that $X' \in [S_\alpha]^{++}_{\fin[\alpha]}$. In fact, there is a maximal (with respect to $\subseteq$) such set $X'$ which we denote by $X^{++}$, and
\[
X^{++} =\{s\in X\setdef X(s)\notin \fin[\gamma(s)]\}. 
\]
Note the use of the partial function $\gamma^\alpha$ in this definition.

Finally, for $s \in \higherdom(S_\alpha)$ we shall write
\[
\dom^s_\infty(X) = \{n\in \nat \setdef X(s \conc n)\in \finpp[\gamma(s\conc n)]\}. 
\]





\subsection{The higher tilde operator}

\begin{dfn}[The higher dimensional $\sim$-operator]
For any finite or infinite set $X \subseteq \nat$, let $\hat X\colon |X| \to \nat$ denote its increasing enumeration.
In analogy to this, given $X \in [S_\alpha]^{++}_{\fin[\alpha]}$, we define a partial function which we also denote by $\hat X$,
\[
\hat X \colon {}^{<\nat}\nat \rightharpoonup S_\alpha
\]
as follows.

Given $s \in {}^{<\nat}\nat$,
define a sequence $\bar s \in {}^{<\nat}\nat$ of at most the same length as $s$ by induction:
Suppose for $n < \lh(s)$ we have defined $\bar s \res n$ (which trivially holds for $n=0$).
Momentarily, let us write
\[
Y = \{s'(n)\in\nat\setdef(\exists s' \in{}^{<\nat}\nat)\; (\bar s \res n) \conc s' \in X\}
\]
and let
\begin{equation*
\bar s(n) =  \hat Y \big(s(n)\big) 
\end{equation*}
if $s(n) \in \dom(\hat Y)$.
Otherwise, say that $s \notin \dom(\hat X)$ and abort the definition of $\bar s$.
Suppose now we succeed in defining $\bar s$ up to length $\lh(s)$. 
If $\bar s\notin S_\alpha$ say that $s \notin \dom(\hat X)$. 
If on the other hand 
$\bar s \in S_\alpha$
say that $s \in \dom(\hat X)$ and
let $\hat X(s) = \bar s$.


Finally, suppose for each $l\in\nat$ we have $X^l \in [S_\alpha]^{++}_{\fin[\alpha]}$ and for simplicity, let us assume that $X^l \cap X^k = \emptyset$ for $l\neq k$ from $\nat$.
Let $\from[A] \in [S]^{++}_{\fin[\alpha]}$ be defined as follows:
\[
\from[A] = \{\hat X^{l}(\hat a) \setdef  \{l\}\cup a \in [A]^{<\infty}\wedge l \consec \min(a) \wedge \hat a \in \dom(\hat X^l)\}.
\]
\end{dfn}

We will see that $\from[A]$ behaves similarly to the $2$-dimensional and $1$-dimensional cases (for the latter, see \cite{pnas})



In particular, we have the following principle of invariance:
\begin{lem}[Invariance Principle]\label{l.alphaD.invariance}
Suppose $A,B\in [\nat]^\infty$. If $A \mathbin{E_0} B$ and $s \in \higherdom(\from[A]) \cap \higherdom(\from[B])$, then $\from[A](s) \Delta \from[B](s) \in \fin[\gamma(s)]$.
\end{lem}
\begin{proof}
This is an easy consequence of the definition of the $\sim$-operator. 
As the reader is invited to verify,  $s \in \higherdom(\from[A]) \cap \higherdom(\from[B])$ holds if and only if there exists $c \in  [A \cap B]^{<\infty}$ such that 
$
s \in  \higherdom(\from[c]).
$ 
Let us fix such a set $c$. 
Find $m\in \nat$ such that  $A \setminus m = B\setminus m$ and $c \subseteq A \cap B \cap m$.
Write $C$ for $c\cup(A\setminus m)$ (whence also $C=c\cup(B\setminus m)$).
Then clearly for $n \in\nat\setminus m$ it holds that 
\[
\from[A](s\conc n)=\from[C](s\conc n)=\from[B](s\conc n).
\qedhere
\]
\end{proof}
\begin{rem}
Note that it is necessary to ask $s \notin \higherdom(\from[A]) \Delta \higherdom(\from[B])$; for otherwise, it may be the case 
that, e.g., $s \notin \higherdom(\from[A])$ and thus $\from[A](s) = \emptyset$, while $s \in \higherdom(\from[B])$ and thus $\from[B](s) \in \finpp[\gamma(s)]$; so clearly, $\from[A](s)\Delta\from[B](s)\notin \finp[\gamma(s)]$ in this case. 
If $s \notin \higherdom(\from[A]) \cup \higherdom(\from[B])$ it holds that $\from[A](s) = \from[B](s)=\emptyset$, but we do not seem to ever need this case.
\end{rem}

Likewise, similar to the two-dimensional case, a pigeonhole principle holds.
In fact, the following formulation provides a much stronger pigeonhole principle than is required for the proof of the main theorem. 
\begin{lem}[Simple Pigeonhole Principle in $\leq\alpha$ dimensions]\label{l.alphaD.pidgeon.simple
Fix $s \in \higherdom(S_\alpha)$. For any $X \subseteq S_\alpha(s)$ and any $A\in[\nat]^{\infty}$ there is $A' \in [A]^{\infty}$ such that 
$\from[A'](s) \subseteq X$ or 
$\from[A'](s) \subseteq S_\alpha(s)\setminus X$.
\end{lem}
Note that the inclusions in the lemma are complete, i.e., with respect to $\subseteq$, instead of just with respect to $\subseteq_{\fin[\alpha]}$. 
But this stronger property is not needed, and it will also fail for the crucial, slightly stronger pigeonhole principle which we shall prove as a corollary to the present, simpler principle.
Also, this stronger property is not essential to the inductive proof of the above lemma which we are about to give (but it does unburden notation slightly).
\begin{proof}
We begin the proof of the lemma by first showing the following:
\begin{claim}\label{c.alphaD.pigeon}
Suppose we are given $A\in[\nat]^{\infty}$, $l \in A$,
and a non-empty set $a \in [A]^{<\infty}$ such that $l < \min(a)$.
Write $s=\hat X^l(\hat a)$.
Then for any $X \subseteq S_\alpha(s)$ there is $A' \in [A]^{\infty}$ such that firstly, 
\[
A' \cap \big(\max(a)+1\big) = \{l\}\cup a
\]
and secondly, 
$\from[A'](s)  \subseteq X$ or 
$\from[A'](s) \subseteq S_\alpha(s)\setminus X$.
\end{claim}
\begin{proof}[Proof of Claim~\ref{c.alphaD.pigeon}]
The proof is by induction on $\gamma(s)$.
For the induction start, suppose $\gamma(s)=1$. 
Write $B=\{l\}\cup a \cup \big(A\setminus (\max(a)+1)\big)$.
Then $\from[B](s) \subseteq \nat$, $X(s) \subseteq \nat$, and $\fin[\gamma(s)]=\fin$.
One of the sets $\from[B](s) \cap X$ or $\from[B](s) \setminus X$ must be infinite; let $C$ denote this set.
Therefore, likewise, one of the sets $\from[B]\cap \{s \conc t \setdef t \in X\}$ or $\from[B]\cap \{s \conc t \setdef t \notin X\}$ must be infinite; 
let $D$ denote this set and observe that $D(s)=C$.
Let 
\[
A' = \{l\}\cup a\cup \{n \in \nat \setdef \hat X^l(\hat a \conc \langle n\rangle) \in C\}.
\]
Then as $a\neq\emptyset$, 
$A'(s)= D(s)=C$.
So clearly $A'$ is as desired.

\medskip

Now suppose that $\gamma(s)>1$. 
We construct increasing sequences $n_0, n_1, n_2, \hdots$ from $A$ and a $\subseteq$-decreasing sequence $A_0, A_1, A_2, \hdots$ from $[A]^{\infty}$ by induction, as follows:

Let $A_0 = A$ and
$n_0 =\min(A_0\setminus a)$.
Suppose now we have already defined $n_k$ and $A_k$.
Write $a_*=a\cup\{n_k\}$ and $s_*= \hat X^{l}(\hat{a_*})$.
Since $\gamma(s_*) < \gamma(s)$ and by the induction hypothesis, we can find $A_{k+1} \in [A_k]^{\infty}$ such that
$A_{k+1} \cap (n_k + 1) = \{l\} \cup a_*$ such that we have either
\[
\from[A_{k+1}](s_*) \subseteq X
\]
or
\[
\from[A_{k+1}](s_*) \subseteq S_\alpha(s_*)\setminus X.
\]
Let $n_{k+1}=\min\big(A_k \setminus(n_k+1)\big)$.
This finishes the construction of $n_0, n_1, n_2, \hdots$ (and $A_0, A_1, A_2, \hdots$, which are not needed anymore).

Letting 
\[
A^k = \{l\}\cup a\cup\{n_i\setdef i \in \nat\setminus k\},
\]
and letting $a_k = a\cup\{n_k\}$ and $s_k = \hat X^l(\hat s_k)$
by construction we have that for each $k\in\nat$, either
\begin{equation}\label{e.case.A.pidgeon1}
\from[A^k](s_k) \subseteq X
\end{equation}
or
\begin{equation}\label{e.case.A.pidgeon2}
\from[A^k](s_k) \subseteq S_\alpha(s_k)\setminus X.
\end{equation}
One of \eqref{e.case.A.pidgeon1} or \eqref{e.case.A.pidgeon2} must holds for infinitely many $k\in \nat$.
So we may find $Y\in[\nat]^{\infty}$ such that either, for all $k\in Y$ \eqref{e.case.A.pidgeon1} holds, or else, for all $k\in Y$ \eqref{e.case.A.pidgeon2} holds.
Finally, let 
\[
A' = \{l\}\cup a \cup\{n_k\setdef k \in Y\}.
\]
Using the definition of the $\sim$-operator and that $a\neq\emptyset$ we see that for any $k\in\nat$ it holds that $\from[A'](s_k)= \from[B^k](s_k)$ where 
$
B^k=\{l\}\cup a\cup\{n_i \setdef i \in Y \setminus k\}. 
$
Thus, by construction, 
the set $A'$ is as promised.
\renewcommand{\qedsymbol}{{\tiny  Claim~\ref{c.alphaD.pigeon}~}$\Box$}
\end{proof}
Given the claim, it is not hard to proove Lemma~\ref{l.alphaD.pidgeon.simple}.
Let $A$,  $s$ and $X$ be given as in said lemma. 
We make a case distinction.

\medskip

\textbf{Case A:} Let us first assume $s\neq\emptyset$.
We may assume $s \in \higherdom(\from[A])$ since otherwise $\from[A](s)=\emptyset$ and we are done. 
Thus we may find $t \in \from[A]$ such that $s \subseteq t$, and
 $l^*\in \nat$ such that $t \in X^{l^*}$.
We have that $s \in \higherdom(\from[A]\cap X^{l^*})$ and so $l^* \prec^{A} \min(a)$, where $a$ is such that
$\hat X^{l^*}(\hat a)=s$.
Now find $A'$ as in the claim.

\medskip

\textbf{Case B:} It remains to show the lemma in case $s=\emptyset$.
Construct an increasing sequence $n_0, n_1, n_2, \hdots$ from $A$ and a $\subseteq$-decreasing sequence $A_0, A_1, A_2, \hdots$ from $[A]^{\infty}$ by induction, as follows:
Let $n_0 = \min(A)$ and $A_0 = A$.

Suppose now we have already constructed $n_k$ and $A_k$.
Use the claim finitely many times---namely, once for each $l \in \{n_i \setdef i <k\}$, with  $\{n_k\}$ for $a$ and with $\{l\}\cup \{n_k\}\cup A_k$ for $A$---to obtain 
$A_{k+1} \in [A_k]^\infty$ such that $n_{k} = \min(A_k)$ and for each $l \in \{n_i \setdef i <k\}$ one of the following holds: 
$\from[\{l\}\cup A_{k+1}](\langle n_k\rangle) \subseteq X$ or
$\from[\{l\}\cup A_{k+1}](\langle n_k\rangle) \subseteq S_\alpha(\langle n_k\rangle)\setminus X$.
This finishes the inductive construction of $n_0, n_1, n_2, \hdots$ (and of $A_0, A_1, A_2, \hdots$, which are no longer required).

Finally, let $A_\infty = \{n_k \setdef k\in\nat\}$.
By construction, for every $\{l,m\}\in A_\infty$ with that $l<m$ it holds that letting $B=\{l\}\cup(A_\infty\setminus m)$, either 
$\from[B](\langle m\rangle) \subseteq X$ or
$\from[B](\langle m\rangle) \subseteq S_\alpha(\langle n_k\rangle)\setminus X$.

Define a coloring
\[
c\colon [A_\infty]^2 \to 2
\]
as follows: For $\{l,m\} \in [A\setminus k]^3$ such that $l<m$, momentarily writing
$B=\{l\}\cup(A_\infty\setminus m)$, let
\[
c(l,m)=\begin{cases}
0 &\text{ if $\from[B](\langle m\rangle) \subseteq X$, }\\
1 &\text{ if $\from[B](\langle m\rangle) \subseteq S_\alpha(\langle m\rangle)\setminus X$.}\\
\end{cases}
\]
By the Infinite Ramsey's Theorem find $A'\in[A_\infty\setminus k]^{\infty}$ such that $c$ takes only one colour on $[A']^2$.
By construction $A'$ is as desired, proving Lemma~\ref{l.alphaD.pidgeon.simple}.
\end{proof}



As a corollary, we also have the following pigeonhole principle, which will be crucial to the proof of our main theorem about $\fin[\alpha]$-\emph{mad} families:
\begin{cor}[Pigeonhole Principle in $\leq\alpha$ dimensions]\label{c.alphaD.pidgeon}
Suppose $s \in \higherdom(S_\alpha)$,  $X \subseteq S_\alpha(s)$, and $n\in \omega$ are given.  For any $A\in[\omega]^{\omega}$ there is $B \in [A]^{\omega}$ such that $B \cap n = A \cap n$ and 
$\from[B](s) \subseteq_{\fin[\gamma(s)]} X$ or $\from[B](s) \subseteq_{\fin[\gamma(s)]} S_\alpha(s)\setminus X$.
\end{cor}
\begin{proof}
This follows easily from the previous lemma: First use said lemma to find $A' \in [A]^\omega$ such that
$\from[A'](s) \subseteq X$ or $\from[A'](s) \subseteq S_\alpha(s)\setminus X$. (Note that $\subseteq_{\fin[\gamma(s)]}$ would be enough!)
Now let 
\[
B = (A \cap n) \cup A'.
\] 
If $s \notin \higherdom(\from[B])$ then clearly $X(s) \cap \from[B](s) = \emptyset$, so let us assume $s \in \higherdom(\from[B])$. 
Since $B \mathbin{E_0} A'$, and by the invariance property of the $\sim$-operator from Lemma~\ref{l.alphaD.invariance}, 
$\from[B](s) \Delta \from[A'](s) \in \fin[\gamma(s)]$ and so  
$\from[B](s) \subseteq_{\fin[\gamma(s)]} X$ or $\from[B](s) \subseteq_{\fin[\gamma(s)]} S_\alpha(s)\setminus X$. 
\end{proof}

\begin{lem}[The Almost Disjointness Principle]\label{l.alphaD.tilde.ad}
For any $\bar A \in \mathcal A$ and any $B \in [\nat]^{\infty}$, there is
$B' \in [B]^{\infty}$ such that $\bar A \cap \from[B']\in \fin[\alpha]$.
\end{lem}
\begin{proof}
We construct a sequence 
$\langle n_k \setdef k\in\nat\rangle$ from $\nat$ by induction. 
Let $n_0 = \min(A)$.
Now suppose we have already defined $n_k$.
Let $n_{k+1}$ be the least element $n \in A\setminus (n_k +1)$ such that letting $s=\hat X^{n_k}(\langle n\rangle)$, we have 
$\bar A (s) \in \fin[\gamma(s)]$; such $n$ exists since $X^{n_k} \cap \bar A \in \fin[\alpha]$.
Finally, let $A' = \{n_k \setdef k\in\nat\}$.
Then clearly, for every consecutive elements $l,m$ of $A'$,  letting $s=\hat X^{l}(\langle m\rangle)$ it holds that $\bar A(s) \in \fin[\gamma(s)]$ and so
$\bar A \cap \from[A'] \in \fin[\alpha]$.
\end{proof}

\subsection{The higher dimensional tree family}

\begin{dfn}
For $\bar X \in {\finalph}^+$ and $d \in [\dom(S_\alpha)]^{<\infty}$ define
\begin{equation*}
T^{\bar X,d}=\{s \in T\setdef (\exists \bar A \in \pi[T_s])\; \bar A \cap \bar X \in{\finalph}^+ \land
 (\forall s\in d)\; \bar A(s) \cap \bar X(s) \in \finp[\gamma(s)]\} 
\end{equation*}
\end{dfn}

It is again easy to see that for any $\bar X,\bar Y \in {\fin[2]}^{+}$ and $d \in \left[\higherdom(S_\alpha)\right]^{<\infty}$ the following hold:
\begin{facts}~\label{f.alphaD.T^z,d}
\begin{enumerate}
\item\label{i.alphaD.T^z,d.invariant} $[(\forall s\in d)\; \bar X(s) \Delta \bar Y(s) \in \fin[\gamma(s)] \land \bar X \Delta \bar Y \in\fin[\alpha] ]\Rightarrow T^{\bar X,d} = T^{\bar Y,d}$,
\item\label{i.alphaD.T^z,d.invariant.corollary} If $A_0 \mathbin{E_0} A_1$ and for each $i\in\{0,1\}$ it holds that $d \subseteq \higherdom(\from[A_i])$, 
then also $T^{\bar X,d} = T^{\bar Y,d}$.

\item $T^{\bar X,d}$ is a sub-tree of $T^{\bar X}$,

\item\label{i.alphaD.T^z,d.pruned} $T^{\bar X,d}$ is pruned, i.e., $t \in T^{\bar X,d} \iff [T^{\bar X,d}]\neq \emptyset$,

\item\label{i.alphaD.T^z,d.non-empty} $T^{\bar X,\emptyset} = T^{\bar X}$, and $T^{\bar X,\emptyset}\neq\emptyset$ if and only if there is $\bar A \in \mathcal A$ such that $A \cap X \in {\finalph}^+$.
\end{enumerate}
\end{facts}
The most crucial fact about these trees is expressed by the following lemma:
\begin{lem}\label{l.alphaD.branch}\label{l.alphaD.branch'}
Suppose $t_0, t_1 \in T^{\bar X}$, $\lh(t_0) = \lh(t_1)$ but $\pi(t_0)\neq \pi(t_1)$.
Then we can find
\begin{itemize} 
\item a set $d \in \big[\higherdom(S_\alpha)\big]^{<\infty}$ which is closed under taking initial segments,
\item nodes  
$t'_0, t'_1 \in  T$ such that 
\[
t'_i \in T^{\bar X,d}_{t_i}
\]
for each $i\in \{0,1\}$,
\item as well as $s \in d$ and $m\in\nat$,
\end{itemize}
such that for all pairs $(w_0,w_1) \in  [T^{\bar X,d}_{t'_0}] \times [T^{\bar X,d}_{t'_1}]$ we have:
\begin{enumerate}[label=(\Roman*),ref=\Roman*]
\item\label{i.alphaD.branch.I} If $\gamma(s)>1$, 
\begin{equation*
\dom^s_\infty(\pi(w_0)\cap\bar X)\cap \dom^s_\infty(\pi(w_1)\cap \bar X) \subseteq m,
\end{equation*}

\item\label{i.alphaD.branch.II} If $\gamma(s) =1$, 
\[
\pi(w_0)(s)\cap \pi(w_1)(s)\subseteq m.
\]
\end{enumerate}
\end{lem}
\begin{rem}
It may be worth noting that the $m$ whose existence the lemma asserts can be taken to be $\max\{n\in\nat\setdef s\conc n\in \higherdom(d) \cup d\}$ (as the reader will see in the proof).
\end{rem}

\iffalse
\begin{rem}\label{r.notation}
Admitting slightly more abstract notation, we can write the lemma so that the common underlying structure of both cases becomes more apparent: 
View $\fin[0] = \{\emptyset\}$ as the trivial ideal on the one-point set $S_0=\{\emptyset\}$ and note that by magic of notation,
$X(s) = \{\emptyset\}$ if $s\in X$ and $X(s)=\emptyset$ otherwise. 
This amounts precisely to viewing $\fin$ as the Fubini sum taken over $\fin$ of $\omega$-many copies of $\fin[0]$.
To further make the notation uniform, we let both $\finpp[0]$ and $\finp[0]$ mean the co-ideal, i.e., $\powerset(S_0)\setminus\fin[0]$ in this case (which consists just of the single set $S_0$).
In other words, $s \in X$ if and only if $X(s) \notin \fin[0]$.
\end{rem}
\fi

\iffalse
With this notation the lemma becomes:
\begin{lem
Suppose $t_0, t_1 \in T^{\bar X}$, $\lh(t_0) = \lh(t_1)$ but $\pi(t_0)\neq \pi(t_1)$.
There are $d \in \big[\higherdom(S_\alpha)\big]^{<\infty}$
and  
$t'_0, t'_1 \in  T$ such that 
\[
t'_0 \in T^{\bar X,d}_{t_0} \text{ and } t'_1 \in T^{\bar X,d}_{t_1}
\]
\emph{and} there are $s \in d$ and $m\in\nat$ such that for all pairs $(w_0,w_1) \in  [T^{\bar X,d}_{t'_0}] \times [T^{\bar X,d}_{t'_1}]$,
\[
(\forall n \geq m) \; \big(\pi(w_0) \cap \pi(w_1) \cap \bar X\big)(s\conc n)\in \fin[\gamma(s\conc n)]
\]
\end{lem}
\fi


\medskip

For the proof of the lemma we need an $\alpha$-dimensional analogue of $\sqsubset_2$.
\begin{dfn}
Given $b^0, b^1 \in [S_\alpha]^{<\infty}$ 
write $b^0 \sqsubset_\alpha b^1$ to mean that
$b^0 \subseteq b^1$ and
 for each $s\in \higherdom(b^0)\cup\{\emptyset\}$,
\[
\max \{n\in\nat \setdef s \conc n \in b\} < \max  \{n\in\nat \setdef s \conc n \in b'\},
\]
that is,
\[
\{n\in\nat \setdef s \conc n \in b\} \sqsubsetneq \max  \{n\in\nat \setdef s \conc n \in b'\}
\]
(where, as we wish to remind the reader, for $a,a'\in[\nat]^{<\infty}$,  $a \sqsubsetneq a'$
 means that
$\hat a$ is proper initial segment of $\hat a'$).

 \end{dfn} 
 By the following obvious fact (which we state without proof), this gives us a way to build sets in the co-ideal:
 \begin{fct}
 If $\langle b_k \setdef k \in \nat\rangle$ satisfies $b_k \sqsubset_\alpha b_{k+1}$ for each $k\in \nat$, 
 it must hold that
 \[
 \bigcup_{k\in\nat} b_k \in {\finalph}^{++}.
 \]
 \end{fct}
 \begin{rem}
 If instead of quantifying over all  $s\in \higherdom(b)\cup\{\emptyset\}$, we only quantify over all $s\in \higherdom(b)$ in the above definition, 
 we would have, e.g., $\emptyset \sqsubset_\alpha \emptyset$, vacuously.
 More seriously, the fact above would fail.
 \end{rem}
 
 The proof of Lemma~\ref{l.alphaD.branch'} above can now be carried out closely following the blueprint of the proof of its two-dimensional analogue, Lemma~\ref{l.2D.branch}.
 %
 %
 %
 %
 %
 %
 \begin{proof}[Proof of Lemma~\ref{l.alphaD.branch'}]
 The proof is almost verbatim as in the 2-dimensional case. 
 Again, assume $\bar X \in {\fin[2]}^{+}$ and
fix $t_0, t_1 \in T^{\bar X}$ such that $\lh(t_0) = \lh(t_1)$ but $\pi(t_0)\neq \pi(t_1)$.
As before we suppose the lemma fails and derive a contradiction.







Analogously to the 2-dimensional case, We build sequences
\begin{itemize}
\item $b^0  \subseteq  b^1  \subseteq  b^2  \subseteq  \hdots$ from $[S_\alpha]^{<\infty}$,
\item $d^0 \subseteq d^1 \subseteq  d^2 \subseteq \hdots$ from $[\higherdom(S_\alpha)]^{<\infty}$,
\item $t^0_i  \subseteq  t^1_i  \subseteq  t^2_i  \subseteq \hdots$ from $T_{t_i}$ for each $i\in\{0,1\}$, 
\end{itemize}
such that
for each $k\in \nat$
\begin{enumerate}[label=(\Alph*)]
\item\label{IH.grow'}  $b^k \sqsubset_\alpha b^{k+1}$,
\item\label{IH.subseteq'} $b_{k+1} \subseteq \pi(t^k_0)\cap \pi(t^k_1)$,
\item\label{IH.keep.going'}\label{IH.last} $t^{k+1}_i \in T^{\bar X,d^k}_{t^k_i}$.
\end{enumerate}
Let $d^0 = \higherdom(b^k)\cup\{\emptyset\}$ (this will ensure that at the first step, i.e., when  $k=0$, the following construction is not vacuous) $b^0=\emptyset$ and $t^0_i = t_i$ for each $i\in\{0,1\}$.

We describe the inductive step of the construction:
Suppose we have constructed $b^k$, $t^k_0$, and $t^1_k$.
We find $b^{k+1}$ satisfying \ref{IH.grow} by appliying finitely many times---once for each $s \in \higherdom(b^k)$---the assumption that Lemma~\ref{l.2D.branch} fails. 

Let $d^{k,0} = d^k$.
Write $\bar j = \lvert d^0 \rvert$  and let $\langle s^j \setdef j < \bar j\rangle$ enumerate  $d^{k,0}$. 
We build finite sequences $\langle d^{k,j} \setdef j \leq \bar j\rangle$,  $\langle b^{k,j} \setdef j \leq \bar j\rangle$, and $\langle t^{k,j}_i \setdef j \leq \bar j\rangle$ for $i \in\{0,1\}$, starting with $t^{k,0}_i = t^k_i$ and $b^{k,0}=b^k$.

Suppose now we already have  $d^{k,j}$, $b^{k,j}$, $t^{k,j}_0$, and $t^{k,j}_1$.
If $\gamma(s_j)>1$, use the failure of \eqref{i.alphaD.branch.II} 
to find $m > \max\big((b^{k,j})_{s_j}\big)$ and $t^{k,j+1}_i$ for each $i\in\{0,1\}$
such that
\[
t^{k,j+1}_i \in T^{\bar X,d^{k,j}\cup\{ s_j\conc m\}}_{t^{k,j}_i}. 
\]
We let $b^{k,j+1} = b^{k,j}$ and $d^{k,j+1} = d^{k,j}\cup\{s_j\conc m\}$ in this case.

If $\gamma(s_j)=1$, use the failure of \eqref{i.alphaD.branch.I} 
to find $m > \max\big((b^{k,j})_{s_j}\big)$ such that
\[
s_j\cap m \in \pi(t^{k,j+1}_0) \cap \pi(t^{k,j+1}_1).
\] 
We let $b^{k,j+1} = b^{k,j}\cup\{s_j\conc m\}$ and $d^{k,j+1} = d^{k,j}$ in this case.

By induction we have
\[
b^{k,j} \subseteq \pi(t^{k,j+1}_0) \cap \pi(t^{k,j+1}_1).
\] 
Finally let $b^{k+1} = b^{k,\bar j}$ and $t^{k+1}_i = t^{k,\bar j}_i$ for each $i\in\{0,1\}$, finishing the inductive step from $k$ to $k+1$ and thus the definition of $b^k$ and $t^k_i$ for each $k\in\nat$ and $i\in\{0,1\}$.
But exactly as in the 2-dimensional case,
\[
\bigcup_{k\in\nat} b^k \subseteq \pi\left(\bigcup_{k\in\nat} t^k_0\right)\cap \pi\left(\bigcup_{k\in\nat} t^k_1\right)
\]
which contradicts that $\mathcal A$ is a $\fin[\alpha]$-almost disjoint family since the left hand side is an element of ${\finalph}^+$ by \ref{IH.grow'}. Having reached a contradiction, the proof of Lemma~\ref{l.alphaD.branch'} is complete.
 \end{proof}
 

\subsection{Proof of the higher dimensional theorem}

We are now ready to state and prove the $\alpha$-dimensional analogue of Theorem~\ref{t.2D.analytic}.

\begin{thm}\label{t.alphaD.analytic}
Suppose $\mathcal A$ is an analytic $\fin[\alpha]$-a.d.\  family  and $\vec x = \langle x^l\setdef l\in\nat\rangle$ is a sequence of pairwise disjoint sets from ${\finalph}^{++}$ each of which is a subset of an element of $\mathcal A$ (analogously as in Fact~\ref{x.sequence}).
For any $W \in [\nat]^{\infty}$ there is $W_0 \in [W]^{\infty}$ such that  $\fromx[\vec x]{W_0}$ is $\fin[\alpha]$-a.d.\  from each element of $\mathcal A$.
\end{thm} 
\begin{proof}
The proof strategy is similar to the 2-dimensional case: 
Let $\mathcal A$ and $\vec x$ as in the lemma be given.
Fix a tree $T$ on $2\times\nat$ such that $\pi[T]=\mathcal A$.

Similarly to the 2-dimensional case, for each $d \in [S_\alpha]^{<\infty}$ we make  the function 
\[
(B,d) \mapsto T^{\from[B],d}
\] 
constant,
using the fact that analytic sets are completely Ramsey and ``invariance'' of each of the trees.
\begin{claim}\label{c.alphaD.constant}
For every $W \in [\nat]^{\infty}$ there is $W_0 \in [W]^{\infty}$ such that 
\[
(\forall W' \in [W_0]^{\infty})(\forall d \in [\higherdom(\from[W'])]^{<\infty})\; T^{\from[W'],d}=T^{\from[W_0],d}
\]
\end{claim}
\begin{proof}[Proof of Claim~\ref{c.alphaD.constant}]
The proof is by a fusion argument similar to that of Claim~\ref{c.2D.constant}.
Let $\langle(d_k, t_k)\setdef k\in\nat\rangle$ enumerate $[S_\alpha]^{<\infty}\times T$ so that each element of $[S_\alpha]^{<\infty}\times T$ occurs infinitely many times in the enumeration.
Let for each $k\in T$
\[
D_k=\{B \in[\nat]^2\setdef t_k \in T^{\from[B],d_k}\}
\]
and note that this set is analytic and hence, completely Ramsey.

\iffalse
We inductively build a sequence $(b_k,C_k) \in [\nat]^{<\infty}\times[\nat]^{\infty}$ for $k\in \nat$.
Let $(b_0, C_0)=(\emptyset, W)$. Suppose now we have constructed $(b_k,C_k)$.
Find $C_{k+1} \in [C_k\setminus b_k]^{\infty}$ such that
\begin{equation}\label{e.make.constant.one.step}
[b_k, C_{k+1}]^{\infty}\subseteq D_k \text{ or } [b_k, C_{k+1}]^{\infty}\subseteq [\nat]^{\infty} \setminus D_k,
\end{equation}
and let $b_{k+1}=b_k\cup\{\min C_{k+1}\}$.
Finally let $W_0 = \bigcup_{k\in\nat} b_k$. 
\fi
Now construct a sequence $(b_k,C_k) \in [\nat]^{<\infty}\times[\nat]^{\infty}$ for $k\in \nat$ and obtain $W_0$ verbatim as in 
the proof of Claim~\ref{c.2D.constant}.

To see that $W_0$ is as desired, let $W'\in[W_0]^{\infty}$ and a finite set $d \subseteq \higherdom(\from[W'])$ which is closed under initial segments be given.
To show $T^{\from[W'],d}=T^{\from[W_0],d}$, consider an arbitrary $t \in T$.
Find $k\in\nat$ such that $(d_k,t_k)=(d,t)$ and $d \subseteq \higherdom(\from[b_k])$.
Since $W' \subseteq_{\fin} C_{k+1}$ we may choose $W''$ such that $W'' \mathbin{E_0} W'$ and $W'' \in [b_k, C_{k+1}]^{\infty}$.
Thus by Equation~\eqref{e.make.constant.one.step},
\[
t \in T^{\from[W''],d} \iff t \in T^{\from[C_{k+1}],d}. 
\]
Moreover, applying conditional invariance of this tree as expressed in Fact\ref{f.alphaD.T^z,d}\eqref{i.alphaD.T^z,d.invariant.corollary}, since
$W'' \mathbin{E_0} W'$ and $d \subseteq \higherdom(\from[W''])$
we have
\[
T^{\from[W''],d} = T^{\from[W'],d}.
\]
and so also
\[
t \in T^{\from[W'],d} \iff t \in T^{\from[C_{k+1}],d}.
\]
The very same argument, again using $\alpha$-dimensional conditional invariance from Fact\ref{f.alphaD.T^z,d}\eqref{i.alphaD.T^z,d.invariant.corollary}, also yields
\[
t \in T^{\from[W'_0],d} \iff t \in T^{\from[C_{k+1}],d},
\]
again proving $T^{\from[W_0],d}=T^{\from[W'],d}$, as $t$ was arbitrary.
\renewcommand{\qedsymbol}{{\tiny  Claim~\ref{c.alphaD.constant}~}$\Box$}
\end{proof}
Again, $W_0$ is ``sufficiently generic'' so that $\from[W_0]$ will be disjoint from every set from $\mathcal A$. 
Again we prove two claims:
\begin{claim}\label{c.alphaD.not1branch}
$\lvert \pi[T^{*,\emptyset}]\rvert \neq 1$.
\end{claim}
\begin{proof}[Proof of Claim~\ref{c.alphaD.not1branch}]
The proof of Claim~\ref{c.2D.not1branch} applies, replacing $\fin[2]$ by $\fin[\alpha]$, and using Lemma~\ref{l.alphaD.tilde.ad}.
\renewcommand{\qedsymbol}{{\tiny  Claim~\ref{c.alphaD.not1branch}~}$\Box$}
\end{proof}
The next and final claim is sufficiently different to warrant a detailed account. In essence, the reader will find that the only major difference is that we must use the Pigeonhole Principle proved in Corollary~\ref{c.alphaD.pidgeon} instead of Fact~\ref{f.from}, as well as the higher dimensional branch lemma, Lemma~\ref{l.alphaD.branch} instead of its 2-dimensional counterpart  Lemma~\ref{l.2D.branch}.
\begin{claim}\label{c.alphaD.one.branch}
$\pi[T^{*,\emptyset}]=\emptyset$.
\end{claim}
\begin{proof}[Proof of Claim~\ref{c.alphaD.one.branch}]
Otherwise by the last claim, $\lvert \pi[T^{*,\emptyset}]\rvert\geq 2$.
Then we can choose $t_0, t_1 \in T^{*,\emptyset}$ with $\lh(t_0) = \lh(t_1)$ and $\pi(t_0)\neq \pi(t_1)$.
Use Lemma~\ref{l.alphaD.branch} to find $d \in [S_\alpha]^{<\infty}$, $s \in D$,
and 
$t'_i \in  T^{*,d}_{t_i}$ for each $i\in \{0,1\}$  
such that for all pairs $(w_0,w_1) \in  [T^{\bar X,d}_{t'_0}] \times [T^{\bar X,d}_{t'_1}]$,
\eqref{i.alphaD.branch.I} and \eqref{i.alphaD.branch.II} of said lemma holds.

Again, we argue by cases. First, let us assume $\gamma(s)>1$, in which case we shall employ \eqref{i.alphaD.branch.I}.
For each $i\in\{0,1\}$ let
\[
X^0_i = \bigcup\{\dom^s_\infty(\pi(w)\cap\from[W_0])\setdef w \in [T^{*,d}_{t'_i}] \}
\]
and
\[
\bar X_i = \{s'\in S_\alpha \setdef s'(\lh(s)) \in X^0_i\}.
\]
Find a finite set $b \in \from[W_0]$ such that $d \subseteq \higherdom(b)$, and $n \in \nat$ such that $b \subseteq \from[W_0 \cap n]$.
Use the Pigeonhole Principle from Corollary~\ref{c.alphaD.pidgeon} to find $W_1 \in [W_0]^{\infty}$ such that 
\begin{equation}\label{e.initial}
W_1 \cap n = W_0 \cap n
\end{equation} 
and such that
$\from[W_1](s)\subseteq_{\fin[\gamma(s)]} \bar X_0 (s)$ or $\from[W_1](s)\subseteq_{\fin[\gamma(s)]} \powerset(S_\alpha(s)) \setminus \bar X_0(s)$.
By \eqref{e.initial}, also $d \subseteq \higherdom(\from[W_1])$.

Just as in the 2-dimensional case, $\bar X_0(s) \cap \bar X_1(s) \in \fin[\gamma(s)]$, so we may fix $i\in\{0,1\}$ so that
\begin{equation}\label{e.alphaD.small}
\from[W_1](s)\cap \bar X_i(s)\in \fin[\gamma(s)].
\end{equation} 
Again, we now show that this contradicts $t'_i \in T^{*,d}$:

Since $T^{*,d} = T^{\from[W_1],d}$, $t'_i  \in T^{\from[W_1],d}$ and so since $s\in d$, by definition of the tree there is $w \in [T_{t'_i}]$ such that 
\begin{equation}\label{e.alphaD.big}
s \in \big(\pi(w) \cap \from[W_1]\big)^{++}. 
\end{equation} 
Also by definition of the tree, $w$  is a branch through $T^{W_1,d}_{t'_i}$ and hence through $T^{*,d}_{t'_i}$. 
But this entails $\pi(w) \subseteq \bar X_i$ which is an absurdity by Equations \eqref{e.alphaD.small} and \eqref{e.alphaD.big}.
Having reached a contradiction, this proves the claim in case $\gamma(s)>1$.

The case $\gamma(s)=1$, using \eqref{i.alphaD.branch.II}, is left to the reader. It differs from the two-dimensional case almost solely in notation.
\renewcommand{\qedsymbol}{{\tiny  Claim~\ref{c.alphaD.one.branch}~}$\Box$}
\end{proof}

By the last two Claims it has to be the case that 
$[T^{\from[W_0]}]=\emptyset$. 
By Facts~\ref{f.alphaD.T^z,d}(\ref{i.alphaD.T^z,d.pruned}) this means that $\emptyset \notin T^{\from[W_0]}$ and so by Facts~\ref{f.alphaD.T^z,d}(\ref{i.alphaD.T^z,d.non-empty}) we conclude that $\mathcal A$ is not maximal.
\renewcommand{\qedsymbol}{{\tiny  Theorem~\ref{t.alphaD.analytic}~}$\Box$}
\end{proof}








\subsection{Corollaries}\label{s.corollaries}

Just as in the two dimensional case, we can now prove our main theorem for $\fin[\alpha]$ as a corollary of the more technical Theorem~\ref{t.alphaD.analytic} which was proved in the previous section.
\begin{cor}\label{c.Finalph}
Theorem~\ref{t.Finalph} holds.
\end{cor}
\begin{proof}
The theorem follows from Theorem~\ref{t.alphaD.analytic} precisely as Theorem~\ref{t.2D.precise} followed from Theorem~\ref{t.2D.analytic} (see Section~\ref{proof.t.2D.precise}, page~\pageref{proof.t.2D.precise}).
\end{proof}

A number of results that were previously shown by somewhat different methods follow quickly from Theorem~\ref{t.Finalph}. 
\begin{cor}[\cite{haga-schrittesser-toernquist}]\label{c.alphaD.no.analytic}
There are no analytic $\fin[\alpha]$-\emph{mad} families.
\end{cor}
\begin{proof}
This clearly follows from Theorem~\ref{t.Finalph} (Corrollary~\ref{c.Finalph}) above taking $\Gamma=\Sigma^1_1$, $\Gamma'=\sigma(\Sigma^1_1)$ and using Jankov-von Neuman uniformization (see \cite[18.1]{kechris}) and the fact that $\sigma(\Sigma^1_1)$ sets have the Ramsey property. Also note Remark~\ref{r.sequence}.
\end{proof}
The special case $\alpha=1$ of the following two corollaries was also shown by Neeman and Norwood \cite{neeman-norwood} under the more general assumption $\AD^{++}$.
Moreover, both of the following corollaries were shown in \cite{haga-schrittesser-toernquist} for a much larger class of ideals.
\begin{cor
Let $\alpha<\aleph_1$ and assume \AD.
There are no infinite $\fin[\alpha]$-\emph{mad} families in $\mathbf{L}(\reals)$.
\end{cor}
\begin{proof}
Suppose otherwise. Then in particular, $\mathbf{L}(\reals)$ satisfies that an
infinite $\fin[\alpha]$-\emph{mad} family $\mathcal A$ exists.
By Solovay's Basis Theorem \cite[p.~1983, 2.29(3)]{handbook}
we can assume that $\mathcal A$ is an element of a scaled point-class $\Gamma$.
In particular, the hypotheses of Theorem~\ref{t.Finalph} (Corrollary~\ref{c.Finalph}) above are satisfied taking $\Gamma=\Gamma'$---
observe here that by \cite{kechris-DC}, $\DC$ holds in $\mathbf{L}(\reals)$. Thus by Theorem~\ref{t.Finalph}, no such $\mathcal A$ can exist, contradiction.
\end{proof}

\begin{cor}[\cite{haga-schrittesser-toernquist}
Let $\alpha<\aleph_1$.
Under $\PD + \DC$, there are no projective $\fin[\alpha]$-\emph{mad} families.
\end{cor}
\begin{proof}
By $\PD$ every subset of $[\nat]^\infty$ has the Ramsey property, and projective uniformization holds.
So the corollary follows by Theorem~\ref{t.Finalph} (Corrollary~\ref{c.Finalph}) and Remark~\ref{r.sequence} above.
\end{proof}



\section{A co-analytic mad family in the Laver model}\label{laver}

We now prove Theorem~\ref{t.laver}, i.e., that there is an infinite $\Pi^1_1$ (lightface) mad family in the Laver extension of $L$.
As has been mentioned in the introduction, this shows that the proofs of the previous theorems do not easily generalize to other forcings (than Mathias forcing) which add a quickly growing real.

\medskip

We will denote by ${\mathbb L}$ the Laver forcing poset. Conditions of ${\mathbb L}$ are stemmed Laver trees, i.e., they are subtrees of $\omega^{<\omega}$ which split infinitely at every note above the stem of the tree,  see \cite[p.~565]{jech}. We order ${\mathbb L}$ by letting $q\leq p$ just in case $q$ is a sub-Laver tree of $p$. We will write $\s(p)$ for the stem of $p$, and for $s\in\omega^{<\omega}$ we let
$$
{\mathbb L}_s=\{p\in{\mathbb L}: s(p)=s\}.
$$
A stemless Laver tree is simply called a Laver tree; whence ${\mathbb L}_{\emptyset}$ is the set of Laver trees.

\begin{dfn}
We write $q\leq^* p$ just in case $q\leq p$ and $s(q)=s(p)$.
\end{dfn}

Given $p\in{\mathbb L}$ and $t\in p$, we let $p/t$ be the tree consisting of all $s\in p$ that are compatible with $t$. Note that $p/t$ is a stemmed Laver tree, whose stem extends $t$.

For $p\in{\mathbb L}$, we write $[p]$ for the set of infinite branches through the tree $p$.

\medskip

The proof of Theorem \ref{t.laver} is built around the same basic ideas as the results about maximal discrete sets in the Sacks and Miller forcing extensions in \cite{mrl}, but applies only to almost disjointness\footnote{The very general theorems about maximal discrete sets in \cite{mrl} are not true for Laver forcing.} 

\medskip

Most of the proof consists of establishing the following lemma:

\begin{lem}[The main lemma]
Let $p\in{\mathbb L}$ and suppose $f:[p]\to[\omega]^\omega$ is continuous. Then there $q\leq p$ and a continuous $\tilde f:[q]\to [\omega]^\omega$ such that $\ran(\tilde f)$ is almost disjoint and $\tilde f(x)\subseteq f(x)$ for all $x\in [q]$.
\end{lem}

The proof is found in the next section. Accepting the Lemma on its face for the moment, the proof of Theorem \ref{t.laver} follows exactly the path of Theorem 3.1 in \cite{mrl}.

We need the following analogue of the perfect set theorem for Laver forcing, which was proved by Arnold Miller in \cite{miller2012}. In this context, a \emph{Hechler tree} is a tree $H\subseteq\omega^{<\omega}$ such that for each $t\in H$, the set
$$
\{i\in\omega: t{^\frown\!} i\in H\}
$$
is cofinal. We will say that a tree $H\subseteq p$, where $p\in{\mathbb L}$ is Hechler \emph{in $p$}, if for all $t\in H$ which are extending the stem of $p$ we have that
$$
\{i\in\omega: t{^\frown\!} i\in H\}
$$
is cofinal.

\begin{thm}[Miller]
(1) Let $A\subseteq \omega^\omega$ be an analytic set. Then either there is a Laver tree $p$ such that $[p]\subseteq A$, or there is a Hechler tree $H$ such that $[H]\cap A=\emptyset$.

(2) If $A$ is $\Sigma^1_1$ (lightface), then the following effective strengthening holds: Either there is a $\Delta^1_1$ Hechler tree $H$ such that $[H]\cap A=\emptyset$, or else there is a Laver tree $p$ such that $[p]\subseteq A$
\end{thm}

We note that while (2) above is not stated explicitly in \cite{miller2012}, it follows rather easily, since the Miller's ordinal analysis argument can be carried out in $L_{\omega_1^{CK}}$.

Miller's theorem gives us the following analogue of Fact 3.3 in \cite{mrl}


\begin{fct}\label{f.miller}
(1) If $A\subseteq\omega^\omega$ is an analytic set and 
$$
p'\Vdash_{{\mathbb L}} \dot x_G\in A,
$$
then there is $p\leq p'$ (indeed, $p\leq^* p'$) such that $[p]\subseteq A$.

(2) If $\psi(x,y)$ is a $\Pi^1_1$ formula, then the set
$$
\{(p,a)\in{\mathbb L}\times\omega^\omega: p\Vdash_{{\mathbb L}}\psi(\dot x_G,\dot a)\}
$$
is $\Pi^1_1$.
\end{fct}
\begin{proof}
(1) If there is no such $p$, then there is a Hechler tree $H$ such that $[H]\cap A=\emptyset$. But then there is $q\leq p'$ such that $q\subseteq H$, contradicting that $p\Vdash x\in A$.

(2) Fix $a\in\omega^\omega$, and let
$$
A_{a,p}=\{x\in [p]: \neg\psi(x,a)\}.
$$
We claim that $p\Vdash \psi(\dot x_G,\check a)$ if and only if there is a Hechler tree $H$ in $p$ which is $\Delta^1_1(a,p)$ such that $[H]\cap A_{a,p}=\emptyset$. The ``if'' direction is clear. The only if direction follows by the effective version of Miller's theorem.

Note that we now have:
$$
p\Vdash \psi(x_G,\check a)\iff (\exists H\in\Delta^1_1(p,a)\text{ Hechler})(\forall x\in H)
\ \psi(x,a).
$$
By the Spector-Gandy theorem, the right hand side gives the desired $\Pi^1_1$ definition.
\end{proof}

\begin{proof}[Proof of Theorem \ref{t.laver}, given the main lemma]
We will define a $\Sigma^1_2$ predicate $\varphi(x)$ which defines a mad family in $L[r]$ (and in $L$), whenever $r$ is a Laver real over $L$. By \cite{tornquist-pi}, it then follows that there is a $\Pi^1_1$ mad family in $L[r]$. We omit the painstaking verification that the predicate $\varphi$ is $\Sigma^1_2$, as this follows exactly as in \cite{mrl}.

We work in $L$ to define $\varphi$. Let $(p_\xi, f_\xi)$, $\xi<\omega_1$, be a $\Sigma^1_2$ enumeration of all pairs of $p\in{\mathbb L}$ and $f:[p]\to [\omega]^\omega$ continuous. Let $\mathcal A_0$ be any $\Pi^0_1$ infinite a.d. family. Suppose $\mathcal A_\gamma$ has been defined for all $\gamma<\xi$. If
$$
p_\xi\Vdash (\forall\gamma<\xi)(\forall y\in \mathcal A_\gamma) |f(x_G)\cap y|<\infty
$$
then by Fact \ref{f.miller} there is $p\leq p_\xi$ such that
$$
(\forall x\in [p])(\forall\gamma<\xi)(\forall y\in \mathcal A_\gamma) |f(x)\cap y|<\infty.
$$
Let $(q,\tilde f)$ be the $<_L$-least pair satisfying the Main Lemma for some such $p$ and $f=f\!\upharpoonright\! [p]$, and let $A_\xi=\ran(\tilde f)\cup\bigcup_{\gamma<\xi}$; otherwise let $\mathcal A_\xi=\bigcup_{\gamma<\xi} \mathcal A_\gamma$. One may quite easily verify that
$$
\mathcal A=\bigcup_{\xi<\omega_1} \mathcal A_\xi
$$
is $\Sigma^1_2$ and a.d. Let $\varphi(x)$ be the natural $\Sigma^1_2$ predicate defining $\mathcal A$.

We claim that $\varphi$ defines a mad family in $L[r]$ whenever $r$ is a Laver real. It is quite clear that $\varphi$ defines an a.d. family in $L[r]$. Suppose, seeking a contradiction, that $\varphi$ doesn't define a mad family, and so there is some $p\in{\mathbb L}$ and some name $\sigma$ for an element $[\omega]^\omega$ such that
$$
p\Vdash (\forall x) (\varphi(x)\to |\sigma\cap x|<\infty).
$$
Since Laver forcing has continuous reading of names, we can assume there is a function $f:[p]\to [\omega]^\omega$ (in $L$) such that
$$
p\Vdash f(x_G)=\sigma.
$$
Then there is $\xi<\omega_1$ such that $(p,f)=(p_\xi,f_\xi)$. Then by Miller's theorem for some $p'\leq p$ we have
$$
(\forall x\in [p'])(\forall\gamma<\xi)(\forall y\in \mathcal A_\gamma) |f(x)\cap y|<\infty.
$$
Taking $(q,\tilde f)$ be $<_L$-least such that the Main Lemma is satisfied for some such $p'$ and $f=f\!\upharpoonright\! [p']$, we get $\ran(\tilde f)\subseteq \mathcal A$, contradicting that $q\Vdash (\forall y\in\mathcal A) |y\cap f(x_G)|<\infty$.
\end{proof}




\subsection{Proof of the Main Lemma}

The following lemma is painfully obvious, but somehow forms the basis of the whole proof of Theorem \ref{t.laver}.

\begin{lem}
Let $\mathcal A$ be a countable family of infinite subsets of $\omega$. Then there is a countable family $\mathcal B$ of infinite subsets of $\omega$ such that
\begin{enumerate}
\item $(\forall B\in\mathcal B)(\exists! A\in\mathcal A)\ B\subseteq A$;
\item the family $\mathcal B$ consists of pairwise disjoint sets.
\end{enumerate}
\end{lem}
We shall call a family $\mathcal B$ as in the previous lemma a \emph{disjoint refinement} of the family $\mathcal A$.

\begin{dfn}
Let $p\in{\mathbb L}$, $i\in\omega$, and let $f:\omega^\omega\to\omega^\omega$ be a continuous function. We say that $p$ \emph{decides $f(x_G)_i$} if there exists $j\in\omega$ such that $p\Vdash f(x_G)_{\check i}=\check j$.
\end{dfn}

{\it Notation}: We let $[\omega]^\omega_{\bullet}$ denote the subset of $\omega^\omega$ of \emph{strictly increasing functions}. Clearly, $[\omega]^\omega_{\bullet}$ can be identified naturally with $[\omega]^\omega$, so the $_\bullet$ is mostly there to remind the reader that we're currently thinking of this set in terms of functions.


\begin{lem}\label{l.type1}
Let $f:\omega^\omega\to[\omega]^\omega_{\bullet}$ be continuous, and let $p\in {\mathbb L}$. Suppose
$$
\{q\leq^* p: q\text{ decides } f(x_G)_i\} 
$$
is $\leq^*$-dense for every $i\in\omega$. Then there is a tree $T\subseteq\omega^\omega$ and $g\in[\omega]^\omega_{\bullet}$ with the properties that
\begin{enumerate}
\item Every non-terminal $t\in T$ has infinitely many immediate extensions in $T$.
\item for each $t\in T$ which is not terminal there is $q\leq^* p/t$ with $q\supseteq T$ such that $q\Vdash f(x_G)_{\check{\lh(t)}}=\check{g(\lh(t))}$.
\item For every non-terminal $t\in T$ and $i\in\omega$, the set
$$
\{q\leq^* p/t:q\text{ decides } f(x_G)_i\}
$$
is $\leq^*$-dense below $p/t$.
\end{enumerate}
\end{lem}
\begin{proof}
Find an infinite sequence
$$
\cdots\leq^* q_1\leq^* q_0\leq^* p
$$
such that $q_i$ decides $f(x_G)_i$, and define $g$ such that $q_i\Vdash f(x_G)_{\check{i}}=\check{g(i)}$. Note that $g(i)<g(i+1)$ since $q_{i+1}\Vdash g(i)=f(x_G)_i< f(x_G)_{i+1}=g(i+1)$. 

Let
$$
T=\bigcup_{i\in\omega} \{t\in q_i: \lh(t)= i+1\}.
$$
It is clear that $T$ is a tree, that all levels of $T$ are infinite, and that $q_i\supseteq T$. Finally, if $t\in T$ with $\lh(t)=i+1$ is not terminal, then $t\in q_{i+1}$, and so $q_{i+1}/t\Vdash f(x_G)_{\check (i+1)}=\check{g(i+1)}$, showing that (2) is satisfied. Finally, (3) is clear since $q_i/t$ decides $f(x_G)_i$ for any $i$.
\end{proof}

\begin{lem}\label{l.type2}
Let $p\in{\mathbb L}$, and let $f:\omega^\omega\to\omega^\omega$ be a continuous function. Suppose there is $i\in\omega$ such that no $q\leq^* p$ decides $f(x_G)_i$. Then there is 
\begin{enumerate}[label=$(\arabic*)$]
\item a wellfounded tree $T\subseteq p$;
\item An injection $\terminal(T)\to\omega:t\mapsto j_t\in\omega$;
\item for each terminal $t\in T$, a condition $p_t\leq p$ with $s(p_t)=t$;
\end{enumerate}
such that for every $t\in T$ with $t\supseteq s(p)$ we have:
\begin{enumerate}[label=$(\alph*)$]
\item if $t$ is terminal in $T$ then $p_t\Vdash f(x_G)_i=j_t$.
\item if $t$ is not terminal in $T$, then no $q\leq^* p/t$ decides $f(x_G)_i$.
\item if $t$ is not terminal in $T$, then $t$ has infinitely many immediate successors, and exactly one of the following hold: 

\begin{enumerate}[label=$(\roman*)$]
\item all immediate extensions $t'\in T$ of $t$ are terminal, whence
$$
\{j_{t'}: t'\in T\wedge t'\supset t\}
$$
is infinite.

\item no immediate extension $t'\in T$ of $t$ is terminal.

\end{enumerate}

\end{enumerate}
\end{lem}


\begin{proof}
We define recursively a sequence of trees $T_0\subseteq T_1\subseteq\cdots\subseteq p$, with $T_0=\{t:t\subseteq s(p)\}$. Suppose $T_i$ has been defined. If $t\in T_i$ is terminal and some $q\leq^* p/t$ decides $f(x_G)_i$, then let $A_t=\{*\}$, where $*$ is some fixed set which is not an element of $\omega$. If $t$ is terminal in $T_i$ and no $q\leq^* p/t$ decides $f(x_G)_i$, then let
$$
A_t=\{k\in\omega: t{^\frown\!} k\in p \text{ and some $q\leq^* p/(t{^\frown\!} k)$ decides $f(x_G)_i$}\};
$$
Then let
\begin{align*}
T_{i+1}=T_i&\cup\{t^{^\frown\!} k: t\in T_i\wedge A_t\neq\{*\}\wedge |A_t|=\infty\wedge k\in A_t\}\\
&\cup\{t^{^\frown\!} k\in p: t\in T_i\wedge A_t\neq\{*\}\wedge |A_t|<\infty\wedge k\notin A_t\}
\end{align*}
and $T=\bigcup_{i\in\omega} T_i$.

By construction,  $A_t=\{*\}$ iff $t$ is terminal in $T$. For each $t\in T$ with $A_t=\{*\}$, let $p_t$ and $j_t$ witness that $A_t=\{*\}$. Then $(a)$ is satisfied.

By definition of $T$, if $A_t\neq\{*\}$, then $(b)$ is satisfied. To see that $(c)$ holds, just notice that $(i)$ holds precisely when $|A_t|=\infty$, and $(ii)$ holds precisely when $|A_t|<\infty$ and $A_t\neq \{*\}$.

It remains only to check that $T$ is wellfounded. Suppose not, and let $x$ be an infinite branch through $T$. Since $f$ is continuous, there must be some $t\subseteq x$ such that any $y\in [p]$ with $t\subseteq y$ has $f(x)_i=f(y)_i$. Then $p/t$ decides $f(x_G)_i$, whence $A_t=\emptyset$, and it follows that $t$ is terminal in $T$, a contradiction.
\end{proof}

\begin{lem}\label{l.refine}
Let $p$, $f$, $i$, $T$, $(j_t)_{t\in\terminal(T)}$ and $(p_t)_{t\in\terminal(T)}$ be so that the hypotheses and conclusions of the previous lemma are satisfied. For each $t\in T$ which is not terminal and satisfies (i) of the previous lemma, let
$$
A_t=\{j_{t'}:t'\in T\wedge t'\supseteq t\},
$$
and let $\mathcal A$ be the family of all the sets $A_t$. Let $\mathcal B$ be any  disjoint refinement of $\mathcal A$, and let $B_t$ be the unique element of $\mathcal B$ such that $B_t\subseteq A_t$. Then
$$
\tilde T=\{s\in T: (\exists t\in\terminal(T))\ s\subset t\wedge j_t\in B_t\}
$$
satisfies Lemma \ref{l.type2} with the same $j_t$ and $p_t$.
\end{lem}
\begin{proof}
The only part of Lemma \ref{l.type2} that could possibly fail by going to the smaller tree $\tilde T\subseteq T$ is (c). Suppose $t\in \tilde T$ is not terminal. Then $t$ is not terminal in $T$, and so $t$ has infinitely many immediate extensions in $T$, and either (i) or (ii) holds for $t$ and $T$. If (i) holds for $t$ and $T$, then it holds for $t$ and $\tilde T$ since $B_t$ is infinite. If (ii) holds for $t$ and $T$, then let $(t_k)_{k\in\omega}$ enumerate the infinitely many immediate extensions of $t$ in $T$. Each of these $t_k$ has an extension $t'_k\supset t_k$ which is terminal in $T$. Then (i) guarantees that all immediate extensions in $T$ of $t'_k\!\upharpoonright\! \lh(t'_k)-1$ are terminal. But then since $\mathcal B$ is a (disjoint) refinement of $\mathcal A$, infinitely many immediate extensions of $t'_k\!\upharpoonright\! \lh(t'_k)-1$ are in $\tilde T$. This shows that $t_k\in \tilde T$ for all $k\in\omega$, and that every $t_k$ has a proper extension in $\tilde T$, so (ii) is satisfied for $\tilde T$.
\end{proof}


\begin{lem}
Let $f:\omega^\omega\to\omega^\omega$ be continuous, $i\in\omega$. Then
$$
\{p\in{\mathbb L}: \{q\leq^* p: q\text{ decides } f(x_G)_i\}\text{ is dense below } p\}
$$
is $\Pi^1_1(f)$.
\end{lem}

\begin{proof}
We first claim that $\{q\leq^* p: q\text{ decides } f(x_G)_i\}$ is dense below $p$ if and only if
$$
(\exists n)(\forall^\infty j)(\forall r\leq^* p/s(p){^\frown\!} j)\ r\not\Vdash f(x_G)_i> n.
$$
For ``if'', note that by pure decision for Laver forcing, it follows that
$$
(\exists n)(\forall^\infty j)(\forall r\leq^* p/s(p){^\frown\!} j)(\exists r'\leq^* r)\ r'\Vdash f(x_G)_i\leq n.
$$
Now if $r\leq^* p$, then for all but finitely many $j$ such that $s(p){^\frown\!} j\in q$ we can find $r_j\leq^* r/s(p){^\frown\!} j$ such that $r_j\Vdash f(x_G)_i\leq n$. Using pure decision again, there is some $k\leq n$ for which there are infinitely many $j$ such that some $r'_j\leq^* r_j$ has $r'_j\Vdash f(x_G)_i=k$. Gluing all these $r'_j$ together yields $q\leq^* r$ with $q\Vdash f(x_G)_i=k$.

For ``only if'', suppose
$$
(\forall n)(\exists^\infty j)(\exists r\leq^* p/s(p){^\frown\!} j)\ r\Vdash f(x_G)_i> n.
$$
Choose an increasing sequence $j_n\in\omega$ and $r_{j_n}\leq^* p/s(p){^\frown\!} j_n$ such that $r_{j_n}\Vdash f(x_G)_i>n$. Let $r=\bigcup_{n\in\omega} r_n$. Then $r\leq^*p$, but no $q\leq^* r$ can decide $f(x_G)_i$.

Finally, note that since $f$ is continuous, saying that $r\not\Vdash f(x_G)_i> n$ simply amounts to saying
$$
(\exists s\in r)(\forall x\in [r/s])\ f(x)_i\leq n.
$$
It follows that the formula above is $\Pi^1_1(f)$.
\end{proof}


\begin{lem}
Let $p\in{\mathbb L}$ and suppose $f:[p]\to[\omega]^\omega$ is continuous. Then there $q\leq p$ and a continuous $\tilde f:[q]\to [\omega]^\omega$ such that $\ran(\tilde f)$ is almost disjoint and $\tilde f(x)\subseteq f(x)$ for all $x\in [q]$.
\end{lem}

\begin{proof}
W.l.o.g., $p=\omega^{<\omega}$. Define $W\subseteq \omega^\omega$ be letting $x\in W$ if and only if
$$
(\forall^\infty n) (\forall i)\ \{q\leq^*p/x\!\upharpoonright\! n: q\text{ decides } f(x_G)_i\} \text{ is } \leq^*\text{-dense below } p/x\!\upharpoonright\! n.
$$
Then $W$ is $\Pi^1_1(f)$, so either there is a Hechler tree $H$ such that $[H]\subseteq W$, or there is a Laver tree $q$ such that $[q]\cap W=\emptyset$.

\medskip

{\sc Case 1}: There is a Hechler tree $H$ such that $[H]\subseteq W$.

\medskip

First note that there must be $s\in H$ such that for all $t\in H$ with $t\supseteq s$ we have that $\{q\leq^* p/t: q\text{ decides } f(x_G)_i\}$ is $\leq^*$ is dense below $p/t$. Indeed, if no such $s\in H$ exists, then we can build sequences $i_j\in\omega$, 
$$
s_0\subsetneq s_1\subsetneq s_2\subsetneq\cdots
$$
in $H$, and $q_j\leq^* p/s_j$ such that no $r\leq^* q_i$ decides $f(x_G)_{i_j}$. But then $\bigcup s_i\notin W$, contrary to that $[H]\subseteq W$.

Fix $s\in H$ as in the previous paragraph. We recursively define two families of subtrees $T_i$ and $T_{i,t}$ of $H_s$, as well as increasing functions $g_{i,t}:\omega\to\omega$, as follows: Let $T_0=T_{0,s}$ and $g_{0,s}$ be the result of applying Lemma \ref{l.type1} with $p=H_s$. If $T_i$ has been defined, then $T_{{i+1},t}$ and $g_{i+1,t}:\omega\to\omega$ are obtained for each $t\in\terminal(T_i)$ by applying Lemma \ref{l.type1} with $p=H_t$; then let $T_{i+1}=\bigcup_{t\in\terminal T_i} T_{i+1,t}$.

Let $q=\bigcup_{i\in\omega} T_i$. It follows from Lemma \ref{l.type1} that $q\leq^* H_s$. Let 
$$
\mathcal B=\{B_{t,i}: i\in\omega\wedge t\in\terminal(T_i)\}
$$ 
be a disjoint refinement of
$$
\mathcal A=\{\ran(g_{t,i}):i\in\omega\wedge t\in\terminal(T_i)\}.
$$
Define for $x\in [q]$
$$
\tilde f(x)=\{n\in\omega: (\exists k)(\exists i)(\exists t)\ x\!\upharpoonright\! k\in T_{i,t}\setminus\terminal(T_{i,t})\wedge n=g_{i,t}(k)\in B_{i,t}\}
$$
It's clear that $\tilde f(x)\subseteq f(x)$, and that $\tilde f$ is continuous (as we only need to know if $x\!\upharpoonright\! k\in T_{i,t}$ to determine if $n\in \tilde f(x)$ or not).

Finally, we show that $\ran(\tilde f)$ is almost disjoint. For this, let $x,x'\in [q]$, and assume $x\neq x'$.

First note that if $x,x'\in [T_{i,t}]$ for some $i,t$ then $\tilde f(x)=\tilde f(x')$. So suppose no such $i,t$ exists. Then either there are infinitely many $k$ such that $x\!\upharpoonright\! k$ is $T_i$-terminal for some $i$, or there are infinitely many $k$ such that $x'\!\upharpoonright\! k$ is $T_i$ terminal for some i. Assume the first is the case. Then, since we assumed that $x\neq x'$, we can find $k$ such that $x\!\upharpoonright\! k\neq x'\!\upharpoonright\! k$ and $x\!\upharpoonright\! k$ is terminal in some $T_i$. Note that since $x\!\upharpoonright\! k\neq x'\!\upharpoonright\! k$, every extension of $x\!\upharpoonright\! k$ is in some $T_{j,s}$ with $s\supseteq x\!\upharpoonright\! k$ and $j>i$, while no extension of $x'\!\upharpoonright\! k$ is in any of these trees. Since $\mathcal B$ is a disjoint refinement of $\mathcal A$ it follows that $\tilde f(x)$ and $\tilde f(x')$ have no elements in common except possible elements of the form $g_{l,x\!\upharpoonright\! m}$ for $l\leq i$ and $m\leq n$, of which there are only finitely many. Thus $\tilde f(x)\cap \tilde f(x')$ is finite.

\medskip

{\sc Case 2:} There is a Laver tree $p$ such that $[p]\cap W=\emptyset$.

Call $t\in p$ a \emph{type 1} node if for all $i\in\omega$, 
$$
\{q\leq^* p: q\text{ decides } f(x_G)_i\}
$$
is $\leq^*$ dense below $p$; otherwise call $t$ a \emph{type 2} node.


\medskip



{\bf Claim:} \emph{If $t\in p$ is a type 1 node, then there is a wellfounded tree $Q_t\subseteq p/t$ with $t\in Q_t$, such that each non-terminal node $s\supseteq t$ in $Q_t$ has infinitely many immediate successors in $Q_t$, and every terminal node $s\in Q_t$ is type 2.}

\medskip

{\it Proof of Claim}. Assume $t\in p$ is type 1. It is enough to show that the tree $T\subseteq p$ produced by Lemma \ref{l.type1} is well-founded. But by (3) of Lemma \ref{l.type1}, any infinite branch through the $T$ produced there belongs to $W$.\hfill\qedsymbol

\medskip

Using the claim, build a family of well-founded trees $T_i\subseteq p$ and $T_{i,t}\subseteq p$, and along with a family of natural numbers $(j_{s,i})_{s\in \terminal(T_{t,i})}$ such that Lemma \ref{l.type2} is satisfied, as follows:

Let $T_{0}=\{s\in p: s\subseteq s(p)\}$. If $T_i$ has been defined, then: For each terminal node in $T_i$ which is type 1, find $Q_t$ as in the claim, and let 
$$
T_i'=T_i\cup\bigcup\{Q_t: t\in\terminal T_i\wedge t\text{ is type 1}\}.
$$
Then $T_i'$ is a well-founded tree such that all terminal nodes are type 2. For each $t\in\terminal T'_i$, apply Lemma \ref{l.type2} to get $T_{t,i}$ and $(j_{s,i}))_{s\in\terminal(T_{t,i})}$. Let
$$
T_{i+1}=\bigcup \{T_{t,i}: t\in\terminal(T_i)\}.
$$
This ends the recursive definition.


For each $s\in T_{t,i}$ such that (i) of Lemma \ref{l.type2} applies, let
$$
A_{s,i}=\{j_{s',i}: s'\supseteq s\wedge s'\in T_{t,i}\}.
$$
Let $\mathcal B$ be a disjoint refinement of all the sets $A_{s,i}$, with $i$ ranging over all of $\omega$ and $s$ ranging over all $s\in T_{t,i}$ which satisfies Lemma \ref{l.type2} for $T_{t,i}$. Let $\tilde T_{t,i}$ be given by Lemma \ref{l.refine}, and define recursively $\tilde T_0=T_0$ and 
$$
\tilde T_{i+1}=\bigcup \{\tilde T_{t,i}: t\in\terminal(\tilde T_i)\}
$$
and let $q=\bigcup T_i$. Define $\tilde f:[q]\to[\omega]^\omega$ by
$$
\tilde f(x)=\{j_{t,i}: i\in\omega\wedge t\subseteq x\}.
$$
Exactly as in case 1, we see that $\tilde f(x)\subseteq f(x)$ for all $x\in [q]$, and that $\ran(\tilde f)$ is an almost disjoint family.
\end{proof}





 

