- English only

# Lab for Automated Reasoning and Analysis LARA

# Substitution Theorems for Propositional Logic

Relate syntax and semantics.

Called metatheorems, because they are not formulas *within* the logic, but formulas *about* the logic.

From semantics we can prove the following lemma by induction.

Lemma: if for every , then .

## Substitutions

Substitution is a maping formulas to formulas,

where is the domain of substitution, usually finite. We write it

Let be set of all substitutions.

Substitution operator *subst* takes such a map and a formula and returns a new formula.

Recursive definition of *subst*:

For we write instead of , so

*Variable substitution* is substitution where the domain is a subset of - it only replaces variables, not complex formulas.

**Theorem:** For formula , interpretation and variable substitution ,

**Corollary (tautology instances):** if , then for every variable substitution .

We say that two formulas are equivalent if .

**Lemma:** If then for every interpretation we have .

From the tautology instances Corrolary we obtain.

**Corollary:** if and is a variable substitution, then .

Does the theorem hold if is not a variable substitution?

This theorem was about transforming formulas from the outside, ignoring the structure of certain subformulas.

We next justify transforming formulas from inside.

We say that is *equivalence-preserving* iff for all where we have .

**Theorem on Substituting Equivalent Subformulas**: if is equivalence-preserving, then for every formula we have .