Volume 12, 2000

University of Bialystok

Copyright (c) 2000 Association of Mizar Users

### The abstract of the Mizar article:

### The Canonical Formulae

**by****Andrzej Trybulec**- Received July 4, 2000
- MML identifier: HILBERT3

- [ Mizar article, MML identifier index ]

environ vocabulary INT_1, MATRIX_2, ARYTM_1, REALSET1, FUNCT_1, KNASTER, RELAT_1, PRALG_1, FUNCT_2, FUNCT_6, BOOLE, FUNCOP_1, HILBERT1, FRAENKEL, FUNCT_3, SUBSET_1, CARD_3, PARTFUN1, FINSEQ_4, FUNCT_5, ZF_LANG, ZF_REFLE, PBOOLE, QC_LANG1, HILBERT2, FUNCT_4, CAT_1, HILBERT3, SGRAPH1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, INT_1, RELAT_1, FUNCT_1, REALSET1, CARD_3, ABIAN, PARTFUN1, FUNCT_2, FUNCT_3, FRAENKEL, CQC_LANG, FUNCT_4, FUNCT_5, FUNCT_6, EXTENS_1, PRALG_1, PRALG_2, PBOOLE, MSUALG_1, PRE_CIRC, MSUALG_3, KNASTER, HILBERT1, HILBERT2; constructors MSUALG_3, CQC_LANG, HILBERT2, KNASTER, PRALG_2, EXTENS_1, PRE_CIRC, DOMAIN_1, CAT_2, INT_1, ABIAN, XCMPLX_0; clusters PRALG_1, RELSET_1, PBOOLE, FUNCT_4, FUNCT_1, HILBERT1, CQC_LANG, FRAENKEL, TEX_2, RELAT_1, SUBSET_1, INT_1, ABIAN, FUNCT_2, MEMBERED, PARTFUN1, NUMBERS, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET; begin :: Preliminaries theorem :: HILBERT3:1 for i being Integer holds i is even iff i-1 is odd; theorem :: HILBERT3:2 for i being Integer holds i is odd iff i-1 is even; theorem :: HILBERT3:3 for X being trivial set, x being set st x in X for f being Function of X,X holds x is_a_fixpoint_of f; definition let A,B,C be set; cluster -> Function-yielding Function of A, Funcs(B,C); end; theorem :: HILBERT3:4 for f being Function-yielding Function holds SubFuncs rng f = rng f; theorem :: HILBERT3:5 for A,B,x being set, f being Function st x in A & f in Funcs(A,B) holds f.x in B; theorem :: HILBERT3:6 for A,B,C being set st C = {} implies B = {} or A = {} for f being Function of A, Funcs(B,C) holds doms f = A --> B; definition cluster {} -> Function-yielding; end; reserve n for Nat, p,q,r,s for Element of HP-WFF; theorem :: HILBERT3:7 for x being set holds ({}).x = {}; definition let A be set, B be functional set; cluster -> Function-yielding Function of A,B; end; theorem :: HILBERT3:8 for X being set, A being Subset of X holds ((0,1) --> (1,0))*chi(A,X) = chi(A`,X); theorem :: HILBERT3:9 for X being set, A being Subset of X holds ((0,1) --> (1,0))*chi(A`,X) = chi(A,X); theorem :: HILBERT3:10 for a,b,x,y,x',y' being set st a <> b & (a,b) --> (x,y) = (a,b) --> (x',y') holds x = x' & y = y'; theorem :: HILBERT3:11 for a,b,x,y,X,Y being set st a<>b & x in X & y in Y holds (a,b) --> (x,y) in product((a,b) --> (X,Y)); theorem :: HILBERT3:12 for D being non empty set for f being Function of 2, D ex d1,d2 being Element of D st f = (0,1) --> (d1,d2); theorem :: HILBERT3:13 for a,b,c,d being set st a <> b holds ((a,b) --> (c,d))*((a,b) --> (b,a)) = (a,b) --> (d,c); theorem :: HILBERT3:14 for a,b,c,d being set, f being Function st a <> b & c in dom f & d in dom f holds f*((a,b) --> (c,d)) = (a,b) --> (f.c,f.d); begin :: the Cartesian product of functions and the Frege function definition let f,g be one-to-one Function; cluster [:f,g:] -> one-to-one; end; theorem :: HILBERT3:15 for A,B being non empty set, C,D being set, f being Function of C,A, g being Function of D,B holds pr1(A,B)*[:f,g:] = f*pr1(C,D); theorem :: HILBERT3:16 for A,B being non empty set, C,D being set, f being Function of C,A, g being Function of D,B holds pr2(A,B)*[:f,g:] = g*pr2(C,D); theorem :: HILBERT3:17 for g being Function holds ({})..g = {}; theorem :: HILBERT3:18 for f being Function-yielding Function, g,h being Function holds (f..g)*h = (f*h)..(g*h); theorem :: HILBERT3:19 for C being set, A being non empty set for f being Function of A, Funcs({} qua set,C), g being Function of A,{} holds rng(f..g) = {{}}; theorem :: HILBERT3:20 for A,B,C being set st B = {} implies A = {} for f being Function of A, Funcs(B,C), g being Function of A,B holds rng(f..g) c= C; theorem :: HILBERT3:21 for A,B,C being set st C = {} implies B = {} or A = {} for f being Function of A, Funcs(B,C) holds dom Frege f = Funcs(A,B); canceled; theorem :: HILBERT3:23 for A,B,C being set st C = {} implies B = {} or A = {} for f being Function of A, Funcs(B,C) holds rng Frege f c= Funcs(A,C); theorem :: HILBERT3:24 for A,B,C being set st C = {} implies B = {} or A = {} for f being Function of A, Funcs(B,C) holds Frege f is Function of Funcs(A,B), Funcs(A,C); begin :: about permutations theorem :: HILBERT3:25 for A,B being set, P being Permutation of A, Q being Permutation of B holds [:P,Q:] is bijective; definition let A,B be non empty set; let P be Permutation of A, Q be Function of B,B; func P => Q -> Function of Funcs(A,B), Funcs(A,B) means :: HILBERT3:def 1 for f being Function of A,B holds it.f = Q*f*P"; end; definition let A,B be non empty set; let P be Permutation of A, Q be Permutation of B; cluster P => Q -> bijective; end; theorem :: HILBERT3:26 for A,B being non empty set for P being Permutation of A, Q being Permutation of B for f being Function of A,B holds (P => Q)".f = Q"*f*P; theorem :: HILBERT3:27 for A,B being non empty set for P being Permutation of A, Q being Permutation of B holds (P => Q)" = P" => (Q"); theorem :: HILBERT3:28 for A,B,C being non empty set, f being Function of A, Funcs(B,C), g being Function of A,B, P being Permutation of B, Q being Permutation of C holds ((P => Q)*f)..(P*g) = Q*(f..g); begin :: set valuations definition mode SetValuation is non-empty ManySortedSet of NAT; end; reserve V for SetValuation; definition let V; func SetVal V -> ManySortedSet of HP-WFF means :: HILBERT3:def 2 it.VERUM = 1 & (for n holds it.prop n = V.n) & for p,q holds it.(p '&' q) = [:it.p, it.q:] & it.(p => q) = Funcs(it.p,it.q); end; definition let V,p; func SetVal(V,p) equals :: HILBERT3:def 3 (SetVal V).p; end; definition let V,p; cluster SetVal(V,p) -> non empty; end; theorem :: HILBERT3:29 SetVal(V,VERUM) = 1; theorem :: HILBERT3:30 SetVal(V,prop n) = V.n; theorem :: HILBERT3:31 SetVal(V,p '&' q) = [:SetVal(V,p), SetVal(V,q):]; theorem :: HILBERT3:32 SetVal(V,p => q) = Funcs(SetVal(V,p),SetVal(V,q)); definition let V,p,q; cluster SetVal(V,p => q) -> functional; end; definition let V,p,q,r; cluster -> Function-yielding Element of SetVal(V,p => (q => r)); end; definition let V,p,q,r; cluster Function-yielding Function of SetVal(V,p => q),SetVal(V,p => r); cluster Function-yielding Element of SetVal(V,p => (q => r)); end; begin :: permuting set valuations definition let V; mode Permutation of V -> Function means :: HILBERT3:def 4 dom it = NAT & for n holds it.n is Permutation of V.n; end; reserve P for Permutation of V; definition let V,P; func Perm P -> ManySortedFunction of SetVal V, SetVal V means :: HILBERT3:def 5 it.VERUM = id 1 & (for n holds it.prop n = P.n) & for p,q ex p' being Permutation of SetVal(V,p), q' being Permutation of SetVal(V,q) st p' = it.p & q' = it.q & it.(p '&' q) = [:p',q':] & it.(p => q) = p' => q'; end; definition let V,P,p; func Perm(P,p) -> Function of SetVal(V,p), SetVal(V,p) equals :: HILBERT3:def 6 (Perm P).p; end; theorem :: HILBERT3:33 Perm(P,VERUM) = id SetVal(V,VERUM); theorem :: HILBERT3:34 Perm(P,prop n) = P.n; theorem :: HILBERT3:35 Perm(P,p '&' q) = [:Perm(P,p),Perm(P,q):]; theorem :: HILBERT3:36 for p' being Permutation of SetVal(V,p), q' being Permutation of SetVal(V,q) st p' = Perm(P,p) & q' = Perm(P,q) holds Perm(P,p => q) = p' => q'; definition let V,P,p; cluster Perm(P,p) -> bijective; end; theorem :: HILBERT3:37 for g being Function of SetVal(V,p), SetVal(V,q) holds Perm(P,p => q).g = Perm(P,q)*g*Perm(P,p)"; theorem :: HILBERT3:38 for g being Function of SetVal(V,p), SetVal(V,q) holds Perm(P,p => q)".g = Perm(P,q)"*g*Perm(P,p); theorem :: HILBERT3:39 for f,g being Function of SetVal(V,p), SetVal(V,q) st f = Perm(P,p => q).g holds Perm(P,q)*g = f*Perm(P,p); theorem :: HILBERT3:40 for V for P being Permutation of V for x being set st x is_a_fixpoint_of Perm(P,p) for f being Function st f is_a_fixpoint_of Perm(P,p => q) holds f.x is_a_fixpoint_of Perm(P,q); begin :: canonical formulae definition let p; attr p is canonical means :: HILBERT3:def 7 for V ex x being set st for P being Permutation of V holds x is_a_fixpoint_of Perm(P,p); end; definition cluster VERUM -> canonical; end; theorem :: HILBERT3:41 p => (q => p) is canonical; theorem :: HILBERT3:42 (p => (q => r)) => ((p => q) => (p => r)) is canonical; theorem :: HILBERT3:43 (p '&' q) => p is canonical; theorem :: HILBERT3:44 (p '&' q) => q is canonical; theorem :: HILBERT3:45 p => (q => (p '&' q)) is canonical; theorem :: HILBERT3:46 p is canonical & p => q is canonical implies q is canonical; theorem :: HILBERT3:47 p in HP_TAUT implies p is canonical; definition cluster canonical Element of HP-WFF; end; begin :: pseudo-canonical formulae definition let p; attr p is pseudo-canonical means :: HILBERT3:def 8 for V for P being Permutation of V ex x being set st x is_a_fixpoint_of Perm(P,p); end; definition cluster canonical -> pseudo-canonical Element of HP-WFF; end; theorem :: HILBERT3:48 p => (q => p) is pseudo-canonical; theorem :: HILBERT3:49 (p => (q => r)) => ((p => q) => (p => r)) is pseudo-canonical; theorem :: HILBERT3:50 (p '&' q) => p is pseudo-canonical; theorem :: HILBERT3:51 (p '&' q) => q is pseudo-canonical; theorem :: HILBERT3:52 p => (q => (p '&' q)) is pseudo-canonical; theorem :: HILBERT3:53 p is pseudo-canonical & p => q is pseudo-canonical implies q is pseudo-canonical; theorem :: HILBERT3:54 for p,q for V for P being Permutation of V st (ex f being set st f is_a_fixpoint_of Perm(P,p)) & not (ex f being set st f is_a_fixpoint_of Perm(P,q)) holds p => q is not pseudo-canonical; theorem :: HILBERT3:55 (prop 0) => (prop 1) => (prop 0) => prop 0 is not pseudo-canonical;

Back to top