# 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

• As a given: re-express it in a non-negated form
• As a goal: try proof by contradiction

### Disjunction

• As a given: use proof by cases
• As a given: if you know one of the disjuncts is false, then you can conclude the other one is true
• As a goal: break the proof into cases. In each case, prove any of the disjuncts

### Implication

• As a given (modus ponens): given $$P \implies Q$$, if $$P$$, then you can conclude $$Q$$
• As a given (modus tollens): given $$P \implies Q$$, if $$\lnot Q$$, then you can conclude $$\lnot P$$
• As a goal: given $$P \implies Q$$, assume $$P$$ and prove $$Q$$
• As a goal: given $$P \implies Q$$, assume $$\lnot Q$$ and prove $$\lnot P$$

### Equivalence

• As a given: re-write as a conjunction between two implications
• As a goal: re-write as a conjunction between two implications and prove both directions

### Universal Quantifier

• As a given (universal instantiation): given $$\forall x \in X \circ P(x)$$ and an element $$q \in X$$, you may conclude $$P(q)$$
• As a goal: declare an arbitrary element of the quantified object and prove the predicate

### Existential Quantifier

• As a given (existential instantiation): introduce an arbitrary value for which the predicate is true
• As a goal: find a value that makes the predicate true

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