# Logic

Notes in propositional logic, predicate logic, and proof strategies

## Quantification

### Universal Quantifier

The universal quantification expresses that a predicate must hold for every element of type .

The quantifier may include a constraint on the type: , which can be translated to an implication on the predicate: .

Negating a universal quantification is equivalent to an existential quantification with a negated predicate: .

### Existential Quantifier

The existential quantification expresses that a predicate holds for at least one element of type .

The quantifier may include a constraint on the type: , which can be translated to a conjunction on the predicate: .

Negating an existential quantification is equivalent to a universal quantification with a negated predicate: .

### Uniqueness Quantifier

The uniqueness quantifier expresses that a predicate must hold for exactly one element of type . This quantifier might be expressed in terms of the existential and universal quantifiers as follows: , 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: .

## 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 , if , then you can conclude
- As a given (modus tollens): given , if , then you can conclude
- As a goal: given , assume and prove
- As a goal: given , assume and prove

### 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 and an element , you may conclude
- 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

### Proof by Contradiction

Given a goal , assume and derive a logical contradiction.