# Substitutions for First-Order Logic

## Motivating Example

It is important to be precise about substitutions in first-order logic. For example, we would like to derive from formula formula , denoted that results from substituting a term instead of . For example, from we would like to derive . Consider, however formula

Consider an interpretation in integers. This formula is true in this domain. Now substitute instead of x the term y+1. We obtain

This formula is false. We say that the variable in term was captured during substitution. When doing substitution in first-order logic we must avoid variable capture. One way to do this is to rename bound variables. Suppose we want to instantiate the formula with . Then we first rename variables in the formula, obtaining

and then after substitution we obtain , which is a correct consequence of .

## Naive and Safe Substitutions

Let be a set of variables (that is, ). A variable substitution is a function where is the set of terms first-order logic.

We define naive substitution recursively, first for terms:

and then for formulas:

Lemma: Let be a variable substitution and a term. Then for every interpretation ,

To avoid variable capture, we introduce in addition to a safe substitution, .

Lemma: Let be a variable substitution and a term. Then for every interpretation ,

Lemma: .