:: HILBERT3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: HILBERT3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer holds
( i is even iff not i - 1 is even )
proof end;

theorem Th2: :: HILBERT3:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Integer holds
( not i is even iff i - 1 is even )
proof end;

theorem Th3: :: HILBERT3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being trivial set
for x being set st x in X holds
for f being Function of X,X holds x is_a_fixpoint_of f
proof end;

registration
let A, B, C be set ;
cluster -> Function-yielding M5(A, Funcs B,C);
coherence
for b1 being Function of A, Funcs B,C holds b1 is Function-yielding
proof end;
end;

theorem Th4: :: HILBERT3:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function-yielding Function holds SubFuncs (rng f) = rng f
proof end;

theorem Th5: :: HILBERT3:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, x being set
for f being Function st x in A & f in Funcs A,B holds
f . x in B
proof end;

theorem Th6: :: HILBERT3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being set st ( not C = {} or B = {} or A = {} ) holds
for f being Function of A, Funcs B,C holds doms f = A --> B
proof end;

registration
cluster {} -> Function-yielding ;
coherence
{} is Function-yielding
proof end;
end;

theorem Th7: :: HILBERT3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set holds {} . x = {}
proof end;

registration
let A be set ;
let B be functional set ;
cluster -> Function-yielding M5(A,B);
coherence
for b1 being Function of A,B holds b1 is Function-yielding
proof end;
end;

theorem Th8: :: HILBERT3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Subset of X holds (0,1 --> 1,0) * (chi A,X) = chi (A ` ),X
proof end;

theorem Th9: :: HILBERT3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for A being Subset of X holds (0,1 --> 1,0) * (chi (A ` ),X) = chi A,X
proof end;

theorem Th10: :: HILBERT3:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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' )
proof end;

theorem Th11: :: HILBERT3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th12: :: HILBERT3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th13: :: HILBERT3:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being set st a <> b holds
(a,b --> c,d) * (a,b --> b,a) = a,b --> d,c
proof end;

theorem Th14: :: HILBERT3:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b, c, d being set
for 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)
proof end;

registration
let f, g be one-to-one Function;
cluster [:f,g:] -> one-to-one ;
coherence
[:f,g:] is one-to-one
proof end;
end;

theorem Th15: :: HILBERT3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty set
for C, D being set
for f being Function of C,A
for g being Function of D,B holds (pr1 A,B) * [:f,g:] = f * (pr1 C,D)
proof end;

theorem Th16: :: HILBERT3:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty set
for C, D being set
for f being Function of C,A
for g being Function of D,B holds (pr2 A,B) * [:f,g:] = g * (pr2 C,D)
proof end;

theorem :: HILBERT3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for g being Function holds {} .. g = {}
proof end;

theorem Th18: :: HILBERT3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function-yielding Function
for g, h being Function holds (f .. g) * h = (f * h) .. (g * h)
proof end;

theorem :: HILBERT3:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being set
for A being non empty set
for f being Function of A, Funcs {} ,C
for g being Function of A, {} holds rng (f .. g) = {{} }
proof end;

theorem Th20: :: HILBERT3:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being set st ( B = {} implies A = {} ) holds
for f being Function of A, Funcs B,C
for g being Function of A,B holds rng (f .. g) c= C
proof end;

theorem Th21: :: HILBERT3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being set st ( not C = {} or B = {} or A = {} ) holds
for f being Function of A, Funcs B,C holds dom (Frege f) = Funcs A,B
proof end;

theorem :: HILBERT3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th23: :: HILBERT3:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being set st ( not C = {} or B = {} or A = {} ) holds
for f being Function of A, Funcs B,C holds rng (Frege f) c= Funcs A,C
proof end;

theorem Th24: :: HILBERT3:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being set st ( not C = {} or B = {} or A = {} ) holds
for f being Function of A, Funcs B,C holds Frege f is Function of Funcs A,B, Funcs A,C
proof end;

theorem Th25: :: HILBERT3:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being set
for P being Permutation of A
for Q being Permutation of B holds [:P,Q:] is bijective
proof end;

definition
let A, B be non empty set ;
let P be Permutation of A;
let Q be Function of B,B;
func P => Q -> Function of Funcs A,B, Funcs A,B means :Def1: :: HILBERT3:def 1
for f being Function of A,B holds it . f = (Q * f) * (P " );
existence
ex b1 being Function of Funcs A,B, Funcs A,B st
for f being Function of A,B holds b1 . f = (Q * f) * (P " )
proof end;
uniqueness
for b1, b2 being Function of Funcs A,B, Funcs A,B st ( for f being Function of A,B holds b1 . f = (Q * f) * (P " ) ) & ( for f being Function of A,B holds b2 . f = (Q * f) * (P " ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines => HILBERT3:def 1 :
for A, B being non empty set
for P being Permutation of A
for Q being Function of B,B
for b5 being Function of Funcs A,B, Funcs A,B holds
( b5 = P => Q iff for f being Function of A,B holds b5 . f = (Q * f) * (P " ) );

registration
let A, B be non empty set ;
let P be Permutation of A;
let Q be Permutation of B;
cluster P => Q -> bijective Function-yielding ;
coherence
P => Q is bijective
proof end;
end;

theorem Th26: :: HILBERT3:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty set
for P being Permutation of A
for Q being Permutation of B
for f being Function of A,B holds ((P => Q) " ) . f = ((Q " ) * f) * P
proof end;

theorem Th27: :: HILBERT3:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty set
for P being Permutation of A
for Q being Permutation of B holds (P => Q) " = (P " ) => (Q " )
proof end;

theorem Th28: :: HILBERT3:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B, C being non empty set
for f being Function of A, Funcs B,C
for g being Function of A,B
for P being Permutation of B
for Q being Permutation of C holds ((P => Q) * f) .. (P * g) = Q * (f .. g)
proof end;

definition
mode SetValuation is V3 ManySortedSet of NAT ;
end;

definition
let V be SetValuation;
func SetVal V -> ManySortedSet of HP-WFF means :Def2: :: HILBERT3:def 2
( it . VERUM = 1 & ( for n being Nat holds it . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( it . (p '&' q) = [:(it . p),(it . q):] & it . (p => q) = Funcs (it . p),(it . q) ) ) );
existence
ex b1 being ManySortedSet of HP-WFF st
( b1 . VERUM = 1 & ( for n being Nat holds b1 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b1 . (p '&' q) = [:(b1 . p),(b1 . q):] & b1 . (p => q) = Funcs (b1 . p),(b1 . q) ) ) )
proof end;
uniqueness
for b1, b2 being ManySortedSet of HP-WFF st b1 . VERUM = 1 & ( for n being Nat holds b1 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b1 . (p '&' q) = [:(b1 . p),(b1 . q):] & b1 . (p => q) = Funcs (b1 . p),(b1 . q) ) ) & b2 . VERUM = 1 & ( for n being Nat holds b2 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b2 . (p '&' q) = [:(b2 . p),(b2 . q):] & b2 . (p => q) = Funcs (b2 . p),(b2 . q) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines SetVal HILBERT3:def 2 :
for V being SetValuation
for b2 being ManySortedSet of HP-WFF holds
( b2 = SetVal V iff ( b2 . VERUM = 1 & ( for n being Nat holds b2 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b2 . (p '&' q) = [:(b2 . p),(b2 . q):] & b2 . (p => q) = Funcs (b2 . p),(b2 . q) ) ) ) );

definition
let V be SetValuation;
let p be Element of HP-WFF ;
func SetVal V,p -> set equals :: HILBERT3:def 3
(SetVal V) . p;
correctness
coherence
(SetVal V) . p is set
;
;
end;

:: deftheorem defines SetVal HILBERT3:def 3 :
for V being SetValuation
for p being Element of HP-WFF holds SetVal V,p = (SetVal V) . p;

registration
let V be SetValuation;
let p be Element of HP-WFF ;
cluster SetVal V,p -> non empty ;
coherence
not SetVal V,p is empty
proof end;
end;

theorem Th29: :: HILBERT3:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being SetValuation holds SetVal V,VERUM = 1 by Def2;

theorem Th30: :: HILBERT3:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for V being SetValuation holds SetVal V,(prop n) = V . n by Def2;

theorem Th31: :: HILBERT3:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF
for V being SetValuation holds SetVal V,(p '&' q) = [:(SetVal V,p),(SetVal V,q):] by Def2;

theorem Th32: :: HILBERT3:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF
for V being SetValuation holds SetVal V,(p => q) = Funcs (SetVal V,p),(SetVal V,q) by Def2;

registration
let V be SetValuation;
let p, q be Element of HP-WFF ;
cluster SetVal V,(p => q) -> non empty functional ;
coherence
SetVal V,(p => q) is functional
proof end;
end;

registration
let V be SetValuation;
let p, q, r be Element of HP-WFF ;
cluster -> Function-yielding Element of SetVal V,(p => (q => r));
coherence
for b1 being Element of SetVal V,(p => (q => r)) holds b1 is Function-yielding
proof end;
end;

registration
let V be SetValuation;
let p, q, r be Element of HP-WFF ;
cluster Function-yielding M5( SetVal V,(p => q), SetVal V,(p => r));
existence
ex b1 being Function of SetVal V,(p => q), SetVal V,(p => r) st b1 is Function-yielding
proof end;
cluster Function-yielding Element of SetVal V,(p => (q => r));
existence
ex b1 being Element of SetVal V,(p => (q => r)) st b1 is Function-yielding
proof end;
end;

definition
let V be SetValuation;
mode Permutation of V -> Function means :Def4: :: HILBERT3:def 4
( dom it = NAT & ( for n being Nat holds it . n is Permutation of V . n ) );
existence
ex b1 being Function st
( dom b1 = NAT & ( for n being Nat holds b1 . n is Permutation of V . n ) )
proof end;
end;

:: deftheorem Def4 defines Permutation HILBERT3:def 4 :
for V being SetValuation
for b2 being Function holds
( b2 is Permutation of V iff ( dom b2 = NAT & ( for n being Nat holds b2 . n is Permutation of V . n ) ) );

definition
let V be SetValuation;
let P be Permutation of V;
func Perm P -> ManySortedFunction of SetVal V, SetVal V means :Def5: :: HILBERT3:def 5
( it . VERUM = id 1 & ( for n being Nat holds it . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p' being Permutation of SetVal V,p ex q' being Permutation of SetVal V,q st
( p' = it . p & q' = it . q & it . (p '&' q) = [:p',q':] & it . (p => q) = p' => q' ) ) );
existence
ex b1 being ManySortedFunction of SetVal V, SetVal V st
( b1 . VERUM = id 1 & ( for n being Nat holds b1 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p' being Permutation of SetVal V,p ex q' being Permutation of SetVal V,q st
( p' = b1 . p & q' = b1 . q & b1 . (p '&' q) = [:p',q':] & b1 . (p => q) = p' => q' ) ) )
proof end;
uniqueness
for b1, b2 being ManySortedFunction of SetVal V, SetVal V st b1 . VERUM = id 1 & ( for n being Nat holds b1 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p' being Permutation of SetVal V,p ex q' being Permutation of SetVal V,q st
( p' = b1 . p & q' = b1 . q & b1 . (p '&' q) = [:p',q':] & b1 . (p => q) = p' => q' ) ) & b2 . VERUM = id 1 & ( for n being Nat holds b2 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p' being Permutation of SetVal V,p ex q' being Permutation of SetVal V,q st
( p' = b2 . p & q' = b2 . q & b2 . (p '&' q) = [:p',q':] & b2 . (p => q) = p' => q' ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Perm HILBERT3:def 5 :
for V being SetValuation
for P being Permutation of V
for b3 being ManySortedFunction of SetVal V, SetVal V holds
( b3 = Perm P iff ( b3 . VERUM = id 1 & ( for n being Nat holds b3 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p' being Permutation of SetVal V,p ex q' being Permutation of SetVal V,q st
( p' = b3 . p & q' = b3 . q & b3 . (p '&' q) = [:p',q':] & b3 . (p => q) = p' => q' ) ) ) );

definition
let V be SetValuation;
let P be Permutation of V;
let p be Element of HP-WFF ;
func Perm P,p -> Function of SetVal V,p, SetVal V,p equals :: HILBERT3:def 6
(Perm P) . p;
correctness
coherence
(Perm P) . p is Function of SetVal V,p, SetVal V,p
;
;
end;

:: deftheorem defines Perm HILBERT3:def 6 :
for V being SetValuation
for P being Permutation of V
for p being Element of HP-WFF holds Perm P,p = (Perm P) . p;

theorem Th33: :: HILBERT3:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being SetValuation
for P being Permutation of V holds Perm P,VERUM = id (SetVal V,VERUM )
proof end;

theorem Th34: :: HILBERT3:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for V being SetValuation
for P being Permutation of V holds Perm P,(prop n) = P . n by Def5;

theorem Th35: :: HILBERT3:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V holds Perm P,(p '&' q) = [:(Perm P,p),(Perm P,q):]
proof end;

theorem Th36: :: HILBERT3:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V
for p' being Permutation of SetVal V,p
for q' being Permutation of SetVal V,q st p' = Perm P,p & q' = Perm P,q holds
Perm P,(p => q) = p' => q'
proof end;

registration
let V be SetValuation;
let P be Permutation of V;
let p be Element of HP-WFF ;
cluster Perm P,p -> bijective ;
coherence
Perm P,p is bijective
proof end;
end;

theorem Th37: :: HILBERT3:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V
for g being Function of SetVal V,p, SetVal V,q holds (Perm P,(p => q)) . g = ((Perm P,q) * g) * ((Perm P,p) " )
proof end;

theorem Th38: :: HILBERT3:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V
for g being Function of SetVal V,p, SetVal V,q holds ((Perm P,(p => q)) " ) . g = (((Perm P,q) " ) * g) * (Perm P,p)
proof end;

theorem Th39: :: HILBERT3:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V
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)
proof end;

theorem Th40: :: HILBERT3:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V
for x being set st x is_a_fixpoint_of Perm P,p holds
for f being Function st f is_a_fixpoint_of Perm P,(p => q) holds
f . x is_a_fixpoint_of Perm P,q
proof end;

definition
let p be Element of HP-WFF ;
attr p is canonical means :Def7: :: HILBERT3:def 7
for V being SetValuation ex x being set st
for P being Permutation of V holds x is_a_fixpoint_of Perm P,p;
end;

:: deftheorem Def7 defines canonical HILBERT3:def 7 :
for p being Element of HP-WFF holds
( p is canonical iff for V being SetValuation ex x being set st
for P being Permutation of V holds x is_a_fixpoint_of Perm P,p );

registration
cluster VERUM -> canonical ;
coherence
VERUM is canonical
proof end;
end;

theorem Th41: :: HILBERT3:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds p => (q => p) is canonical
proof end;

theorem Th42: :: HILBERT3:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being Element of HP-WFF holds (p => (q => r)) => ((p => q) => (p => r)) is canonical
proof end;

theorem Th43: :: HILBERT3:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds (p '&' q) => p is canonical
proof end;

theorem Th44: :: HILBERT3:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds (p '&' q) => q is canonical
proof end;

theorem Th45: :: HILBERT3:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds p => (q => (p '&' q)) is canonical
proof end;

theorem Th46: :: HILBERT3:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF st p is canonical & p => q is canonical holds
q is canonical
proof end;

theorem :: HILBERT3:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of HP-WFF st p in HP_TAUT holds
p is canonical
proof end;

registration
cluster canonical Element of HP-WFF ;
existence
ex b1 being Element of HP-WFF st b1 is canonical
proof end;
end;

definition
let p be Element of HP-WFF ;
attr p is pseudo-canonical means :Def8: :: HILBERT3:def 8
for V being SetValuation
for P being Permutation of V ex x being set st x is_a_fixpoint_of Perm P,p;
end;

:: deftheorem Def8 defines pseudo-canonical HILBERT3:def 8 :
for p being Element of HP-WFF holds
( p is pseudo-canonical iff for V being SetValuation
for P being Permutation of V ex x being set st x is_a_fixpoint_of Perm P,p );

registration
cluster canonical -> pseudo-canonical Element of HP-WFF ;
coherence
for b1 being Element of HP-WFF st b1 is canonical holds
b1 is pseudo-canonical
proof end;
end;

theorem :: HILBERT3:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds p => (q => p) is pseudo-canonical
proof end;

theorem :: HILBERT3:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being Element of HP-WFF holds (p => (q => r)) => ((p => q) => (p => r)) is pseudo-canonical
proof end;

theorem :: HILBERT3:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds (p '&' q) => p is pseudo-canonical
proof end;

theorem :: HILBERT3:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds (p '&' q) => q is pseudo-canonical
proof end;

theorem :: HILBERT3:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds p => (q => (p '&' q)) is pseudo-canonical
proof end;

theorem :: HILBERT3:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF st p is pseudo-canonical & p => q is pseudo-canonical holds
q is pseudo-canonical
proof end;

theorem Th54: :: HILBERT3:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V st ex f being set st f is_a_fixpoint_of Perm P,p & ( for f being set holds not f is_a_fixpoint_of Perm P,q ) holds
not p => q is pseudo-canonical
proof end;

theorem :: HILBERT3:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
not (((prop 0) => (prop 1)) => (prop 0)) => (prop 0) is pseudo-canonical
proof end;