2
$\begingroup$

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.

$\endgroup$

1 Answer 1

2
$\begingroup$

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$).

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .