Substitution Definition(Substitution(Instantiation). If p is a formula and v a variable, we write pv)to denote the fact that v occurs free in p o If t is a term, then o(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 p We call p(t) an instance of p o If p(t)contains no free variables, we call it a ground instance ofφpSubstitution Definition (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 ϕ. Yi Li (Fudan University) Discrete Mathematics May 22, 2012 10 / 1