Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### A First Order Language

**by****Piotr Rudnicki, and****Andrzej Trybulec**- Received August 8, 1989
- MML identifier: QC_LANG1

- [ Mizar article, MML identifier index ]

environ vocabulary MCART_1, FINSEQ_1, RELAT_1, BOOLE, ZF_LANG, FUNCT_1, PRE_TOPC, QC_LANG1, FUNCOP_1; notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, MCART_1, NAT_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, FUNCOP_1, FINSEQ_1; constructors MCART_1, NAT_1, FUNCT_2, ENUMSET1, FINSEQ_1, XREAL_0, MEMBERED, XBOOLE_0, FUNCOP_1; clusters RELSET_1, FINSEQ_1, SUBSET_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin :: Preliminaries theorem :: QC_LANG1:1 for D1 being non empty set, D2 being set, k being Element of D1 holds [: {k}, D2 :] c= [: D1, D2 :]; theorem :: QC_LANG1:2 for D1 being non empty set, D2 being set, k1, k2, k3 being Element of D1 holds [: {k1, k2, k3}, D2 :] c= [: D1, D2 :]; reserve k, l, m, n for Nat; definition func QC-variables -> set equals :: QC_LANG1:def 1 [: { 4, 5, 6 }, NAT :]; end; definition cluster QC-variables -> non empty; end; canceled; theorem :: QC_LANG1:4 QC-variables c= [: NAT, NAT :]; definition mode QC-variable is Element of QC-variables; func bound_QC-variables -> Subset of QC-variables equals :: QC_LANG1:def 2 [: {4}, NAT :]; func fixed_QC-variables -> Subset of QC-variables equals :: QC_LANG1:def 3 [: {5}, NAT :]; func free_QC-variables -> Subset of QC-variables equals :: QC_LANG1:def 4 [: {6}, NAT :]; func QC-pred_symbols -> set equals :: QC_LANG1:def 5 { [k, l]: 7 <= k }; end; definition cluster bound_QC-variables -> non empty; cluster fixed_QC-variables -> non empty; cluster free_QC-variables -> non empty; cluster QC-pred_symbols -> non empty; end; canceled 5; theorem :: QC_LANG1:10 QC-pred_symbols c= [: NAT, NAT :]; definition mode QC-pred_symbol is Element of QC-pred_symbols; end; definition let P be Element of QC-pred_symbols; func the_arity_of P -> Nat means :: QC_LANG1:def 6 P`1 = 7+it; end; reserve P for QC-pred_symbol; definition let k; func k-ary_QC-pred_symbols -> Subset of QC-pred_symbols equals :: QC_LANG1:def 7 { P : the_arity_of P = k }; end; definition let k; cluster k-ary_QC-pred_symbols -> non empty; end; definition mode bound_QC-variable is Element of bound_QC-variables; mode fixed_QC-variable is Element of fixed_QC-variables; mode free_QC-variable is Element of free_QC-variables; let k; mode QC-pred_symbol of k is Element of k-ary_QC-pred_symbols; end; definition let k be Nat; mode QC-variable_list of k -> FinSequence of QC-variables means :: QC_LANG1:def 8 len it = k; end; definition let D be set; attr D is QC-closed means :: QC_LANG1:def 9 D is Subset of [:NAT, NAT:]* & :: Includes atomic formulae (for k being Nat, p being (QC-pred_symbol of k), ll being QC-variable_list of k holds <*p*>^ll in D) & :: Is closed under VERUM, 'not', '&', and quantification <*[0, 0]*> in D & (for p being FinSequence of [:NAT,NAT:] st p in D holds <*[1, 0]*>^p in D) & (for p, q being FinSequence of [:NAT, NAT:] st p in D & q in D holds <*[2, 0]*>^p^q in D) & (for x being bound_QC-variable, p being FinSequence of [:NAT, NAT:] st p in D holds <*[3, 0]*>^<*x*>^p in D); end; definition func QC-WFF -> non empty set means :: QC_LANG1:def 10 it is QC-closed & :: Is the smallest that is_QC-closed for D being non empty set st D is QC-closed holds it c= D; end; canceled 10; theorem :: QC_LANG1:21 QC-WFF is QC-closed; definition mode QC-formula is Element of QC-WFF; end; definition let P be QC-pred_symbol,l be FinSequence of QC-variables; assume the_arity_of P = len l; func P!l -> Element of QC-WFF equals :: QC_LANG1:def 11 <*P*>^l; end; canceled; theorem :: QC_LANG1:23 for k being Nat, p being QC-pred_symbol of k, ll be QC-variable_list of k holds p!ll = <*p*>^ll; definition let p be Element of QC-WFF; func @p -> FinSequence of [:NAT, NAT:] equals :: QC_LANG1:def 12 p; end; definition func VERUM -> QC-formula equals :: QC_LANG1:def 13 <*[0, 0]*>; let p be Element of QC-WFF; func 'not' p -> QC-formula equals :: QC_LANG1:def 14 <*[1, 0]*>^@p; let q be Element of QC-WFF; func p '&' q -> QC-formula equals :: QC_LANG1:def 15 <*[2, 0]*>^@p^@q; end; definition let x be bound_QC-variable, p be Element of QC-WFF; func All(x, p) -> QC-formula equals :: QC_LANG1:def 16 <*[3, 0]*>^<*x*>^@p; end; reserve F for Element of QC-WFF; scheme QC_Ind { Prop[Element of QC-WFF] }: for F being Element of QC-WFF holds Prop[F] provided for k being Nat, P being (QC-pred_symbol of k), ll being QC-variable_list of k holds Prop[P!ll] and Prop[VERUM] and for p being Element of QC-WFF st Prop[p] holds Prop['not' p] and for p, q being Element of QC-WFF st Prop[p] & Prop[q] holds Prop[p '&' q] and for x being bound_QC-variable, p being Element of QC-WFF st Prop[p] holds Prop[All(x, p)]; definition let F be Element of QC-WFF; attr F is atomic means :: QC_LANG1:def 17 ex k being Nat, p being (QC-pred_symbol of k), ll being QC-variable_list of k st F = p!ll; attr F is negative means :: QC_LANG1:def 18 ex p being Element of QC-WFF st F = 'not' p; attr F is conjunctive means :: QC_LANG1:def 19 ex p, q being Element of QC-WFF st F = p '&' q; attr F is universal means :: QC_LANG1:def 20 ex x being bound_QC-variable, p being Element of QC-WFF st F = All(x, p); end; canceled 9; theorem :: QC_LANG1:33 for F being Element of QC-WFF holds F = VERUM or F is atomic or F is negative or F is conjunctive or F is universal; theorem :: QC_LANG1:34 for F being Element of QC-WFF holds 1 <= len @F; reserve Q for QC-pred_symbol; theorem :: QC_LANG1:35 for k being Nat, P being QC-pred_symbol of k holds the_arity_of P = k; reserve F, G for (Element of QC-WFF), k,n for Nat, s for FinSequence; theorem :: QC_LANG1:36 ((@F.1)`1 = 0 implies F = VERUM) & ((@F.1)`1 = 1 implies F is negative) & ((@F.1)`1 = 2 implies F is conjunctive) & ((@F.1)`1 = 3 implies F is universal) & ((ex k being Nat st @F.1 is QC-pred_symbol of k) implies F is atomic); theorem :: QC_LANG1:37 @F = @G^s implies @F = @G; definition let F be Element of QC-WFF such that F is atomic; func the_pred_symbol_of F -> QC-pred_symbol means :: QC_LANG1:def 21 ex k being Nat, ll being (QC-variable_list of k), P being QC-pred_symbol of k st it = P & F = P!ll; end; definition let F be Element of QC-WFF such that F is atomic; func the_arguments_of F -> FinSequence of QC-variables means :: QC_LANG1:def 22 ex k being Nat, P being (QC-pred_symbol of k), ll being QC-variable_list of k st it = ll & F = P!ll; end; definition let F be Element of QC-WFF such that F is negative; func the_argument_of F -> QC-formula means :: QC_LANG1:def 23 F = 'not' it; end; definition let F be Element of QC-WFF such that F is conjunctive; func the_left_argument_of F -> QC-formula means :: QC_LANG1:def 24 ex q being Element of QC-WFF st F = it '&' q; end; definition let F be Element of QC-WFF such that F is conjunctive; func the_right_argument_of F -> QC-formula means :: QC_LANG1:def 25 ex p being Element of QC-WFF st F = p '&' it; end; definition let F be Element of QC-WFF such that F is universal; func bound_in F -> bound_QC-variable means :: QC_LANG1:def 26 ex p being Element of QC-WFF st F = All(it, p); func the_scope_of F -> QC-formula means :: QC_LANG1:def 27 ex x being bound_QC-variable st F = All(x, it); end; reserve p for Element of QC-WFF; canceled 7; theorem :: QC_LANG1:45 p is negative implies len @the_argument_of p < len @p; theorem :: QC_LANG1:46 p is conjunctive implies len @the_left_argument_of p < len @p & len @the_right_argument_of p < len @p; theorem :: QC_LANG1:47 p is universal implies len @the_scope_of p < len @p; scheme QC_Ind2 { Prop[Element of QC-WFF] }: for p being Element of QC-WFF holds Prop[p] provided for p being Element of QC-WFF holds (p is atomic implies Prop[p]) & Prop[VERUM] & (p is negative & Prop[the_argument_of p] implies Prop[p]) & (p is conjunctive & Prop[the_left_argument_of p] & Prop[the_right_argument_of p] implies Prop[p]) & (p is universal & Prop[the_scope_of p] implies Prop[p]); reserve F for Element of QC-WFF; theorem :: QC_LANG1:48 for k being Nat, P being QC-pred_symbol of k holds P`1 <> 0 & P`1 <> 1 & P`1 <> 2 & P`1 <> 3; theorem :: QC_LANG1:49 (@VERUM.1)`1 = 0 & (F is atomic implies ex k being Nat st @F.1 is QC-pred_symbol of k) & (F is negative implies (@F.1)`1 = 1) & (F is conjunctive implies (@F.1)`1 = 2) & (F is universal implies (@F.1)`1 = 3); theorem :: QC_LANG1:50 F is atomic implies (@F.1)`1 <> 0 & (@F.1)`1 <> 1 & (@F.1)`1 <> 2 & (@F.1)`1 <> 3; reserve p for Element of QC-WFF; theorem :: QC_LANG1:51 not (VERUM is atomic or VERUM is negative or VERUM is conjunctive or VERUM is universal) & not (ex p st p is atomic & p is negative or p is atomic & p is conjunctive or p is atomic & p is universal or p is negative & p is conjunctive or p is negative & p is universal or p is conjunctive & p is universal); scheme QC_Func_Ex { 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()} : ex F being Function of QC-WFF, D() st F.VERUM = V() & for p being Element of QC-WFF holds (p is atomic implies F.p = A(p)) & (p is negative implies F.p = N(F.the_argument_of p)) & (p is conjunctive implies F.p = C(F.the_left_argument_of p, F.the_right_argument_of p)) & (p is universal implies F.p = Q(p, F.the_scope_of p)); reserve j,k for Nat; definition let ll be FinSequence of QC-variables; func still_not-bound_in ll -> Element of (bool bound_QC-variables) equals :: QC_LANG1:def 28 { ll.k : 1 <= k & k <= len ll & ll.k in bound_QC-variables }; end; definition let b be bound_QC-variable; redefine func { b } -> Element of bool bound_QC-variables; end; definition let X, Y be Element of bool bound_QC-variables; redefine func X \/ Y -> Element of bool bound_QC-variables; func X \ Y -> Element of bool bound_QC-variables; end; reserve k for Nat; definition let p be QC-formula; func still_not-bound_in p -> Element of bool bound_QC-variables means :: QC_LANG1:def 29 ex F being Function of QC-WFF, bool bound_QC-variables st it = F.p & for p being Element of QC-WFF holds F.VERUM = {} & (p is atomic implies F.p = { (the_arguments_of p).k : 1 <= k & k <= len the_arguments_of p & (the_arguments_of p).k in bound_QC-variables }) & (p is negative implies F.p = F.the_argument_of p) & (p is conjunctive implies F.p = (F.the_left_argument_of p) \/ (F.the_right_argument_of p)) & (p is universal implies F.p = (F.the_scope_of p) \ {bound_in p}); end; definition let p be QC-formula; attr p is closed means :: QC_LANG1:def 30 still_not-bound_in p = {}; end;

Back to top