Background Let I = (B,C,F,P,T) be a finite signature of MSFOL, Fg be the set of E-formulas, and A Fy. Recall that the members of Fy are certain strings of symbols. A subformula of A is a Be Fy such that B is a substring of A. For example, let A be the formula (0 = 2) A (34)), i.e., A is the string "((0 =2) 4 (3 | 4)). Then "(0 = 2)", "(3 | 4)", and "((0= 2) A (3 | 4))" are the subformulas of A, and "(0= and A are two substrings of A that are not subformulas of A. A function f:A + B is total if it is defined on all members of A. A function f : A + B is a partial if it is be undefined on some members of A. For example, the square root function :R + R is a partial function since VT is undefined for all r ER with r