Logic

Notes in propositional logic, predicate logic, and proof strategies

Quantification

Universal Quantifier

The universal quantification \forall x \in X \bullet P(x) expresses that a predicate P must hold for every element of type X .

The quantifier may include a constraint on the type: \forall x \in X \mid X \subseteq Y \bullet P(x) , which can be translated to an implication on the predicate: \forall x \in X \bullet X \subseteq Y \implies P(x) .

Negating a universal quantification is equivalent to an existential quantification with a negated predicate: \lnot \forall x \in X \bullet P(x) \iff \exists x \in X \bullet \lnot P(x) .

Existential Quantifier

The existential quantification \exists x \in X \bullet P(x) expresses that a predicate P holds for at least one element of type X .

The quantifier may include a constraint on the type: \exists x \in X \mid X \subseteq Y \bullet P(x) , which can be translated to a conjunction on the predicate: \exists x \in X \bullet X \subseteq Y \land P(x) .

Negating an existential quantification is equivalent to a universal quantification with a negated predicate: \lnot \exists x \in X \bullet P(x) \iff \forall x \in X \bullet \lnot P(x) .

Uniqueness Quantifier

The uniqueness quantifier \exists_{1} x \in X \bullet P(x) expresses that a predicate P must hold for exactly one element of type X . This quantifier might be expressed in terms of the existential and universal quantifiers as follows: \exists_{1} x \in X \bullet P(x) \iff \exists x \in X \bullet P(x) \land \forall y \in X \bullet P(y) \implies y = x , therefore the result of negating a uniqueness quantifier looks like this:

\begin{align} \lnot \exists_{1} x \in X \bullet P(x) &\iff \lnot \exists x \in X \bullet P(x) \land \forall y \in X \bullet P(y) \implies y = x \\ &\iff \forall x \in X \bullet \lnot (P(x) \land \forall y \in X \bullet P(y) \implies y = x) \\ &\iff \forall x \in X \bullet \lnot P(x) \lor \exists y \in X \bullet \lnot (P(y) \implies y = x) \\ &\iff \forall x \in X \bullet \lnot P(x) \lor \exists y \in X \bullet P(y) \land y \neq x \\ &\iff \forall x \in X \bullet P(x) \implies \exists y \in X \bullet P(y) \land y \neq x \end{align}

Similarly to the existential quantifier, A constraint in a uniqueness quantifier becomes a conjunction in the predicate: \exists_{1} x \in X \mid X \subseteq Y \bullet P(x) \iff \exists_{1} x \in X \bullet X \subseteq Y \land P(x) .

Proof Strategies

Negation

Disjunction

Implication

Equivalence

Universal Quantifier

Existential Quantifier

Proof by Contradiction

Given a goal X , assume \lnot X and derive a logical contradiction.