:: Hilbert Positive Propositional Calculus
:: by Adam Grabowski
::
:: Received February 20, 1999
:: Copyright (c) 1999-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSEQ_1, CARD_1, ORDINAL4, SUBSET_1, NUMBERS, ARYTM_3, TARSKI,
RELAT_1, XBOOLE_0, FUNCT_1, QC_LANG1, XBOOLEAN, HILBERT1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1,
FUNCT_1, FINSEQ_1;
constructors NAT_1, FINSEQ_1, NUMBERS;
registrations SUBSET_1, ORDINAL1, FUNCT_1, FINSEQ_1, XCMPLX_0;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI;
expansions TARSKI;
theorems TARSKI, FINSEQ_1, XBOOLE_0, XBOOLE_1;
schemes XFAMILY;
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 Element of 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;
hence thesis;
end;
registration
cluster HP-closed -> with_VERUM with_implication with_conjunction
with_propositional_variables non empty for set;
coherence by Lm1;
cluster with_VERUM with_implication with_conjunction
with_propositional_variables -> HP-closed for Subset of NAT*;
coherence;
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
A1: <*0*> in NAT* by FINSEQ_1:def 11;
defpred P[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* & P[x] from XFAMILY:
sch 1;
A3: for D being set st D is HP-closed holds <*0*> in D by Def1;
then reconsider D0 as non empty set by A2,A1;
take D0;
A4: D0 c= NAT*
by A2;
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
A5: p in D0 and
A6: 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;
assume
A9: D is HP-closed;
then
A10: q in D by A2,A6;
p in D by A2,A5,A9;
hence thesis by A9,A10,Def3;
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 thesis by A2,A8;
end;
then
A11: D0 is with_conjunction;
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
A12: p in D0 and
A13: 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;
assume
A16: D is HP-closed;
then
A17: q in D by A2,A13;
p in D by A2,A12,A16;
hence thesis by A16,A17,Def2;
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 thesis by A2,A15;
end;
then
A18: D0 is with_implication;
for n being Element of NAT holds <*3+n*> in D0
proof
let n be Element of NAT;
set p = 3+n;
reconsider h = <*p*> as FinSequence of NAT;
A19: h in NAT* by FINSEQ_1:def 11;
for D being set st D is HP-closed holds <*p*> in D by Def4;
hence thesis by A2,A19;
end;
then
A20: D0 is with_propositional_variables;
<*0*> in D0 by A2,A1,A3;
then D0 is with_VERUM;
hence D0 is HP-closed by A4,A20,A18,A11;
let D be set such that
A21: D is HP-closed;
let x be object;
assume x in D0;
hence thesis by A2,A21;
end;
uniqueness
proof
let D1, D2 be set such 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;
A26: D2 c= D1 by A22,A25;
D1 c= D2 by A23,A24;
hence thesis by A26,XBOOLE_0:def 10;
end;
end;
registration
cluster HP-WFF -> HP-closed;
coherence by Def6;
end;
registration
cluster HP-closed non empty for set;
existence
proof
take HP-WFF;
thus thesis;
end;
end;
registration
cluster HP-WFF -> functional;
coherence
proof
HP-WFF c= NAT* by Def5;
hence thesis;
end;
end;
registration
cluster -> FinSequence-like for Element of HP-WFF;
coherence
proof
let p be Element of HP-WFF;
HP-WFF c= NAT* by Def5;
hence thesis;
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 XFAMILY:
sch 1;
Y c= HP-WFF
by A1;
then reconsider Z = Y as Subset of HP-WFF;
take Z;
thus thesis 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 object holds a in Y iff a in Z
proof
let a be object;
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 thesis by A2;
end;
hence thesis by TARSKI:2;
end;
end;
definition
func HP_TAUT -> Subset of HP-WFF equals
CnPos({}(HP-WFF));
correctness;
end;
theorem Th1:
VERUM in CnPos (X)
proof
T is Hilbert_theory & X c= T implies VERUM in T;
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;
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;
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;
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;
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;
hence thesis by Def11;
end;
theorem Th7:
p in CnPos(X) & p => q in CnPos(X) implies q in CnPos(X)
proof
assume that
A1: p in CnPos(X) and
A2: p => q in CnPos(X);
T is Hilbert_theory & X c= T implies q in T
proof
assume that
A3: T is Hilbert_theory and
A4: X c= T;
A5: p => q in T by A2,A3,A4,Def11;
p in T by A1,A3,A4,Def11;
hence thesis by A3,A5;
end;
hence thesis by Def11;
end;
theorem Th8:
T is Hilbert_theory & X c= T implies CnPos(X) c= T
by Def11;
theorem Th9:
X c= CnPos(X)
proof
let a be object;
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 thesis 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 object;
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;
hence thesis by A2,A3,Def11;
end;
hence thesis by Def11;
end;
end;
Lm2: CnPos(CnPos(X)) c= CnPos(X)
proof
let a be object;
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 thesis by A1,A2,Def11;
end;
hence thesis by Def11;
end;
theorem
CnPos(CnPos(X)) = CnPos(X)
proof
A1: CnPos(X) c= CnPos(CnPos(X)) by Th9;
CnPos(CnPos(X)) c= CnPos(X) by Lm2;
hence thesis by A1,XBOOLE_0:def 10;
end;
Lm3: CnPos(X) is Hilbert_theory
by Th1,Th4,Th3,Th5,Th6,Th2,Th7;
registration
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: CnPos(T) c= T
by A1,Def11;
T c= CnPos(T) by Th9;
hence CnPos(T) = T by A2,XBOOLE_0:def 10;
end;
thus thesis;
end;
theorem
T is Hilbert_theory implies HP_TAUT c= T
proof
assume
A1: T is Hilbert_theory;
HP_TAUT c= CnPos(T) by Th10,XBOOLE_1:2;
hence thesis by A1,Th12;
end;
registration
cluster HP_TAUT -> Hilbert_theory;
coherence;
end;
begin :: The tautologies of the Hilbert calculus - implicational part
theorem Th14:
p => p in HP_TAUT
proof
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 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 by Th1,Th15;
theorem
(p => q) => (p => p) in HP_TAUT by Th14,Th15;
theorem
(q => p) => (p => p) in HP_TAUT by Th14,Th15;
theorem Th19:
(q => r) => ((p => q) => (p => r)) in HP_TAUT
proof
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 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;
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 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 thesis 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 thesis 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))) 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 thesis by A1,Def10;
end;
theorem
((p => q) => r) => (q => r) in HP_TAUT
proof
A1: (q => (p => q)) => (((p => q) => r) => (q => r)) in HP_TAUT by Th21;
q => (p => q) in HP_TAUT by Def10;
hence thesis by A1,Def10;
end;
theorem Th26: :: Contraposition
(p => (q => r)) => (q => (p => r)) in HP_TAUT
proof
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 thesis by Th20;
end;
theorem Th27: :: A Hilbert axiom
(p => (p => q)) => (p => q) in HP_TAUT
proof
(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 thesis by A1,Def10;
end;
theorem :: Modus ponendo ponens
q => ((q => p) => p) in HP_TAUT
proof
A1: ((q => p) => (q => p)) => (q => ((q => p) => p)) in HP_TAUT by Th26;
(q => p) => (q => p) in HP_TAUT by Th14;
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 that
A1: s => (q => p) in HP_TAUT and
A2: 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 A2,Def10;
end;
begin :: Conjunctional part of the calculus
theorem Th30:
p => (p '&' p) in HP_TAUT
proof
A1: (p => (p => (p '&' p))) => (p => (p '&' p)) in HP_TAUT by Th27;
p => (p => (p '&' p)) in HP_TAUT by Def10;
hence thesis by A1,Def10;
end;
theorem Th31:
(p '&' q) in HP_TAUT iff p in HP_TAUT & q in HP_TAUT
proof
hereby
A1: (p '&' q) => q in HP_TAUT by Def10;
assume
A2: p '&' 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;
end;
assume that
A3: p in HP_TAUT and
A4: q in HP_TAUT;
p => (q => (p '&' q)) in HP_TAUT by Def10;
then q => (p '&' q) in HP_TAUT by A3,Def10;
hence thesis by A4,Def10;
end;
theorem
(p '&' q) in HP_TAUT implies (q '&' p) in HP_TAUT
proof
assume
A1: p '&' q in HP_TAUT;
then
A2: q in HP_TAUT by Th31;
p in HP_TAUT by A1,Th31;
hence thesis by A2,Th31;
end;
theorem Th33:
(( p '&' q ) => r ) => ( p => ( q => r )) in HP_TAUT
proof
set qp = ( q => ( p '&' q ));
set pr = (( p '&' q ) => r) => ( q => r );
A1: ( p => ( qp => pr )) => ( ( p => qp ) => ( p => pr )) 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 => qp ) => ( p => pr )) 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 thesis by A3,Def10;
end;
theorem Th34:
( p => ( q => r )) => (( p '&' q ) => r ) in HP_TAUT
proof
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 thesis by A4,Th23;
end;
theorem Th35:
( r => p ) => (( r => q ) => ( r => ( p '&' q ))) in HP_TAUT
proof
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 thesis by A1,Th23;
end;
theorem Th36:
( (p => q) '&' p ) => q in HP_TAUT
proof
set P = p => q;
A1: P => P in HP_TAUT by Th14;
( P => P ) => (( P '&' p ) => q ) in HP_TAUT by Th34;
hence thesis by A1,Def10;
end;
theorem
(( (p => q) '&' p ) '&' s ) => q in HP_TAUT
proof
set P = (p => q) '&' p;
A1: P => q in HP_TAUT by Th36;
(P '&' s) => P in HP_TAUT by Def10;
hence thesis by A1,Th23;
end;
theorem
(q => s) => (( p '&' q ) => s) in HP_TAUT
proof
set P = p '&' q;
A1: P => q in HP_TAUT by Def10;
(P => q) => ((q => s) => (P => s)) in HP_TAUT by Th21;
hence thesis by A1,Def10;
end;
theorem Th39:
(q => s) => (( q '&' p ) => s) in HP_TAUT
proof
set P = q '&' p;
A1: P => q in HP_TAUT by Def10;
(P => q) => ((q => s) => (P => s)) in HP_TAUT by Th21;
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 => q ) => (( P => s ) => ( P => ( q '&' s ))) in HP_TAUT by Th35;
P => s in HP_TAUT by Def10;
hence thesis by A1,Th29;
end;
theorem Th41:
( p => q ) => ((p '&' s) => (q '&' s)) in HP_TAUT
proof
A1: ( (p '&' s) => q ) => ((p '&' s) => (q '&' s)) in HP_TAUT by Th40;
(p => q) => (( p '&' s ) => q) in HP_TAUT by Th39;
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) in HP_TAUT by Th41;
( P => ( Q => S )) => (( P '&' Q ) => S ) in HP_TAUT by Th34;
hence thesis by A1,Def10;
end;
theorem Th43:
( p '&' q ) => ( q '&' p ) in HP_TAUT
proof
set P = p '&' q;
A1: P => q in HP_TAUT by Def10;
A2: P => p in HP_TAUT by Def10;
( P => q ) => (( P => p ) => ( P => ( q '&' p ))) in HP_TAUT by Th35;
then ( P => p ) => ( P => ( q '&' p )) in HP_TAUT by A1,Def10;
hence thesis by A2,Def10;
end;
theorem Th44:
( p => q ) '&' ( p '&' s ) => ( s '&' q ) in HP_TAUT
proof
A1: ( q '&' s ) => ( s '&' q ) in HP_TAUT by Th43;
( p => q ) '&' ( p '&' s ) => ( q '&' s ) in HP_TAUT by Th42;
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 in HP_TAUT by Th44;
(( P '&' Q ) => S ) => ( P => ( Q => S )) in HP_TAUT by Th33;
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) in HP_TAUT by Th45;
A2: T => Q in HP_TAUT by Th43;
(P => (Q => S)) => ((T => Q) => (P => (T => S))) in HP_TAUT by Th24;
then (T => Q) => (P => (T => S)) in HP_TAUT by A1,Def10;
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 in HP_TAUT by Th43;
( P => Q ) => (( p '&' P ) => ( p '&' Q )) in HP_TAUT by Th46;
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) in HP_TAUT by Th35;
( P => ( Q => S )) => (( P '&' Q ) => S ) in HP_TAUT by Th34;
hence thesis by A1,Def10;
end;
Lm5: ( (p '&' q) '&' s ) => q in HP_TAUT
proof
A1: (p '&' q) => q in HP_TAUT by Def10;
((p '&' q) '&' s) => (p '&' 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 in HP_TAUT by Lm5;
( P => q ) => (( P '&' P ) => ( P '&' q )) in HP_TAUT by Th46;
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 ) '&' q
in HP_TAUT by Lm6;
( (p '&' q) '&' s ) => ( (p '&' q) '&' s ) '&' ( (p '&' q) '&' s ) in
HP_TAUT by Th30;
hence thesis by A1,Th23;
end;
Lm8: (p '&' q) '&' s => (p '&' s) in HP_TAUT
proof
set P = p '&' q;
A1: P => p in HP_TAUT by Def10;
( P => p ) => ((P '&' s) => (p '&' s)) in HP_TAUT by Th41;
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 in HP_TAUT by Lm8;
( P => Q ) => ((P '&' q) => (Q '&' q)) in HP_TAUT by Th41;
hence thesis by A1,Def10;
end;
Lm10: (p '&' q) '&' s => (p '&' s) '&' q in HP_TAUT
proof
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 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 in HP_TAUT by Th43;
( P => Q ) => ((P '&' q) => (Q '&' q)) in HP_TAUT by Th41;
hence thesis by A1,Def10;
end;
Lm12: (p '&' q) '&' s => (s '&' p) '&' q in HP_TAUT
proof
A1: (p '&' s) '&' q => (s '&' p) '&' q in HP_TAUT by Lm11;
(p '&' q) '&' s => (p '&' s) '&' q in HP_TAUT by Lm10;
hence thesis by A1,Th23;
end;
Lm13: (p '&' q) '&' s => (s '&' q) '&' p in HP_TAUT
proof
A1: (s '&' p) '&' q => (s '&' q) '&' p in HP_TAUT by Lm10;
(p '&' q) '&' s => (s '&' p) '&' q in HP_TAUT by Lm12;
hence thesis by A1,Th23;
end;
Lm14: (p '&' q) '&' s => p '&' (s '&' q) in HP_TAUT
proof
A1: (s '&' q) '&' p => p '&' (s '&' q) in HP_TAUT by Th43;
(p '&' q) '&' s => (s '&' q) '&' p in HP_TAUT by Lm13;
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: s '&' q => q '&' s in HP_TAUT by Th43;
( P => Q ) => (( p '&' P ) => ( p '&' Q )) in HP_TAUT by Th46;
hence thesis by A1,Def10;
end;
theorem
(p '&' q) '&' s => p '&' (q '&' s) in HP_TAUT
proof
A1: p '&' (s '&' q) => p '&' (q '&' s) in HP_TAUT by Lm15;
(p '&' q) '&' s => p '&' (s '&' q) in HP_TAUT by Lm14;
hence thesis by A1,Th23;
end;
Lm16: p '&' (q '&' s) => (s '&' q) '&' p in HP_TAUT
proof
A1: p '&' (s '&' q) => (s '&' q) '&' p in HP_TAUT by Th43;
p '&' (q '&' s) => p '&' (s '&' q) in HP_TAUT by Lm15;
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: s '&' q => q '&' s in HP_TAUT by Th43;
( P => Q ) => ((P '&' p) => (Q '&' p)) in HP_TAUT by Th41;
hence thesis by A1,Def10;
end;
Lm18: p '&' (q '&' s) => (q '&' s) '&' p in HP_TAUT
proof
A1: (s '&' q) '&' p => (q '&' s) '&' p in HP_TAUT by Lm17;
p '&' (q '&' s) => (s '&' q) '&' p in HP_TAUT by Lm16;
hence thesis by A1,Th23;
end;
Lm19: p '&' (q '&' s) => (p '&' s) '&' q in HP_TAUT
proof
A1: (q '&' s) '&' p => (p '&' s) '&' q in HP_TAUT by Lm13;
p '&' (q '&' s) => (q '&' s) '&' p in HP_TAUT by Lm18;
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: q '&' s => s '&' q in HP_TAUT by Th43;
( P => Q ) => (( p '&' P ) => ( p '&' Q )) in HP_TAUT by Th46;
hence thesis by A1,Def10;
end;
theorem
p '&' (q '&' s) => (p '&' q) '&' s in HP_TAUT
proof
A1: p '&' (s '&' q) => (p '&' q) '&' s in HP_TAUT by Lm19;
p '&' (q '&' s) => p '&' (s '&' q) in HP_TAUT by Lm20;
hence thesis by A1,Th23;
end;