Substitution( Continued A substitution e is finite iff{∈∑(x)≠x}is finite a substitution o is a substitution for variables iff the only primitive symbols such that 0(a)* are variables Let I1,...,In be distinct primitive symbols and let Y1, ... Yn be formulas. Sy, ym is a substitution e such that Y if x C if c E{x1,…,m Logic in Computer Science -p 8/39Substitution(Continued) • A substitution θ is finite iff { x ∈ Σ|θ ( x ) 6= x } is finite. • A substitution θ is a substitution fo r variables iff the only primitive symbols x such that θ ( x ) 6= x are variables. • Let x 1, · · · , x n b e distinct primitive symbols and let Y1, · · · , Yn b e formulas. S x 1,···,x n Y1,···,Yn is a substitution θ such that θ ( x ) =    Yi if x = x i, 1 ≤ i ≤ n x if x 6∈ { x 1, · · · , x n } Logic in Computer Science – p.8/39