Closed Substitutions.

The map Sub[A,x,i] replace i for x in A. We assume that i is some closed term of the language (hence no renaming of free variables in i is required in order to avoid ``capture''). The only non-trivial clauses concern quantifiers: we do not replace x with i in Ex["x",A], Un["x",A], because x is bound in this case.

Substitution replaces substrings "x" by substrings i in the atomic subformulas of A. Substitution has a bug: if there are variables "x","x0", then Sub["x0=3","x","a"] is "a0=3". Avoid a variable name included, or including, another variable name.

In[103]:=

Sub[Conj[A_, B_], x_, i_]            &n ... ring, x_, i_]          := StringReplace[A, x i] ;

An example of substitution. Remark that when the variable we substitue upon is binded, the substitution does not take place.

In[111]:=

F0 = F5[[2]] ;

In[112]:=

Lin[F0] Lin[Sub[F0, "x", "3"]] Lin[Sub[F0, "y", "3"]]

Out[112]=

¬¬(∃y.P(x,y)∨¬∃y.P(x,y))

Out[113]=

¬¬(∃y.P(3,y)∨¬∃y.P(3,y))

Out[114]=

¬¬(∃y.P(x,y)∨¬∃y.P(x,y))

Created by Mathematica  (October 17, 2006)