semantic properties of substitutability

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

  1. 1.

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

    xA[x/z]yA[y/z]  and  xA[x/z]yA[y/z]
  2. 2.

    (substitution theorem)

    • (t1=t2)(s[t1/x]=s[t2/x])

    • (t1=t2)(A[t1/x]=A[t2/x])

  3. 3.

    Every wff A is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to a wff A in the sense AA such that A 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