:: by Adam Grabowski

::

:: Received February 20, 1999

:: Copyright (c) 1999-2012 Association of Mizar Users

begin

:: deftheorem Def1 defines with_VERUM HILBERT1:def 1 :

for D being set holds

( D is with_VERUM iff <*0*> in D );

for D being set holds

( D is with_VERUM iff <*0*> in D );

definition

let D be set ;

end;
attr D is with_implication means :Def2: :: HILBERT1:def 2

for p, q being FinSequence st p in D & q in D holds

(<*1*> ^ p) ^ q in D;

for p, q being FinSequence st p in D & q in D holds

(<*1*> ^ p) ^ q 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 );

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 );

definition

let D be set ;

end;
attr D is with_conjunction means :Def3: :: HILBERT1:def 3

for p, q being FinSequence st p in D & q in D holds

(<*2*> ^ p) ^ q in D;

for p, q being FinSequence st p in D & q in D holds

(<*2*> ^ 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 );

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 );

definition

let D be set ;

end;
attr D is with_propositional_variables means :Def4: :: HILBERT1:def 4

for n being Element of NAT holds <*(3 + n)*> in D;

for n being Element of NAT holds <*(3 + n)*> 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 );

for D being set holds

( D is with_propositional_variables iff for n being Element of NAT holds <*(3 + n)*> in D );

definition

let D be set ;

end;
attr D is HP-closed means :Def5: :: HILBERT1:def 5

( D c= NAT * & D is with_VERUM & D is with_implication & D is with_conjunction & D is with_propositional_variables );

( D c= NAT * & D is with_VERUM & D is with_implication & D is with_conjunction & D is with_propositional_variables );

:: 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 ) );

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

proof end;

registration

for b_{1} being set st b_{1} is HP-closed holds

( b_{1} is with_VERUM & b_{1} is with_implication & b_{1} is with_conjunction & b_{1} is with_propositional_variables & not b_{1} is empty )
by Def5, Lm1;

for b_{1} being Subset of (NAT *) st b_{1} is with_VERUM & b_{1} is with_implication & b_{1} is with_conjunction & b_{1} is with_propositional_variables holds

b_{1} is HP-closed
by Def5;

end;

cluster HP-closed -> non empty with_VERUM with_implication with_conjunction with_propositional_variables for set ;

coherence for b

( b

cluster with_VERUM with_implication with_conjunction with_propositional_variables -> HP-closed for Element of K6((NAT *));

coherence for b

b

definition

ex b_{1} being set st

( b_{1} is HP-closed & ( for D being set st D is HP-closed holds

b_{1} c= D ) )

for b_{1}, b_{2} being set st b_{1} is HP-closed & ( for D being set st D is HP-closed holds

b_{1} c= D ) & b_{2} is HP-closed & ( for D being set st D is HP-closed holds

b_{2} c= D ) holds

b_{1} = b_{2}
end;

func HP-WFF -> set means :Def6: :: HILBERT1:def 6

( it is HP-closed & ( for D being set st D is HP-closed holds

it c= D ) );

existence ( it is HP-closed & ( for D being set st D is HP-closed holds

it c= D ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def6 defines HP-WFF HILBERT1:def 6 :

for b_{1} being set holds

( b_{1} = HP-WFF iff ( b_{1} is HP-closed & ( for D being set st D is HP-closed holds

b_{1} c= D ) ) );

for b

( b

b

registration
end;

registration
end;

definition

correctness

coherence

<*0*> is HP-formula;

by Def1;

let p, q be Element of HP-WFF ;

coherence

(<*1*> ^ p) ^ q is HP-formula by Def2;

correctness

coherence

(<*2*> ^ p) ^ q is HP-formula;

by Def3;

end;
coherence

<*0*> is HP-formula;

by Def1;

let p, q be Element of HP-WFF ;

coherence

(<*1*> ^ p) ^ q is HP-formula by Def2;

correctness

coherence

(<*2*> ^ p) ^ q is HP-formula;

by Def3;

:: deftheorem defines => HILBERT1:def 8 :

for p, q being Element of HP-WFF holds p => q = (<*1*> ^ p) ^ q;

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;

for p, q being Element of HP-WFF holds p '&' q = (<*2*> ^ p) ^ q;

definition

let T be Subset of HP-WFF;

;

end;
attr T is Hilbert_theory means :Def10: :: HILBERT1:def 10

( 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 ) ) ) );

correctness ( 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 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 ) ) ) ) );

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 ) ) ) ) );

definition

let X be Subset of HP-WFF;

ex b_{1} being Subset of HP-WFF st

for r being Element of HP-WFF holds

( r in b_{1} iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds

r in T )

for b_{1}, b_{2} being Subset of HP-WFF st ( for r being Element of HP-WFF holds

( r in b_{1} iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds

r in T ) ) & ( for r being Element of HP-WFF holds

( r in b_{2} iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds

r in T ) ) holds

b_{1} = b_{2}

end;
func CnPos X -> Subset of HP-WFF means :Def11: :: HILBERT1:def 11

for r being Element of HP-WFF holds

( r in it iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds

r in T );

existence for r being Element of HP-WFF holds

( r in it iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds

r in T );

ex b

for r being Element of HP-WFF holds

( r in b

r in T )

proof end;

uniqueness for b

( r in b

r in T ) ) & ( for r being Element of HP-WFF holds

( r in b

r in T ) ) holds

b

proof end;

:: deftheorem Def11 defines CnPos HILBERT1:def 11 :

for X, b_{2} being Subset of HP-WFF holds

( b_{2} = CnPos X iff for r being Element of HP-WFF holds

( r in b_{2} iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds

r in T ) );

for X, b

( b

( r in b

r in T ) );

theorem Th2: :: HILBERT1:2

for X being Subset of HP-WFF

for p, q being Element of HP-WFF holds p => (q => (p '&' q)) in CnPos X

for p, q being Element of HP-WFF holds p => (q => (p '&' q)) in CnPos X

proof end;

theorem Th3: :: HILBERT1:3

for X being Subset of HP-WFF

for p, q, r being Element of HP-WFF holds (p => (q => r)) => ((p => q) => (p => r)) in CnPos X

for p, q, r being Element of HP-WFF holds (p => (q => r)) => ((p => q) => (p => r)) in CnPos X

proof end;

theorem Th7: :: HILBERT1:7

for X being Subset of HP-WFF

for p, q being Element of HP-WFF st p in CnPos X & p => q in CnPos X holds

q in CnPos X

for p, q being Element of HP-WFF st p in CnPos X & p => q in CnPos X holds

q in CnPos X

proof end;

Lm2: for X being Subset of HP-WFF holds CnPos (CnPos X) c= CnPos X

proof end;

Lm3: for X being Subset of HP-WFF holds CnPos X is Hilbert_theory

proof end;

begin

theorem :: HILBERT1:17

theorem :: HILBERT1:18

theorem Th23: :: HILBERT1:23

for p, q, r being Element of HP-WFF st p => q in HP_TAUT & q => r in HP_TAUT holds

p => r in HP_TAUT

p => r in HP_TAUT

proof end;

Lm4: for q, r, p, s being Element of HP-WFF holds (((q => r) => (p => r)) => s) => ((p => q) => s) in HP_TAUT

proof end;

theorem Th24: :: HILBERT1:24

for p, q, r, s being Element of HP-WFF holds (p => (q => r)) => ((s => q) => (p => (s => r))) in HP_TAUT

proof end;

theorem Th29: :: HILBERT1:29

for s, q, p being Element of HP-WFF st s => (q => p) in HP_TAUT & q in HP_TAUT holds

s => p in HP_TAUT

s => p in HP_TAUT

proof end;

begin

Lm5: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => q in HP_TAUT

proof end;

Lm6: for p, q, s being Element of HP-WFF holds (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in HP_TAUT

proof end;

Lm7: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT

proof end;

Lm8: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' s) in HP_TAUT

proof end;

Lm9: for p, q, s being Element of HP-WFF holds (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT

proof end;

Lm10: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((p '&' s) '&' q) in HP_TAUT

proof end;

Lm11: for p, s, q being Element of HP-WFF holds ((p '&' s) '&' q) => ((s '&' p) '&' q) in HP_TAUT

proof end;

Lm12: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((s '&' p) '&' q) in HP_TAUT

proof end;

Lm13: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((s '&' q) '&' p) in HP_TAUT

proof end;

Lm14: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' (s '&' q)) in HP_TAUT

proof end;

Lm15: for p, s, q being Element of HP-WFF holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT

proof end;

Lm16: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT

proof end;

Lm17: for s, q, p being Element of HP-WFF holds ((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT

proof end;

Lm18: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT

proof end;

Lm19: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((p '&' s) '&' q) in HP_TAUT

proof end;

Lm20: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT

proof end;