In some case, we may substitute a variable with another term Definition 6(Substitution(Instantiation)). If p is a formula and v a variable, we write p(u)to denote the fact that v occurs free in p 1. Ift is a term, then o(t), or if we wish to be more explicit, p(u/t), is the result of substituting C or instantiating) t for all free occurrences of v in e. We call o(t) an instance of p 2. If p(t) contains no free variables, we call it a ground instance of y Consider the following example Example 6. Given a formula((vr(e, y))v(yS(a, y) 1. t is (a/s, y/t)=((Va)R(a, t))v((y)S(s, y)) 3. (a/c,y/d)=((v)R(r, c)V(y)S(s, d)) Generally, we have the following rules Example 7. The recursive definition of p(a/t) with substitution to. The recursive definition of to 1. t is a constant, t[r/tol ta/tol 3.t=g(t1,t2,…,tk), t[a/to]= g(t1[/to], t2[c/to],., tk[/to]) 4. p(a, y) is an atomic formula, p/to= p(to, y) 5.9==v/,p{/tol=-{/tol 6. p=9102, p/to]=p1a/to op2(c/to 7. p(a, y)=Q2v(, 3, 2), pr/tol Q2(v{/to),x≠ Consider the following substitution Example 8. Given a formula p (a)=y(a+y=0) and s(a)=r+l. Consider the substitution (/s(y)). We just assume that both variables are integersIn some case, we may substitute a variable with another term. Definition 6 (Substitution(Instantiation)). If ϕ is a formula and v a variable, we write ϕ(v) to denote the fact that v occurs free in ϕ. 1. If t is a term, then ϕ(t), or if we wish to be more explicit, ϕ(v/t), is the result of substituting ( or instantiating) t for all free occurrences of v in ϕ. We call ϕ(t) an instance of ϕ. 2. If ϕ(t) contains no free variables, we call it a ground instance of ϕ. Consider the following example. Example 6. Given a formula ((∀x)R(x, y)) ∨ ((∃y)S(x, y)), 1. It is denoted as ϕ(x, y). 2. ϕ(x/s, y/t) = ((∀x)R(x, t)) ∨ ((∃y)S(s, y)). 3. ϕ(x/c, y/d) = ((∀x)R(x, c)) ∨ ((∃y)S(s, d)). Generally, we have the following rules. Example 7. The recursive definition of ϕ(x/t) with substitution t0. The recursive definition of t0 to x in t. 1. t is a constant, t[x/t0] = t 2. t is a variable, t[x/t0] = ( t0 if t = x t o.w. (t 6= x) 3. t = g(t1, t2, . . . , tk), t[x/t0] = g(t1[x/t0], t2[x/t0], . . . , tk[x/t0]) 4. ϕ(x, y) is an atomic formula, ϕ[x/t0] = ϕ(t0, y) 5. ϕ = ¬ψ, ϕ[x/t0] = ¬ψ[x/t0] 6. ϕ = ϕ1ϕ2, ϕ[x/t0] = ϕ1[x/t0]ϕ2[x/t0] 7. ϕ(x, y) = Qzψ(x, y, z), ϕ[x/t0] = ( ϕ, x = z Qz(ψ[x/t0]), x 6= z Consider the following substitution. Example 8. Given a formula ϕ(x) = (∃y)(x + y = 0) and s(x) = x + 1. Consider the substitution ϕ(x/s(y)). We just assume that both variables are integers. 3