Copyright (c) 1999 Association of Mizar Users
environ
vocabulary FINSEQ_1, RELAT_1, FUNCT_1, QC_LANG1, ZF_LANG, BOOLE, HILBERT1;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, RELAT_1, FUNCT_1, NAT_1,
FINSEQ_1;
constructors NAT_1, CQC_LANG, MEMBERED;
clusters RELSET_1, MEMBERED, NUMBERS, ORDINAL2;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI;
theorems TARSKI, FINSEQ_1, XBOOLE_0, XBOOLE_1;
schemes XBOOLE_0;
begin :: Definition of the language
definition let D be set;
attr D is with_VERUM means :Def1:
<*0*> in D;
end;
definition let D be set;
attr D is with_implication means :Def2:
for p, q being FinSequence st
p in D & q in D holds <*1*>^p^q in D;
end;
definition let D be set;
attr D is with_conjunction means :Def3:
for p, q being FinSequence st
p in D & q in D holds <*2*>^p^q in D;
end;
definition let D be set;
attr D is with_propositional_variables means :Def4:
for n being Nat holds <*3+n*> in D;
end;
definition let D be set;
attr D is HP-closed means :Def5:
D c= NAT* &
D is with_VERUM with_implication with_conjunction
with_propositional_variables;
end;
Lm1: for D be set st D is HP-closed holds D is non empty
proof
let D be set;
assume D is HP-closed;
then D is with_VERUM by Def5;
hence thesis by Def1;
end;
definition
cluster HP-closed -> with_VERUM with_implication
with_conjunction with_propositional_variables non empty set;
coherence by Def5,Lm1;
cluster with_VERUM with_implication
with_conjunction with_propositional_variables -> HP-closed Subset of NAT*
;
coherence by Def5;
end;
definition
func HP-WFF -> set means :Def6:
it is HP-closed &
for D being set st D is HP-closed holds it c= D;
existence
proof
defpred P[set] means for D being set st D is HP-closed holds $1 in D;
consider D0 being set such that
A1: for x being set holds x in D0 iff x in NAT* & P[x]
from Separation;
A2: <*0*> in NAT* by FINSEQ_1:def 11;
A3: for D being set st D is HP-closed holds <*0*> in D
proof
let D be set; assume D is HP-closed;
then D is with_VERUM by Def5;
hence thesis by Def1;
end;
then reconsider D0 as non empty set by A1,A2;
take D0;
A4: D0 c= NAT*
proof let x be set;
thus thesis by A1;
end;
<*0*> in D0 by A1,A2,A3;
then A5:D0 is with_VERUM by Def1;
for n being Nat holds <*3+n*> in D0
proof let n be Nat;
set p = 3+n;
reconsider h = <*p*> as FinSequence of NAT;
A6: h in NAT* by FINSEQ_1:def 11;
for D being set st D is HP-closed holds <*p*> in D
proof
let D be set;
assume D is HP-closed;
then D is with_propositional_variables by Def5;
hence thesis by Def4;
end;
hence thesis by A1,A6;
end;
then A7:D0 is with_propositional_variables by Def4;
for p, q being FinSequence
st p in D0 & q in D0 holds <*1*>^p^q in D0
proof
let p, q be FinSequence such that
A8: p in D0 & q in D0;
p in NAT* & q in NAT* by A1,A8;
then reconsider p'=p, q'=q as FinSequence of NAT by FINSEQ_1:def 11
;
A9: <*1*>^p'^q' in NAT* by FINSEQ_1:def 11;
for D being set
st D is HP-closed holds <*1*>^p^q in D
proof let D be set; assume
A10: D is HP-closed;
then A11: D is with_implication by Def5;
p in D & q in D by A1,A8,A10;
hence thesis by A11,Def2;
end;
hence <*1*>^p^q in D0 by A1,A9;
end;
then A12: D0 is with_implication by Def2;
for p, q being FinSequence
st p in D0 & q in D0 holds <*2*>^p^q in D0
proof
let p, q be FinSequence such that
A13: p in D0 & q in D0;
p in NAT* & q in NAT* by A1,A13;
then reconsider p'=p, q'=q as FinSequence of NAT by FINSEQ_1:def 11
;
A14: <*2*>^p'^q' in NAT* by FINSEQ_1:def 11;
for D being set
st D is HP-closed holds <*2*>^p^q in D
proof let D be set; assume
A15: D is HP-closed;
then A16: D is with_conjunction by Def5;
p in D & q in D by A1,A13,A15;
hence thesis by A16,Def3;
end;
hence <*2*>^p^q in D0 by A1,A14;
end;
then D0 is with_conjunction by Def3;
hence D0 is HP-closed by A4,A5,A7,A12,Def5;
let D be set such that
A17: D is HP-closed;
let x be set; assume
x in D0;
hence thesis by A1,A17;
end;
uniqueness
proof
let D1, D2 be set such that
A18: D1 is HP-closed & for D being set
st D is HP-closed holds D1 c= D and
A19: D2 is HP-closed & for D being set
st D is HP-closed holds D2 c= D;
D1 c= D2 & D2 c= D1 by A18,A19;
hence D1 = D2 by XBOOLE_0:def 10;
end;
end;
definition
cluster HP-WFF -> HP-closed;
coherence by Def6;
end;
definition
cluster HP-closed non empty set;
existence
proof
take HP-WFF;
thus thesis;
end;
end;
definition
cluster -> Relation-like Function-like Element of HP-WFF;
coherence
proof let p be Element of HP-WFF;
HP-WFF c= NAT* & p in HP-WFF by Def5;
hence thesis by FINSEQ_1:def 11;
end;
end;
definition
cluster -> FinSequence-like Element of HP-WFF;
coherence
proof let p be Element of HP-WFF;
HP-WFF c= NAT* & p in HP-WFF by Def5;
hence thesis by FINSEQ_1:def 11;
end;
end;
definition
mode HP-formula is Element of HP-WFF;
end;
definition
func VERUM -> HP-formula equals
<*0*>;
correctness by Def1;
let p, q be Element of HP-WFF;
func p => q -> HP-formula equals
<*1*>^p^q;
coherence by Def2;
func p '&' q -> HP-formula equals
<*2*>^p^q;
correctness by Def3;
end;
reserve T, X, Y for Subset of HP-WFF;
reserve p, q, r, s for Element of HP-WFF;
definition let T be Subset of HP-WFF;
attr T is Hilbert_theory means :Def10:
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;
definition let X;
func CnPos X -> Subset of HP-WFF means
:Def11: r in it iff for T st T is Hilbert_theory & X c= T holds r in T;
existence
proof
defpred P[set] means
(for T 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 & P[a] from Separation;
Y c= HP-WFF
proof
let a be set; assume a in Y;
hence a in HP-WFF by A1;
end;
then reconsider Z = Y as Subset of HP-WFF;
take Z;
thus r in Z iff for T st T is Hilbert_theory & X c= T holds r in T by A1;
end;
uniqueness
proof
let Y,Z be Subset of HP-WFF such that
A2: r in Y iff for T st T is Hilbert_theory & X c= T holds r in T and
A3: r in Z iff for T st T is Hilbert_theory & X c= T holds r in T;
for a being set holds a in Y iff a in Z
proof
let a be set;
hereby assume A4: a in Y;
then reconsider t=a as Element of HP-WFF;
for T st T is Hilbert_theory & X c= T holds t in T by A2,A4;
hence a in Z by A3;
end;
assume A5: a in Z;
then reconsider t=a as Element of HP-WFF;
for T st T is Hilbert_theory & X c= T holds t in T by A3,A5;
hence a in Y by A2;
end;
hence thesis by TARSKI:2;
end;
end;
definition
func HP_TAUT -> Subset of HP-WFF equals :Def12:
CnPos({}(HP-WFF));
correctness;
end;
theorem Th1:
VERUM in CnPos (X)
proof
T is Hilbert_theory & X c= T implies VERUM in T by Def10;
hence thesis by Def11;
end;
theorem Th2:
p => (q => (p '&' q)) in CnPos (X)
proof
T is Hilbert_theory & X c= T implies p => (q => (p '&' q)) in T by Def10;
hence thesis by Def11;
end;
theorem Th3:
(p => (q => r)) => ((p => q) => (p => r)) in CnPos (X)
proof
T is Hilbert_theory & X c= T implies
(p => (q => r)) => ((p => q) => (p => r)) in T by Def10;
hence thesis by Def11;
end;
theorem Th4:
p => (q => p) in CnPos (X)
proof
T is Hilbert_theory & X c= T implies p => (q => p) in T by Def10;
hence thesis by Def11;
end;
theorem Th5:
p '&' q => p in CnPos(X)
proof
T is Hilbert_theory & X c= T implies p '&' q => p in T by Def10;
hence thesis by Def11;
end;
theorem Th6:
p '&' q => q in CnPos(X)
proof
T is Hilbert_theory & X c= T implies p '&' q => q in T by Def10;
hence thesis by Def11;
end;
theorem Th7:
p in CnPos(X) & p => q in CnPos(X) implies q in CnPos(X)
proof
assume A1: p in CnPos(X) & p => q in CnPos(X);
T is Hilbert_theory & X c= T implies q in T
proof
assume A2: T is Hilbert_theory & X c= T;
then p in T & p => q in T by A1,Def11;
hence thesis by A2,Def10;
end;
hence thesis by Def11;
end;
theorem Th8: T is Hilbert_theory & X c= T implies CnPos(X) c= T
proof
assume that A1:T is Hilbert_theory and A2: X c= T;
let a be set;
thus thesis by A1,A2,Def11;
end;
theorem Th9:
X c= CnPos(X)
proof
let a be set;
assume A1: a in X;
then reconsider t = a as Element of HP-WFF;
for T st T is Hilbert_theory & X c= T holds t in T by A1;
hence a in CnPos(X) by Def11;
end;
theorem Th10:
X c= Y implies CnPos(X) c= CnPos(Y)
proof
assume A1: X c= Y;
thus CnPos(X) c= CnPos(Y)
proof
let a be set; assume A2: a in CnPos(X);
then reconsider t = a as Element of HP-WFF;
for T st T is Hilbert_theory & Y c= T holds t in T
proof
let T such that A3: T is Hilbert_theory and A4: Y c= T;
X c= T by A1,A4,XBOOLE_1:1;
hence t in T by A2,A3,Def11;
end;
hence thesis by Def11;
end;
end;
Lm2: CnPos(CnPos(X)) c= CnPos(X)
proof
let a be set; assume A1: a in CnPos(CnPos(X));
then reconsider t = a as Element of HP-WFF;
for T st T is Hilbert_theory & X c= T holds t in T
proof
let T; assume that A2: T is Hilbert_theory and A3: X c= T;
CnPos(X) c= T by A2,A3,Th8;
hence t in T by A1,A2,Def11;
end;
hence thesis by Def11;
end;
theorem
CnPos(CnPos(X)) = CnPos(X)
proof
CnPos(CnPos(X)) c= CnPos(X) & CnPos(X) c= CnPos(CnPos(X)) by Lm2,Th9;
hence thesis by XBOOLE_0:def 10;
end;
Lm3:
CnPos(X) is Hilbert_theory
proof
thus VERUM in CnPos(X) by Th1;
let p, q, r;
thus p => (q => p) in CnPos(X) by Th4;
thus (p => (q => r)) => ((p => q) => (p => r)) in CnPos(X) by Th3;
thus (p '&' q) => p in CnPos(X) by Th5;
thus (p '&' q) => q in CnPos(X) by Th6;
thus p => (q => (p '&' q)) in CnPos(X) by Th2;
thus (p in CnPos(X) & p => q in CnPos(X) implies q in CnPos(X)) by Th7;
end;
definition let X be Subset of HP-WFF;
cluster CnPos(X) -> Hilbert_theory;
coherence by Lm3;
end;
theorem Th12:
T is Hilbert_theory iff CnPos(T) = T
proof
hereby assume A1: T is Hilbert_theory;
A2: T c= CnPos(T) by Th9;
CnPos(T) c= T
proof
let a be set; assume a in CnPos(T);
hence a in T by A1,Def11;
end;
hence CnPos(T) = T by A2,XBOOLE_0:def 10;
end;
thus CnPos(T) = T implies T is Hilbert_theory;
end;
theorem
T is Hilbert_theory implies HP_TAUT c= T
proof
assume A1: T is Hilbert_theory;
{}(HP-WFF) c= T by XBOOLE_1:2;
then HP_TAUT c= CnPos(T) by Def12,Th10;
hence thesis by A1,Th12;
end;
definition
cluster HP_TAUT -> Hilbert_theory;
coherence by Def12;
end;
begin :: The tautologies of the Hilbert calculus - implicational part
theorem Th14: :: Identity law
p => p in HP_TAUT
proof
A1:p => (p => p) in HP_TAUT by Def10;
A2:(p => ((p => p) => p))
=> ((p => (p => p)) => (p => p)) in HP_TAUT by Def10;
p => ((p => p) => p) in HP_TAUT by Def10;
then (p => (p => p)) => (p => p) in HP_TAUT by A2,Def10;
hence thesis by A1,Def10;
end;
theorem Th15:
q in HP_TAUT implies p => q in HP_TAUT
proof
q => (p => q) in HP_TAUT by Def10;
hence thesis by Def10;
end;
theorem
p => VERUM in HP_TAUT
proof
VERUM in HP_TAUT by Def12,Th1;
hence thesis by Th15;
end;
theorem
(p => q) => (p => p) in HP_TAUT
proof
(p => p) in HP_TAUT by Th14;
hence thesis by Th15;
end;
theorem
(q => p) => (p => p) in HP_TAUT
proof
(p => p) in HP_TAUT by Th14;
hence thesis by Th15;
end;
theorem Th19:
(q => r) => ((p => q) => (p => r)) in HP_TAUT
proof
A1:((p => (q => r)) => ((p => q) => (p => r))) =>
( (q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) in HP_TAUT
by Def10;
((p => (q => r)) => ((p => q) => (p => r))) in HP_TAUT by Def10;
then A2: ( (q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) in HP_TAUT
by A1,Def10;
( (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;
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 thesis by A3,Def10;
end;
theorem Th20:
p => (q => r) in HP_TAUT implies q => (p => r) in HP_TAUT
proof
assume A1: p => (q => r) in HP_TAUT;
(p => (q => r)) => ((p => q) => (p => r)) in HP_TAUT by Def10;
then A2: ((p => q) => (p => r)) in HP_TAUT by A1,Def10;
((p => q) => (p => r)) => ((q => (p => q)) => (q => (p => r))) in HP_TAUT
by Th19;
then A3:((q => (p => q)) => (q => (p => r))) in HP_TAUT by A2,Def10;
q => (p => q) in HP_TAUT by Def10;
hence thesis by A3,Def10;
end;
theorem Th21: :: Hypothetical syllogism
(p => q) => ((q => r) => (p => r)) in HP_TAUT
proof
(q => r) => ((p => q) => (p => r)) in HP_TAUT by Th19;
hence thesis by Th20;
end;
theorem Th22:
p => q in HP_TAUT implies (q => r) => (p => r) in HP_TAUT
proof assume
A1: p => q 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;
end;
theorem Th23:
p => q in HP_TAUT & q => r in HP_TAUT implies p => r in HP_TAUT
proof assume that
A1: p => q in HP_TAUT and
A2: q => 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;
end;
Lm4: (((q => r) => (p => r)) => s) => ((p => q) => s) in HP_TAUT
proof
(p => q) => ((q => r) => (p => r)) in HP_TAUT by Th21;
hence thesis by Th22;
end;
theorem Th24:
(p => (q => r)) => ((s => q) => (p => (s => r))) in HP_TAUT
proof
A1: ((((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;
(((q => r) => (s => r)) => (p => (s => r))) =>
((s => q) => (p => (s => r))) in HP_TAUT by Lm4;
hence thesis by A1,Def10;
end;
theorem
((p => q) => r) => (q => r) in HP_TAUT
proof
q => (p => q) in HP_TAUT &
(q => (p => q)) => (((p => q) => r) => (q => r)) in HP_TAUT
by Def10,Th21;
hence thesis by Def10;
end;
theorem Th26: :: Contraposition
(p => (q => r)) => (q => (p => r)) in HP_TAUT
proof
(p => (q => r)) => ((p => q) => (p => r)) in HP_TAUT by Def10;
then A1:(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 A2:(q => (p => q)) => (q => ((p => (q => r)) => (p => r))) in HP_TAUT
by A1,Def10;
q => (p => q) in HP_TAUT by Def10;
then (q => ((p => (q => r)) => (p => r))) in HP_TAUT by A2,Def10;
hence thesis by Th20;
end;
theorem Th27: :: A Hilbert axiom
(p => (p => q)) => (p => q) in HP_TAUT
proof
A1:p => p in HP_TAUT by Th14;
(p => (p => q)) => ((p => p) => (p => q)) in HP_TAUT by Def10;
then (p => p) => ((p => (p => q)) => (p => q)) in HP_TAUT by Th20;
hence thesis by A1,Def10;
end;
theorem :: Modus ponendo ponens
q => ((q => p) => p) in HP_TAUT
proof
A1:(q => p) => (q => p) in HP_TAUT by Th14;
((q => p) => (q => p)) => (q => ((q => p) => p)) in HP_TAUT by Th26;
hence thesis by A1,Def10;
end;
theorem Th29:
s => (q => p) in HP_TAUT & q in HP_TAUT implies s => p in HP_TAUT
proof
assume A1: s => (q => p) in HP_TAUT & q 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 thesis by A1,Def10;
end;
begin :: Conjunctional part of the calculus
theorem Th30:
p => (p '&' p) in HP_TAUT
proof
A1:p => (p => (p '&' p)) in HP_TAUT by Def10;
(p => (p => (p '&' p))) => (p => (p '&' p)) in HP_TAUT by Th27;
hence thesis by A1,Def10;
end;
theorem Th31:
(p '&' q) in HP_TAUT iff p in HP_TAUT & q in HP_TAUT
proof
hereby assume A1: p '&' q in HP_TAUT;
(p '&' q) => p in HP_TAUT & (p '&' q) => q in HP_TAUT by Def10;
hence p in HP_TAUT & q in HP_TAUT by A1,Def10;
end;
assume A2: p in HP_TAUT & q in HP_TAUT;
p => (q => (p '&' q)) in HP_TAUT by Def10;
then q => (p '&' q) in HP_TAUT by A2,Def10;
hence thesis by A2,Def10;
end;
theorem
(p '&' q) in HP_TAUT iff (q '&' p) in HP_TAUT
proof
hereby assume p '&' q in HP_TAUT;
then p in HP_TAUT & q in HP_TAUT by Th31;
hence q '&' p in HP_TAUT by Th31;
end;
assume q '&' p in HP_TAUT;
then q in HP_TAUT & p in HP_TAUT by Th31;
hence p '&' q in HP_TAUT by Th31;
end;
theorem Th33:
(( p '&' q ) => r ) => ( p => ( q => r )) in HP_TAUT
proof
( q => ( p '&' q )) => ((( p '&' q ) => r ) => ( q => r )) in HP_TAUT
by Th21;
then A1: p => (( q => ( p '&' q )) => ((( p '&' q ) => r ) => ( q => r )))
in HP_TAUT by Th15;
set qp = ( q => ( p '&' q ));
set pr = (( p '&' q ) => r) => ( q => r );
( p => ( qp => pr )) => ( ( p => qp ) => ( p => pr )) in HP_TAUT by Def10
;
then A2: ( ( p => qp ) => ( p => pr )) in HP_TAUT by A1,Def10;
p => ( q => ( p '&' q )) in HP_TAUT by 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 thesis by A3,Def10;
end;
theorem Th34:
( p => ( q => r )) => (( p '&' q ) => r ) in HP_TAUT
proof
A1: ( p '&' q ) => q in HP_TAUT by Def10;
(( p '&' q ) => q) => (( q => r ) => (( p '&' q ) => r )) in HP_TAUT
by Th21;
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;
p => (( q => r ) => (( p '&' q ) => r )) =>
((p => ( q => r )) => ( p => (( p '&' q ) => r ))) in HP_TAUT
by Def10;
then A3: (p => ( q => r )) => ( p => (( p '&' q ) => r )) in HP_TAUT
by A2,Def10;
( p => (( p '&' q ) => r )) => ((p '&' q ) => ( p => r )) in HP_TAUT
by Th26;
then A4: (p => ( q => r )) => ((p '&' q ) => ( p => r )) in HP_TAUT by A3,
Th23;
A5: ((p '&' q ) => ( p => r )) => ((( p '&' q ) => p ) => (( p '&' q )
=> r )) in HP_TAUT by Def10;
( p '&' q ) => p in HP_TAUT by Def10;
then ((p '&' q ) => ( p => r )) => (( p '&' q ) => r ) in HP_TAUT by A5,
Th29;
hence thesis by A4,Th23;
end;
theorem Th35:
( r => p ) => (( r => q ) => ( r => ( p '&' q ))) in HP_TAUT
proof
p => ( q => ( p '&' q )) in HP_TAUT by Def10;
then A1: 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 A2: ( r => p ) => ( r => ( q => ( p '&' q ))) in HP_TAUT by A1,Def10;
( r => ( q => ( p '&' q ))) => (( r => q ) => ( r => ( p '&' q )))
in HP_TAUT by Def10;
hence thesis by A2,Th23;
end;
theorem Th36:
( (p => q) '&' p ) => q in HP_TAUT
proof
set P = p => q;
A1:( P => P ) => (( P '&' p ) => q ) in HP_TAUT by Th34;
P => P in HP_TAUT by Th14;
hence thesis by A1,Def10;
end;
theorem
(( (p => q) '&' p ) '&' s ) => q in HP_TAUT
proof
set P = (p => q) '&' p;
A1:(P '&' s) => P in HP_TAUT by Def10;
P => q in HP_TAUT by Th36;
hence thesis by A1,Th23;
end;
theorem
(q => s) => (( p '&' q ) => s) in HP_TAUT
proof
set P = p '&' q;
A1:(P => q) => ((q => s) => (P => s)) in HP_TAUT by Th21;
P => q in HP_TAUT by Def10;
hence thesis by A1,Def10;
end;
theorem Th39:
(q => s) => (( q '&' p ) => s) in HP_TAUT
proof
set P = q '&' p;
A1:(P => q) => ((q => s) => (P => s)) in HP_TAUT by Th21;
P => q in HP_TAUT by Def10;
hence thesis by A1,Def10;
end;
theorem Th40:
( (p '&' s) => q ) => ((p '&' s) => (q '&' s)) in HP_TAUT
proof
set P = p '&' s;
A1:P => s in HP_TAUT by Def10;
( P => q ) => (( P => s ) => ( P => ( q '&' s ))) in HP_TAUT by Th35;
hence thesis by A1,Th29;
end;
theorem Th41:
( p => q ) => ((p '&' s) => (q '&' s)) in HP_TAUT
proof
A1:(p => q) => (( p '&' s ) => q) in HP_TAUT by Th39;
( (p '&' s) => q ) => ((p '&' s) => (q '&' s)) in HP_TAUT by Th40;
hence thesis by A1,Th23;
end;
theorem Th42:
( p => q ) '&' ( p '&' s ) => ( q '&' s ) in HP_TAUT
proof
set P = p => q, Q = p '&' s, S = q '&' s;
A1:( P => ( Q => S )) => (( P '&' Q ) => S ) in HP_TAUT by Th34;
P => (Q => S) in HP_TAUT by Th41;
hence thesis by A1,Def10;
end;
theorem Th43:
( p '&' q ) => ( q '&' p ) in HP_TAUT
proof
set P = p '&' q;
A1:( P => q ) => (( P => p ) => ( P => ( q '&' p ))) in HP_TAUT by Th35;
P => q in HP_TAUT by Def10;
then A2:( P => p ) => ( P => ( q '&' p )) in HP_TAUT by A1,Def10;
P => p in HP_TAUT by Def10;
hence thesis by A2,Def10;
end;
theorem Th44:
( p => q ) '&' ( p '&' s ) => ( s '&' q ) in HP_TAUT
proof
A1:( p => q ) '&' ( p '&' s ) => ( q '&' s ) in HP_TAUT by Th42;
( q '&' s ) => ( s '&' q ) in HP_TAUT by Th43;
hence thesis by A1,Th23;
end;
theorem Th45:
( p => q ) => (( p '&' s ) => ( s '&' q )) in HP_TAUT
proof
set P = p => q, Q = p '&' s, S = s '&' q;
A1:(( P '&' Q ) => S ) => ( P => ( Q => S )) in HP_TAUT by Th33;
P '&' Q => S in HP_TAUT by Th44;
hence thesis by A1,Def10;
end;
theorem Th46:
( p => q ) => (( s '&' p ) => ( s '&' q )) in HP_TAUT
proof
set P = p => q, Q = p '&' s, S = s '&' q, T = s '&' p;
A1:(P => (Q => S)) => ((T => Q) => (P => (T => S))) in HP_TAUT by Th24;
P => (Q => S) in HP_TAUT by Th45;
then A2:(T => Q) => (P => (T => S)) in HP_TAUT by A1,Def10;
T => Q in HP_TAUT by Th43;
hence thesis by A2,Def10;
end;
theorem
( p '&' (s '&' q) ) => ( p '&' (q '&' s) ) in HP_TAUT
proof
set P = s '&' q, Q = q '&' s;
A1:( P => Q ) => (( p '&' P ) => ( p '&' Q )) in HP_TAUT by Th46;
P => Q in HP_TAUT by Th43;
hence thesis by A1,Def10;
end;
theorem
( ( p => q ) '&' (p => s) ) => ( p => (q '&' s) ) in HP_TAUT
proof
set P = p => q, Q = p => s, S = p => (q '&' s);
A1:( P => ( Q => S )) => (( P '&' Q ) => S ) in HP_TAUT by Th34;
P => (Q => S) in HP_TAUT by Th35;
hence thesis by A1,Def10;
end;
Lm5:
( (p '&' q) '&' s ) => q in HP_TAUT
proof
A1:((p '&' q) '&' s) => (p '&' q) in HP_TAUT by Def10;
(p '&' q) => q in HP_TAUT by Def10;
hence thesis by A1,Th23;
end;
Lm6:
( (p '&' q) '&' s ) '&' ( (p '&' q) '&' s ) => ( (p '&' q) '&' s ) '&' q
in HP_TAUT
proof
set P = (p '&' q) '&' s;
A1:( P => q ) => (( P '&' P ) => ( P '&' q )) in HP_TAUT by Th46;
P => q in HP_TAUT by Lm5;
hence thesis by A1,Def10;
end;
Lm7:
(p '&' q) '&' s => ((p '&' q) '&' s) '&' q in HP_TAUT
proof
A1:( (p '&' q) '&' s ) => ( (p '&' q) '&' s ) '&' ( (p '&' q) '&' s )
in HP_TAUT by Th30;
( (p '&' q) '&' s ) '&' ( (p '&' q) '&' s ) => ( (p '&' q) '&' s ) '&' q
in HP_TAUT by Lm6;
hence thesis by A1,Th23;
end;
Lm8:
(p '&' q) '&' s => (p '&' s) in HP_TAUT
proof
set P = p '&' q;
A1:( P => p ) => ((P '&' s) => (p '&' s)) in HP_TAUT by Th41;
P => p in HP_TAUT by Def10;
hence thesis by A1,Def10;
end;
Lm9:
(p '&' q) '&' s '&' q => (p '&' s) '&' q in HP_TAUT
proof
set P = p '&' q '&' s, Q = p '&' s;
A1:( P => Q ) => ((P '&' q) => (Q '&' q)) in HP_TAUT by Th41;
P => Q in HP_TAUT by Lm8;
hence thesis by A1,Def10;
end;
Lm10:
(p '&' q) '&' s => (p '&' s) '&' q in HP_TAUT
proof
A1:(p '&' q) '&' s => ((p '&' q) '&' s) '&' q in HP_TAUT by Lm7;
(p '&' q) '&' s '&' q => (p '&' s) '&' q in HP_TAUT by Lm9;
hence thesis by A1,Th23;
end;
Lm11:
(p '&' s) '&' q => (s '&' p) '&' q in HP_TAUT
proof
set P = p '&' s, Q = s '&' p;
A1:( P => Q ) => ((P '&' q) => (Q '&' q)) in HP_TAUT by Th41;
P => Q in HP_TAUT by Th43;
hence thesis by A1,Def10;
end;
Lm12:
(p '&' q) '&' s => (s '&' p) '&' q in HP_TAUT
proof
A1:(p '&' q) '&' s => (p '&' s) '&' q in HP_TAUT by Lm10;
(p '&' s) '&' q => (s '&' p) '&' q in HP_TAUT by Lm11;
hence thesis by A1,Th23;
end;
Lm13:
(p '&' q) '&' s => (s '&' q) '&' p in HP_TAUT
proof
A1:(p '&' q) '&' s => (s '&' p) '&' q in HP_TAUT by Lm12;
(s '&' p) '&' q => (s '&' q) '&' p in HP_TAUT by Lm10;
hence thesis by A1,Th23;
end;
Lm14:
(p '&' q) '&' s => p '&' (s '&' q) in HP_TAUT
proof
A1:(p '&' q) '&' s => (s '&' q) '&' p in HP_TAUT by Lm13;
(s '&' q) '&' p => p '&' (s '&' q) in HP_TAUT by Th43;
hence thesis by A1,Th23;
end;
Lm15:
p '&' (s '&' q) => p '&' (q '&' s) in HP_TAUT
proof
set P = s '&' q, Q = q '&' s;
A1:( P => Q ) => (( p '&' P ) => ( p '&' Q )) in HP_TAUT by Th46;
s '&' q => q '&' s in HP_TAUT by Th43;
hence thesis by A1,Def10;
end;
theorem
(p '&' q) '&' s => p '&' (q '&' s) in HP_TAUT
proof
A1:(p '&' q) '&' s => p '&' (s '&' q) in HP_TAUT by Lm14;
p '&' (s '&' q) => p '&' (q '&' s) in HP_TAUT by Lm15;
hence thesis by A1,Th23;
end;
Lm16:
p '&' (q '&' s) => (s '&' q) '&' p in HP_TAUT
proof
A1:p '&' (q '&' s) => p '&' (s '&' q) in HP_TAUT by Lm15;
p '&' (s '&' q) => (s '&' q) '&' p in HP_TAUT by Th43;
hence thesis by A1,Th23;
end;
Lm17:
(s '&' q) '&' p => (q '&' s) '&' p in HP_TAUT
proof
set P = s '&' q, Q = q '&' s;
A1:( P => Q ) => ((P '&' p) => (Q '&' p)) in HP_TAUT by Th41;
s '&' q => q '&' s in HP_TAUT by Th43;
hence thesis by A1,Def10;
end;
Lm18:
p '&' (q '&' s) => (q '&' s) '&' p in HP_TAUT
proof
A1:p '&' (q '&' s) => (s '&' q) '&' p in HP_TAUT by Lm16;
(s '&' q) '&' p => (q '&' s) '&' p in HP_TAUT by Lm17;
hence thesis by A1,Th23;
end;
Lm19:
p '&' (q '&' s) => (p '&' s) '&' q in HP_TAUT
proof
A1:p '&' (q '&' s) => (q '&' s) '&' p in HP_TAUT by Lm18;
(q '&' s) '&' p => (p '&' s) '&' q in HP_TAUT by Lm13;
hence thesis by A1,Th23;
end;
Lm20:
p '&' (q '&' s) => p '&' (s '&' q) in HP_TAUT
proof
set P = q '&' s, Q = s '&' q;
A1:( P => Q ) => (( p '&' P ) => ( p '&' Q )) in HP_TAUT by Th46;
q '&' s => s '&' q in HP_TAUT by Th43;
hence thesis by A1,Def10;
end;
theorem
p '&' (q '&' s) => (p '&' q) '&' s in HP_TAUT
proof
A1:p '&' (q '&' s) => p '&' (s '&' q) in HP_TAUT by Lm20;
p '&' (s '&' q) => (p '&' q) '&' s in HP_TAUT by Lm19;
hence thesis by A1,Th23;
end;