semantic properties of substitutability

In addition, we also have the following semantic properties on substitutability:

1. If $x,y$ are respectively free for $z$ in $A$, and do not occur free in $A$, then

   $$\vDash \exists xA[x/z]\leftrightarrow \exists yA[y/z]\mathit{\hspace{1em}\hspace{1em}}\text{and}\mathit{\hspace{1em}\hspace{1em}}\vDash \forall xA[x/z]\leftrightarrow \forall yA[y/z]$$

2. (substitution theorem)

   • $\vDash (t_1=t_2)\to (s[t_1/x]=s[t_2/x])$

   • $\vDash (t_1=t_2)\to (A[t_1/x]=A[t_2/x])$

3. Every wff $A$ is equivalent to a wff $A^{\prime }$ in the sense $\vDash A\leftrightarrow A^{\prime }$ such that $A^{\prime }$ contains no variables that are both free and bound.

Title	semantic properties of substitutability
Canonical name	SemanticPropertiesOfSubstitutability
Date of creation	2013-03-22 19:36:00
Last modified on	2013-03-22 19:36:00
Owner	CWoo (3771)
Last modified by	CWoo (3771)
Numerical id	6
Author	CWoo (3771)
Entry type	Result
Classification	msc 03B10
Classification	msc 03B05