The finite word calculus for the Halpern–Läuchli argument

Fix a positive integer $d$. For each $1\le i\le d$ introduce four formal quantifier symbols

$\mathrm{\exists }{A}_i,\mathrm{\forall }{x}_i,\mathrm{\forall }{a}_i,\mathrm{\exists }{x}_i\mathrm{.}$

The language $L_d$ consists of the words of length $2d$ that, for every coordinate $i$, contain exactly one of the following ordered pairs:

$\mathrm{\exists }{A}_i\cdots \mathrm{\forall }{x}_i\text{or}\mathrm{\forall }{a}_i\cdots \mathrm{\exists }{x}_i\mathrm{.}$

The displayed order is part of the condition, while symbols belonging to different coordinates may be interleaved. Thus every word chooses one of two coordinate types and uses precisely two symbols for that coordinate.

Write $U,V$ for possibly empty words. A one-step derivation is an instance of one of the following schemes, provided both displayed words belong to $L_d$.

1. Elementary commutation. Two adjacent existential symbols may be interchanged, two adjacent universal symbols may be interchanged, and an existential symbol may be moved to the right past an adjacent universal symbol:

   $U\mathrm{\exists }\alpha \mathrm{\exists }\beta V⟷U\mathrm{\exists }\beta \mathrm{\exists }\alpha V,$ $U\mathrm{\forall }\alpha \mathrm{\forall }\beta V⟷U\mathrm{\forall }\beta \mathrm{\forall }\alpha V,$ $U\mathrm{\exists }\alpha \mathrm{\forall }\beta V⟶U\mathrm{\forall }\beta \mathrm{\exists }\alpha V\mathrm{.}$

2. Matched-pair replacement. For one coordinate $i$,

   $U\mathrm{\forall }{a}_i\mathrm{\exists }{x}_{i}V⟷U\mathrm{\exists }{A}_i\mathrm{\forall }{x}_{i}V\mathrm{.}$

3. Finite block permutation. If $\sigma$ is a permutation of $\{1,\dots ,d\}$ and $1\le r<d$, then

   $U\mathrm{\forall }{a}_{\sigma (1)}\cdots \mathrm{\forall }{a}_{\sigma (r)}\mathrm{\exists }{A}_{\sigma (r+1)}\cdots \mathrm{\exists }{A}_{\sigma (d)}V$ $⟶U\mathrm{\exists }{A}_{\sigma (r+1)}\cdots \mathrm{\exists }{A}_{\sigma (d)}\mathrm{\forall }{a}_{\sigma (1)}\cdots \mathrm{\forall }{a}_{\sigma (r)}V\mathrm{.}$

Here Rule 3 applies only when the two displayed blocks are adjacent. It is not ordinary pointwise quantifier logic; its later semantic use requires finite density-preserving thinning.

For $W,W^{\mathrm{\prime }}\in L_d$, write $W{⊢}_d{W}^{\mathrm{\prime }}$ if there is a finite, possibly empty, sequence of one-step derivations from $W$ to $W^{\mathrm{\prime }}$. This is the reflexive-transitive closure of the three rule classes. The definition is purely syntactic and makes no semantic claim about trees or a set $Q$.