• English only

# Lecture 8

### Substitution theorem

Recall the statement in the optional part of Homework 1.

Review of

• semantics of first-order logic
• definition of capture-avoiding substitution and the set of free variables
• structural induction on algebraic data types and comparison to induction on natural numbers
• proof of substitution theorem using structural induction
• the case of a quantifier as a justification for the definition of capture-avoiding substitution

### Quantifier elimination from Homework 2

• transformation to conjunctions of literals
• the idea of Fourier-Motzkin elimination

### Resolution through an example

```(ALL x. EX y. R(x,y))  &
(ALL x y z. R(x,y) --> R(x, plus(y,z)))  &
(Ev(x) | Ev(plus(x,1))) -->
(ALL x. EX y. R(x,y) & E(y))```

The intuitive infinite model. Example finite model where this holds.

Review of transformation to clauses, unification, resolution rule in this example.

The meaning of completeness and soundness of resolution.

### Homework 3 review

Galois connection. Characterization of injective and surjective functions. Two equivalent definitions of Galois connection. 