Predicate Substitution

Predicate substitution is a logical substitution that applies in predicate logic, and is more complicated than its propositional counterpart. It involves replacing variables with terms. Renaming is a form of predicate substitution operating on bound variables.

#tosee is there any use for predicate substitution / renaming that is non-proper??

Definition §

Predicate Substitution ^definition

A predicate substitution, $\theta$, is a logical substitution in predicate logic that maps free variables to terms (which can also be variables)

$$\theta :\{x_1,x_2,\dots \}\text{ where xi is free}\to \{t_1,t_2,\dots \}$$

• $\{x_1,x_2,\dots \}$ represents the set of all free variables (not bound by a quantifier)
• $\{t_1,t_2,\dots \}$ represents the set of all terms, that is, any constant $\{a,b,c,\dots \}$, variable $\{x,y,z,\dots \}$ or function of terms

Conventionally, we tend to use the notation $\theta =\{x_1\mapsto t_1,x_2\mapsto t_2,\dots \}$ for predicate substitution

Substitution and Quantifiers

Unlike propositional logic, predicate substitution does not preserve logical equivalence! See the section on scoping for more information

Renaming §

Renaming ^definition-renaming

Renaming is a logical substitution that explicitly maps bound variables to variables:

$$\rho :\{x_1,x_2,\dots \}\text{ where xi is bound}\to \{x,y,z,\dots \}$$

If $\phi$ is a formula, then $\phi [\rho ]$ is its renamed instance

Proper Renaming §

Proper Renaming ^definition-renaming-proper

A proper renaming of a formula $\phi$ is a renaming of (bound variable) $x$ that has any renamed variable $x^{\prime }$ outside the quantifier scope of $x$. Equivalently:

• $x^{\prime }$ is not free for $x$ in $\phi$

Substitutions & Quantifiers §

Unlike in propositional logic, we have quantifiers that range a variable over a domain. Substitution then has some extra restrictions to ensure it preserves logical equivalence (the meaning of the formula):

• A proper renaming preserves semantic properties (and hence logical equivalence)
• An invalid renaming#todo
• A predicate substitution on free variables does not preserve semantic consequences, but it does preserve satisfiability!

#tosee does invalid renaming stay equisatisfiable?

For example, take the formula $P(x,y):\forall x(F(x)\wedge G(y))$. We can identify that (in the quantifier scope), $x$ is a bound variable and $y$ is a free variable:

• $P(x,y)[x:=z]=\forall z(F(z)\wedge G(y))$ is a substitution of a bound variable to an out-of-scope variable, $z$. Hence, it is a proper renaming and semantic properties are preserved i.e. the meaning of the formula is unchanged.
• $P(x,y)[x:=y]=\forall y(F(y)\wedge G(y))$ is a substitution of a bound variable to an in-scope variable. It is a renaming, but not a proper one. This formula has a very different meaning to the original $P(x,y)$. Hence, semantic properties are not preserved.
• $P(x,y)[y:=z]=\forall x(F(x)\wedge G(z))$ is a substitution of a free variable. Semantic consequences are not preserved.

Theorems §

T1: Proper renaming preserves semantic properties ^t1

That is, a formula $\phi$ is logically equivalent to it’s renamed instance $\phi [\rho ]$ iff $\rho$ is a proper renaming

$$\phi [\rho ]\equiv \phi$$

T2: Predicate substitution does not preserve semantic properties, but does preserve satisfiability, ^t2

That is, a formula $\phi$ with a predicate substitution $\theta$ is equisatisfiable (but not logically equivalent) to its renamed instance:

$$\phi [\theta ]\not\equiv \phi \text{ but }\phi [\theta ]\approx \phi$$

Examples §

For example:

$$E=P(f(x),g(y,y,b))$$

Recall the convention around terms ($f$ is a function, $y$ is a variable, $b$ is a constant). Then, let $\theta =\{x\mapsto h(u),y\mapsto a,z\mapsto c\}$. Under $\theta$ we have:

$$E[\theta ]=P(f(h(u),g(a,a,b))$$