Equivalence

In Chapter 5, we saw DeMorgan’s laws for quantifiers – that if we have some domain, and if P(x) is a predicate for individuals in that domain, then the following statements are equivalent:

• ¬(∃ x P(x)) is equivalent to ∀ x ¬P(x)
• ¬(∀ x P(x)) is equivalent to ∃ x ¬P(x)

The process of proving that two predicate logic statements are equivalent is the same as it was in propositional logic – we must prove the second proposition using the first as a premise, and we must prove the first given the second as a premise.

Example - how to prove equivalence

For example, to prove that ¬(∃ x P(x)) is equivalent to ∀ x ¬P(x), we must prove the sequents:

    (
        ¬(∃((x: T) => P(x)))
    )
⊢
    (
        ∀((x: T) => ¬P(x))
    )

and

    (
        ∀((x: T) => ¬P(x))
    )
⊢
    (
        ¬(∃((x: T) => P(x)))
    )

We prove both directions below:

    (
        ¬(∃((x: T) => P(x)))
    )
⊢
    (
        ∀((x: T) => ¬P(x))
    )
Proof(
    1 (     ¬(∃((x: T) => P(x)))        ) by Premise,

    2 Let ( (a: T) => SubProof(

        3 SubProof(
            4 Assume (  P(a)  ),
            5 (     ∃((x: T) => P(x))   ) by ExistsI[T](3),
            6 (     F                   ) by NegE(4, 1)
        ),
        7 (     ¬P(a)                   ) by NegI(3)

    )),
    8 (  ∀((x: T) => ¬P(x))             ) by AllI[T](2)
)

And:

    (
        ∀((x: T) => ¬P(x))
    )
⊢
    (
        ¬(∃((x: T) => P(x)))
    )
Proof(
    1 (     ∀((x: T) => ¬P(x))          )   by Premise,

    2 SubProof(
        3 Assume (  ∃((x: T) => P(x))   ),

        4 Let ( (a: T) => SubProof(
            5 Assume (  P(a)  ),
            6 (     ¬P(a)               )   by AllE[T](1),
            7 (     F                   )   by NegE(5, 6),
        )),
        8 (     F                       )   By ExistsE[T](3, 4)
    
    ),
    9 (     ¬(∃((x: T) => P(x)))        )   by NegI(2)
)

More extensive list of equivalences

Here is a more extensive list of equivalences in predicate logic. The remaining proofs are left as exercises for the reader:

• ¬(∃ x P(x)) is equivalent to ∀ x ¬P(x)
• ¬(∀ x P(x)) is equivalent to ∃ x ¬P(x)
• ∀ x (P(x) → ¬Q(x)) is equivalent to ¬(∃ x P(x) ∧ Q(x))
• ∀ x ∀ y P(x, y) is equivalent to ∀ y ∀ x P(x, y)
• ∃ x ∃ y P(x, y) is equivalent to ∃ y ∃ x P(x, y)
• Q ∧ (∀ x P(x)) is equivalent to ∀ x (Q ∧ P(x)) (where x does not appear in Q)
• Q v (∀ x P(x)) is equivalent to ∀ x (Q V P(x)) (where x does not appear in Q)
• Q ∧ (∃ x P(x)) is equivalent to ∃ x (Q ∧ P(x)) (where x does not appear in Q)
• Q V (∃ x P(x)) is equivalent to ∃ x (Q V P(x)) (where x does not appear in Q)