Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Variables in Formulae of the First Order Language

**by****Czeslaw Bylinski, and****Grzegorz Bancerek**- Received November 23, 1989
- MML identifier: QC_LANG3

- [ Mizar article, MML identifier index ]

environ vocabulary QC_LANG1, FINSEQ_1, FUNCT_1, ZF_LANG, BOOLE, QC_LANG2, PRE_TOPC, ZF_MODEL, QC_LANG3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, NAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, QC_LANG1, QC_LANG2; constructors FUNCT_2, QC_LANG2, XREAL_0, XCMPLX_0, MEMBERED, XBOOLE_0; clusters SUBSET_1, RELSET_1, QC_LANG1, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET; begin reserve i,j,k for Nat; reserve x for bound_QC-variable; reserve a for free_QC-variable; reserve p,q for Element of QC-WFF; reserve l for FinSequence of QC-variables; reserve P,Q for QC-pred_symbol; reserve V for non empty Subset of QC-variables; scheme QC_Func_Uniq { D() -> non empty set, F1() -> (Function of QC-WFF, D()), F2() -> (Function of QC-WFF, D()), V() -> (Element of D()), A(set) -> (Element of D()), N(set) -> (Element of D()), C(set,set) -> (Element of D()), Q(set,set) -> Element of D()} : F1() = F2() provided for p for d1,d2 being Element of D() holds (p = VERUM implies F1().p = V()) & (p is atomic implies F1().p = A(p)) & (p is negative & d1 = F1().the_argument_of p implies F1().p = N(d1)) & (p is conjunctive & d1 = F1().the_left_argument_of p & d2 = F1().the_right_argument_of p implies F1().p = C(d1, d2)) & (p is universal & d1 = F1().the_scope_of p implies F1().p = Q(p, d1)) and for p for d1,d2 being Element of D() holds (p = VERUM implies F2().p = V()) & (p is atomic implies F2().p = A(p)) & (p is negative & d1 = F2().the_argument_of p implies F2().p = N(d1)) & (p is conjunctive & d1 = F2().the_left_argument_of p & d2 = F2().the_right_argument_of p implies F2().p = C(d1, d2)) & (p is universal & d1 = F2().the_scope_of p implies F2().p = Q(p, d1)); scheme QC_Def_D { D() -> non empty set, V() -> (Element of D()), p() -> (Element of QC-WFF), A(Element of QC-WFF) -> (Element of D()), N(Element of D()) -> (Element of D()), C((Element of D()), Element of D()) -> (Element of D()), Q((Element of QC-WFF), Element of D()) -> Element of D()} : (ex d being (Element of D()), F being Function of QC-WFF, D() st d = F.p() & for p being Element of QC-WFF for d1,d2 being Element of D() holds (p = VERUM implies F.p = V()) & (p is atomic implies F.p = A(p)) & (p is negative & d1 = F.the_argument_of p implies F.p = N(d1)) & (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p implies F.p = C(d1, d2)) & (p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) ) & for x1,x2 being Element of D() st (ex F being Function of QC-WFF, D() st x1 = F.p() & for p being Element of QC-WFF for d1,d2 being Element of D() holds (p = VERUM implies F.p = V()) & (p is atomic implies F.p = A(p)) & (p is negative & d1 = F.the_argument_of p implies F.p = N(d1)) & (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p implies F.p = C(d1, d2)) & (p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) ) & (ex F being Function of QC-WFF, D() st x2 = F.p() & for p being Element of QC-WFF for d1,d2 being Element of D() holds (p = VERUM implies F.p = V()) & (p is atomic implies F.p = A(p)) & (p is negative & d1 = F.the_argument_of p implies F.p = N(d1)) & (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p implies F.p = C(d1, d2)) & (p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) ) holds x1 = x2; scheme QC_D_Result'VERUM { D() -> non empty set, F(Element of QC-WFF) -> (Element of D()), V() -> (Element of D()), A(Element of QC-WFF) -> (Element of D()), N(Element of D()) -> (Element of D()), C((Element of D()), Element of D()) -> (Element of D()), Q((Element of QC-WFF), Element of D()) -> Element of D()} : F(VERUM) = V() provided for p being QC-formula, d being Element of D() holds d = F(p) iff ex F being Function of QC-WFF, D() st d = F.p & for p being Element of QC-WFF for d1,d2 being Element of D() holds (p = VERUM implies F.p = V()) & (p is atomic implies F.p = A(p)) & (p is negative & d1 = F.the_argument_of p implies F.p = N(d1)) & (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p implies F.p = C(d1, d2)) & (p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)); scheme QC_D_Result'atomic { D() -> non empty set, V() -> (Element of D()), F(Element of QC-WFF) -> (Element of D()), p() -> QC-formula, A(Element of QC-WFF) -> (Element of D()), N(Element of D()) -> (Element of D()), C((Element of D()), Element of D()) -> (Element of D()), Q((Element of QC-WFF), Element of D()) -> Element of D()} : F(p()) = A(p()) provided for p being QC-formula, d being Element of D() holds d = F(p) iff ex F being Function of QC-WFF, D() st d = F.p & for p being Element of QC-WFF for d1,d2 being Element of D() holds (p = VERUM implies F.p = V()) & (p is atomic implies F.p = A(p)) & (p is negative & d1 = F.the_argument_of p implies F.p = N(d1)) & (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p implies F.p = C(d1, d2)) & (p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) and p() is atomic; scheme QC_D_Result'negative { D() -> non empty set, V() -> (Element of D()), p() -> QC-formula, A(Element of QC-WFF) -> (Element of D()), N(Element of D()) -> (Element of D()), C((Element of D()), Element of D()) -> (Element of D()), Q((Element of QC-WFF), Element of D()) -> (Element of D()), F(Element of QC-WFF) -> (Element of D()) } : F(p()) = N(F(the_argument_of p())) provided for p being QC-formula, d being Element of D() holds d = F(p) iff ex F being Function of QC-WFF, D() st d = F.p & for p being Element of QC-WFF for d1,d2 being Element of D() holds (p = VERUM implies F.p = V()) & (p is atomic implies F.p = A(p)) & (p is negative & d1 = F.the_argument_of p implies F.p = N(d1)) & (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p implies F.p = C(d1, d2)) & (p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) and p() is negative; scheme QC_D_Result'conjunctive { D() -> non empty set, V() -> (Element of D()), A(Element of QC-WFF) -> (Element of D()), N(Element of D()) -> (Element of D()), C((Element of D()), Element of D()) -> (Element of D()), Q((Element of QC-WFF), Element of D()) -> (Element of D()), F(Element of QC-WFF) -> (Element of D()), p() -> QC-formula } : for d1,d2 being Element of D() st d1 = F(the_left_argument_of p()) & d2 = F(the_right_argument_of p()) holds F(p()) = C(d1,d2) provided for p being QC-formula, d being Element of D() holds d = F(p) iff ex F being Function of QC-WFF, D() st d = F.p & for p being Element of QC-WFF for d1,d2 being Element of D() holds (p = VERUM implies F.p = V()) & (p is atomic implies F.p = A(p)) & (p is negative & d1 = F.the_argument_of p implies F.p = N(d1)) & (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p implies F.p = C(d1, d2)) & (p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) and p() is conjunctive; scheme QC_D_Result'universal { D() -> non empty set, V() -> (Element of D()), p() -> QC-formula, A(Element of QC-WFF) -> (Element of D()), N(Element of D()) -> (Element of D()), C((Element of D()), Element of D()) -> (Element of D()), Q((Element of QC-WFF), Element of D()) -> (Element of D()), F(Element of QC-WFF) -> (Element of D()) } : F(p()) = Q(p(),F(the_scope_of p())) provided for p being QC-formula, d being Element of D() holds d = F(p) iff ex F being Function of QC-WFF, D() st d = F.p & for p being Element of QC-WFF for d1,d2 being Element of D() holds (p = VERUM implies F.p = V()) & (p is atomic implies F.p = A(p)) & (p is negative & d1 = F.the_argument_of p implies F.p = N(d1)) & (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p implies F.p = C(d1, d2)) & (p is universal & d1 = F.the_scope_of p implies F.p = Q(p, d1)) and p() is universal; canceled 2; theorem :: QC_LANG3:3 P is QC-pred_symbol of the_arity_of P; definition let l; let V; canceled; func variables_in(l,V) -> Element of bool V equals :: QC_LANG3:def 2 { l.k : 1 <= k & k <= len l & l.k in V }; end; canceled 2; theorem :: QC_LANG3:6 still_not-bound_in l = variables_in(l,bound_QC-variables); theorem :: QC_LANG3:7 still_not-bound_in VERUM = {}; theorem :: QC_LANG3:8 for p being QC-formula st p is atomic holds still_not-bound_in p = still_not-bound_in the_arguments_of p; theorem :: QC_LANG3:9 for P being QC-pred_symbol of k for l being QC-variable_list of k holds still_not-bound_in (P!l) = still_not-bound_in l; theorem :: QC_LANG3:10 for p being QC-formula st p is negative holds still_not-bound_in p = still_not-bound_in the_argument_of p; theorem :: QC_LANG3:11 for p being QC-formula holds still_not-bound_in 'not' p = still_not-bound_in p; theorem :: QC_LANG3:12 still_not-bound_in FALSUM = {}; theorem :: QC_LANG3:13 for p being QC-formula st p is conjunctive holds still_not-bound_in p = (still_not-bound_in the_left_argument_of p) \/ (still_not-bound_in the_right_argument_of p); theorem :: QC_LANG3:14 for p,q being QC-formula holds still_not-bound_in(p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q); theorem :: QC_LANG3:15 for p being QC-formula st p is universal holds still_not-bound_in p = (still_not-bound_in the_scope_of p) \ {bound_in p}; theorem :: QC_LANG3:16 for p being QC-formula holds still_not-bound_in All(x,p) = (still_not-bound_in p) \ {x}; theorem :: QC_LANG3:17 for p being QC-formula st p is disjunctive holds still_not-bound_in p = (still_not-bound_in the_left_disjunct_of p) \/ (still_not-bound_in the_right_disjunct_of p); theorem :: QC_LANG3:18 for p,q being QC-formula holds still_not-bound_in p 'or' q = (still_not-bound_in p) \/ (still_not-bound_in q); theorem :: QC_LANG3:19 for p being QC-formula st p is conditional holds still_not-bound_in p = (still_not-bound_in the_antecedent_of p) \/ (still_not-bound_in the_consequent_of p); theorem :: QC_LANG3:20 for p,q being QC-formula holds still_not-bound_in p => q = (still_not-bound_in p) \/ (still_not-bound_in q); theorem :: QC_LANG3:21 for p being QC-formula st p is biconditional holds still_not-bound_in p = (still_not-bound_in the_left_side_of p) \/ (still_not-bound_in the_right_side_of p); theorem :: QC_LANG3:22 for p,q being QC-formula holds still_not-bound_in p <=> q = (still_not-bound_in p) \/ (still_not-bound_in q); theorem :: QC_LANG3:23 for p being QC-formula holds still_not-bound_in Ex(x,p) = (still_not-bound_in p) \ {x}; theorem :: QC_LANG3:24 VERUM is closed & FALSUM is closed; theorem :: QC_LANG3:25 for p being QC-formula holds p is closed iff 'not' p is closed; theorem :: QC_LANG3:26 for p,q being QC-formula holds p is closed & q is closed iff p '&' q is closed; theorem :: QC_LANG3:27 for p being QC-formula holds All(x,p) is closed iff still_not-bound_in p c= {x}; theorem :: QC_LANG3:28 for p being QC-formula st p is closed holds All(x,p) is closed; theorem :: QC_LANG3:29 for p,q being QC-formula holds p is closed & q is closed iff p 'or' q is closed; theorem :: QC_LANG3:30 for p,q being QC-formula holds p is closed & q is closed iff p => q is closed; theorem :: QC_LANG3:31 for p,q being QC-formula holds p is closed & q is closed iff p <=> q is closed; theorem :: QC_LANG3:32 for p being QC-formula holds Ex(x,p) is closed iff still_not-bound_in p c= {x}; theorem :: QC_LANG3:33 for p being QC-formula st p is closed holds Ex(x,p) is closed; definition let k; func x.k -> bound_QC-variable equals :: QC_LANG3:def 3 [4,k]; end; canceled; theorem :: QC_LANG3:35 x.i = x.j implies i = j; theorem :: QC_LANG3:36 ex i st x.i = x; definition let k; func a.k -> free_QC-variable equals :: QC_LANG3:def 4 [6,k]; end; canceled; theorem :: QC_LANG3:38 a.i = a.j implies i = j; theorem :: QC_LANG3:39 ex i st a.i = a; theorem :: QC_LANG3:40 for c being Element of fixed_QC-variables for a being Element of free_QC-variables holds c <> a; theorem :: QC_LANG3:41 for c being Element of fixed_QC-variables for x being Element of bound_QC-variables holds c <> x; theorem :: QC_LANG3:42 for a being Element of free_QC-variables for x being Element of bound_QC-variables holds a <> x; definition let V; let V1,V2 be Element of bool V; redefine func V1 \/ V2 -> Element of bool V; end; definition let V; let p; func Vars(p,V) -> Element of bool V means :: QC_LANG3:def 5 ex F being Function of QC-WFF, bool V st it = F.p & for p being Element of QC-WFF for d1,d2 being Element of bool V holds (p = VERUM implies F.p = {}(V)) & (p is atomic implies F.p = variables_in(the_arguments_of p,V)) & (p is negative & d1 = F.the_argument_of p implies F.p = d1) & (p is conjunctive & d1 = F.the_left_argument_of p & d2 = F.the_right_argument_of p implies F.p = d1 \/ d2) & (p is universal & d1 = F.the_scope_of p implies F.p = d1); end; canceled 3; theorem :: QC_LANG3:46 Vars(VERUM,V) = {}; theorem :: QC_LANG3:47 p is atomic implies Vars(p,V) = variables_in(the_arguments_of p, V) & Vars(p,V) = { (the_arguments_of p).k : 1 <= k & k <= len (the_arguments_of p) & (the_arguments_of p).k in V }; theorem :: QC_LANG3:48 for P being QC-pred_symbol of k for l being QC-variable_list of k holds Vars(P!l,V) = variables_in(l, V) & Vars((P!l),V) = { l.i : 1 <= i & i <= len l & l.i in V }; theorem :: QC_LANG3:49 p is negative implies Vars(p,V) = Vars(the_argument_of p,V); theorem :: QC_LANG3:50 Vars('not' p,V) = Vars(p,V); theorem :: QC_LANG3:51 Vars(FALSUM,V) = {}; theorem :: QC_LANG3:52 p is conjunctive implies Vars(p,V) = Vars(the_left_argument_of p,V) \/ Vars(the_right_argument_of p,V); theorem :: QC_LANG3:53 Vars(p '&' q,V) = Vars(p,V) \/ Vars(q,V); theorem :: QC_LANG3:54 p is universal implies Vars(p,V) = Vars(the_scope_of p,V); theorem :: QC_LANG3:55 Vars(All(x,p),V) = Vars(p,V); theorem :: QC_LANG3:56 p is disjunctive implies Vars(p,V) = Vars(the_left_disjunct_of p,V) \/ Vars(the_right_disjunct_of p,V); theorem :: QC_LANG3:57 Vars(p 'or' q, V) = Vars(p,V) \/ Vars(q,V); theorem :: QC_LANG3:58 p is conditional implies Vars(p,V) = Vars(the_antecedent_of p,V) \/ Vars(the_consequent_of p,V); theorem :: QC_LANG3:59 Vars(p => q,V) = Vars(p,V) \/ Vars(q,V); theorem :: QC_LANG3:60 p is biconditional implies Vars(p,V) = Vars(the_left_side_of p,V) \/ Vars(the_right_side_of p,V); theorem :: QC_LANG3:61 Vars(p <=> q,V) = Vars(p,V) \/ Vars(q,V); theorem :: QC_LANG3:62 p is existential implies Vars(p,V) = Vars(the_argument_of the_scope_of the_argument_of p, V); theorem :: QC_LANG3:63 Vars(Ex(x,p), V) = Vars(p,V); definition let p; func Free p -> Element of bool free_QC-variables equals :: QC_LANG3:def 6 Vars(p,free_QC-variables); end; canceled; theorem :: QC_LANG3:65 Free VERUM = {}; theorem :: QC_LANG3:66 for P being QC-pred_symbol of k for l being QC-variable_list of k holds Free(P!l) = { l.i : 1 <= i & i <= len l & l.i in free_QC-variables }; theorem :: QC_LANG3:67 Free 'not' p = Free p; theorem :: QC_LANG3:68 Free FALSUM = {}; theorem :: QC_LANG3:69 Free(p '&' q) = Free p \/ Free q; theorem :: QC_LANG3:70 Free(All(x,p)) = Free(p); theorem :: QC_LANG3:71 Free(p 'or' q) = Free p \/ Free q; theorem :: QC_LANG3:72 Free(p => q) = Free p \/ Free q; theorem :: QC_LANG3:73 Free(p <=> q) = Free p \/ Free q; theorem :: QC_LANG3:74 Free Ex(x,p) = Free p; definition let p; func Fixed p -> Element of bool fixed_QC-variables equals :: QC_LANG3:def 7 Vars(p,fixed_QC-variables); end; canceled; theorem :: QC_LANG3:76 Fixed VERUM = {}; theorem :: QC_LANG3:77 for P being QC-pred_symbol of k for l being QC-variable_list of k holds Fixed(P!l) = { l.i : 1 <= i & i <= len l & l.i in fixed_QC-variables }; theorem :: QC_LANG3:78 Fixed 'not' p = Fixed p; theorem :: QC_LANG3:79 Fixed FALSUM = {}; theorem :: QC_LANG3:80 Fixed(p '&' q) = Fixed p \/ Fixed q; theorem :: QC_LANG3:81 Fixed(All(x,p)) = Fixed(p); theorem :: QC_LANG3:82 Fixed(p 'or' q) = Fixed p \/ Fixed q; theorem :: QC_LANG3:83 Fixed(p => q) = Fixed p \/ Fixed q; theorem :: QC_LANG3:84 Fixed(p <=> q) = Fixed p \/ Fixed q; theorem :: QC_LANG3:85 Fixed Ex(x,p) = Fixed p;

Back to top