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.