begin
:: deftheorem Def1 defines with_VERUM HILBERT1:def 1 :
for D being set holds
( D is with_VERUM iff <*0*> in D );
:: deftheorem Def2 defines with_implication HILBERT1:def 2 :
for D being set holds
( D is with_implication iff for p, q being FinSequence st p in D & q in D holds
(<*1*> ^ p) ^ q in D );
:: deftheorem Def3 defines with_conjunction HILBERT1:def 3 :
for D being set holds
( D is with_conjunction iff for p, q being FinSequence st p in D & q in D holds
(<*2*> ^ p) ^ q in D );
:: deftheorem Def4 defines with_propositional_variables HILBERT1:def 4 :
for D being set holds
( D is with_propositional_variables iff for n being Element of NAT holds <*(3 + n)*> in D );
:: deftheorem Def5 defines HP-closed HILBERT1:def 5 :
for D being set holds
( D is HP-closed iff ( D c= NAT * & D is with_VERUM & D is with_implication & D is with_conjunction & D is with_propositional_variables ) );
Lm1:
for D being set st D is HP-closed holds
not D is empty
:: deftheorem Def6 defines HP-WFF HILBERT1:def 6 :
for b1 being set holds
( b1 = HP-WFF iff ( b1 is HP-closed & ( for D being set st D is HP-closed holds
b1 c= D ) ) );
:: deftheorem defines VERUM HILBERT1:def 7 :
VERUM = <*0*>;
:: deftheorem defines => HILBERT1:def 8 :
for p, q being Element of HP-WFF holds p => q = (<*1*> ^ p) ^ q;
:: deftheorem defines '&' HILBERT1:def 9 :
for p, q being Element of HP-WFF holds p '&' q = (<*2*> ^ p) ^ q;
:: deftheorem Def10 defines Hilbert_theory HILBERT1:def 10 :
for T being Subset of HP-WFF holds
( T is Hilbert_theory iff ( VERUM in T & ( for p, q, r being Element of HP-WFF holds
( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & ( p in T & p => q in T implies q in T ) ) ) ) );
:: deftheorem Def11 defines CnPos HILBERT1:def 11 :
for X, b2 being Subset of HP-WFF holds
( b2 = CnPos X iff for r being Element of HP-WFF holds
( r in b2 iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) );
:: deftheorem defines HP_TAUT HILBERT1:def 12 :
HP_TAUT = CnPos ({} HP-WFF);
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
Lm2:
for X being Subset of HP-WFF holds CnPos (CnPos X) c= CnPos X
theorem
Lm3:
for X being Subset of HP-WFF holds CnPos X is Hilbert_theory
theorem Th12:
theorem
begin
theorem Th14:
theorem Th15:
theorem
theorem
theorem
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
Lm4:
for q, r, p, s being Element of HP-WFF holds (((q => r) => (p => r)) => s) => ((p => q) => s) in HP_TAUT
theorem Th24:
theorem
theorem Th26:
theorem Th27:
theorem
theorem Th29:
begin
theorem Th30:
theorem Th31:
theorem
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem
theorem
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem
theorem
Lm5:
for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => q in HP_TAUT
Lm6:
for p, q, s being Element of HP-WFF holds (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in HP_TAUT
Lm7:
for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT
Lm8:
for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' s) in HP_TAUT
Lm9:
for p, q, s being Element of HP-WFF holds (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT
Lm10:
for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((p '&' s) '&' q) in HP_TAUT
Lm11:
for p, s, q being Element of HP-WFF holds ((p '&' s) '&' q) => ((s '&' p) '&' q) in HP_TAUT
Lm12:
for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((s '&' p) '&' q) in HP_TAUT
Lm13:
for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((s '&' q) '&' p) in HP_TAUT
Lm14:
for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' (s '&' q)) in HP_TAUT
Lm15:
for p, s, q being Element of HP-WFF holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT
theorem
Lm16:
for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT
Lm17:
for s, q, p being Element of HP-WFF holds ((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT
Lm18:
for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT
Lm19:
for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((p '&' s) '&' q) in HP_TAUT
Lm20:
for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT
theorem