:: HILBERT1 semantic presentation
begin
definition
let D be set ;
attrD is with_VERUM means :Def1: :: HILBERT1:def 1
<*0*> in D;
end;
:: deftheorem Def1 defines with_VERUM HILBERT1:def_1_:_
for D being set holds
( D is with_VERUM iff <*0*> in D );
definition
let D be set ;
attrD 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;
end;
:: 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 );
definition
let D be set ;
attrD 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;
end;
:: 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 );
definition
let D be set ;
attrD is with_propositional_variables means :Def4: :: HILBERT1:def 4
for n being Element of NAT holds <*(3 + n)*> in D;
end;
:: 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 );
definition
let D be set ;
attrD 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 );
end;
:: 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
proof
let D be set ; ::_thesis: ( D is HP-closed implies not D is empty )
assume D is HP-closed ; ::_thesis: not D is empty
then D is with_VERUM by Def5;
hence not D is empty by Def1; ::_thesis: verum
end;
registration
cluster HP-closed -> non empty with_VERUM with_implication with_conjunction with_propositional_variables for 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, Lm1;
cluster with_VERUM with_implication with_conjunction with_propositional_variables -> HP-closed for Element of K6((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
( it is HP-closed & ( for D being set st D is HP-closed holds
it c= D ) );
existence
ex b1 being set st
( b1 is HP-closed & ( for D being set st D is HP-closed holds
b1 c= D ) )
proof
A1: <*0*> in NAT * by FINSEQ_1:def_11;
defpred S1[ set ] means for D being set st D is HP-closed holds
$1 in D;
consider D0 being set such that
A2: for x being set holds
( x in D0 iff ( x in NAT * & S1[x] ) ) from XBOOLE_0:sch_1();
A3: for D being set st D is HP-closed holds
<*0*> in D by Def1;
then reconsider D0 = D0 as non empty set by A2, A1;
take D0 ; ::_thesis: ( D0 is HP-closed & ( for D being set st D is HP-closed holds
D0 c= D ) )
A4: D0 c= NAT *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D0 or x in NAT * )
thus ( not x in D0 or x in NAT * ) by A2; ::_thesis: verum
end;
for p, q being FinSequence st p in D0 & q in D0 holds
(<*2*> ^ p) ^ q in D0
proof
let p, q be FinSequence; ::_thesis: ( p in D0 & q in D0 implies (<*2*> ^ p) ^ q in D0 )
assume that
A5: p in D0 and
A6: q in D0 ; ::_thesis: (<*2*> ^ p) ^ q in D0
A7: q in NAT * by A2, A6;
A8: for D being set st D is HP-closed holds
(<*2*> ^ p) ^ q in D
proof
let D be set ; ::_thesis: ( D is HP-closed implies (<*2*> ^ p) ^ q in D )
assume A9: D is HP-closed ; ::_thesis: (<*2*> ^ p) ^ q in D
then A10: q in D by A2, A6;
p in D by A2, A5, A9;
hence (<*2*> ^ p) ^ q in D by A9, A10, Def3; ::_thesis: verum
end;
p in NAT * by A2, A5;
then reconsider p9 = p, q9 = q as FinSequence of NAT by A7, FINSEQ_1:def_11;
(<*2*> ^ p9) ^ q9 in NAT * by FINSEQ_1:def_11;
hence (<*2*> ^ p) ^ q in D0 by A2, A8; ::_thesis: verum
end;
then A11: D0 is with_conjunction by Def3;
for p, q being FinSequence st p in D0 & q in D0 holds
(<*1*> ^ p) ^ q in D0
proof
let p, q be FinSequence; ::_thesis: ( p in D0 & q in D0 implies (<*1*> ^ p) ^ q in D0 )
assume that
A12: p in D0 and
A13: q in D0 ; ::_thesis: (<*1*> ^ p) ^ q in D0
A14: q in NAT * by A2, A13;
A15: for D being set st D is HP-closed holds
(<*1*> ^ p) ^ q in D
proof
let D be set ; ::_thesis: ( D is HP-closed implies (<*1*> ^ p) ^ q in D )
assume A16: D is HP-closed ; ::_thesis: (<*1*> ^ p) ^ q in D
then A17: q in D by A2, A13;
p in D by A2, A12, A16;
hence (<*1*> ^ p) ^ q in D by A16, A17, Def2; ::_thesis: verum
end;
p in NAT * by A2, A12;
then reconsider p9 = p, q9 = q as FinSequence of NAT by A14, FINSEQ_1:def_11;
(<*1*> ^ p9) ^ q9 in NAT * by FINSEQ_1:def_11;
hence (<*1*> ^ p) ^ q in D0 by A2, A15; ::_thesis: verum
end;
then A18: D0 is with_implication by Def2;
for n being Element of NAT holds <*(3 + n)*> in D0
proof
let n be Element of NAT ; ::_thesis: <*(3 + n)*> in D0
set p = 3 + n;
reconsider h = <*(3 + n)*> as FinSequence of NAT ;
A19: h in NAT * by FINSEQ_1:def_11;
for D being set st D is HP-closed holds
<*(3 + n)*> in D by Def4;
hence <*(3 + n)*> in D0 by A2, A19; ::_thesis: verum
end;
then A20: D0 is with_propositional_variables by Def4;
<*0*> in D0 by A2, A1, A3;
then D0 is with_VERUM by Def1;
hence D0 is HP-closed by A4, A20, A18, A11; ::_thesis: for D being set st D is HP-closed holds
D0 c= D
let D be set ; ::_thesis: ( D is HP-closed implies D0 c= D )
assume A21: D is HP-closed ; ::_thesis: D0 c= D
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D0 or x in D )
assume x in D0 ; ::_thesis: x in D
hence x in D by A2, A21; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st b1 is HP-closed & ( for D being set st D is HP-closed holds
b1 c= D ) & b2 is HP-closed & ( for D being set st D is HP-closed holds
b2 c= D ) holds
b1 = b2
proof
let D1, D2 be set ; ::_thesis: ( D1 is HP-closed & ( for D being set st D is HP-closed holds
D1 c= D ) & D2 is HP-closed & ( for D being set st D is HP-closed holds
D2 c= D ) implies D1 = D2 )
assume that
A22: D1 is HP-closed and
A23: for D being set st D is HP-closed holds
D1 c= D and
A24: D2 is HP-closed and
A25: for D being set st D is HP-closed holds
D2 c= D ; ::_thesis: D1 = D2
A26: D2 c= D1 by A22, A25;
D1 c= D2 by A23, A24;
hence D1 = D2 by A26, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: 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 ) ) );
registration
cluster HP-WFF -> HP-closed ;
coherence
HP-WFF is HP-closed by Def6;
end;
registration
cluster non empty HP-closed for set ;
existence
ex b1 being set st
( b1 is HP-closed & not b1 is empty )
proof
take HP-WFF ; ::_thesis: ( HP-WFF is HP-closed & not HP-WFF is empty )
thus ( HP-WFF is HP-closed & not HP-WFF is empty ) ; ::_thesis: verum
end;
end;
registration
cluster HP-WFF -> functional ;
coherence
HP-WFF is functional
proof
HP-WFF c= NAT * by Def5;
hence HP-WFF is functional ; ::_thesis: verum
end;
end;
registration
cluster -> FinSequence-like for Element of HP-WFF ;
coherence
for b1 being Element of HP-WFF holds b1 is FinSequence-like
proof
let p be Element of HP-WFF ; ::_thesis: p is FinSequence-like
HP-WFF c= NAT * by Def5;
hence p is FinSequence-like ; ::_thesis: verum
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 p, q be Element of HP-WFF ;
funcp => q -> HP-formula equals :: HILBERT1:def 8
(<*1*> ^ p) ^ q;
coherence
(<*1*> ^ p) ^ q is HP-formula by Def2;
funcp '&' q -> HP-formula equals :: HILBERT1:def 9
(<*2*> ^ p) ^ q;
correctness
coherence
(<*2*> ^ p) ^ q is HP-formula;
by Def3;
end;
:: 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;
definition
let T be Subset of HP-WFF;
attrT 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
;
end;
:: 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 ) ) ) ) );
definition
let X be Subset of HP-WFF;
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
ex b1 being Subset of HP-WFF st
for r being Element of HP-WFF holds
( r in b1 iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T )
proof
defpred S1[ set ] means for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
$1 in T;
consider Y being set such that
A1: for a being set holds
( a in Y iff ( a in HP-WFF & S1[a] ) ) from XBOOLE_0:sch_1();
Y c= HP-WFF
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in HP-WFF )
assume a in Y ; ::_thesis: a in HP-WFF
hence a in HP-WFF by A1; ::_thesis: verum
end;
then reconsider Z = Y as Subset of HP-WFF ;
take Z ; ::_thesis: for r being Element of HP-WFF holds
( r in Z iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T )
thus for r being Element of HP-WFF holds
( r in Z iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of HP-WFF st ( for r being Element of HP-WFF holds
( r in b1 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 b2 iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) ) holds
b1 = b2
proof
let Y, Z be Subset of HP-WFF; ::_thesis: ( ( for r being Element of HP-WFF holds
( r in Y 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 Z iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) ) implies Y = Z )
assume that
A2: for r being Element of HP-WFF holds
( r in Y iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) and
A3: for r being Element of HP-WFF holds
( r in Z iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) ; ::_thesis: Y = Z
for a being set holds
( a in Y iff a in Z )
proof
let a be set ; ::_thesis: ( a in Y iff a in Z )
hereby ::_thesis: ( a in Z implies a in Y )
assume A4: a in Y ; ::_thesis: a in Z
then reconsider t = a as Element of HP-WFF ;
for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
t in T by A2, A4;
hence a in Z by A3; ::_thesis: verum
end;
assume A5: a in Z ; ::_thesis: a in Y
then reconsider t = a as Element of HP-WFF ;
for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
t in T by A3, A5;
hence a in Y by A2; ::_thesis: verum
end;
hence Y = Z by TARSKI:1; ::_thesis: verum
end;
end;
:: 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 ) );
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 defines HP_TAUT HILBERT1:def_12_:_
HP_TAUT = CnPos ({} HP-WFF);
theorem Th1: :: HILBERT1:1
for X being Subset of HP-WFF holds VERUM in CnPos X
proof
let X be Subset of HP-WFF; ::_thesis: VERUM in CnPos X
for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
VERUM in T by Def10;
hence VERUM in CnPos X by Def11; ::_thesis: verum
end;
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
proof
let X be Subset of HP-WFF; ::_thesis: for p, q being Element of HP-WFF holds p => (q => (p '&' q)) in CnPos X
let p, q be Element of HP-WFF ; ::_thesis: p => (q => (p '&' q)) in CnPos X
for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
p => (q => (p '&' q)) in T by Def10;
hence p => (q => (p '&' q)) in CnPos X by Def11; ::_thesis: verum
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
proof
let X be Subset of HP-WFF; ::_thesis: for p, q, r being Element of HP-WFF holds (p => (q => r)) => ((p => q) => (p => r)) in CnPos X
let p, q, r be Element of HP-WFF ; ::_thesis: (p => (q => r)) => ((p => q) => (p => r)) in CnPos X
for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
(p => (q => r)) => ((p => q) => (p => r)) in T by Def10;
hence (p => (q => r)) => ((p => q) => (p => r)) in CnPos X by Def11; ::_thesis: verum
end;
theorem Th4: :: HILBERT1:4
for X being Subset of HP-WFF
for p, q being Element of HP-WFF holds p => (q => p) in CnPos X
proof
let X be Subset of HP-WFF; ::_thesis: for p, q being Element of HP-WFF holds p => (q => p) in CnPos X
let p, q be Element of HP-WFF ; ::_thesis: p => (q => p) in CnPos X
for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
p => (q => p) in T by Def10;
hence p => (q => p) in CnPos X by Def11; ::_thesis: verum
end;
theorem Th5: :: HILBERT1:5
for X being Subset of HP-WFF
for p, q being Element of HP-WFF holds (p '&' q) => p in CnPos X
proof
let X be Subset of HP-WFF; ::_thesis: for p, q being Element of HP-WFF holds (p '&' q) => p in CnPos X
let p, q be Element of HP-WFF ; ::_thesis: (p '&' q) => p in CnPos X
for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
(p '&' q) => p in T by Def10;
hence (p '&' q) => p in CnPos X by Def11; ::_thesis: verum
end;
theorem Th6: :: HILBERT1:6
for X being Subset of HP-WFF
for p, q being Element of HP-WFF holds (p '&' q) => q in CnPos X
proof
let X be Subset of HP-WFF; ::_thesis: for p, q being Element of HP-WFF holds (p '&' q) => q in CnPos X
let p, q be Element of HP-WFF ; ::_thesis: (p '&' q) => q in CnPos X
for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
(p '&' q) => q in T by Def10;
hence (p '&' q) => q in CnPos X by Def11; ::_thesis: verum
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
proof
let X be Subset of HP-WFF; ::_thesis: for p, q being Element of HP-WFF st p in CnPos X & p => q in CnPos X holds
q in CnPos X
let p, q be Element of HP-WFF ; ::_thesis: ( p in CnPos X & p => q in CnPos X implies q in CnPos X )
assume that
A1: p in CnPos X and
A2: p => q in CnPos X ; ::_thesis: q in CnPos X
for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
q in T
proof
let T be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory & X c= T implies q in T )
assume that
A3: T is Hilbert_theory and
A4: X c= T ; ::_thesis: q in T
A5: p => q in T by A2, A3, A4, Def11;
p in T by A1, A3, A4, Def11;
hence q in T by A3, A5, Def10; ::_thesis: verum
end;
hence q in CnPos X by Def11; ::_thesis: verum
end;
theorem Th8: :: HILBERT1:8
for T, X being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
CnPos X c= T
proof
let T, X be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory & X c= T implies CnPos X c= T )
assume that
A1: T is Hilbert_theory and
A2: X c= T ; ::_thesis: CnPos X c= T
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnPos X or a in T )
thus ( not a in CnPos X or a in T ) by A1, A2, Def11; ::_thesis: verum
end;
theorem Th9: :: HILBERT1:9
for X being Subset of HP-WFF holds X c= CnPos X
proof
let X be Subset of HP-WFF; ::_thesis: X c= CnPos X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in CnPos X )
assume A1: a in X ; ::_thesis: a in CnPos X
then reconsider t = a as Element of HP-WFF ;
for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
t in T by A1;
hence a in CnPos X by Def11; ::_thesis: verum
end;
theorem Th10: :: HILBERT1:10
for X, Y being Subset of HP-WFF st X c= Y holds
CnPos X c= CnPos Y
proof
let X, Y be Subset of HP-WFF; ::_thesis: ( X c= Y implies CnPos X c= CnPos Y )
assume A1: X c= Y ; ::_thesis: CnPos X c= CnPos Y
thus CnPos X c= CnPos Y ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnPos X or a in CnPos Y )
assume A2: a in CnPos X ; ::_thesis: a in CnPos Y
then reconsider t = a as Element of HP-WFF ;
for T being Subset of HP-WFF st T is Hilbert_theory & Y c= T holds
t in T
proof
let T be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory & Y c= T implies t in T )
assume that
A3: T is Hilbert_theory and
A4: Y c= T ; ::_thesis: t in T
X c= T by A1, A4, XBOOLE_1:1;
hence t in T by A2, A3, Def11; ::_thesis: verum
end;
hence a in CnPos Y by Def11; ::_thesis: verum
end;
end;
Lm2: for X being Subset of HP-WFF holds CnPos (CnPos X) c= CnPos X
proof
let X be Subset of HP-WFF; ::_thesis: CnPos (CnPos X) c= CnPos X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnPos (CnPos X) or a in CnPos X )
assume A1: a in CnPos (CnPos X) ; ::_thesis: a in CnPos X
then reconsider t = a as Element of HP-WFF ;
for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
t in T
proof
let T be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory & X c= T implies t in T )
assume that
A2: T is Hilbert_theory and
A3: X c= T ; ::_thesis: t in T
CnPos X c= T by A2, A3, Th8;
hence t in T by A1, A2, Def11; ::_thesis: verum
end;
hence a in CnPos X by Def11; ::_thesis: verum
end;
theorem :: HILBERT1:11
for X being Subset of HP-WFF holds CnPos (CnPos X) = CnPos X
proof
let X be Subset of HP-WFF; ::_thesis: CnPos (CnPos X) = CnPos X
A1: CnPos X c= CnPos (CnPos X) by Th9;
CnPos (CnPos X) c= CnPos X by Lm2;
hence CnPos (CnPos X) = CnPos X by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm3: for X being Subset of HP-WFF holds CnPos X is Hilbert_theory
proof
let X be Subset of HP-WFF; ::_thesis: CnPos X is Hilbert_theory
thus VERUM in CnPos X by Th1; :: according to HILBERT1:def_10 ::_thesis: for p, q, r being Element of HP-WFF holds
( p => (q => p) in CnPos X & (p => (q => r)) => ((p => q) => (p => r)) in CnPos X & (p '&' q) => p in CnPos X & (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
let p, q, r be Element of HP-WFF ; ::_thesis: ( p => (q => p) in CnPos X & (p => (q => r)) => ((p => q) => (p => r)) in CnPos X & (p '&' q) => p in CnPos X & (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
thus p => (q => p) in CnPos X by Th4; ::_thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in CnPos X & (p '&' q) => p in CnPos X & (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
thus (p => (q => r)) => ((p => q) => (p => r)) in CnPos X by Th3; ::_thesis: ( (p '&' q) => p in CnPos X & (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
thus (p '&' q) => p in CnPos X by Th5; ::_thesis: ( (p '&' q) => q in CnPos X & p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
thus (p '&' q) => q in CnPos X by Th6; ::_thesis: ( p => (q => (p '&' q)) in CnPos X & ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) )
thus p => (q => (p '&' q)) in CnPos X by Th2; ::_thesis: ( p in CnPos X & p => q in CnPos X implies q in CnPos X )
thus ( p in CnPos X & p => q in CnPos X implies q in CnPos X ) by Th7; ::_thesis: verum
end;
registration
let X be Subset of HP-WFF;
cluster CnPos X -> Hilbert_theory ;
coherence
CnPos X is Hilbert_theory by Lm3;
end;
theorem Th12: :: HILBERT1:12
for T being Subset of HP-WFF holds
( T is Hilbert_theory iff CnPos T = T )
proof
let T be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory iff CnPos T = T )
hereby ::_thesis: ( CnPos T = T implies T is Hilbert_theory )
assume A1: T is Hilbert_theory ; ::_thesis: CnPos T = T
A2: CnPos T c= T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnPos T or a in T )
assume a in CnPos T ; ::_thesis: a in T
hence a in T by A1, Def11; ::_thesis: verum
end;
T c= CnPos T by Th9;
hence CnPos T = T by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
thus ( CnPos T = T implies T is Hilbert_theory ) ; ::_thesis: verum
end;
theorem :: HILBERT1:13
for T being Subset of HP-WFF st T is Hilbert_theory holds
HP_TAUT c= T
proof
let T be Subset of HP-WFF; ::_thesis: ( T is Hilbert_theory implies HP_TAUT c= T )
assume A1: T is Hilbert_theory ; ::_thesis: HP_TAUT c= T
HP_TAUT c= CnPos T by Th10, XBOOLE_1:2;
hence HP_TAUT c= T by A1, Th12; ::_thesis: verum
end;
registration
cluster HP_TAUT -> Hilbert_theory ;
coherence
HP_TAUT is Hilbert_theory ;
end;
begin
theorem Th14: :: HILBERT1:14
for p being Element of HP-WFF holds p => p in HP_TAUT
proof
let p be Element of HP-WFF ; ::_thesis: p => p in HP_TAUT
A1: p => (p => p) in HP_TAUT by Def10;
A2: p => ((p => p) => p) in HP_TAUT by Def10;
(p => ((p => p) => p)) => ((p => (p => p)) => (p => p)) in HP_TAUT by Def10;
then (p => (p => p)) => (p => p) in HP_TAUT by A2, Def10;
hence p => p in HP_TAUT by A1, Def10; ::_thesis: verum
end;
theorem Th15: :: HILBERT1:15
for q, p being Element of HP-WFF st q in HP_TAUT holds
p => q in HP_TAUT
proof
let q, p be Element of HP-WFF ; ::_thesis: ( q in HP_TAUT implies p => q in HP_TAUT )
q => (p => q) in HP_TAUT by Def10;
hence ( q in HP_TAUT implies p => q in HP_TAUT ) by Def10; ::_thesis: verum
end;
theorem :: HILBERT1:16
for p being Element of HP-WFF holds p => VERUM in HP_TAUT by Th1, Th15;
theorem :: HILBERT1:17
for p, q being Element of HP-WFF holds (p => q) => (p => p) in HP_TAUT by Th14, Th15;
theorem :: HILBERT1:18
for q, p being Element of HP-WFF holds (q => p) => (p => p) in HP_TAUT by Th14, Th15;
theorem Th19: :: HILBERT1:19
for q, r, p being Element of HP-WFF holds (q => r) => ((p => q) => (p => r)) in HP_TAUT
proof
let q, r, p be Element of HP-WFF ; ::_thesis: (q => r) => ((p => q) => (p => r)) in HP_TAUT
A1: (p => (q => r)) => ((p => q) => (p => r)) in HP_TAUT by Def10;
A2: ((q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) => (((q => r) => (p => (q => r))) => ((q => r) => ((p => q) => (p => r)))) in HP_TAUT by Def10;
((p => (q => r)) => ((p => q) => (p => r))) => ((q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) in HP_TAUT by Def10;
then (q => r) => ((p => (q => r)) => ((p => q) => (p => r))) in HP_TAUT by A1, Def10;
then A3: ((q => r) => (p => (q => r))) => ((q => r) => ((p => q) => (p => r))) in HP_TAUT by A2, Def10;
(q => r) => (p => (q => r)) in HP_TAUT by Def10;
hence (q => r) => ((p => q) => (p => r)) in HP_TAUT by A3, Def10; ::_thesis: verum
end;
theorem Th20: :: HILBERT1:20
for p, q, r being Element of HP-WFF st p => (q => r) in HP_TAUT holds
q => (p => r) in HP_TAUT
proof
let p, q, r be Element of HP-WFF ; ::_thesis: ( p => (q => r) in HP_TAUT implies q => (p => r) in HP_TAUT )
assume A1: p => (q => r) in HP_TAUT ; ::_thesis: q => (p => r) in HP_TAUT
A2: ((p => q) => (p => r)) => ((q => (p => q)) => (q => (p => r))) in HP_TAUT by Th19;
(p => (q => r)) => ((p => q) => (p => r)) in HP_TAUT by Def10;
then (p => q) => (p => r) in HP_TAUT by A1, Def10;
then A3: (q => (p => q)) => (q => (p => r)) in HP_TAUT by A2, Def10;
q => (p => q) in HP_TAUT by Def10;
hence q => (p => r) in HP_TAUT by A3, Def10; ::_thesis: verum
end;
theorem Th21: :: HILBERT1:21
for p, q, r being Element of HP-WFF holds (p => q) => ((q => r) => (p => r)) in HP_TAUT
proof
let p, q, r be Element of HP-WFF ; ::_thesis: (p => q) => ((q => r) => (p => r)) in HP_TAUT
(q => r) => ((p => q) => (p => r)) in HP_TAUT by Th19;
hence (p => q) => ((q => r) => (p => r)) in HP_TAUT by Th20; ::_thesis: verum
end;
theorem Th22: :: HILBERT1:22
for p, q, r being Element of HP-WFF st p => q in HP_TAUT holds
(q => r) => (p => r) in HP_TAUT
proof
let p, q, r be Element of HP-WFF ; ::_thesis: ( p => q in HP_TAUT implies (q => r) => (p => r) in HP_TAUT )
assume A1: p => q in HP_TAUT ; ::_thesis: (q => r) => (p => r) in HP_TAUT
(p => q) => ((q => r) => (p => r)) in HP_TAUT by Th21;
hence (q => r) => (p => r) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
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
proof
let p, q, r be Element of HP-WFF ; ::_thesis: ( p => q in HP_TAUT & q => r in HP_TAUT implies p => r in HP_TAUT )
assume that
A1: p => q in HP_TAUT and
A2: q => r in HP_TAUT ; ::_thesis: p => r in HP_TAUT
(p => q) => ((q => r) => (p => r)) in HP_TAUT by Th21;
then (q => r) => (p => r) in HP_TAUT by A1, Def10;
hence p => r in HP_TAUT by A2, Def10; ::_thesis: verum
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
let q, r, p, s be Element of HP-WFF ; ::_thesis: (((q => r) => (p => r)) => s) => ((p => q) => s) in HP_TAUT
(p => q) => ((q => r) => (p => r)) in HP_TAUT by Th21;
hence (((q => r) => (p => r)) => s) => ((p => q) => s) in HP_TAUT by Th22; ::_thesis: verum
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
let p, q, r, s be Element of HP-WFF ; ::_thesis: (p => (q => r)) => ((s => q) => (p => (s => r))) in HP_TAUT
A1: (((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r))) in HP_TAUT by Lm4;
((((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r)))) => ((p => (q => r)) => ((s => q) => (p => (s => r)))) in HP_TAUT by Lm4;
hence (p => (q => r)) => ((s => q) => (p => (s => r))) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
theorem :: HILBERT1:25
for p, q, r being Element of HP-WFF holds ((p => q) => r) => (q => r) in HP_TAUT
proof
let p, q, r be Element of HP-WFF ; ::_thesis: ((p => q) => r) => (q => r) in HP_TAUT
A1: (q => (p => q)) => (((p => q) => r) => (q => r)) in HP_TAUT by Th21;
q => (p => q) in HP_TAUT by Def10;
hence ((p => q) => r) => (q => r) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
theorem Th26: :: HILBERT1:26
for p, q, r being Element of HP-WFF holds (p => (q => r)) => (q => (p => r)) in HP_TAUT
proof
let p, q, r be Element of HP-WFF ; ::_thesis: (p => (q => r)) => (q => (p => r)) in HP_TAUT
A1: q => (p => q) in HP_TAUT by Def10;
(p => (q => r)) => ((p => q) => (p => r)) in HP_TAUT by Def10;
then A2: (p => q) => ((p => (q => r)) => (p => r)) in HP_TAUT by Th20;
((p => q) => ((p => (q => r)) => (p => r))) => ((q => (p => q)) => (q => ((p => (q => r)) => (p => r)))) in HP_TAUT by Th19;
then (q => (p => q)) => (q => ((p => (q => r)) => (p => r))) in HP_TAUT by A2, Def10;
then q => ((p => (q => r)) => (p => r)) in HP_TAUT by A1, Def10;
hence (p => (q => r)) => (q => (p => r)) in HP_TAUT by Th20; ::_thesis: verum
end;
theorem Th27: :: HILBERT1:27
for p, q being Element of HP-WFF holds (p => (p => q)) => (p => q) in HP_TAUT
proof
let p, q be Element of HP-WFF ; ::_thesis: (p => (p => q)) => (p => q) in HP_TAUT
(p => (p => q)) => ((p => p) => (p => q)) in HP_TAUT by Def10;
then A1: (p => p) => ((p => (p => q)) => (p => q)) in HP_TAUT by Th20;
p => p in HP_TAUT by Th14;
hence (p => (p => q)) => (p => q) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
theorem :: HILBERT1:28
for q, p being Element of HP-WFF holds q => ((q => p) => p) in HP_TAUT
proof
let q, p be Element of HP-WFF ; ::_thesis: q => ((q => p) => p) in HP_TAUT
A1: ((q => p) => (q => p)) => (q => ((q => p) => p)) in HP_TAUT by Th26;
(q => p) => (q => p) in HP_TAUT by Th14;
hence q => ((q => p) => p) in HP_TAUT by A1, Def10; ::_thesis: verum
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
proof
let s, q, p be Element of HP-WFF ; ::_thesis: ( s => (q => p) in HP_TAUT & q in HP_TAUT implies s => p in HP_TAUT )
assume that
A1: s => (q => p) in HP_TAUT and
A2: q in HP_TAUT ; ::_thesis: s => p in HP_TAUT
(s => (q => p)) => (q => (s => p)) in HP_TAUT by Th26;
then q => (s => p) in HP_TAUT by A1, Def10;
hence s => p in HP_TAUT by A2, Def10; ::_thesis: verum
end;
begin
theorem Th30: :: HILBERT1:30
for p being Element of HP-WFF holds p => (p '&' p) in HP_TAUT
proof
let p be Element of HP-WFF ; ::_thesis: p => (p '&' p) in HP_TAUT
A1: (p => (p => (p '&' p))) => (p => (p '&' p)) in HP_TAUT by Th27;
p => (p => (p '&' p)) in HP_TAUT by Def10;
hence p => (p '&' p) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
theorem Th31: :: HILBERT1:31
for p, q being Element of HP-WFF holds
( p '&' q in HP_TAUT iff ( p in HP_TAUT & q in HP_TAUT ) )
proof
let p, q be Element of HP-WFF ; ::_thesis: ( p '&' q in HP_TAUT iff ( p in HP_TAUT & q in HP_TAUT ) )
hereby ::_thesis: ( p in HP_TAUT & q in HP_TAUT implies p '&' q in HP_TAUT )
A1: (p '&' q) => q in HP_TAUT by Def10;
assume A2: p '&' q in HP_TAUT ; ::_thesis: ( p in HP_TAUT & q in HP_TAUT )
(p '&' q) => p in HP_TAUT by Def10;
hence ( p in HP_TAUT & q in HP_TAUT ) by A2, A1, Def10; ::_thesis: verum
end;
assume that
A3: p in HP_TAUT and
A4: q in HP_TAUT ; ::_thesis: p '&' q in HP_TAUT
p => (q => (p '&' q)) in HP_TAUT by Def10;
then q => (p '&' q) in HP_TAUT by A3, Def10;
hence p '&' q in HP_TAUT by A4, Def10; ::_thesis: verum
end;
theorem :: HILBERT1:32
for p, q being Element of HP-WFF st p '&' q in HP_TAUT holds
q '&' p in HP_TAUT
proof
let p, q be Element of HP-WFF ; ::_thesis: ( p '&' q in HP_TAUT implies q '&' p in HP_TAUT )
assume A1: p '&' q in HP_TAUT ; ::_thesis: q '&' p in HP_TAUT
then A2: q in HP_TAUT by Th31;
p in HP_TAUT by A1, Th31;
hence q '&' p in HP_TAUT by A2, Th31; ::_thesis: verum
end;
theorem Th33: :: HILBERT1:33
for p, q, r being Element of HP-WFF holds ((p '&' q) => r) => (p => (q => r)) in HP_TAUT
proof
let p, q, r be Element of HP-WFF ; ::_thesis: ((p '&' q) => r) => (p => (q => r)) in HP_TAUT
set qp = q => (p '&' q);
set pr = ((p '&' q) => r) => (q => r);
A1: (p => ((q => (p '&' q)) => (((p '&' q) => r) => (q => r)))) => ((p => (q => (p '&' q))) => (p => (((p '&' q) => r) => (q => r)))) in HP_TAUT by Def10;
A2: p => (q => (p '&' q)) in HP_TAUT by Def10;
p => ((q => (p '&' q)) => (((p '&' q) => r) => (q => r))) in HP_TAUT by Th15, Th21;
then (p => (q => (p '&' q))) => (p => (((p '&' q) => r) => (q => r))) in HP_TAUT by A1, Def10;
then A3: p => (((p '&' q) => r) => (q => r)) in HP_TAUT by A2, Def10;
(p => (((p '&' q) => r) => (q => r))) => (((p '&' q) => r) => (p => (q => r))) in HP_TAUT by Th26;
hence ((p '&' q) => r) => (p => (q => r)) in HP_TAUT by A3, Def10; ::_thesis: verum
end;
theorem Th34: :: HILBERT1:34
for p, q, r being Element of HP-WFF holds (p => (q => r)) => ((p '&' q) => r) in HP_TAUT
proof
let p, q, r be Element of HP-WFF ; ::_thesis: (p => (q => r)) => ((p '&' q) => r) in HP_TAUT
A1: ((p '&' q) => q) => ((q => r) => ((p '&' q) => r)) in HP_TAUT by Th21;
(p '&' q) => q in HP_TAUT by Def10;
then (q => r) => ((p '&' q) => r) in HP_TAUT by A1, Def10;
then A2: p => ((q => r) => ((p '&' q) => r)) in HP_TAUT by Th15;
A3: (p => ((p '&' q) => r)) => ((p '&' q) => (p => r)) in HP_TAUT by Th26;
(p => ((q => r) => ((p '&' q) => r))) => ((p => (q => r)) => (p => ((p '&' q) => r))) in HP_TAUT by Def10;
then (p => (q => r)) => (p => ((p '&' q) => r)) in HP_TAUT by A2, Def10;
then A4: (p => (q => r)) => ((p '&' q) => (p => r)) in HP_TAUT by A3, Th23;
A5: (p '&' q) => p in HP_TAUT by Def10;
((p '&' q) => (p => r)) => (((p '&' q) => p) => ((p '&' q) => r)) in HP_TAUT by Def10;
then ((p '&' q) => (p => r)) => ((p '&' q) => r) in HP_TAUT by A5, Th29;
hence (p => (q => r)) => ((p '&' q) => r) in HP_TAUT by A4, Th23; ::_thesis: verum
end;
theorem Th35: :: HILBERT1:35
for r, p, q being Element of HP-WFF holds (r => p) => ((r => q) => (r => (p '&' q))) in HP_TAUT
proof
let r, p, q be Element of HP-WFF ; ::_thesis: (r => p) => ((r => q) => (r => (p '&' q))) in HP_TAUT
A1: (r => (q => (p '&' q))) => ((r => q) => (r => (p '&' q))) in HP_TAUT by Def10;
p => (q => (p '&' q)) in HP_TAUT by Def10;
then A2: r => (p => (q => (p '&' q))) in HP_TAUT by Th15;
(r => (p => (q => (p '&' q)))) => ((r => p) => (r => (q => (p '&' q)))) in HP_TAUT by Def10;
then (r => p) => (r => (q => (p '&' q))) in HP_TAUT by A2, Def10;
hence (r => p) => ((r => q) => (r => (p '&' q))) in HP_TAUT by A1, Th23; ::_thesis: verum
end;
theorem Th36: :: HILBERT1:36
for p, q being Element of HP-WFF holds ((p => q) '&' p) => q in HP_TAUT
proof
let p, q be Element of HP-WFF ; ::_thesis: ((p => q) '&' p) => q in HP_TAUT
set P = p => q;
A1: (p => q) => (p => q) in HP_TAUT by Th14;
((p => q) => (p => q)) => (((p => q) '&' p) => q) in HP_TAUT by Th34;
hence ((p => q) '&' p) => q in HP_TAUT by A1, Def10; ::_thesis: verum
end;
theorem :: HILBERT1:37
for p, q, s being Element of HP-WFF holds (((p => q) '&' p) '&' s) => q in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (((p => q) '&' p) '&' s) => q in HP_TAUT
set P = (p => q) '&' p;
A1: ((p => q) '&' p) => q in HP_TAUT by Th36;
(((p => q) '&' p) '&' s) => ((p => q) '&' p) in HP_TAUT by Def10;
hence (((p => q) '&' p) '&' s) => q in HP_TAUT by A1, Th23; ::_thesis: verum
end;
theorem :: HILBERT1:38
for q, s, p being Element of HP-WFF holds (q => s) => ((p '&' q) => s) in HP_TAUT
proof
let q, s, p be Element of HP-WFF ; ::_thesis: (q => s) => ((p '&' q) => s) in HP_TAUT
set P = p '&' q;
A1: (p '&' q) => q in HP_TAUT by Def10;
((p '&' q) => q) => ((q => s) => ((p '&' q) => s)) in HP_TAUT by Th21;
hence (q => s) => ((p '&' q) => s) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
theorem Th39: :: HILBERT1:39
for q, s, p being Element of HP-WFF holds (q => s) => ((q '&' p) => s) in HP_TAUT
proof
let q, s, p be Element of HP-WFF ; ::_thesis: (q => s) => ((q '&' p) => s) in HP_TAUT
set P = q '&' p;
A1: (q '&' p) => q in HP_TAUT by Def10;
((q '&' p) => q) => ((q => s) => ((q '&' p) => s)) in HP_TAUT by Th21;
hence (q => s) => ((q '&' p) => s) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
theorem Th40: :: HILBERT1:40
for p, s, q being Element of HP-WFF holds ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in HP_TAUT
proof
let p, s, q be Element of HP-WFF ; ::_thesis: ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in HP_TAUT
set P = p '&' s;
A1: ((p '&' s) => q) => (((p '&' s) => s) => ((p '&' s) => (q '&' s))) in HP_TAUT by Th35;
(p '&' s) => s in HP_TAUT by Def10;
hence ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in HP_TAUT by A1, Th29; ::_thesis: verum
end;
theorem Th41: :: HILBERT1:41
for p, q, s being Element of HP-WFF holds (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT
A1: ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in HP_TAUT by Th40;
(p => q) => ((p '&' s) => q) in HP_TAUT by Th39;
hence (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT by A1, Th23; ::_thesis: verum
end;
theorem Th42: :: HILBERT1:42
for p, q, s being Element of HP-WFF holds ((p => q) '&' (p '&' s)) => (q '&' s) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p => q) '&' (p '&' s)) => (q '&' s) in HP_TAUT
set P = p => q;
set Q = p '&' s;
set S = q '&' s;
A1: (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT by Th41;
((p => q) => ((p '&' s) => (q '&' s))) => (((p => q) '&' (p '&' s)) => (q '&' s)) in HP_TAUT by Th34;
hence ((p => q) '&' (p '&' s)) => (q '&' s) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
theorem Th43: :: HILBERT1:43
for p, q being Element of HP-WFF holds (p '&' q) => (q '&' p) in HP_TAUT
proof
let p, q be Element of HP-WFF ; ::_thesis: (p '&' q) => (q '&' p) in HP_TAUT
set P = p '&' q;
A1: (p '&' q) => q in HP_TAUT by Def10;
A2: (p '&' q) => p in HP_TAUT by Def10;
((p '&' q) => q) => (((p '&' q) => p) => ((p '&' q) => (q '&' p))) in HP_TAUT by Th35;
then ((p '&' q) => p) => ((p '&' q) => (q '&' p)) in HP_TAUT by A1, Def10;
hence (p '&' q) => (q '&' p) in HP_TAUT by A2, Def10; ::_thesis: verum
end;
theorem Th44: :: HILBERT1:44
for p, q, s being Element of HP-WFF holds ((p => q) '&' (p '&' s)) => (s '&' q) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p => q) '&' (p '&' s)) => (s '&' q) in HP_TAUT
A1: (q '&' s) => (s '&' q) in HP_TAUT by Th43;
((p => q) '&' (p '&' s)) => (q '&' s) in HP_TAUT by Th42;
hence ((p => q) '&' (p '&' s)) => (s '&' q) in HP_TAUT by A1, Th23; ::_thesis: verum
end;
theorem Th45: :: HILBERT1:45
for p, q, s being Element of HP-WFF holds (p => q) => ((p '&' s) => (s '&' q)) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (p => q) => ((p '&' s) => (s '&' q)) in HP_TAUT
set P = p => q;
set Q = p '&' s;
set S = s '&' q;
A1: ((p => q) '&' (p '&' s)) => (s '&' q) in HP_TAUT by Th44;
(((p => q) '&' (p '&' s)) => (s '&' q)) => ((p => q) => ((p '&' s) => (s '&' q))) in HP_TAUT by Th33;
hence (p => q) => ((p '&' s) => (s '&' q)) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
theorem Th46: :: HILBERT1:46
for p, q, s being Element of HP-WFF holds (p => q) => ((s '&' p) => (s '&' q)) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (p => q) => ((s '&' p) => (s '&' q)) in HP_TAUT
set P = p => q;
set Q = p '&' s;
set S = s '&' q;
set T = s '&' p;
A1: (p => q) => ((p '&' s) => (s '&' q)) in HP_TAUT by Th45;
A2: (s '&' p) => (p '&' s) in HP_TAUT by Th43;
((p => q) => ((p '&' s) => (s '&' q))) => (((s '&' p) => (p '&' s)) => ((p => q) => ((s '&' p) => (s '&' q)))) in HP_TAUT by Th24;
then ((s '&' p) => (p '&' s)) => ((p => q) => ((s '&' p) => (s '&' q))) in HP_TAUT by A1, Def10;
hence (p => q) => ((s '&' p) => (s '&' q)) in HP_TAUT by A2, Def10; ::_thesis: verum
end;
theorem :: HILBERT1:47
for p, s, q being Element of HP-WFF holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT
proof
let p, s, q be Element of HP-WFF ; ::_thesis: (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT
set P = s '&' q;
set Q = q '&' s;
A1: (s '&' q) => (q '&' s) in HP_TAUT by Th43;
((s '&' q) => (q '&' s)) => ((p '&' (s '&' q)) => (p '&' (q '&' s))) in HP_TAUT by Th46;
hence (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
theorem :: HILBERT1:48
for p, q, s being Element of HP-WFF holds ((p => q) '&' (p => s)) => (p => (q '&' s)) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p => q) '&' (p => s)) => (p => (q '&' s)) in HP_TAUT
set P = p => q;
set Q = p => s;
set S = p => (q '&' s);
A1: (p => q) => ((p => s) => (p => (q '&' s))) in HP_TAUT by Th35;
((p => q) => ((p => s) => (p => (q '&' s)))) => (((p => q) '&' (p => s)) => (p => (q '&' s))) in HP_TAUT by Th34;
hence ((p => q) '&' (p => s)) => (p => (q '&' s)) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
Lm5: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => q in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => q in HP_TAUT
A1: (p '&' q) => q in HP_TAUT by Def10;
((p '&' q) '&' s) => (p '&' q) in HP_TAUT by Def10;
hence ((p '&' q) '&' s) => q in HP_TAUT by A1, Th23; ::_thesis: verum
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
let p, q, s be Element of HP-WFF ; ::_thesis: (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in HP_TAUT
set P = (p '&' q) '&' s;
A1: ((p '&' q) '&' s) => q in HP_TAUT by Lm5;
(((p '&' q) '&' s) => q) => ((((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q)) in HP_TAUT by Th46;
hence (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
Lm7: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT
A1: (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in HP_TAUT by Lm6;
((p '&' q) '&' s) => (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) in HP_TAUT by Th30;
hence ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT by A1, Th23; ::_thesis: verum
end;
Lm8: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' s) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => (p '&' s) in HP_TAUT
set P = p '&' q;
A1: (p '&' q) => p in HP_TAUT by Def10;
((p '&' q) => p) => (((p '&' q) '&' s) => (p '&' s)) in HP_TAUT by Th41;
hence ((p '&' q) '&' s) => (p '&' s) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
Lm9: for p, q, s being Element of HP-WFF holds (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT
set P = (p '&' q) '&' s;
set Q = p '&' s;
A1: ((p '&' q) '&' s) => (p '&' s) in HP_TAUT by Lm8;
(((p '&' q) '&' s) => (p '&' s)) => ((((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q)) in HP_TAUT by Th41;
hence (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
Lm10: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((p '&' s) '&' q) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => ((p '&' s) '&' q) in HP_TAUT
A1: (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT by Lm9;
((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT by Lm7;
hence ((p '&' q) '&' s) => ((p '&' s) '&' q) in HP_TAUT by A1, Th23; ::_thesis: verum
end;
Lm11: for p, s, q being Element of HP-WFF holds ((p '&' s) '&' q) => ((s '&' p) '&' q) in HP_TAUT
proof
let p, s, q be Element of HP-WFF ; ::_thesis: ((p '&' s) '&' q) => ((s '&' p) '&' q) in HP_TAUT
set P = p '&' s;
set Q = s '&' p;
A1: (p '&' s) => (s '&' p) in HP_TAUT by Th43;
((p '&' s) => (s '&' p)) => (((p '&' s) '&' q) => ((s '&' p) '&' q)) in HP_TAUT by Th41;
hence ((p '&' s) '&' q) => ((s '&' p) '&' q) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
Lm12: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((s '&' p) '&' q) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => ((s '&' p) '&' q) in HP_TAUT
A1: ((p '&' s) '&' q) => ((s '&' p) '&' q) in HP_TAUT by Lm11;
((p '&' q) '&' s) => ((p '&' s) '&' q) in HP_TAUT by Lm10;
hence ((p '&' q) '&' s) => ((s '&' p) '&' q) in HP_TAUT by A1, Th23; ::_thesis: verum
end;
Lm13: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((s '&' q) '&' p) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => ((s '&' q) '&' p) in HP_TAUT
A1: ((s '&' p) '&' q) => ((s '&' q) '&' p) in HP_TAUT by Lm10;
((p '&' q) '&' s) => ((s '&' p) '&' q) in HP_TAUT by Lm12;
hence ((p '&' q) '&' s) => ((s '&' q) '&' p) in HP_TAUT by A1, Th23; ::_thesis: verum
end;
Lm14: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' (s '&' q)) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => (p '&' (s '&' q)) in HP_TAUT
A1: ((s '&' q) '&' p) => (p '&' (s '&' q)) in HP_TAUT by Th43;
((p '&' q) '&' s) => ((s '&' q) '&' p) in HP_TAUT by Lm13;
hence ((p '&' q) '&' s) => (p '&' (s '&' q)) in HP_TAUT by A1, Th23; ::_thesis: verum
end;
Lm15: for p, s, q being Element of HP-WFF holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT
proof
let p, s, q be Element of HP-WFF ; ::_thesis: (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT
set P = s '&' q;
set Q = q '&' s;
A1: (s '&' q) => (q '&' s) in HP_TAUT by Th43;
((s '&' q) => (q '&' s)) => ((p '&' (s '&' q)) => (p '&' (q '&' s))) in HP_TAUT by Th46;
hence (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
theorem :: HILBERT1:49
for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' (q '&' s)) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: ((p '&' q) '&' s) => (p '&' (q '&' s)) in HP_TAUT
A1: (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT by Lm15;
((p '&' q) '&' s) => (p '&' (s '&' q)) in HP_TAUT by Lm14;
hence ((p '&' q) '&' s) => (p '&' (q '&' s)) in HP_TAUT by A1, Th23; ::_thesis: verum
end;
Lm16: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT
A1: (p '&' (s '&' q)) => ((s '&' q) '&' p) in HP_TAUT by Th43;
(p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT by Lm15;
hence (p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT by A1, Th23; ::_thesis: verum
end;
Lm17: for s, q, p being Element of HP-WFF holds ((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT
proof
let s, q, p be Element of HP-WFF ; ::_thesis: ((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT
set P = s '&' q;
set Q = q '&' s;
A1: (s '&' q) => (q '&' s) in HP_TAUT by Th43;
((s '&' q) => (q '&' s)) => (((s '&' q) '&' p) => ((q '&' s) '&' p)) in HP_TAUT by Th41;
hence ((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
Lm18: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT
A1: ((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT by Lm17;
(p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT by Lm16;
hence (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT by A1, Th23; ::_thesis: verum
end;
Lm19: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((p '&' s) '&' q) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (p '&' (q '&' s)) => ((p '&' s) '&' q) in HP_TAUT
A1: ((q '&' s) '&' p) => ((p '&' s) '&' q) in HP_TAUT by Lm13;
(p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT by Lm18;
hence (p '&' (q '&' s)) => ((p '&' s) '&' q) in HP_TAUT by A1, Th23; ::_thesis: verum
end;
Lm20: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT
set P = q '&' s;
set Q = s '&' q;
A1: (q '&' s) => (s '&' q) in HP_TAUT by Th43;
((q '&' s) => (s '&' q)) => ((p '&' (q '&' s)) => (p '&' (s '&' q))) in HP_TAUT by Th46;
hence (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT by A1, Def10; ::_thesis: verum
end;
theorem :: HILBERT1:50
for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((p '&' q) '&' s) in HP_TAUT
proof
let p, q, s be Element of HP-WFF ; ::_thesis: (p '&' (q '&' s)) => ((p '&' q) '&' s) in HP_TAUT
A1: (p '&' (s '&' q)) => ((p '&' q) '&' s) in HP_TAUT by Lm19;
(p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT by Lm20;
hence (p '&' (q '&' s)) => ((p '&' q) '&' s) in HP_TAUT by A1, Th23; ::_thesis: verum
end;