WELL-FORMED FORMULA

Remark: All stuff is defined by recursion.
Remark: We will use #a, #b, #c, ... as meta variables.

Definition L.W.1 - constant
(1) C is a constant.
(2) If #a is a constant then #a' is a constants. 

Examples: C; C'; C''.

Definition L.W.2 - variables
(3) x is a variable.

(4) If #a is a variable then #a' is a variable.

Examples: x; x'; x'';

Definition L.W.3 - operators
(5) F is an operator.

(6) If #f is a operator 
    then #f' is a operator.

Examples: F; F'; F''. 

Definition L.W.5 - terms
(7) If #a is a constant then #a is a term.

(8) If #a is a variable then #a is a term.

(10) If #a is a term then #a is a sequence of terms.

(11) If #s is a sequence of terms and #a is a term 
     then #s,#a is a sequence of terms.  

(12) If #f is an operator 
     and #s is a sequence of terms
     then #f(#s) is a term.

Examples: F; x; F(C); F(C,x); 
F'(F(x),C); F'(F(x),F(C)).

Definition L.W.6 - predicate constructor
(13) P is a predicate constructor.

(14) If #p is a predicate constructor 
     then #p' is a predicate constructor.

Examples: P; P'; P''.

Definition L.W.4 - differing 
(a) If #a is a constant then C differs from #a'.

(b) If #a is a variable then x differs from #a'.

(c) If #a is a operator then F differs from #a'.

(d) If #a is a predicate constructor 
    then P differs from #a'.

(e) If #a differs from #b then #a' differs from #b'.

(f) If #a differs from #b then #b differs from #a. 


Definition L.W.7 - predicates
(15) If #p is a predicate constructor 
     and #s is a sequence of terms
     then #p(#s) is a predicate.

Examples: P(C), P(x,x'), P'(F(x),F''(C,x));

Definition L.W.8 -  formula
(16) If #p is a predicate then #p is a formula.

(17) If #p and #q are formulas 
     then (#p and #q) is a formula.

(18) If #p and #q are formulas 
     then (#p or #q) is a formula.

(19) If #p and #q are formulas 
     then (#p => #q) is a formula.

(20) If #p and #q are formulas
     then (#p <=> #q) is a formula.

(21) If #p is a formula
     then !(#p) is a formula.

(22) If (#p) is a formula then #p is a formula.

(23) If #f is a formula and 
     #a is variable
     then /\(#a) #f is a formula.

(24) If #f is a formula and #a is a variable
     then \/(#a) #f is a formula.
	 
Examples: 
P(x); (P(x) and P'(x'));
((P(x,C) and P(x)) or P'(C'));
(P(x,C) and P(x) or P'(C'));
(P(C')=>P(x,x''));
/\(x) P(x); /\(x) \/(x') P(x,x');
/\(x)\/(x') P'(x,x');

Definition L.W.9 - containing variables
Let #a be a variable.

(25) #a contains #a.

(26) If #s is a sequence of terms
     then #s,#a contains #a.

(27) If #s is a sequence of terms, #s contains #a,
     and #b is a term 
     then #s,#b contains #a.

(28) If #f is an operator
     #s contains #a, 
     and #s is a sequence of terms
     then #f(#s) contains #a.

(29) If #p is a predicate constructor, 
     #s is a sequence of terms,
     and #s contains #a.
     then #p(#s) contains #a.

(30) If #p and #q are formulas and 
     #p contains #a,
     then every formula below contains #a.
     (a) (#p and #q)
     (b) (#q and #p)
     (c) (#p or #q)
     (d) (#q or #p)
     (e) (#p => #q)
     (f) (#q => #p)
     (g) (#p <=> #q)
     (h) (#q <=> #p)
     

(31) If (#p) is a formula and (#p) contains #a
     then #p contains #a.

(32) If #b is a variable, #f is a formula,
     and #f contains #a
     then /\(#b) #f contains #a.

(33) If #b is a variable, #f is a formula,
     and f contains #a
     then \/(#b) #f contains #a.

(34) If #f is a formula then /\(#a) #f contains #a.

(35) If #f is a formula then \/(#a) #f contains #a. 

Definition L.W.10 - free variables
Let #a be variable.

(36) If #p is a predicate and #p contain #a
     then #a is a free variable in #p.

(37) If #p and #q are formulas and 
     #a is a free variable in #p,
     then #a is a free variable in:
     (a) (#p and #q)
     (b) (#q and #p)
     (c) (#p or #q)
     (d) (#q or #p)
     (e) (#p => #q)
     (f) (#q => #p)
     (g) (#p <=> #q)
     (h) (#q <=> #p)
     

(38) If (#p) is a formula and 
     #a is a free variable in (#p) 
     then #a is a free variable in #p. 

(39) If #a is a free variable in #f,
     #b is a variable and #a differs from #b
     then #a is a free variable in /\(#b) #f.

(40) If #a is a free variable in #f,
     #b is a variable and #a differs from #b
     then #a is a free variable in \/(#b) #f.

Definition L.W.11 - well-formed formula
(41) If #p is a predicate then #p is a well-formed formula.

(42) If #p and #q are well-formed formulas 
     then (#p and #q) is a well-formed formula.

(43) If #p and #q are well-formed formulas 
     then (#p or #q) is a well-formed formula.

(44) If #p and #q are well-formed formulas 
     then (#p => #q) is a well-formed formula.

(45) If #p and #q are well-formed formulas
     then (#p <=> #q) is well-formed formula. 

(46) If #p is a well-formed formula
     then !(#p) is a well-formed formula.

(47) If (#p) is a well-formed formula then #p is a well-formed formula.

(48) If #f is a well-formed formula and 
     #a is a free variable in #f
     then /\(#a) #f is a well-formed formula.

(49) If #f is a well-formed formula and 
     #a is a free variable in #f
     then \/(#a) #f is a well-formed formula.      

Definition L.W.9 - not containing variables
Let #a be a variable.
Let #b be a variable that differs from #a.

(50) #b doesn't contain #a.

(51) If #s is a sequence of terms and #s doesn't contain #a
     then #s,#b doesn't contain #a.

(52) If #f is an operator, 
     #s is a sequence of terms,
     and #s doesn't contain #a
     then #f(#s) doesn't contain #a.

(53) If #p is a predicate constructor, 
     #s is a sequence of terms,
     and #s doesn't contain #a
     then #p(#s) doesn't contain #a.

(54) If #p and #q are formulas, 
     #p doesn't contain #a,
     #q doesn't contain #a
     then every formula below doesn't contain #a.
     (a) (#p and #q)
     (b) (#q and #p)
     (c) (#p or #q)
     (d) (#q or #p)
     (e) (#p => #q)
     (f) (#q => #p)
     (g) (#p <=> #q)
     (h) (#q <=> #p)
     

(55) If (#p) is a formula and (#p) doesn't contain #a
     then #p doesn't contain #a.

(56) If #f is a formula,
     and #f doesn't contain #a
     then /\(#b) #f doesn't contains #a.

(57) If #f is a formula,
     and #f doesn't contain #a
     then \/(#b) #f doesn't contain #a.