Statements in prenex normal form in classical first order logic where the variables in the matrix (quantifier-free part) each appear exactly once seem to have an interesting property where $\land$ and $\lor$ "distribute" over the prefix. What's this property called?
Consider a statement in classical first-order logic in prenex normal form. $x$ and $y$ are variables and $f$ is a 1-place predicate. The universe of discourse that we're quantifying over is implicit.
$$ \forall x. \exists y. f(x) \land f(y) $$
Consider breaking it up into a quantifier sequence (here labelled $M$ and an expression labelled $P$)
$$ M . P $$
This expression is a closed term (might not be the right terminology?) that actually has a truth value. In this case $M$ is $\forall x\forall y$ and $P$ is $f(x) \land f(y)$.
So, $M$ is a little bit of a weird entity, since I'm "rebracketing" the expression compared to how it's normally thought of (i.e. $\forall x. ( \forall y . f(x) \land f(y) )$ ). I still think this construction works.
So, let's restrict our attention to cases where the matrix (quantifier-free part) does not contain any duplicated variables.
I think the following property holds if every variable in $P \land Q$ appears exactly once:
$$ M . (P \land Q) \Longleftrightarrow (M . P) \land (M . Q) $$
and similarly for disjunction
$$ M . (P \lor Q) \Longleftrightarrow (M . P) \lor (M . Q) $$
For the sake of concreteness, here's an expression that doesn't respect the property, but is ruled out because the variable $x$ is duplicated in the matrix.
$$ \forall x . f(x) \land \lnot f(x) $$
Is there a name for this property? I think it falls right out of the fact that if each variable appears once, then one of the branches will be "constant" from the perspective of that variable.
You are more or less correct, but it would be easier to see if you did use "normal" syntax.
Even constructively we have the following equivalences: $$\forall x.P(x)\land Q(x) \iff (\forall x.P(x))\land(\forall x.Q(x))$$ $$\exists x.P(x)\lor Q(x)\iff (\exists x.P(x))\lor(\exists x.Q(x))$$ $$\exists x.P(x)\land Q\iff (\exists x.P(x))\land Q$$
If we further assume a classical logic with rules that enforce a non-empty domain, we have the following equivalences: $$\forall x.P(x)\lor Q \iff(\forall x.P(x))\lor Q$$ as well as $Q\iff \forall x.Q \iff \exists x.Q$. We can thus say $$\forall x.P(x)\lor Q\iff (\forall x.P(x))\lor(\forall x.Q)\qquad \exists x.P(x)\land Q\iff (\exists x.P(x))\land(\exists x.Q)$$
Your claim then follows by induction on the number of quantifiers (and the commutativity of $\land$ and $\lor$).