:: HILBERT1 semantic presentation

definition
let c1 be set ;
attr a1 is with_VERUM means :Def1: :: HILBERT1:def 1
<*0*> in a1;
end;

:: deftheorem Def1 defines with_VERUM HILBERT1:def 1 :
for b1 being set holds
( b1 is with_VERUM iff <*0*> in b1 );

definition
let c1 be set ;
attr a1 is with_implication means :Def2: :: HILBERT1:def 2
for b1, b2 being FinSequence st b1 in a1 & b2 in a1 holds
(<*1*> ^ b1) ^ b2 in a1;
end;

:: deftheorem Def2 defines with_implication HILBERT1:def 2 :
for b1 being set holds
( b1 is with_implication iff for b2, b3 being FinSequence st b2 in b1 & b3 in b1 holds
(<*1*> ^ b2) ^ b3 in b1 );

definition
let c1 be set ;
attr a1 is with_conjunction means :Def3: :: HILBERT1:def 3
for b1, b2 being FinSequence st b1 in a1 & b2 in a1 holds
(<*2*> ^ b1) ^ b2 in a1;
end;

:: deftheorem Def3 defines with_conjunction HILBERT1:def 3 :
for b1 being set holds
( b1 is with_conjunction iff for b2, b3 being FinSequence st b2 in b1 & b3 in b1 holds
(<*2*> ^ b2) ^ b3 in b1 );

definition
let c1 be set ;
attr a1 is with_propositional_variables means :Def4: :: HILBERT1:def 4
for b1 being Nat holds <*(3 + b1)*> in a1;
end;

:: deftheorem Def4 defines with_propositional_variables HILBERT1:def 4 :
for b1 being set holds
( b1 is with_propositional_variables iff for b2 being Nat holds <*(3 + b2)*> in b1 );

definition
let c1 be set ;
attr a1 is HP-closed means :Def5: :: HILBERT1:def 5
( a1 c= NAT * & a1 is with_VERUM & a1 is with_implication & a1 is with_conjunction & a1 is with_propositional_variables );
end;

:: deftheorem Def5 defines HP-closed HILBERT1:def 5 :
for b1 being set holds
( b1 is HP-closed iff ( b1 c= NAT * & b1 is with_VERUM & b1 is with_implication & b1 is with_conjunction & b1 is with_propositional_variables ) );

Lemma6: for b1 being set st b1 is HP-closed holds
not b1 is empty
proof end;

registration
cluster HP-closed -> non empty with_VERUM with_implication with_conjunction with_propositional_variables set ;
coherence
for b1 being set st b1 is HP-closed holds
( b1 is with_VERUM & b1 is with_implication & b1 is with_conjunction & b1 is with_propositional_variables & not b1 is empty ) by Def5, Lemma6;
cluster with_VERUM with_implication with_conjunction with_propositional_variables -> HP-closed Element of K40((NAT * ));
coherence
for b1 being Subset of (NAT * ) st b1 is with_VERUM & b1 is with_implication & b1 is with_conjunction & b1 is with_propositional_variables holds
b1 is HP-closed by Def5;
end;

definition
func HP-WFF -> set means :Def6: :: HILBERT1:def 6
( a1 is HP-closed & ( for b1 being set st b1 is HP-closed holds
a1 c= b1 ) );
existence
ex b1 being set st
( b1 is HP-closed & ( for b2 being set st b2 is HP-closed holds
b1 c= b2 ) )
proof end;
uniqueness
for b1, b2 being set st b1 is HP-closed & ( for b3 being set st b3 is HP-closed holds
b1 c= b3 ) & b2 is HP-closed & ( for b3 being set st b3 is HP-closed holds
b2 c= b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines HP-WFF HILBERT1:def 6 :
for b1 being set holds
( b1 = HP-WFF iff ( b1 is HP-closed & ( for b2 being set st b2 is HP-closed holds
b1 c= b2 ) ) );

registration
cluster HP-WFF -> non empty with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ;
coherence
HP-WFF is HP-closed by Def6;
end;

registration
cluster non empty with_VERUM with_implication with_conjunction with_propositional_variables HP-closed set ;
existence
ex b1 being set st
( b1 is HP-closed & not b1 is empty )
proof end;
end;

registration
cluster HP-WFF -> non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ;
coherence
HP-WFF is functional
proof end;
end;

registration
cluster -> FinSequence-like Element of HP-WFF ;
coherence
for b1 being Element of HP-WFF holds b1 is FinSequence-like
proof end;
end;

definition
mode HP-formula is Element of HP-WFF ;
end;

definition
func VERUM -> HP-formula equals :: HILBERT1:def 7
<*0*>;
correctness
coherence
<*0*> is HP-formula;
by Def1;
let c1, c2 be Element of HP-WFF ;
func c1 => c2 -> HP-formula equals :: HILBERT1:def 8
(<*1*> ^ a1) ^ a2;
coherence
(<*1*> ^ c1) ^ c2 is HP-formula by Def2;
func c1 '&' c2 -> HP-formula equals :: HILBERT1:def 9
(<*2*> ^ a1) ^ a2;
correctness
coherence
(<*2*> ^ c1) ^ c2 is HP-formula;
by Def3;
end;

:: deftheorem Def7 defines VERUM HILBERT1:def 7 :
VERUM = <*0*>;

:: deftheorem Def8 defines => HILBERT1:def 8 :
for b1, b2 being Element of HP-WFF holds b1 => b2 = (<*1*> ^ b1) ^ b2;

:: deftheorem Def9 defines '&' HILBERT1:def 9 :
for b1, b2 being Element of HP-WFF holds b1 '&' b2 = (<*2*> ^ b1) ^ b2;

definition
let c1 be Subset of HP-WFF ;
attr a1 is Hilbert_theory means :Def10: :: HILBERT1:def 10
( VERUM in a1 & ( for b1, b2, b3 being Element of HP-WFF holds
( b1 => (b2 => b1) in a1 & (b1 => (b2 => b3)) => ((b1 => b2) => (b1 => b3)) in a1 & (b1 '&' b2) => b1 in a1 & (b1 '&' b2) => b2 in a1 & b1 => (b2 => (b1 '&' b2)) in a1 & ( b1 in a1 & b1 => b2 in a1 implies b2 in a1 ) ) ) );
correctness
;
end;

:: deftheorem Def10 defines Hilbert_theory HILBERT1:def 10 :
for b1 being Subset of HP-WFF holds
( b1 is Hilbert_theory iff ( VERUM in b1 & ( for b2, b3, b4 being Element of HP-WFF holds
( b2 => (b3 => b2) in b1 & (b2 => (b3 => b4)) => ((b2 => b3) => (b2 => b4)) in b1 & (b2 '&' b3) => b2 in b1 & (b2 '&' b3) => b3 in b1 & b2 => (b3 => (b2 '&' b3)) in b1 & ( b2 in b1 & b2 => b3 in b1 implies b3 in b1 ) ) ) ) );

definition
let c1 be Subset of HP-WFF ;
func CnPos c1 -> Subset of HP-WFF means :Def11: :: HILBERT1:def 11
for b1 being Element of HP-WFF holds
( b1 in a2 iff for b2 being Subset of HP-WFF st b2 is Hilbert_theory & a1 c= b2 holds
b1 in b2 );
existence
ex b1 being Subset of HP-WFF st
for b2 being Element of HP-WFF holds
( b2 in b1 iff for b3 being Subset of HP-WFF st b3 is Hilbert_theory & c1 c= b3 holds
b2 in b3 )
proof end;
uniqueness
for b1, b2 being Subset of HP-WFF st ( for b3 being Element of HP-WFF holds
( b3 in b1 iff for b4 being Subset of HP-WFF st b4 is Hilbert_theory & c1 c= b4 holds
b3 in b4 ) ) & ( for b3 being Element of HP-WFF holds
( b3 in b2 iff for b4 being Subset of HP-WFF st b4 is Hilbert_theory & c1 c= b4 holds
b3 in b4 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines CnPos HILBERT1:def 11 :
for b1, b2 being Subset of HP-WFF holds
( b2 = CnPos b1 iff for b3 being Element of HP-WFF holds
( b3 in b2 iff for b4 being Subset of HP-WFF st b4 is Hilbert_theory & b1 c= b4 holds
b3 in b4 ) );

definition
func HP_TAUT -> Subset of HP-WFF equals :: HILBERT1:def 12
 CnPos ({} HP-WFF );
correctness
coherence
CnPos ({} HP-WFF ) is Subset of HP-WFF ;
;
end;

:: deftheorem Def12 defines HP_TAUT HILBERT1:def 12 :
HP_TAUT = CnPos ({} HP-WFF );

theorem Th1: :: HILBERT1:1
for b1 being Subset of HP-WFF holds VERUM in CnPos b1
proof end;

theorem Th2: :: HILBERT1:2
for b1 being Subset of HP-WFF
for b2, b3 being Element of HP-WFF holds b2 => (b3 => (b2 '&' b3)) in CnPos b1
proof end;

theorem Th3: :: HILBERT1:3
for b1 being Subset of HP-WFF
for b2, b3, b4 being Element of HP-WFF holds (b2 => (b3 => b4)) => ((b2 => b3) => (b2 => b4)) in CnPos b1
proof end;

theorem Th4: :: HILBERT1:4
for b1 being Subset of HP-WFF
for b2, b3 being Element of HP-WFF holds b2 => (b3 => b2) in CnPos b1
proof end;

theorem Th5: :: HILBERT1:5
for b1 being Subset of HP-WFF
for b2, b3 being Element of HP-WFF holds (b2 '&' b3) => b2 in CnPos b1
proof end;

theorem Th6: :: HILBERT1:6
for b1 being Subset of HP-WFF
for b2, b3 being Element of HP-WFF holds (b2 '&' b3) => b3 in CnPos b1
proof end;

theorem Th7: :: HILBERT1:7
for b1 being Subset of HP-WFF
for b2, b3 being Element of HP-WFF st b2 in CnPos b1 & b2 => b3 in CnPos b1 holds
b3 in CnPos b1
proof end;

theorem Th8: :: HILBERT1:8
for b1, b2 being Subset of HP-WFF st b1 is Hilbert_theory & b2 c= b1 holds
CnPos b2 c= b1
proof end;

theorem Th9: :: HILBERT1:9
for b1 being Subset of HP-WFF holds b1 c= CnPos b1
proof end;

theorem Th10: :: HILBERT1:10
for b1, b2 being Subset of HP-WFF st b1 c= b2 holds
CnPos b1 c= CnPos b2
proof end;

Lemma20: for b1 being Subset of HP-WFF holds CnPos (CnPos b1) c= CnPos b1
proof end;

theorem Th11: :: HILBERT1:11
for b1 being Subset of HP-WFF holds CnPos (CnPos b1) = CnPos b1
proof end;

Lemma21: for b1 being Subset of HP-WFF holds CnPos b1 is Hilbert_theory
proof end;

registration
let c1 be Subset of HP-WFF ;
cluster CnPos a1 -> Hilbert_theory ;
coherence
CnPos c1 is Hilbert_theory by Lemma21;
end;

theorem Th12: :: HILBERT1:12
for b1 being Subset of HP-WFF holds
( b1 is Hilbert_theory iff CnPos b1 = b1 )
proof end;

theorem Th13: :: HILBERT1:13
for b1 being Subset of HP-WFF st b1 is Hilbert_theory holds
HP_TAUT c= b1
proof end;

registration
cluster HP_TAUT -> Hilbert_theory ;
coherence
HP_TAUT is Hilbert_theory ;
end;

theorem Th14: :: HILBERT1:14
for b1 being Element of HP-WFF holds b1 => b1 in HP_TAUT
proof end;

theorem Th15: :: HILBERT1:15
for b1, b2 being Element of HP-WFF st b1 in HP_TAUT holds
b2 => b1 in HP_TAUT
proof end;

theorem Th16: :: HILBERT1:16
for b1 being Element of HP-WFF holds b1 => VERUM in HP_TAUT
proof end;

theorem Th17: :: HILBERT1:17
for b1, b2 being Element of HP-WFF holds (b1 => b2) => (b1 => b1) in HP_TAUT
proof end;

theorem Th18: :: HILBERT1:18
for b1, b2 being Element of HP-WFF holds (b1 => b2) => (b2 => b2) in HP_TAUT
proof end;

theorem Th19: :: HILBERT1:19
for b1, b2, b3 being Element of HP-WFF holds (b1 => b2) => ((b3 => b1) => (b3 => b2)) in HP_TAUT
proof end;

theorem Th20: :: HILBERT1:20
for b1, b2, b3 being Element of HP-WFF st b1 => (b2 => b3) in HP_TAUT holds
b2 => (b1 => b3) in HP_TAUT
proof end;

theorem Th21: :: HILBERT1:21
for b1, b2, b3 being Element of HP-WFF holds (b1 => b2) => ((b2 => b3) => (b1 => b3)) in HP_TAUT
proof end;

theorem Th22: :: HILBERT1:22
for b1, b2, b3 being Element of HP-WFF st b1 => b2 in HP_TAUT holds
(b2 => b3) => (b1 => b3) in HP_TAUT
proof end;

theorem Th23: :: HILBERT1:23
for b1, b2, b3 being Element of HP-WFF st b1 => b2 in HP_TAUT & b2 => b3 in HP_TAUT holds
b1 => b3 in HP_TAUT
proof end;

Lemma30: for b1, b2, b3, b4 being Element of HP-WFF holds (((b1 => b2) => (b3 => b2)) => b4) => ((b3 => b1) => b4) in HP_TAUT
proof end;

theorem Th24: :: HILBERT1:24
for b1, b2, b3, b4 being Element of HP-WFF holds (b1 => (b2 => b3)) => ((b4 => b2) => (b1 => (b4 => b3))) in HP_TAUT
proof end;

theorem Th25: :: HILBERT1:25
for b1, b2, b3 being Element of HP-WFF holds ((b1 => b2) => b3) => (b2 => b3) in HP_TAUT
proof end;

theorem Th26: :: HILBERT1:26
for b1, b2, b3 being Element of HP-WFF holds (b1 => (b2 => b3)) => (b2 => (b1 => b3)) in HP_TAUT
proof end;

theorem Th27: :: HILBERT1:27
for b1, b2 being Element of HP-WFF holds (b1 => (b1 => b2)) => (b1 => b2) in HP_TAUT
proof end;

theorem Th28: :: HILBERT1:28
for b1, b2 being Element of HP-WFF holds b1 => ((b1 => b2) => b2) in HP_TAUT
proof end;

theorem Th29: :: HILBERT1:29
for b1, b2, b3 being Element of HP-WFF st b1 => (b2 => b3) in HP_TAUT & b2 in HP_TAUT holds
b1 => b3 in HP_TAUT
proof end;

theorem Th30: :: HILBERT1:30
for b1 being Element of HP-WFF holds b1 => (b1 '&' b1) in HP_TAUT
proof end;

theorem Th31: :: HILBERT1:31
for b1, b2 being Element of HP-WFF holds
( b1 '&' b2 in HP_TAUT iff ( b1 in HP_TAUT & b2 in HP_TAUT ) )
proof end;

theorem Th32: :: HILBERT1:32
for b1, b2 being Element of HP-WFF holds
( b1 '&' b2 in HP_TAUT iff b2 '&' b1 in HP_TAUT )
proof end;

theorem Th33: :: HILBERT1:33
for b1, b2, b3 being Element of HP-WFF holds ((b1 '&' b2) => b3) => (b1 => (b2 => b3)) in HP_TAUT
proof end;

theorem Th34: :: HILBERT1:34
for b1, b2, b3 being Element of HP-WFF holds (b1 => (b2 => b3)) => ((b1 '&' b2) => b3) in HP_TAUT
proof end;

theorem Th35: :: HILBERT1:35
for b1, b2, b3 being Element of HP-WFF holds (b1 => b2) => ((b1 => b3) => (b1 => (b2 '&' b3))) in HP_TAUT
proof end;

theorem Th36: :: HILBERT1:36
for b1, b2 being Element of HP-WFF holds ((b1 => b2) '&' b1) => b2 in HP_TAUT
proof end;

theorem Th37: :: HILBERT1:37
for b1, b2, b3 being Element of HP-WFF holds (((b1 => b2) '&' b1) '&' b3) => b2 in HP_TAUT
proof end;

theorem Th38: :: HILBERT1:38
for b1, b2, b3 being Element of HP-WFF holds (b1 => b2) => ((b3 '&' b1) => b2) in HP_TAUT
proof end;

theorem Th39: :: HILBERT1:39
for b1, b2, b3 being Element of HP-WFF holds (b1 => b2) => ((b1 '&' b3) => b2) in HP_TAUT
proof end;

theorem Th40: :: HILBERT1:40
for b1, b2, b3 being Element of HP-WFF holds ((b1 '&' b2) => b3) => ((b1 '&' b2) => (b3 '&' b2)) in HP_TAUT
proof end;

theorem Th41: :: HILBERT1:41
for b1, b2, b3 being Element of HP-WFF holds (b1 => b2) => ((b1 '&' b3) => (b2 '&' b3)) in HP_TAUT
proof end;

theorem Th42: :: HILBERT1:42
for b1, b2, b3 being Element of HP-WFF holds ((b1 => b2) '&' (b1 '&' b3)) => (b2 '&' b3) in HP_TAUT
proof end;

theorem Th43: :: HILBERT1:43
for b1, b2 being Element of HP-WFF holds (b1 '&' b2) => (b2 '&' b1) in HP_TAUT
proof end;

theorem Th44: :: HILBERT1:44
for b1, b2, b3 being Element of HP-WFF holds ((b1 => b2) '&' (b1 '&' b3)) => (b3 '&' b2) in HP_TAUT
proof end;

theorem Th45: :: HILBERT1:45
for b1, b2, b3 being Element of HP-WFF holds (b1 => b2) => ((b1 '&' b3) => (b3 '&' b2)) in HP_TAUT
proof end;

theorem Th46: :: HILBERT1:46
for b1, b2, b3 being Element of HP-WFF holds (b1 => b2) => ((b3 '&' b1) => (b3 '&' b2)) in HP_TAUT
proof end;

theorem Th47: :: HILBERT1:47
for b1, b2, b3 being Element of HP-WFF holds (b1 '&' (b2 '&' b3)) => (b1 '&' (b3 '&' b2)) in HP_TAUT
proof end;

theorem Th48: :: HILBERT1:48
for b1, b2, b3 being Element of HP-WFF holds ((b1 => b2) '&' (b1 => b3)) => (b1 => (b2 '&' b3)) in HP_TAUT
proof end;

Lemma49: for b1, b2, b3 being Element of HP-WFF holds ((b1 '&' b2) '&' b3) => b2 in HP_TAUT
proof end;

Lemma50: for b1, b2, b3 being Element of HP-WFF holds (((b1 '&' b2) '&' b3) '&' ((b1 '&' b2) '&' b3)) => (((b1 '&' b2) '&' b3) '&' b2) in HP_TAUT
proof end;

Lemma51: for b1, b2, b3 being Element of HP-WFF holds ((b1 '&' b2) '&' b3) => (((b1 '&' b2) '&' b3) '&' b2) in HP_TAUT
proof end;

Lemma52: for b1, b2, b3 being Element of HP-WFF holds ((b1 '&' b2) '&' b3) => (b1 '&' b3) in HP_TAUT
proof end;

Lemma53: for b1, b2, b3 being Element of HP-WFF holds (((b1 '&' b2) '&' b3) '&' b2) => ((b1 '&' b3) '&' b2) in HP_TAUT
proof end;

Lemma54: for b1, b2, b3 being Element of HP-WFF holds ((b1 '&' b2) '&' b3) => ((b1 '&' b3) '&' b2) in HP_TAUT
proof end;

Lemma55: for b1, b2, b3 being Element of HP-WFF holds ((b1 '&' b2) '&' b3) => ((b2 '&' b1) '&' b3) in HP_TAUT
proof end;

Lemma56: for b1, b2, b3 being Element of HP-WFF holds ((b1 '&' b2) '&' b3) => ((b3 '&' b1) '&' b2) in HP_TAUT
proof end;

Lemma57: for b1, b2, b3 being Element of HP-WFF holds ((b1 '&' b2) '&' b3) => ((b3 '&' b2) '&' b1) in HP_TAUT
proof end;

Lemma58: for b1, b2, b3 being Element of HP-WFF holds ((b1 '&' b2) '&' b3) => (b1 '&' (b3 '&' b2)) in HP_TAUT
proof end;

Lemma59: for b1, b2, b3 being Element of HP-WFF holds (b1 '&' (b2 '&' b3)) => (b1 '&' (b3 '&' b2)) in HP_TAUT
proof end;

theorem Th49: :: HILBERT1:49
for b1, b2, b3 being Element of HP-WFF holds ((b1 '&' b2) '&' b3) => (b1 '&' (b2 '&' b3)) in HP_TAUT
proof end;

Lemma60: for b1, b2, b3 being Element of HP-WFF holds (b1 '&' (b2 '&' b3)) => ((b3 '&' b2) '&' b1) in HP_TAUT
proof end;

Lemma61: for b1, b2, b3 being Element of HP-WFF holds ((b1 '&' b2) '&' b3) => ((b2 '&' b1) '&' b3) in HP_TAUT
proof end;

Lemma62: for b1, b2, b3 being Element of HP-WFF holds (b1 '&' (b2 '&' b3)) => ((b2 '&' b3) '&' b1) in HP_TAUT
proof end;

Lemma63: for b1, b2, b3 being Element of HP-WFF holds (b1 '&' (b2 '&' b3)) => ((b1 '&' b3) '&' b2) in HP_TAUT
proof end;

Lemma64: for b1, b2, b3 being Element of HP-WFF holds (b1 '&' (b2 '&' b3)) => (b1 '&' (b3 '&' b2)) in HP_TAUT
proof end;

theorem Th50: :: HILBERT1:50
for b1, b2, b3 being Element of HP-WFF holds (b1 '&' (b2 '&' b3)) => ((b1 '&' b2) '&' b3) in HP_TAUT
proof end;