Our cookies follow Google AdSense policy.

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