:: HILBERT3 semantic presentation

theorem Th1: :: HILBERT3:1

for b₁ being Integer holds
( b₁ is even iff not b₁ - 1 is even )

proof end;

theorem Th2: :: HILBERT3:2

for b₁ being Integer holds
( not b₁ is even iff b₁ - 1 is even )

proof end;

theorem Th3: :: HILBERT3:3

for b₁ being trivial set
for b₂ being set st b₂ in b₁ holds
for b₃ being Function of b₁,b₁ holds b₂ is_a_fixpoint_of b₃

proof end;

registration

let c₁, c₂, c₃ be set ;
cluster -> Function-yielding M5(a₁, Funcs a₂,a₃);
coherence

proof end;

end;

theorem Th4: :: HILBERT3:4

for b₁ being Function-yielding Function holds SubFuncs (rng b₁) = rng b₁

proof end;

theorem Th5: :: HILBERT3:5

for b₁, b₂, b₃ being set
for b₄ being Function st b₃ in b₁ & b₄ in Funcs b₁,b₂ holds
b₄ . b₃ in b₂

proof end;

theorem Th6: :: HILBERT3:6

for b₁, b₂, b₃ being set st ( not b₃ = {} or b₂ = {} or b₁ = {} ) holds
for b₄ being Function of b₁, Funcs b₂,b₃ holds doms b₄ = b₁ --> b₂

proof end;

registration

cluster {} -> Function-yielding ;
coherence

proof end;

end;

theorem Th7: :: HILBERT3:7

for b₁ being set holds {} . b₁ = {}

proof end;

registration

let c₁ be set ;
let c₂ be functional set ;
cluster -> Function-yielding M5(a₁,a₂);
coherence

proof end;

end;

theorem Th8: :: HILBERT3:8

for b₁ being set
for b₂ being Subset of b₁ holds (0,1 --> 1,0) * (chi b₂,b₁) = chi (b₂ ` ),b₁

proof end;

theorem Th9: :: HILBERT3:9

for b₁ being set
for b₂ being Subset of b₁ holds (0,1 --> 1,0) * (chi (b₂ ` ),b₁) = chi b₂,b₁

proof end;

theorem Th10: :: HILBERT3:10

for b₁, b₂, b₃, b₄, b₅, b₆ being set st b₁ <> b₂ & b₁,b₂ --> b₃,b₄ = b₁,b₂ --> b₅,b₆ holds
( b₃ = b₅ & b₄ = b₆ )

proof end;

theorem Th11: :: HILBERT3:11

for b₁, b₂, b₃, b₄, b₅, b₆ being set st b₁ <> b₂ & b₃ in b₅ & b₄ in b₆ holds
b₁,b₂ --> b₃,b₄ in product (b₁,b₂ --> b₅,b₆)

proof end;

theorem Th12: :: HILBERT3:12

for b₁ being non empty set
for b₂ being Function of 2,b₁ ex b₃, b₄ being Element of b₁ st b₂ = 0,1 --> b₃,b₄

proof end;

theorem Th13: :: HILBERT3:13

for b₁, b₂, b₃, b₄ being set st b₁ <> b₂ holds
(b₁,b₂ --> b₃,b₄) * (b₁,b₂ --> b₂,b₁) = b₁,b₂ --> b₄,b₃

proof end;

theorem Th14: :: HILBERT3:14

for b₁, b₂, b₃, b₄ being set
for b₅ being Function st b₁ <> b₂ & b₃ in dom b₅ & b₄ in dom b₅ holds
b₅ * (b₁,b₂ --> b₃,b₄) = b₁,b₂ --> (b₅ . b₃),(b₅ . b₄)

proof end;

registration

let c₁, c₂ be one-to-one Function;
cluster [:a₁,a₂:] -> one-to-one ;
coherence

proof end;

end;

theorem Th15: :: HILBERT3:15

for b₁, b₂ being non empty set
for b₃, b₄ being set
for b₅ being Function of b₃,b₁
for b₆ being Function of b₄,b₂ holds (pr1 b₁,b₂) * [:b₅,b₆:] = b₅ * (pr1 b₃,b₄)

proof end;

theorem Th16: :: HILBERT3:16

for b₁, b₂ being non empty set
for b₃, b₄ being set
for b₅ being Function of b₃,b₁
for b₆ being Function of b₄,b₂ holds (pr2 b₁,b₂) * [:b₅,b₆:] = b₆ * (pr2 b₃,b₄)

proof end;

theorem Th17: :: HILBERT3:17

for b₁ being Function holds {} .. b₁ = {}

proof end;

theorem Th18: :: HILBERT3:18

for b₁ being Function-yielding Function
for b₂, b₃ being Function holds (b₁ .. b₂) * b₃ = (b₁ * b₃) .. (b₂ * b₃)

proof end;

theorem Th19: :: HILBERT3:19

for b₁ being set
for b₂ being non empty set
for b₃ being Function of b₂, Funcs {} ,b₁
for b₄ being Function of b₂, {} holds rng (b₃ .. b₄) = {{} }

proof end;

theorem Th20: :: HILBERT3:20

for b₁, b₂, b₃ being set st ( b₂ = {} implies b₁ = {} ) holds
for b₄ being Function of b₁, Funcs b₂,b₃
for b₅ being Function of b₁,b₂ holds rng (b₄ .. b₅) c= b₃

proof end;

theorem Th21: :: HILBERT3:21

for b₁, b₂, b₃ being set st ( not b₃ = {} or b₂ = {} or b₁ = {} ) holds
for b₄ being Function of b₁, Funcs b₂,b₃ holds dom (Frege b₄) = Funcs b₁,b₂

proof end;

theorem Th22: :: HILBERT3:22

canceled;

theorem Th23: :: HILBERT3:23

for b₁, b₂, b₃ being set st ( not b₃ = {} or b₂ = {} or b₁ = {} ) holds
for b₄ being Function of b₁, Funcs b₂,b₃ holds rng (Frege b₄) c= Funcs b₁,b₃

proof end;

theorem Th24: :: HILBERT3:24

for b₁, b₂, b₃ being set st ( not b₃ = {} or b₂ = {} or b₁ = {} ) holds
for b₄ being Function of b₁, Funcs b₂,b₃ holds Frege b₄ is Function of Funcs b₁,b₂, Funcs b₁,b₃

proof end;

theorem Th25: :: HILBERT3:25

for b₁, b₂ being set
for b₃ being Permutation of b₁
for b₄ being Permutation of b₂ holds [:b₃,b₄:] is bijective

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be Permutation of c₁;
let c₄ be Function of c₂,c₂;
func c₃ => c₄ -> Function of Funcs a₁,a₂, Funcs a₁,a₂ means :Def1: :: HILBERT3:def 1
for b₁ being Function of a₁,a₂ holds a₅ . b₁ = (a₄ * b₁) * (a₃ " );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines => HILBERT3:def 1 :

registration

let c₁, c₂ be non empty set ;
let c₃ be Permutation of c₁;
let c₄ be Permutation of c₂;
cluster a₃ => a₄ -> bijective Function-yielding ;
coherence

proof end;

end;

theorem Th26: :: HILBERT3:26

for b₁, b₂ being non empty set
for b₃ being Permutation of b₁
for b₄ being Permutation of b₂
for b₅ being Function of b₁,b₂ holds ((b₃ => b₄) " ) . b₅ = ((b₄ " ) * b₅) * b₃

proof end;

theorem Th27: :: HILBERT3:27

for b₁, b₂ being non empty set
for b₃ being Permutation of b₁
for b₄ being Permutation of b₂ holds (b₃ => b₄) " = (b₃ " ) => (b₄ " )

proof end;

theorem Th28: :: HILBERT3:28

for b₁, b₂, b₃ being non empty set
for b₄ being Function of b₁, Funcs b₂,b₃
for b₅ being Function of b₁,b₂
for b₆ being Permutation of b₂
for b₇ being Permutation of b₃ holds ((b₆ => b₇) * b₄) .. (b₆ * b₅) = b₇ * (b₄ .. b₅)

proof end;

definition

mode SetValuation is V3 ManySortedSet of NAT ;

end;

definition

let c₁ be SetValuation;
func SetVal c₁ -> ManySortedSet of HP-WFF means :Def2: :: HILBERT3:def 2
( a₂ . VERUM = 1 & ( for b₁ being Nat holds a₂ . (prop b₁) = a₁ . b₁ ) & ( for b₁, b₂ being Element of HP-WFF holds
( a₂ . (b₁ '&' b₂) = [:(a₂ . b₁),(a₂ . b₂):] & a₂ . (b₁ => b₂) = Funcs (a₂ . b₁),(a₂ . b₂) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines SetVal HILBERT3:def 2 :

definition

let c₁ be SetValuation;
let c₂ be Element of HP-WFF ;
func SetVal c₁,c₂ -> set equals :: HILBERT3:def 3
(SetVal a₁) . a₂;
correctness ;

end;

:: deftheorem Def3 defines SetVal HILBERT3:def 3 :

registration

let c₁ be SetValuation;
let c₂ be Element of HP-WFF ;
cluster SetVal a₁,a₂ -> non empty ;
coherence

proof end;

end;

theorem Th29: :: HILBERT3:29

for b₁ being SetValuation holds SetVal b₁,VERUM = 1 by Def2;

theorem Th30: :: HILBERT3:30

for b₁ being Nat
for b₂ being SetValuation holds SetVal b₂,(prop b₁) = b₂ . b₁ by Def2;

theorem Th31: :: HILBERT3:31

for b₁, b₂ being Element of HP-WFF
for b₃ being SetValuation holds SetVal b₃,(b₁ '&' b₂) = [:(SetVal b₃,b₁),(SetVal b₃,b₂):] by Def2;

theorem Th32: :: HILBERT3:32

for b₁, b₂ being Element of HP-WFF
for b₃ being SetValuation holds SetVal b₃,(b₁ => b₂) = Funcs (SetVal b₃,b₁),(SetVal b₃,b₂) by Def2;

registration

let c₁ be SetValuation;
let c₂, c₃ be Element of HP-WFF ;
cluster SetVal a₁,(a₂ => a₃) -> non empty functional ;
coherence

proof end;

end;

registration

let c₁ be SetValuation;
let c₂, c₃, c₄ be Element of HP-WFF ;
cluster -> Function-yielding Element of SetVal a₁,(a₂ => (a₃ => a₄));
coherence

proof end;

end;

registration

let c₁ be SetValuation;
let c₂, c₃, c₄ be Element of HP-WFF ;
cluster Function-yielding M5( SetVal a₁,(a₂ => a₃), SetVal a₁,(a₂ => a₄));
existence

proof end;

cluster Function-yielding Element of SetVal a₁,(a₂ => (a₃ => a₄));
existence

proof end;

end;

definition

let c₁ be SetValuation;
mode Permutation of c₁ -> Function means :Def4: :: HILBERT3:def 4
( dom a₂ = NAT & ( for b₁ being Nat holds a₂ . b₁ is Permutation of a₁ . b₁ ) );
existence

proof end;

end;

:: deftheorem Def4 defines Permutation HILBERT3:def 4 :

definition

let c₁ be SetValuation;
let c₂ be Permutation of c₁;
func Perm c₂ -> ManySortedFunction of SetVal a₁, SetVal a₁ means :Def5: :: HILBERT3:def 5
( a₃ . VERUM = id 1 & ( for b₁ being Nat holds a₃ . (prop b₁) = a₂ . b₁ ) & ( for b₁, b₂ being Element of HP-WFF ex b₃ being Permutation of SetVal a₁,b₁ex b₄ being Permutation of SetVal a₁,b₂ st
( b₃ = a₃ . b₁ & b₄ = a₃ . b₂ & a₃ . (b₁ '&' b₂) = [:b₃,b₄:] & a₃ . (b₁ => b₂) = b₃ => b₄ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Perm HILBERT3:def 5 :

definition

let c₁ be SetValuation;
let c₂ be Permutation of c₁;
let c₃ be Element of HP-WFF ;
func Perm c₂,c₃ -> Function of SetVal a₁,a₃, SetVal a₁,a₃ equals :: HILBERT3:def 6
(Perm a₂) . a₃;
correctness ;

end;

:: deftheorem Def6 defines Perm HILBERT3:def 6 :

theorem Th33: :: HILBERT3:33

for b₁ being SetValuation
for b₂ being Permutation of b₁ holds Perm b₂,VERUM = id (SetVal b₁,VERUM )

proof end;

theorem Th34: :: HILBERT3:34

for b₁ being Nat
for b₂ being SetValuation
for b₃ being Permutation of b₂ holds Perm b₃,(prop b₁) = b₃ . b₁ by Def5;

theorem Th35: :: HILBERT3:35

for b₁, b₂ being Element of HP-WFF
for b₃ being SetValuation
for b₄ being Permutation of b₃ holds Perm b₄,(b₁ '&' b₂) = [:(Perm b₄,b₁),(Perm b₄,b₂):]

proof end;

theorem Th36: :: HILBERT3:36

for b₁, b₂ being Element of HP-WFF
for b₃ being SetValuation
for b₄ being Permutation of b₃
for b₅ being Permutation of SetVal b₃,b₁
for b₆ being Permutation of SetVal b₃,b₂ st b₅ = Perm b₄,b₁ & b₆ = Perm b₄,b₂ holds
Perm b₄,(b₁ => b₂) = b₅ => b₆

proof end;

registration

let c₁ be SetValuation;
let c₂ be Permutation of c₁;
let c₃ be Element of HP-WFF ;
cluster Perm a₂,a₃ -> bijective ;
coherence

proof end;

end;

theorem Th37: :: HILBERT3:37

for b₁, b₂ being Element of HP-WFF
for b₃ being SetValuation
for b₄ being Permutation of b₃
for b₅ being Function of SetVal b₃,b₁, SetVal b₃,b₂ holds (Perm b₄,(b₁ => b₂)) . b₅ = ((Perm b₄,b₂) * b₅) * ((Perm b₄,b₁) " )

proof end;

theorem Th38: :: HILBERT3:38

for b₁, b₂ being Element of HP-WFF
for b₃ being SetValuation
for b₄ being Permutation of b₃
for b₅ being Function of SetVal b₃,b₁, SetVal b₃,b₂ holds ((Perm b₄,(b₁ => b₂)) " ) . b₅ = (((Perm b₄,b₂) " ) * b₅) * (Perm b₄,b₁)

proof end;

theorem Th39: :: HILBERT3:39

for b₁, b₂ being Element of HP-WFF
for b₃ being SetValuation
for b₄ being Permutation of b₃
for b₅, b₆ being Function of SetVal b₃,b₁, SetVal b₃,b₂ st b₅ = (Perm b₄,(b₁ => b₂)) . b₆ holds
(Perm b₄,b₂) * b₆ = b₅ * (Perm b₄,b₁)

proof end;

theorem Th40: :: HILBERT3:40

for b₁, b₂ being Element of HP-WFF
for b₃ being SetValuation
for b₄ being Permutation of b₃
for b₅ being set st b₅ is_a_fixpoint_of Perm b₄,b₁ holds
for b₆ being Function st b₆ is_a_fixpoint_of Perm b₄,(b₁ => b₂) holds
b₆ . b₅ is_a_fixpoint_of Perm b₄,b₂

proof end;

definition

let c₁ be Element of HP-WFF ;
attr a₁ is canonical means :Def7: :: HILBERT3:def 7
for b₁ being SetValuation ex b₂ being set st
for b₃ being Permutation of b₁ holds b₂ is_a_fixpoint_of Perm b₃,a₁;

end;

:: deftheorem Def7 defines canonical HILBERT3:def 7 :

registration

cluster VERUM -> canonical ;
coherence

proof end;

end;

theorem Th41: :: HILBERT3:41

for b₁, b₂ being Element of HP-WFF holds b₁ => (b₂ => b₁) is canonical

proof end;

theorem Th42: :: HILBERT3:42

for b₁, b₂, b₃ being Element of HP-WFF holds (b₁ => (b₂ => b₃)) => ((b₁ => b₂) => (b₁ => b₃)) is canonical

proof end;

theorem Th43: :: HILBERT3:43

for b₁, b₂ being Element of HP-WFF holds (b₁ '&' b₂) => b₁ is canonical

proof end;

theorem Th44: :: HILBERT3:44

for b₁, b₂ being Element of HP-WFF holds (b₁ '&' b₂) => b₂ is canonical

proof end;

theorem Th45: :: HILBERT3:45

for b₁, b₂ being Element of HP-WFF holds b₁ => (b₂ => (b₁ '&' b₂)) is canonical

proof end;

theorem Th46: :: HILBERT3:46

for b₁, b₂ being Element of HP-WFF st b₁ is canonical & b₁ => b₂ is canonical holds
b₂ is canonical

proof end;

theorem Th47: :: HILBERT3:47

for b₁ being Element of HP-WFF st b₁ in HP_TAUT holds
b₁ is canonical

proof end;

registration

cluster canonical Element of HP-WFF ;
existence

proof end;

end;

definition

let c₁ be Element of HP-WFF ;
attr a₁ is pseudo-canonical means :Def8: :: HILBERT3:def 8
for b₁ being SetValuation
for b₂ being Permutation of b₁ ex b₃ being set st b₃ is_a_fixpoint_of Perm b₂,a₁;

end;

:: deftheorem Def8 defines pseudo-canonical HILBERT3:def 8 :

registration

cluster canonical -> pseudo-canonical Element of HP-WFF ;
coherence

proof end;

end;

theorem Th48: :: HILBERT3:48

for b₁, b₂ being Element of HP-WFF holds b₁ => (b₂ => b₁) is pseudo-canonical

proof end;

theorem Th49: :: HILBERT3:49

for b₁, b₂, b₃ being Element of HP-WFF holds (b₁ => (b₂ => b₃)) => ((b₁ => b₂) => (b₁ => b₃)) is pseudo-canonical

proof end;

theorem Th50: :: HILBERT3:50

for b₁, b₂ being Element of HP-WFF holds (b₁ '&' b₂) => b₁ is pseudo-canonical

proof end;

theorem Th51: :: HILBERT3:51

for b₁, b₂ being Element of HP-WFF holds (b₁ '&' b₂) => b₂ is pseudo-canonical

proof end;

theorem Th52: :: HILBERT3:52

for b₁, b₂ being Element of HP-WFF holds b₁ => (b₂ => (b₁ '&' b₂)) is pseudo-canonical

proof end;

theorem Th53: :: HILBERT3:53

for b₁, b₂ being Element of HP-WFF st b₁ is pseudo-canonical & b₁ => b₂ is pseudo-canonical holds
b₂ is pseudo-canonical

proof end;

theorem Th54: :: HILBERT3:54

for b₁, b₂ being Element of HP-WFF
for b₃ being SetValuation
for b₄ being Permutation of b₃ st ex b₅ being set st b₅ is_a_fixpoint_of Perm b₄,b₁ & ( for b₅ being set holds not b₅ is_a_fixpoint_of Perm b₄,b₂ ) holds
not b₁ => b₂ is pseudo-canonical

proof end;

theorem Th55: :: HILBERT3:55

not (((prop 0) => (prop 1)) => (prop 0)) => (prop 0) is pseudo-canonical

proof end;