# 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.
```