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.