Equivalences

Contents/Index

1. Introduction
2. Propositional Extension
3. Syntax
4. Semantics
5. Natural Deduction
@6. Equivalences

There is a list of equivalences between quantifiers. Here we present it. Some are quite intuitive, for example stating "it is not the case that every mammal is a person" is the same as stating "there exists some mammal that is not a person". Some of the equivalences are proven. Maybe only the one way.

We in general have that

1. $\neg \forall x . \phi \dashv \vdash \exists x . \neg \phi$
2. $\neg \exists x . \phi \dashv \vdash \forall x . \neg \phi$

Assuming $x$ is not free in $\psi$ we have that

1. $\forall x . \phi \land \psi \dashv \vdash \forall x . (\phi \land \psi)$
2. $\forall x . \phi \lor \psi \dashv \vdash \forall x . (\phi \lor \psi)$
3. $\exists x . \phi \land \psi \dashv \vdash \exists x . (\phi \land \psi)$
4. $\exists x . \phi \lor \psi \dashv \vdash \exists x . (\phi \lor \psi)$
5. $\forall x . (\phi \rightarrow \psi) \dashv \vdash \phi \rightarrow \forall x . \psi$
6. $\exists x . (\phi \rightarrow \psi) \dashv \vdash \forall x . \phi \rightarrow \psi$
7. $\forall x . (\phi \rightarrow \psi)\dashv \vdash \exists x . \phi \rightarrow \psi$
8. $\exists x . (\phi \rightarrow \psi)\dashv \vdash \phi \rightarrow \exists x . \psi$
9. $\forall x . (\phi \land \psi)\dashv \vdash \forall x . \phi \land \forall x . \psi$
10. $\exists x . (\phi \lor \psi) \dashv \vdash \exists x . \phi \lor \exists x . \psi$
11. $\forall x . \forall y . \phi \dashv \vdash \forall y . \forall x . \phi$
12. $\exists x . \exists y . \phi \dashv \vdash \exists y . \exists x . \phi$

Note that (i) is not the case for disjunction. Say we have $\forall x . (P(x) \lor Q(x))$, where $P(x)$ is true for half the amount of $x$, $Q(x)$ is true for the other half. If we are looking at the domain of people, we could let $P(x)$ be the predicate that $x$ is male, $Q(x)$ the predicate that $x$ is female (in a binary gender world). But now we neither have $\forall x . P(x)$ nor $\forall x . Q(x)$. Note also that (j) is not the case for conjunction.

Proofs for some of the equivalences

We can prove the right direction of (i). We get

~ all ([x] P x) assumption; [l1] ( ~ exi ([x] ~ P x) assumption; [l2] (var [x_0] ( ~ P x_0 assumption; [l3] exi ([x] ~ P x) by exi_i x_0 l3 ; [l4] bot by neg_e l4 l2 ) ; [pbc1] P x_0 by pbc pbc1 ) ; [all1] all ([x] P x) by all_i all1 ; [l6] bot by neg_e l6 l1 ) ; [pbc2] exi ([x] ~ P x) by pbc pbc2 .

We can prove the right direction of (ii). We get

~ exi ([x] P x) assumption; [l1] (var [x_0] ( P x_0 assumption; [l2] exi ([x] P x) by exi_i x_0 l2 ; [l3] bot by neg_e l3 l1 ) ; [neg1] ~ P x_0 by neg_i neg1 ) ; [all1] all ([x] ~ P x) by all_i all1 .

We can prove the left direction of (j). We get

all ([x] P x) /\ all ([x] Q x) assumption; [l1] (var [x_0] all ([x] P x) by con_e1 l1 ; [l2] all ([x] Q x) by con_e2 l1 ; [l3] P x_0 by all_e x_0 l2 ; [l4] Q x_0 by all_e x_0 l3 ; [l5] P x_0 /\ Q x_0 by con_i l4 l5 ) ; [all1] all ([x] P x /\ Q x) by all_i all1 .

We can show the right direction of (j). We get

exi ([x] P x \/ Q x) assumption; [l1] (var [x_0] P x_0 \/ Q x_0 assumption; [l2] ( P x_0 assumption; [l3] exi ([x] P x) by exi_i x_0 l3 ; [l4] exi ([x] P x) \/ exi ([x] Q x) by dis_i1 l4 ) ; [dis1] ( Q x_0 assumption; [l3] exi ([x] Q x) by exi_i x_0 l3 ; [l4] exi ([x] P x) \/ exi ([x] Q x) by dis_i2 l4 ) ; [dis2] exi ([x] P x) \/ exi ([x] Q x) by dis_e l2 dis1 dis2 ) ; [exi1] exi ([x] P x) \/ exi ([x] Q x) by exi_e l1 exi1 .

More proofs might come.