:: A First Order Language :: by Piotr Rudnicki and Andrzej Trybulec :: :: Received August 8, 1989 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, SUBSET_1, ZFMISC_1, TARSKI, XXREAL_0, MARGREL1, MCART_1, ARYTM_3, NAT_1, FINSEQ_1, RELAT_1, ORDINAL4, CARD_1, REALSET1, XBOOLEAN, BVFUNC_2, ZF_LANG, CLASSES2, FUNCT_1, FUNCOP_1, RCOMP_1, QC_LANG1, WELLORD1, RELAT_2, MEMBER_1; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, MCART_1, RELAT_1, FUNCT_1, RELSET_1, NAT_1, FUNCT_2, FUNCOP_1, FINSEQ_1, WELLORD1, WELLORD2, RELAT_2; constructors ENUMSET1, FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, RELSET_1, WELLORD1, WELLORD2, RELAT_2, XTUPLE_0, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, FINSEQ_1, XTUPLE_0, NAT_1; 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 :]; definition mode QC-alphabet -> set means :: QC_LANG1:def 1 it is non empty set & ex X being set st NAT c= X & it = [: NAT, X :]; end; registration cluster -> non empty Relation-like for QC-alphabet; end; reserve A for QC-alphabet; reserve k,n,m for Nat; definition let A be QC-alphabet; func QC-symbols(A) -> non empty set equals :: QC_LANG1:def 2 rng A; end; definition let A be QC-alphabet; mode QC-symbol of A is Element of QC-symbols(A); end; theorem :: QC_LANG1:3 NAT c= QC-symbols(A) & 0 in QC-symbols(A); registration let A be QC-alphabet; cluster QC-symbols(A) -> non empty; end; definition let A be QC-alphabet; func QC-variables(A) -> set equals :: QC_LANG1:def 3 [: {6}, NAT :] \/ [: {4,5}, QC-symbols(A) :]; end; registration let A be QC-alphabet; cluster QC-variables(A) -> non empty; end; theorem :: QC_LANG1:4 QC-variables(A) c= [: NAT, QC-symbols(A) :]; definition let A be QC-alphabet; mode QC-variable of A is Element of QC-variables(A); func bound_QC-variables(A) -> Subset of QC-variables(A) equals :: QC_LANG1:def 4 [: {4}, QC-symbols(A) :]; func fixed_QC-variables(A) -> Subset of QC-variables(A) equals :: QC_LANG1:def 5 [: {5}, QC-symbols(A) :]; func free_QC-variables(A) -> Subset of QC-variables(A) equals :: QC_LANG1:def 6 [: {6}, NAT :]; func QC-pred_symbols(A) -> set equals :: QC_LANG1:def 7 { [n, x] where x is QC-symbol of A : 7 <= n }; end; registration let A be QC-alphabet; cluster bound_QC-variables(A) -> non empty; cluster fixed_QC-variables(A) -> non empty; cluster free_QC-variables(A) -> non empty; cluster QC-pred_symbols(A) -> non empty; end; theorem :: QC_LANG1:5 A = [: NAT, QC-symbols(A) :]; theorem :: QC_LANG1:6 QC-pred_symbols(A) c= [: NAT, QC-symbols(A) :]; definition let A be QC-alphabet; mode QC-pred_symbol of A is Element of QC-pred_symbols(A); end; definition let A be QC-alphabet; let P be Element of QC-pred_symbols(A); func the_arity_of P -> Nat means :: QC_LANG1:def 8 P`1 = 7+it; end; reserve P for QC-pred_symbol of A; definition let A,k; func k-ary_QC-pred_symbols(A) -> Subset of QC-pred_symbols(A) equals :: QC_LANG1:def 9 { P : the_arity_of P = k }; end; registration let k, A; cluster k-ary_QC-pred_symbols(A) -> non empty; end; definition let A be QC-alphabet; mode bound_QC-variable of A is Element of bound_QC-variables(A); mode fixed_QC-variable of A is Element of fixed_QC-variables(A); mode free_QC-variable of A is Element of free_QC-variables(A); let k; mode QC-pred_symbol of k, A is Element of k-ary_QC-pred_symbols(A); end; registration let k be Nat; let A be QC-alphabet; cluster k-element for FinSequence of QC-variables(A); end; definition let k be Nat; let A be QC-alphabet; mode QC-variable_list of k, A is k-element FinSequence of QC-variables(A); end; definition let A be QC-alphabet; let D be set; attr D is A-closed means :: QC_LANG1:def 10 D is Subset of [:NAT, QC-symbols(A):]* & :: Includes atomic formulae (for k being Nat, p being (QC-pred_symbol of k,A), ll being QC-variable_list of k,A holds <*p*>^ll in D) & :: Is closed under VERUM, 'not', '&', and quantification <*[0, 0]*> in D & (for p being FinSequence of [:NAT,QC-symbols(A):] st p in D holds <*[1, 0]*>^p in D) & (for p, q being FinSequence of [:NAT, QC-symbols(A):] st p in D & q in D holds <*[2, 0]*>^p^q in D) & (for x being bound_QC-variable of A, p being FinSequence of [:NAT, QC-symbols(A):] st p in D holds <*[3, 0]*>^<*x*>^p in D); end; definition let A be QC-alphabet; func QC-WFF(A) -> non empty set means :: QC_LANG1:def 11 it is A-closed & for D being non empty set st D is A-closed holds it c= D; end; theorem :: QC_LANG1:7 QC-WFF(A) is A-closed; registration let A be QC-alphabet; cluster A-closed non empty for set; end; definition let A be QC-alphabet; mode QC-formula of A is Element of QC-WFF(A); end; definition let A be QC-alphabet; let P be QC-pred_symbol of A; let l be FinSequence of QC-variables(A); assume the_arity_of P = len l; func P!l -> Element of QC-WFF(A) equals :: QC_LANG1:def 12 <*P*>^l; end; theorem :: QC_LANG1:8 for k being Nat, p being QC-pred_symbol of k, A, ll be QC-variable_list of k, A holds p!ll = <*p*>^ll; definition let A be QC-alphabet; let p be Element of QC-WFF(A); func @p -> FinSequence of [:NAT, QC-symbols(A):] equals :: QC_LANG1:def 13 p; end; definition let A be QC-alphabet; func VERUM(A) -> QC-formula of A equals :: QC_LANG1:def 14 <*[0, 0]*>; let p be Element of QC-WFF(A); func 'not' p -> QC-formula of A equals :: QC_LANG1:def 15 <*[1, 0]*>^@p; let q be Element of QC-WFF(A); func p '&' q -> QC-formula of A equals :: QC_LANG1:def 16 <*[2, 0]*>^@p^@q; end; definition let A be QC-alphabet; let x be bound_QC-variable of A, p be Element of QC-WFF(A); func All(x, p) -> QC-formula of A equals :: QC_LANG1:def 17 <*[3, 0]*>^<*x*>^@p; end; reserve F for Element of QC-WFF(A); scheme :: QC_LANG1:sch 1 QCInd { A() -> QC-alphabet, Prop[Element of QC-WFF(A())] }: for F being Element of QC-WFF(A()) holds Prop[F] provided for k being Nat, P being (QC-pred_symbol of k, A()), ll being QC-variable_list of k, A() holds Prop[P!ll] and Prop[VERUM(A())] and for p being Element of QC-WFF(A()) st Prop[p] holds Prop['not' p] and for p, q being Element of QC-WFF(A()) st Prop[p] & Prop[q] holds Prop[p '&' q] and for x being bound_QC-variable of A(), p being Element of QC-WFF(A()) st Prop[p] holds Prop[All(x, p)]; definition let A be QC-alphabet; let F be Element of QC-WFF(A); attr F is atomic means :: QC_LANG1:def 18 ex k being Nat, p being ( QC-pred_symbol of k, A), ll being QC-variable_list of k, A st F = p!ll; attr F is negative means :: QC_LANG1:def 19 ex p being Element of QC-WFF(A) st F = 'not' p; attr F is conjunctive means :: QC_LANG1:def 20 ex p, q being Element of QC-WFF(A) st F = p '&' q; attr F is universal means :: QC_LANG1:def 21 ex x being bound_QC-variable of A, p being Element of QC-WFF(A) st F = All(x, p); end; theorem :: QC_LANG1:9 for F being Element of QC-WFF(A) holds F = VERUM(A) or F is atomic or F is negative or F is conjunctive or F is universal; theorem :: QC_LANG1:10 for F being Element of QC-WFF(A) holds 1 <= len @F; reserve Q for QC-pred_symbol of A; theorem :: QC_LANG1:11 for k being Nat, P being QC-pred_symbol of k, A holds the_arity_of P = k; reserve F, G for (Element of QC-WFF(A)), s for FinSequence; theorem :: QC_LANG1:12 ((@F.1)`1 = 0 implies F = VERUM(A)) & ((@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, A) implies F is atomic); theorem :: QC_LANG1:13 @F = @G^s implies @F = @G; definition let A be QC-alphabet; let F be Element of QC-WFF(A) such that F is atomic; func the_pred_symbol_of F -> QC-pred_symbol of A means :: QC_LANG1:def 22 ex k being Nat, ll being (QC-variable_list of k, A), P being QC-pred_symbol of k, A st it = P & F = P!ll; end; definition let A be QC-alphabet; let F be Element of QC-WFF(A) such that F is atomic; func the_arguments_of F -> FinSequence of QC-variables(A) means :: QC_LANG1:def 23 ex k being Nat, P being (QC-pred_symbol of k, A), ll being QC-variable_list of k, A st it = ll & F = P!ll; end; definition let A be QC-alphabet; let F be Element of QC-WFF(A) such that F is negative; func the_argument_of F -> QC-formula of A means :: QC_LANG1:def 24 F = 'not' it; end; definition let A be QC-alphabet; let F be Element of QC-WFF(A) such that F is conjunctive; func the_left_argument_of F -> QC-formula of A means :: QC_LANG1:def 25 ex q being Element of QC-WFF(A) st F = it '&' q; end; definition let A be QC-alphabet; let F be Element of QC-WFF(A) such that F is conjunctive; func the_right_argument_of F -> QC-formula of A means :: QC_LANG1:def 26 ex p being Element of QC-WFF(A) st F = p '&' it; end; definition let A be QC-alphabet; let F be Element of QC-WFF(A) such that F is universal; func bound_in F -> bound_QC-variable of A means :: QC_LANG1:def 27 ex p being Element of QC-WFF(A) st F = All(it, p); func the_scope_of F -> QC-formula of A means :: QC_LANG1:def 28 ex x being bound_QC-variable of A st F = All(x, it); end; reserve p for Element of QC-WFF(A); theorem :: QC_LANG1:14 p is negative implies len @the_argument_of p < len @p; theorem :: QC_LANG1:15 p is conjunctive implies len @the_left_argument_of p < len @p & len @the_right_argument_of p < len @p; theorem :: QC_LANG1:16 p is universal implies len @the_scope_of p < len @p; scheme :: QC_LANG1:sch 2 QCInd2 { A() -> QC-alphabet, P[Element of QC-WFF(A())] }: for p being Element of QC-WFF(A()) holds P[p] provided for p being Element of QC-WFF(A()) holds (p is atomic implies P[p]) & P[ VERUM(A())] & (p is negative & P[the_argument_of p] implies P[p]) & (p is conjunctive & P[the_left_argument_of p] & P[the_right_argument_of p] implies P[ p]) & (p is universal & P[the_scope_of p] implies P[p]); reserve F for Element of QC-WFF(A); theorem :: QC_LANG1:17 for k being Nat, P being QC-pred_symbol of k, A holds P `1 <> 0 & P`1 <> 1 & P`1 <> 2 & P`1 <> 3; theorem :: QC_LANG1:18 (@VERUM(A).1)`1 = 0 & (F is atomic implies ex k being Nat st @F.1 is QC-pred_symbol of k, A) & (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:19 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(A); theorem :: QC_LANG1:20 not (VERUM(A) is atomic or VERUM(A) is negative or VERUM(A) is conjunctive or VERUM(A) 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_LANG1:sch 3 QCFuncEx { Al() -> QC-alphabet, D() -> non empty set, V() -> (Element of D()), A(Element of QC-WFF(Al())) -> (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(Al())), Element of D()) -> Element of D()} : ex F being Function of QC-WFF(Al()), D() st F.VERUM(Al()) = V() & for p being Element of QC-WFF(Al()) 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 A be QC-alphabet; let ll be FinSequence of QC-variables(A); func still_not-bound_in ll -> Subset of bound_QC-variables(A) equals :: QC_LANG1:def 29 { ll.k : 1 <= k & k <= len ll & ll.k in bound_QC-variables(A) }; end; reserve k for Nat; definition let A be QC-alphabet; let p be QC-formula of A; func still_not-bound_in p -> Subset of bound_QC-variables(A) means :: QC_LANG1:def 30 ex F being Function of QC-WFF(A), bool bound_QC-variables(A) st it = F.p & for p being Element of QC-WFF(A) holds F.VERUM(A) = {} & (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(A) }) & (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 A be QC-alphabet; let p be QC-formula of A; attr p is closed means :: QC_LANG1:def 31 still_not-bound_in p = {}; end; reserve s,t,u,v for QC-symbol of A; definition let A; mode Relation of A -> Relation means :: QC_LANG1:def 32 it well_orders QC-symbols(A) \ NAT; end; definition let A,s,t; pred s <= t means :: QC_LANG1:def 33 ex n,m st n = s & m = t & n <= m if s in NAT & t in NAT, [s,t] in the Relation of A if not s in NAT & not t in NAT otherwise t in NAT; end; definition let A,s,t; pred s < t means :: QC_LANG1:def 34 s <= t & s <> t; end; theorem :: QC_LANG1:21 s <= t & t <= u implies s <= u; theorem :: QC_LANG1:22 t <= t; theorem :: QC_LANG1:23 t <= u & u <= t implies u = t; theorem :: QC_LANG1:24 t <= u or u <= t; theorem :: QC_LANG1:25 s < t iff not t <= s; theorem :: QC_LANG1:26 s < t or s = t or t < s; definition let A; let Y be non empty Subset of QC-symbols(A); func min Y -> QC-symbol of A means :: QC_LANG1:def 35 it in Y & for t st t in Y holds it <= t; end; definition let A; func 0(A) -> QC-symbol of A means :: QC_LANG1:def 36 for t holds it <= t; end; definition let A,s; func Seg s -> non empty Subset of QC-symbols(A) equals :: QC_LANG1:def 37 { t : s < t }; end; definition let A,s; func s++ -> QC-symbol of A equals :: QC_LANG1:def 38 min (Seg s); end; theorem :: QC_LANG1:27 s < s++; theorem :: QC_LANG1:28 for Y1,Y2 being non empty Subset of QC-symbols(A) st Y1 c= Y2 holds min Y2 <= min Y1; theorem :: QC_LANG1:29 s <= t & t < v implies s < v; theorem :: QC_LANG1:30 s < t & t <= v implies s < v; definition let A; let s be set; func s@A -> QC-symbol of A equals :: QC_LANG1:def 39 s if s is QC-symbol of A otherwise 0; end; definition let A,t,n; func t + n -> QC-symbol of A means :: QC_LANG1:def 40 ex f being sequence of QC-symbols(A) st it = f.n & f.0 = t & for k holds f.(k+1) = (f.k)++; end; theorem :: QC_LANG1:31 t <= t+n; definition let A; let Y be set; func A-one_in Y -> QC-symbol of A equals :: QC_LANG1:def 41 the Element of Y if Y is non empty Subset of QC-symbols(A) otherwise 0(A); end;