:: The canonical formulae
:: by Andrzej Trybulec
::
:: Received July 4, 2000
:: Copyright (c) 2000-2016 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 INT_1, ABIAN, ARYTM_1, ZFMISC_1, FUNCT_1, RELAT_1, TARSKI,
FUNCOP_1, FUNCT_2, FUNCT_6, XBOOLE_0, PBOOLE, SUBSET_1, NUMBERS, NAT_1,
HILBERT1, CARD_1, FUNCT_3, CARD_3, MCART_1, PARTFUN1, FINSEQ_4, XBOOLEAN,
QC_LANG1, HILBERT2, FUNCT_5, ARYTM_3, FUNCT_4, XXREAL_0, HILBERT3,
XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
INT_1, RELAT_1, FUNCT_1, PBOOLE, CARD_1, CARD_3, ABIAN, PARTFUN1,
FUNCT_2, BINOP_1, XXREAL_0, FUNCT_3, FUNCOP_1, FUNCT_4, FUNCT_5, FUNCT_6,
PRALG_1, PRALG_2, MSUALG_3, HILBERT1, HILBERT2;
constructors XXREAL_0, NAT_D, ABIAN, CAT_2, PRALG_1, PRALG_2, MSUALG_3,
HILBERT2, RELSET_1, FUNCT_5, FUNCT_4;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1,
FUNCT_2, FUNCOP_1, FUNCT_4, NUMBERS, XREAL_0, INT_1, PBOOLE, ABIAN,
HILBERT1, RELSET_1, ZFMISC_1, MSSUBFAM, CARD_1;
requirements NUMERALS, BOOLE, SUBSET;
begin :: Preliminaries
registration
let m,n be non zero Nat;
cluster (0,n)-->(m,0) -> one-to-one;
cluster (n,0)-->(0,m) -> one-to-one;
end;
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;
::$CT
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;
reserve n for Element of NAT,
p,q,r,s for Element of HP-WFF;
theorem :: HILBERT3:7
for x being set holds {}.x = {};
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,x9,y9 being set st a <> b &
(a,b) --> (x,y) = (a,b) --> (x9,y9) holds x = x9 & y = y9;
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);
theorem :: HILBERT3:15
(0,1) --> (1,0) is Permutation of 2;
begin :: the Cartesian product of functions and the Frege function
registration
let f,g be one-to-one Function;
cluster [:f,g:] -> one-to-one;
end;
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 pr1(A,B)*[:f,g:] = f*pr1(C,D);
theorem :: HILBERT3:17
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:18
for g being Function holds ({})..g = {};
theorem :: HILBERT3:19
for f being Function-yielding Function, g,h being Function holds
(f..g)*h = (f*h)..(g*h);
theorem :: HILBERT3:20
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:21
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:22
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);
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
registration
let A,B be set, P be Permutation of A, Q be Permutation of B;
cluster [:P,Q:] -> bijective for Function of [:A,B:],[:A,B:];
end;
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;
registration
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) -> set equals
:: HILBERT3:def 3
(SetVal V).p;
end;
registration
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));
registration
let V,p,q;
cluster SetVal(V,p => q) -> functional;
end;
registration
let V,p,q,r;
cluster -> Function-yielding for Element of SetVal(V,p => (q => r));
end;
registration
let V,p,q,r;
cluster Function-yielding for Function of SetVal(V,p => q),SetVal(V,p => r);
cluster Function-yielding for 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 p9 being Permutation of SetVal(V,p),
q9 being Permutation of SetVal(V,q) st p9 = it.p & q9 = it.q &
it.(p '&' q) = [:p9,q9:] & it.(p => q) = p9 => q9;
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 p9 being Permutation of SetVal(V,p), q9 being Permutation of
SetVal(V,q) st p9 = Perm(P,p) & q9 = Perm(P,q) holds Perm(P,p => q) = p9 => q9;
registration
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;
registration
cluster VERUM -> canonical;
end;
registration
let p,q;
cluster p => (q => p) -> canonical;
cluster (p '&' q) => p -> canonical;
cluster (p '&' q) => q -> canonical;
cluster p => (q => (p '&' q)) -> canonical;
end;
registration
let p,q,r;
cluster (p => (q => r)) => ((p => q) => (p => r)) -> canonical;
end;
theorem :: HILBERT3:41
p is canonical & p => q is canonical implies q is canonical;
theorem :: HILBERT3:42
p in HP_TAUT implies p is canonical;
registration
cluster canonical for 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;
registration
cluster canonical -> pseudo-canonical for Element of HP-WFF;
end;
theorem :: HILBERT3:43
p is pseudo-canonical & p => q is pseudo-canonical implies
q is pseudo-canonical;
theorem :: HILBERT3:44
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:45
for a, b being Element of NAT st a <> b holds
(prop a) => (prop b) => (prop a) => (prop a) is non pseudo-canonical;