Logic


Notes in propositional logic, predicate logic, and proof strategies

Quantification

Universal Quantifier

The universal quantification \(\forall x \in X \circ 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 \vert X \subseteq Y \circ P(x)\), which can be translated to an implication on the predicate: \(\forall x \in X \circ 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 \circ P(x) \iff \exists x \in X \circ \lnot P(x)\).

Existential Quantifier

The existential quantification \(\exists x \in X \circ 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 \vert X \subseteq Y \circ P(x)\), which can be translated to a conjunction on the predicate: \(\exists x \in X \circ 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 \circ P(x) \iff \forall x \in X \circ \lnot P(x)\).

Uniqueness Quantifier

The uniqueness quantifier \(\exists_{1} x \in X \circ 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 \circ P(x) \iff \exists x \in X \circ P(x) \land \forall y \in X \circ P(y) \implies y = x\), therefore the result of negating a uniqueness quantifier looks like this:

Similarly to the existential quantifier, A constraint in a uniqueness quantifier becomes a conjunction in the predicate: \(\exists_{1} x \in X \vert X \subseteq Y \circ P(x) \iff \exists_{1} x \in X \circ 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.