Discussions of and reference for when the axiom of "moving a quantifier past a formula" holds as an equivalence

Question

One of the usual axioms of first-order predicate calculus is, roughly:

if $P_0$ and $P_1$ are formulas, and if in $P_0$ the variable does not occur freely, then the following is valid:

$ \bigl(\forall x:T\quad (P_0\rightarrow P_1)\bigr)\rightarrow (P_0\rightarrow \forall x:T\quad P_1)$

Sometimes, this is an equivalence, i.e., in some situations, also

$ \bigl(\forall x:T\quad (P_0\rightarrow P_1)\bigr)\leftarrow (P_0\rightarrow \forall x:T\quad P_1)$

is valid.

Question: can you recommend references where this is discussed, preferably in general (precise general conditions of when the converse implication holds, examples perhaps, and perhaps a discussion why it is so usual to only give the first-cited implication)?

Remarks.

• I am more interested in high-level discussions of this issue, or perhaps stories of the kind "Yeah, this is called such and such, and I needed this too for this and that.", less in elementary explanations of first-order logic.

• The type-theoretic notation $x:T$ was not used for a particular reason; rather, I am currently working with this notation, and would therefore prefer to read somewhat "type-theoretically-informed" discussions

• Motivation for this question is that I had to convince myself that a certain assignation of morphisms to morphisms in a category is really a functor. I was suspecting that something was wrong with it, and found myself constructing a formal proof that composition is preserved. In it, I need the equivalence

$ \bigl(\forall x:T\quad (P_0\rightarrow P_1)\bigr)\leftrightarrow (P_0\rightarrow \forall x:T\quad P_1)$

which happens to hold at that point. When it comes to presenting this to readers or an audience, the issue arises of what to appeal to. The off-the-shelf axioms known to me only state the implication.

Answer 1

This is indeed a logical equivalence, i.e. the equivalence always holds, not just sometimes.

Here is a not quite formal discussion as to whym (sorry, I have no reference ... I just do this by pure logic)

You can see any universal as a kind of conjunction. That is, you can think of $\forall x: T \quad P(x)$ as saying: 'object $a$ has property $P$, and object $b$ has property $P$, and ...'. In other words (and here is where things are not quite formal!):

$$\forall x: T \ P(x) \approx P(a) \land P(b) \land ....$$

As such, we can explain the logical equivalence $\forall x (P_0 \lor P(x)) \Leftrightarrow (P_0 \lor \forall x P(x))$ where $P_0$ does not contain $x$ as a free variable:

$$\forall x (P_0 \lor P(x)) \approx$$

$$(P_0 \lor P(a) \land (P_0 \lor P(b) \land ... \Leftrightarrow \text{ (Reverse Distribution)}$$

$$P_0 \lor (P(a) \land P(b) \land ...) \approx $$

$$P_0 \lor \forall x P(x)$$

(using formal semantics, you can prove this equivalence mathematically, but you said you wanted it not too technical/detailed)

Anyway, with that equivalence in place, we can prove your equivalence as well:

$$\forall x (P_0 \to P(x)) \Leftrightarrow \text{ (Implication)}$$

$$\forall x (\neg P_0 \lor P(x)) \Leftrightarrow \text{ (given what we just showed)}$$

$$\neg P_0 \lor \forall x \ P(x) \Leftrightarrow \text{ (Implication)}$$

$$P_0 \to \forall x \ P(x)$$

Answer 2

I am not familiar with your notation. In more standard predicate notation, I'm guessing you meant $$\forall x:[T(x) \implies [P_0 \implies P_1(x)]]\space \equiv \space [P_0\implies \forall x:[T(x) \implies P_1(x)]]$$

We can derive this axiom (actually a theorem) as follows using other simpler and easier-to-use axioms.

1. $\forall x:[T(x) \implies [P_0 \implies P_1(x)]]\space$ (Premise)

2. $P_0\space$ (Premise)

3. $T(a)\space$ (Premise)

4. $T(a) \implies [P_0 \implies P_1(a)]\space$ (Universal Specification, 1)

5. $P_0 \implies P_1(a)\space$ (Detachment, 4, 3)

6. $P_1(a)\space$ (Detachment, 5, 2)

7. $\forall x :[T(x) \implies P_1(x)]\space$ (Conclusion, 3)

8. $P_0 \implies \forall x: [T(x) \implies P_1(x)]\space$ (Conclusion, 2)

9. $\forall x:[T(x) \implies [P_0 \implies P_1(x)]]\implies [P_0\implies \forall x:[T(x) \implies P_1(x)]]\space$ (Conclusion, 1)

Similarly, prove the converse.