Is there a way to define universal quantification in such a way, that I can prove$\forall xPx\land Q\iff \forall x(Px\land Q)$ and similar statements?

Question

What I've tried so far:

Under the assumption that the domain of discourse has a finite number of elements, I defined universal quantification with the help of a recursive function:

$\forall x\in A:P(x) \iff \text{forall}(A, P, n_A)$

$n_A$ refers to the cardinality of set $A$. Since we assumed the set to be finite, $n(a)$ is always a natural number.

The function $\text{forall}$ is defined as follows

$\text{forall}(A, P, n) \iff P(A_n) \land \text{forall}(A, P, n-1)$ if $n\geq1$

$\text{forall}(A, P, n) \iff True$ if $n=0$

Now, let us "fix" a predefined, random order on the elements of set A, so that $A_1$ always comes first, $A_2$ comes second, and so on. The universal quantifier should give us the same result, regardless of which order we choose. As such, $A_n$ refers to the $n$-th element of set $A$. In this sense, set $A$ is looking more like a n-tuple than a set, but I'm afraid I can't explain myself any better than that with my limited knowledge on set theory.

Now that we have defined universal quantification formally, let's try to prove some simple statements regarding it, e.g:

$\forall A,P,Q(\forall x\in A:Px\land \forall x\in A:Qx\iff \forall x\in A(Px\land Qx))$

Let's substitute the universal quantifications with our own recursive definition:

$\forall A,P,Q(\text{forall}(A, P, n_A) \land \text{forall}(A, Q, n_A) \iff \text{forall}(A, P\cap Q, n_A))$

I'm not certain about how to express the following formally, but if the above statement is true for every set $A$, that's it's also true for every (finite) length of the set, so:

$\forall A,P,Q\forall n_A\in N_0(\text{forall}(A, P, n_A) \land \text{forall}(A, Q, n_A) \iff \text{forall}(A, P\cap Q, n_A))$

From here I use induction on n_A.

$\text{forall}(A, P, n_A+1) \land \text{forall}(A, Q, n_A+1)$

$\iff \text{forall}(A, P, n_A) \land PA_{n_A+1} \land \text{forall}(A, Q, n_A) \land QA_{n_A+1}$

$\text{forall}(A, P\cap Q, n_A) \land PA_{n_A+1} \land QA_{n_A+1}$ by the induction hypothesis

$\text{forall}(A, P\cap Q, n_A+1)$

So far so good... but does such a proof/definition/method also hold true when talking about infinite sets? I heard something about transfinite induction, where you can "apply induction" (for lack of better wording) in any well-ordered set. Since the order of the elements shouldn't matter in universal quantification, maybe we can just "fix" a random order and use this type of induction then? Maybe this is exactly the type of induction that I used to solve the proof for finite sets? If so, maybe someone could help me formalize the concept of "fixing" a random order and/or further clarify why the order does not matter (in retrospective, this might be because conjuction is both commutative and associative)?

Thank you in advance!

Answer 1

You can prove this equivalence this way over a finite domain, but there are other ways to this type of equivalence that work for infinite domains and are easier. I actually don't know whether the method you outline above can be generalized to transfinite induction if you are building your model on top of an arbitrary ordinal instead of restricting attention to natural numbers. I suspect it wouldn't work in general since there are axioms of infinity like $(\lnot \exists x \mathop. s(x) = 0) \land (\forall x \forall y \mathop. s(x) = s(y) \to x = y)$, but there may be classes of formulas for which transfinite induction works.

---

In the example above, $Q$ is a nullary predicate.

This means it is either always true or always false.

Suppose $Q$ is always true.

$(\forall x \mathop. P(x))$ is equivalent to $(\forall x \mathop. P(x)) \land \top$.

$(\forall x \mathop. P(x))$ is also equivalent to $(\forall x \mathop. P(x) \land \top)$.

Suppose $Q$ is always false.

$(\forall x \mathop. P(x) \land \bot)$ is equivalent to $(\forall x \mathop. \bot)$.

$(\forall x \mathop. P(x)) \land \bot)$ is equivalent to $\bot$.

Assuming that you do not allow the domain of discourse to be empty, then $\bot$ is equivalent to $(\forall x \mathop. \bot)$.

If you allow the domain of discourse to be empty, then this shows that your theorem does not hold.

In addition to this kind of semi-formal argument, there are also formal proof calculi for first-order logic.

Two straightforward ones are:

• The method of analytic tableaux without unification for first-order logic link.
• System LK.
• Fitch-style systems

There are others, like Hilbert systems, but these can produce very long proofs.