:: INTPRO_1 semantic presentation
begin
definition
let E be set ;
attrE is with_FALSUM means :Def1: :: INTPRO_1:def 1
<*0*> in E;
end;
:: deftheorem Def1 defines with_FALSUM INTPRO_1:def_1_:_
for E being set holds
( E is with_FALSUM iff <*0*> in E );
definition
let E be set ;
attrE is with_int_implication means :Def2: :: INTPRO_1:def 2
for p, q being FinSequence st p in E & q in E holds
(<*1*> ^ p) ^ q in E;
end;
:: deftheorem Def2 defines with_int_implication INTPRO_1:def_2_:_
for E being set holds
( E is with_int_implication iff for p, q being FinSequence st p in E & q in E holds
(<*1*> ^ p) ^ q in E );
definition
let E be set ;
attrE is with_int_conjunction means :Def3: :: INTPRO_1:def 3
for p, q being FinSequence st p in E & q in E holds
(<*2*> ^ p) ^ q in E;
end;
:: deftheorem Def3 defines with_int_conjunction INTPRO_1:def_3_:_
for E being set holds
( E is with_int_conjunction iff for p, q being FinSequence st p in E & q in E holds
(<*2*> ^ p) ^ q in E );
definition
let E be set ;
attrE is with_int_disjunction means :Def4: :: INTPRO_1:def 4
for p, q being FinSequence st p in E & q in E holds
(<*3*> ^ p) ^ q in E;
end;
:: deftheorem Def4 defines with_int_disjunction INTPRO_1:def_4_:_
for E being set holds
( E is with_int_disjunction iff for p, q being FinSequence st p in E & q in E holds
(<*3*> ^ p) ^ q in E );
definition
let E be set ;
attrE is with_int_propositional_variables means :Def5: :: INTPRO_1:def 5
for n being Element of NAT holds <*(5 + (2 * n))*> in E;
end;
:: deftheorem Def5 defines with_int_propositional_variables INTPRO_1:def_5_:_
for E being set holds
( E is with_int_propositional_variables iff for n being Element of NAT holds <*(5 + (2 * n))*> in E );
definition
let E be set ;
attrE is with_modal_operator means :Def6: :: INTPRO_1:def 6
for p being FinSequence st p in E holds
<*6*> ^ p in E;
end;
:: deftheorem Def6 defines with_modal_operator INTPRO_1:def_6_:_
for E being set holds
( E is with_modal_operator iff for p being FinSequence st p in E holds
<*6*> ^ p in E );
definition
let E be set ;
attrE is MC-closed means :Def7: :: INTPRO_1:def 7
( E c= NAT * & E is with_FALSUM & E is with_int_implication & E is with_int_conjunction & E is with_int_disjunction & E is with_int_propositional_variables & E is with_modal_operator );
end;
:: deftheorem Def7 defines MC-closed INTPRO_1:def_7_:_
for E being set holds
( E is MC-closed iff ( E c= NAT * & E is with_FALSUM & E is with_int_implication & E is with_int_conjunction & E is with_int_disjunction & E is with_int_propositional_variables & E is with_modal_operator ) );
Lm1: for E being set st E is MC-closed holds
not E is empty
proof
let E be set ; ::_thesis: ( E is MC-closed implies not E is empty )
assume E is MC-closed ; ::_thesis: not E is empty
then E is with_FALSUM by Def7;
hence not E is empty by Def1; ::_thesis: verum
end;
registration
cluster MC-closed -> non empty with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator for set ;
coherence
for b1 being set st b1 is MC-closed holds
( b1 is with_FALSUM & b1 is with_int_implication & b1 is with_int_conjunction & b1 is with_int_disjunction & b1 is with_int_propositional_variables & b1 is with_modal_operator & not b1 is empty ) by Def7, Lm1;
cluster with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator -> MC-closed for Element of K6((NAT *));
coherence
for b1 being Subset of (NAT *) st b1 is with_FALSUM & b1 is with_int_implication & b1 is with_int_conjunction & b1 is with_int_disjunction & b1 is with_int_propositional_variables & b1 is with_modal_operator holds
b1 is MC-closed by Def7;
end;
definition
func MC-wff -> set means :Def8: :: INTPRO_1:def 8
( it is MC-closed & ( for E being set st E is MC-closed holds
it c= E ) );
existence
ex b1 being set st
( b1 is MC-closed & ( for E being set st E is MC-closed holds
b1 c= E ) )
proof
A1: <*0*> in NAT * by FINSEQ_1:def_11;
defpred S1[ set ] means for E being set st E is MC-closed holds
$1 in E;
consider E0 being set such that
A2: for x being set holds
( x in E0 iff ( x in NAT * & S1[x] ) ) from XBOOLE_0:sch_1();
A3: for E being set st E is MC-closed holds
<*0*> in E by Def1;
then reconsider E0 = E0 as non empty set by A2, A1;
take E0 ; ::_thesis: ( E0 is MC-closed & ( for E being set st E is MC-closed holds
E0 c= E ) )
A4: E0 c= NAT *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in E0 or x in NAT * )
thus ( not x in E0 or x in NAT * ) by A2; ::_thesis: verum
end;
for p being FinSequence st p in E0 holds
<*6*> ^ p in E0
proof
let p be FinSequence; ::_thesis: ( p in E0 implies <*6*> ^ p in E0 )
assume A5: p in E0 ; ::_thesis: <*6*> ^ p in E0
p in NAT * by A2, A5;
then reconsider p9 = p as FinSequence of NAT by FINSEQ_1:def_11;
A6: for E being set st E is MC-closed holds
<*6*> ^ p in E
proof
let E be set ; ::_thesis: ( E is MC-closed implies <*6*> ^ p in E )
assume A7: E is MC-closed ; ::_thesis: <*6*> ^ p in E
then p in E by A2, A5;
hence <*6*> ^ p in E by A7, Def6; ::_thesis: verum
end;
<*6*> ^ p9 in NAT * by FINSEQ_1:def_11;
hence <*6*> ^ p in E0 by A2, A6; ::_thesis: verum
end;
then A8: E0 is with_modal_operator by Def6;
for n being Element of NAT holds <*(5 + (2 * n))*> in E0
proof
let n be Element of NAT ; ::_thesis: <*(5 + (2 * n))*> in E0
set p = 5 + (2 * n);
reconsider h = <*(5 + (2 * n))*> as FinSequence of NAT ;
A9: h in NAT * by FINSEQ_1:def_11;
for E being set st E is MC-closed holds
<*(5 + (2 * n))*> in E by Def5;
hence <*(5 + (2 * n))*> in E0 by A2, A9; ::_thesis: verum
end;
then A10: E0 is with_int_propositional_variables by Def5;
for p, q being FinSequence st p in E0 & q in E0 holds
(<*3*> ^ p) ^ q in E0
proof
let p, q be FinSequence; ::_thesis: ( p in E0 & q in E0 implies (<*3*> ^ p) ^ q in E0 )
assume that
A11: p in E0 and
A12: q in E0 ; ::_thesis: (<*3*> ^ p) ^ q in E0
A13: q in NAT * by A2, A12;
A14: for E being set st E is MC-closed holds
(<*3*> ^ p) ^ q in E
proof
let E be set ; ::_thesis: ( E is MC-closed implies (<*3*> ^ p) ^ q in E )
assume A15: E is MC-closed ; ::_thesis: (<*3*> ^ p) ^ q in E
then A16: q in E by A2, A12;
p in E by A2, A11, A15;
hence (<*3*> ^ p) ^ q in E by A15, A16, Def4; ::_thesis: verum
end;
p in NAT * by A2, A11;
then reconsider p9 = p, q9 = q as FinSequence of NAT by A13, FINSEQ_1:def_11;
(<*3*> ^ p9) ^ q9 in NAT * by FINSEQ_1:def_11;
hence (<*3*> ^ p) ^ q in E0 by A2, A14; ::_thesis: verum
end;
then A17: E0 is with_int_disjunction by Def4;
for p, q being FinSequence st p in E0 & q in E0 holds
(<*2*> ^ p) ^ q in E0
proof
let p, q be FinSequence; ::_thesis: ( p in E0 & q in E0 implies (<*2*> ^ p) ^ q in E0 )
assume that
A18: p in E0 and
A19: q in E0 ; ::_thesis: (<*2*> ^ p) ^ q in E0
A20: q in NAT * by A2, A19;
A21: for E being set st E is MC-closed holds
(<*2*> ^ p) ^ q in E
proof
let E be set ; ::_thesis: ( E is MC-closed implies (<*2*> ^ p) ^ q in E )
assume A22: E is MC-closed ; ::_thesis: (<*2*> ^ p) ^ q in E
then A23: q in E by A2, A19;
p in E by A2, A18, A22;
hence (<*2*> ^ p) ^ q in E by A22, A23, Def3; ::_thesis: verum
end;
p in NAT * by A2, A18;
then reconsider p9 = p, q9 = q as FinSequence of NAT by A20, FINSEQ_1:def_11;
(<*2*> ^ p9) ^ q9 in NAT * by FINSEQ_1:def_11;
hence (<*2*> ^ p) ^ q in E0 by A2, A21; ::_thesis: verum
end;
then A24: E0 is with_int_conjunction by Def3;
for p, q being FinSequence st p in E0 & q in E0 holds
(<*1*> ^ p) ^ q in E0
proof
let p, q be FinSequence; ::_thesis: ( p in E0 & q in E0 implies (<*1*> ^ p) ^ q in E0 )
assume that
A25: p in E0 and
A26: q in E0 ; ::_thesis: (<*1*> ^ p) ^ q in E0
A27: q in NAT * by A2, A26;
A28: for E being set st E is MC-closed holds
(<*1*> ^ p) ^ q in E
proof
let E be set ; ::_thesis: ( E is MC-closed implies (<*1*> ^ p) ^ q in E )
assume A29: E is MC-closed ; ::_thesis: (<*1*> ^ p) ^ q in E
then A30: q in E by A2, A26;
p in E by A2, A25, A29;
hence (<*1*> ^ p) ^ q in E by A29, A30, Def2; ::_thesis: verum
end;
p in NAT * by A2, A25;
then reconsider p9 = p, q9 = q as FinSequence of NAT by A27, FINSEQ_1:def_11;
(<*1*> ^ p9) ^ q9 in NAT * by FINSEQ_1:def_11;
hence (<*1*> ^ p) ^ q in E0 by A2, A28; ::_thesis: verum
end;
then A31: E0 is with_int_implication by Def2;
<*0*> in E0 by A2, A1, A3;
then E0 is with_FALSUM by Def1;
hence E0 is MC-closed by A4, A10, A31, A24, A17, A8; ::_thesis: for E being set st E is MC-closed holds
E0 c= E
let E be set ; ::_thesis: ( E is MC-closed implies E0 c= E )
assume A32: E is MC-closed ; ::_thesis: E0 c= E
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in E0 or x in E )
assume x in E0 ; ::_thesis: x in E
hence x in E by A2, A32; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st b1 is MC-closed & ( for E being set st E is MC-closed holds
b1 c= E ) & b2 is MC-closed & ( for E being set st E is MC-closed holds
b2 c= E ) holds
b1 = b2
proof
let E1, E2 be set ; ::_thesis: ( E1 is MC-closed & ( for E being set st E is MC-closed holds
E1 c= E ) & E2 is MC-closed & ( for E being set st E is MC-closed holds
E2 c= E ) implies E1 = E2 )
assume that
A33: E1 is MC-closed and
A34: for E being set st E is MC-closed holds
E1 c= E and
A35: E2 is MC-closed and
A36: for E being set st E is MC-closed holds
E2 c= E ; ::_thesis: E1 = E2
A37: E2 c= E1 by A33, A36;
E1 c= E2 by A34, A35;
hence E1 = E2 by A37, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines MC-wff INTPRO_1:def_8_:_
for b1 being set holds
( b1 = MC-wff iff ( b1 is MC-closed & ( for E being set st E is MC-closed holds
b1 c= E ) ) );
registration
cluster MC-wff -> MC-closed ;
coherence
MC-wff is MC-closed by Def8;
end;
registration
cluster non empty MC-closed for set ;
existence
ex b1 being set st
( b1 is MC-closed & not b1 is empty )
proof
take MC-wff ; ::_thesis: ( MC-wff is MC-closed & not MC-wff is empty )
thus ( MC-wff is MC-closed & not MC-wff is empty ) ; ::_thesis: verum
end;
end;
registration
cluster MC-wff -> functional ;
coherence
MC-wff is functional
proof
MC-wff c= NAT * by Def7;
hence MC-wff is functional ; ::_thesis: verum
end;
end;
registration
cluster -> FinSequence-like for Element of MC-wff ;
coherence
for b1 being Element of MC-wff holds b1 is FinSequence-like
proof
let p be Element of MC-wff ; ::_thesis: p is FinSequence-like
MC-wff c= NAT * by Def7;
hence p is FinSequence-like ; ::_thesis: verum
end;
end;
definition
mode MC-formula is Element of MC-wff ;
end;
definition
func FALSUM -> MC-formula equals :: INTPRO_1:def 9
<*0*>;
correctness
coherence
<*0*> is MC-formula;
by Def1;
let p, q be Element of MC-wff ;
funcp => q -> MC-formula equals :: INTPRO_1:def 10
(<*1*> ^ p) ^ q;
correctness
coherence
(<*1*> ^ p) ^ q is MC-formula;
by Def2;
funcp '&' q -> MC-formula equals :: INTPRO_1:def 11
(<*2*> ^ p) ^ q;
correctness
coherence
(<*2*> ^ p) ^ q is MC-formula;
by Def3;
funcp 'or' q -> MC-formula equals :: INTPRO_1:def 12
(<*3*> ^ p) ^ q;
correctness
coherence
(<*3*> ^ p) ^ q is MC-formula;
by Def4;
end;
:: deftheorem defines FALSUM INTPRO_1:def_9_:_
FALSUM = <*0*>;
:: deftheorem defines => INTPRO_1:def_10_:_
for p, q being Element of MC-wff holds p => q = (<*1*> ^ p) ^ q;
:: deftheorem defines '&' INTPRO_1:def_11_:_
for p, q being Element of MC-wff holds p '&' q = (<*2*> ^ p) ^ q;
:: deftheorem defines 'or' INTPRO_1:def_12_:_
for p, q being Element of MC-wff holds p 'or' q = (<*3*> ^ p) ^ q;
definition
let p be Element of MC-wff ;
func Nes p -> MC-formula equals :: INTPRO_1:def 13
<*6*> ^ p;
correctness
coherence
<*6*> ^ p is MC-formula;
by Def6;
end;
:: deftheorem defines Nes INTPRO_1:def_13_:_
for p being Element of MC-wff holds Nes p = <*6*> ^ p;
definition
let T be Subset of MC-wff;
attrT is IPC_theory means :Def14: :: INTPRO_1:def 14
for p, q, r being Element of MC-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 => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & ( p in T & p => q in T implies q in T ) );
correctness
;
end;
:: deftheorem Def14 defines IPC_theory INTPRO_1:def_14_:_
for T being Subset of MC-wff holds
( T is IPC_theory iff for p, q, r being Element of MC-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 => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & ( p in T & p => q in T implies q in T ) ) );
definition
let X be Subset of MC-wff;
func CnIPC X -> Subset of MC-wff means :Def15: :: INTPRO_1:def 15
for r being Element of MC-wff holds
( r in it iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T );
existence
ex b1 being Subset of MC-wff st
for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T )
proof
defpred S1[ set ] means for T being Subset of MC-wff st T is IPC_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 MC-wff & S1[a] ) ) from XBOOLE_0:sch_1();
Y c= MC-wff
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in MC-wff )
assume a in Y ; ::_thesis: a in MC-wff
hence a in MC-wff by A1; ::_thesis: verum
end;
then reconsider Z = Y as Subset of MC-wff ;
take Z ; ::_thesis: for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T )
thus for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of MC-wff st ( for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) ) & ( for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) ) holds
b1 = b2
proof
let Y, Z be Subset of MC-wff; ::_thesis: ( ( for r being Element of MC-wff holds
( r in Y iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) ) & ( for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) ) implies Y = Z )
assume that
A2: for r being Element of MC-wff holds
( r in Y iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) and
A3: for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is IPC_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 MC-wff ;
for T being Subset of MC-wff st T is IPC_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 MC-wff ;
for T being Subset of MC-wff st T is IPC_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 Def15 defines CnIPC INTPRO_1:def_15_:_
for X, b2 being Subset of MC-wff holds
( b2 = CnIPC X iff for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) );
definition
func IPC-Taut -> Subset of MC-wff equals :: INTPRO_1:def 16
CnIPC ({} MC-wff);
correctness
coherence
CnIPC ({} MC-wff) is Subset of MC-wff;
;
end;
:: deftheorem defines IPC-Taut INTPRO_1:def_16_:_
IPC-Taut = CnIPC ({} MC-wff);
definition
let p be Element of MC-wff ;
func neg p -> MC-formula equals :: INTPRO_1:def 17
p => FALSUM;
correctness
coherence
p => FALSUM is MC-formula;
;
end;
:: deftheorem defines neg INTPRO_1:def_17_:_
for p being Element of MC-wff holds neg p = p => FALSUM;
definition
func IVERUM -> MC-formula equals :: INTPRO_1:def 18
FALSUM => FALSUM;
correctness
coherence
FALSUM => FALSUM is MC-formula;
;
end;
:: deftheorem defines IVERUM INTPRO_1:def_18_:_
IVERUM = FALSUM => FALSUM;
theorem Th1: :: INTPRO_1:1
for X being Subset of MC-wff
for p, q being Element of MC-wff holds p => (q => p) in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff holds p => (q => p) in CnIPC X
let p, q be Element of MC-wff ; ::_thesis: p => (q => p) in CnIPC X
for T being Subset of MC-wff st T is IPC_theory & X c= T holds
p => (q => p) in T by Def14;
hence p => (q => p) in CnIPC X by Def15; ::_thesis: verum
end;
theorem Th2: :: INTPRO_1:2
for X being Subset of MC-wff
for p, q, r being Element of MC-wff holds (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, q, r being Element of MC-wff holds (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X
let p, q, r be Element of MC-wff ; ::_thesis: (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X
for T being Subset of MC-wff st T is IPC_theory & X c= T holds
(p => (q => r)) => ((p => q) => (p => r)) in T by Def14;
hence (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X by Def15; ::_thesis: verum
end;
theorem Th3: :: INTPRO_1:3
for X being Subset of MC-wff
for p, q being Element of MC-wff holds (p '&' q) => p in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff holds (p '&' q) => p in CnIPC X
let p, q be Element of MC-wff ; ::_thesis: (p '&' q) => p in CnIPC X
for T being Subset of MC-wff st T is IPC_theory & X c= T holds
(p '&' q) => p in T by Def14;
hence (p '&' q) => p in CnIPC X by Def15; ::_thesis: verum
end;
theorem Th4: :: INTPRO_1:4
for X being Subset of MC-wff
for p, q being Element of MC-wff holds (p '&' q) => q in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff holds (p '&' q) => q in CnIPC X
let p, q be Element of MC-wff ; ::_thesis: (p '&' q) => q in CnIPC X
for T being Subset of MC-wff st T is IPC_theory & X c= T holds
(p '&' q) => q in T by Def14;
hence (p '&' q) => q in CnIPC X by Def15; ::_thesis: verum
end;
theorem Th5: :: INTPRO_1:5
for X being Subset of MC-wff
for p, q being Element of MC-wff holds p => (q => (p '&' q)) in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff holds p => (q => (p '&' q)) in CnIPC X
let p, q be Element of MC-wff ; ::_thesis: p => (q => (p '&' q)) in CnIPC X
for T being Subset of MC-wff st T is IPC_theory & X c= T holds
p => (q => (p '&' q)) in T by Def14;
hence p => (q => (p '&' q)) in CnIPC X by Def15; ::_thesis: verum
end;
theorem Th6: :: INTPRO_1:6
for X being Subset of MC-wff
for p, q being Element of MC-wff holds p => (p 'or' q) in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff holds p => (p 'or' q) in CnIPC X
let p, q be Element of MC-wff ; ::_thesis: p => (p 'or' q) in CnIPC X
for T being Subset of MC-wff st T is IPC_theory & X c= T holds
p => (p 'or' q) in T by Def14;
hence p => (p 'or' q) in CnIPC X by Def15; ::_thesis: verum
end;
theorem Th7: :: INTPRO_1:7
for X being Subset of MC-wff
for q, p being Element of MC-wff holds q => (p 'or' q) in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for q, p being Element of MC-wff holds q => (p 'or' q) in CnIPC X
let q, p be Element of MC-wff ; ::_thesis: q => (p 'or' q) in CnIPC X
for T being Subset of MC-wff st T is IPC_theory & X c= T holds
q => (p 'or' q) in T by Def14;
hence q => (p 'or' q) in CnIPC X by Def15; ::_thesis: verum
end;
theorem Th8: :: INTPRO_1:8
for X being Subset of MC-wff
for p, r, q being Element of MC-wff holds (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, r, q being Element of MC-wff holds (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X
let p, r, q be Element of MC-wff ; ::_thesis: (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X
for T being Subset of MC-wff st T is IPC_theory & X c= T holds
(p => r) => ((q => r) => ((p 'or' q) => r)) in T by Def14;
hence (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X by Def15; ::_thesis: verum
end;
theorem Th9: :: INTPRO_1:9
for X being Subset of MC-wff
for p being Element of MC-wff holds FALSUM => p in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p being Element of MC-wff holds FALSUM => p in CnIPC X
let p be Element of MC-wff ; ::_thesis: FALSUM => p in CnIPC X
for T being Subset of MC-wff st T is IPC_theory & X c= T holds
FALSUM => p in T by Def14;
hence FALSUM => p in CnIPC X by Def15; ::_thesis: verum
end;
theorem Th10: :: INTPRO_1:10
for X being Subset of MC-wff
for p, q being Element of MC-wff st p in CnIPC X & p => q in CnIPC X holds
q in CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff st p in CnIPC X & p => q in CnIPC X holds
q in CnIPC X
let p, q be Element of MC-wff ; ::_thesis: ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X )
assume that
A1: p in CnIPC X and
A2: p => q in CnIPC X ; ::_thesis: q in CnIPC X
for T being Subset of MC-wff st T is IPC_theory & X c= T holds
q in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is IPC_theory & X c= T implies q in T )
assume that
A3: T is IPC_theory and
A4: X c= T ; ::_thesis: q in T
A5: p => q in T by A2, A3, A4, Def15;
p in T by A1, A3, A4, Def15;
hence q in T by A3, A5, Def14; ::_thesis: verum
end;
hence q in CnIPC X by Def15; ::_thesis: verum
end;
theorem Th11: :: INTPRO_1:11
for T, X being Subset of MC-wff st T is IPC_theory & X c= T holds
CnIPC X c= T
proof
let T, X be Subset of MC-wff; ::_thesis: ( T is IPC_theory & X c= T implies CnIPC X c= T )
assume that
A1: T is IPC_theory and
A2: X c= T ; ::_thesis: CnIPC X c= T
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnIPC X or a in T )
thus ( not a in CnIPC X or a in T ) by A1, A2, Def15; ::_thesis: verum
end;
theorem Th12: :: INTPRO_1:12
for X being Subset of MC-wff holds X c= CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: X c= CnIPC X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in CnIPC X )
assume A1: a in X ; ::_thesis: a in CnIPC X
then reconsider t = a as Element of MC-wff ;
for T being Subset of MC-wff st T is IPC_theory & X c= T holds
t in T by A1;
hence a in CnIPC X by Def15; ::_thesis: verum
end;
theorem Th13: :: INTPRO_1:13
for X, Y being Subset of MC-wff st X c= Y holds
CnIPC X c= CnIPC Y
proof
let X, Y be Subset of MC-wff; ::_thesis: ( X c= Y implies CnIPC X c= CnIPC Y )
assume A1: X c= Y ; ::_thesis: CnIPC X c= CnIPC Y
thus CnIPC X c= CnIPC Y ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnIPC X or a in CnIPC Y )
assume A2: a in CnIPC X ; ::_thesis: a in CnIPC Y
then reconsider t = a as Element of MC-wff ;
for T being Subset of MC-wff st T is IPC_theory & Y c= T holds
t in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is IPC_theory & Y c= T implies t in T )
assume that
A3: T is IPC_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, Def15; ::_thesis: verum
end;
hence a in CnIPC Y by Def15; ::_thesis: verum
end;
end;
Lm2: for X being Subset of MC-wff holds CnIPC (CnIPC X) c= CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: CnIPC (CnIPC X) c= CnIPC X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnIPC (CnIPC X) or a in CnIPC X )
assume A1: a in CnIPC (CnIPC X) ; ::_thesis: a in CnIPC X
then reconsider t = a as Element of MC-wff ;
for T being Subset of MC-wff st T is IPC_theory & X c= T holds
t in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is IPC_theory & X c= T implies t in T )
assume that
A2: T is IPC_theory and
A3: X c= T ; ::_thesis: t in T
CnIPC X c= T by A2, A3, Th11;
hence t in T by A1, A2, Def15; ::_thesis: verum
end;
hence a in CnIPC X by Def15; ::_thesis: verum
end;
theorem :: INTPRO_1:14
for X being Subset of MC-wff holds CnIPC (CnIPC X) = CnIPC X
proof
let X be Subset of MC-wff; ::_thesis: CnIPC (CnIPC X) = CnIPC X
A1: CnIPC X c= CnIPC (CnIPC X) by Th12;
CnIPC (CnIPC X) c= CnIPC X by Lm2;
hence CnIPC (CnIPC X) = CnIPC X by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm3: for X being Subset of MC-wff holds CnIPC X is IPC_theory
proof
let X be Subset of MC-wff; ::_thesis: CnIPC X is IPC_theory
let p be Element of MC-wff ; :: according to INTPRO_1:def_14 ::_thesis: for q, r being Element of MC-wff holds
( p => (q => p) in CnIPC X & (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X & (p '&' q) => p in CnIPC X & (p '&' q) => q in CnIPC X & p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
let q, r be Element of MC-wff ; ::_thesis: ( p => (q => p) in CnIPC X & (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X & (p '&' q) => p in CnIPC X & (p '&' q) => q in CnIPC X & p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus p => (q => p) in CnIPC X by Th1; ::_thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X & (p '&' q) => p in CnIPC X & (p '&' q) => q in CnIPC X & p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus (p => (q => r)) => ((p => q) => (p => r)) in CnIPC X by Th2; ::_thesis: ( (p '&' q) => p in CnIPC X & (p '&' q) => q in CnIPC X & p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus (p '&' q) => p in CnIPC X by Th3; ::_thesis: ( (p '&' q) => q in CnIPC X & p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus (p '&' q) => q in CnIPC X by Th4; ::_thesis: ( p => (q => (p '&' q)) in CnIPC X & p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus p => (q => (p '&' q)) in CnIPC X by Th5; ::_thesis: ( p => (p 'or' q) in CnIPC X & q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus p => (p 'or' q) in CnIPC X by Th6; ::_thesis: ( q => (p 'or' q) in CnIPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus q => (p 'or' q) in CnIPC X by Th7; ::_thesis: ( (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X & FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X by Th8; ::_thesis: ( FALSUM => p in CnIPC X & ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) )
thus FALSUM => p in CnIPC X by Th9; ::_thesis: ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X )
thus ( p in CnIPC X & p => q in CnIPC X implies q in CnIPC X ) by Th10; ::_thesis: verum
end;
registration
let X be Subset of MC-wff;
cluster CnIPC X -> IPC_theory ;
coherence
CnIPC X is IPC_theory by Lm3;
end;
theorem Th15: :: INTPRO_1:15
for T being Subset of MC-wff holds
( T is IPC_theory iff CnIPC T = T )
proof
let T be Subset of MC-wff; ::_thesis: ( T is IPC_theory iff CnIPC T = T )
hereby ::_thesis: ( CnIPC T = T implies T is IPC_theory )
assume A1: T is IPC_theory ; ::_thesis: CnIPC T = T
A2: CnIPC T c= T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnIPC T or a in T )
assume a in CnIPC T ; ::_thesis: a in T
hence a in T by A1, Def15; ::_thesis: verum
end;
T c= CnIPC T by Th12;
hence CnIPC T = T by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
thus ( CnIPC T = T implies T is IPC_theory ) ; ::_thesis: verum
end;
theorem :: INTPRO_1:16
for T being Subset of MC-wff st T is IPC_theory holds
IPC-Taut c= T
proof
let T be Subset of MC-wff; ::_thesis: ( T is IPC_theory implies IPC-Taut c= T )
assume A1: T is IPC_theory ; ::_thesis: IPC-Taut c= T
IPC-Taut c= CnIPC T by Th13, XBOOLE_1:2;
hence IPC-Taut c= T by A1, Th15; ::_thesis: verum
end;
registration
cluster IPC-Taut -> IPC_theory ;
coherence
IPC-Taut is IPC_theory ;
end;
begin
theorem Th17: :: INTPRO_1:17
for p being Element of MC-wff holds p => p in IPC-Taut
proof
let p be Element of MC-wff ; ::_thesis: p => p in IPC-Taut
A1: p => (p => p) in IPC-Taut by Def14;
A2: p => ((p => p) => p) in IPC-Taut by Def14;
(p => ((p => p) => p)) => ((p => (p => p)) => (p => p)) in IPC-Taut by Def14;
then (p => (p => p)) => (p => p) in IPC-Taut by A2, Def14;
hence p => p in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem Th18: :: INTPRO_1:18
for q, p being Element of MC-wff st q in IPC-Taut holds
p => q in IPC-Taut
proof
let q, p be Element of MC-wff ; ::_thesis: ( q in IPC-Taut implies p => q in IPC-Taut )
q => (p => q) in IPC-Taut by Def14;
hence ( q in IPC-Taut implies p => q in IPC-Taut ) by Def14; ::_thesis: verum
end;
theorem :: INTPRO_1:19
IVERUM in IPC-Taut by Def14;
theorem :: INTPRO_1:20
for p, q being Element of MC-wff holds (p => q) => (p => p) in IPC-Taut by Th17, Th18;
theorem :: INTPRO_1:21
for q, p being Element of MC-wff holds (q => p) => (p => p) in IPC-Taut by Th17, Th18;
theorem Th22: :: INTPRO_1:22
for q, r, p being Element of MC-wff holds (q => r) => ((p => q) => (p => r)) in IPC-Taut
proof
let q, r, p be Element of MC-wff ; ::_thesis: (q => r) => ((p => q) => (p => r)) in IPC-Taut
A1: (p => (q => r)) => ((p => q) => (p => r)) in IPC-Taut by Def14;
A2: ((q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) => (((q => r) => (p => (q => r))) => ((q => r) => ((p => q) => (p => r)))) in IPC-Taut by Def14;
((p => (q => r)) => ((p => q) => (p => r))) => ((q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) in IPC-Taut by Def14;
then (q => r) => ((p => (q => r)) => ((p => q) => (p => r))) in IPC-Taut by A1, Def14;
then A3: ((q => r) => (p => (q => r))) => ((q => r) => ((p => q) => (p => r))) in IPC-Taut by A2, Def14;
(q => r) => (p => (q => r)) in IPC-Taut by Def14;
hence (q => r) => ((p => q) => (p => r)) in IPC-Taut by A3, Def14; ::_thesis: verum
end;
theorem Th23: :: INTPRO_1:23
for p, q, r being Element of MC-wff st p => (q => r) in IPC-Taut holds
q => (p => r) in IPC-Taut
proof
let p, q, r be Element of MC-wff ; ::_thesis: ( p => (q => r) in IPC-Taut implies q => (p => r) in IPC-Taut )
assume A1: p => (q => r) in IPC-Taut ; ::_thesis: q => (p => r) in IPC-Taut
A2: ((p => q) => (p => r)) => ((q => (p => q)) => (q => (p => r))) in IPC-Taut by Th22;
(p => (q => r)) => ((p => q) => (p => r)) in IPC-Taut by Def14;
then (p => q) => (p => r) in IPC-Taut by A1, Def14;
then A3: (q => (p => q)) => (q => (p => r)) in IPC-Taut by A2, Def14;
q => (p => q) in IPC-Taut by Def14;
hence q => (p => r) in IPC-Taut by A3, Def14; ::_thesis: verum
end;
theorem Th24: :: INTPRO_1:24
for p, q, r being Element of MC-wff holds (p => q) => ((q => r) => (p => r)) in IPC-Taut
proof
let p, q, r be Element of MC-wff ; ::_thesis: (p => q) => ((q => r) => (p => r)) in IPC-Taut
(q => r) => ((p => q) => (p => r)) in IPC-Taut by Th22;
hence (p => q) => ((q => r) => (p => r)) in IPC-Taut by Th23; ::_thesis: verum
end;
theorem Th25: :: INTPRO_1:25
for p, q, r being Element of MC-wff st p => q in IPC-Taut holds
(q => r) => (p => r) in IPC-Taut
proof
let p, q, r be Element of MC-wff ; ::_thesis: ( p => q in IPC-Taut implies (q => r) => (p => r) in IPC-Taut )
assume A1: p => q in IPC-Taut ; ::_thesis: (q => r) => (p => r) in IPC-Taut
(p => q) => ((q => r) => (p => r)) in IPC-Taut by Th24;
hence (q => r) => (p => r) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem Th26: :: INTPRO_1:26
for p, q, r being Element of MC-wff st p => q in IPC-Taut & q => r in IPC-Taut holds
p => r in IPC-Taut
proof
let p, q, r be Element of MC-wff ; ::_thesis: ( p => q in IPC-Taut & q => r in IPC-Taut implies p => r in IPC-Taut )
assume that
A1: p => q in IPC-Taut and
A2: q => r in IPC-Taut ; ::_thesis: p => r in IPC-Taut
(p => q) => ((q => r) => (p => r)) in IPC-Taut by Th24;
then (q => r) => (p => r) in IPC-Taut by A1, Def14;
hence p => r in IPC-Taut by A2, Def14; ::_thesis: verum
end;
Lm4: for q, r, p, s being Element of MC-wff holds (((q => r) => (p => r)) => s) => ((p => q) => s) in IPC-Taut
proof
let q, r, p, s be Element of MC-wff ; ::_thesis: (((q => r) => (p => r)) => s) => ((p => q) => s) in IPC-Taut
(p => q) => ((q => r) => (p => r)) in IPC-Taut by Th24;
hence (((q => r) => (p => r)) => s) => ((p => q) => s) in IPC-Taut by Th25; ::_thesis: verum
end;
theorem Th27: :: INTPRO_1:27
for p, q, r, s being Element of MC-wff holds (p => (q => r)) => ((s => q) => (p => (s => r))) in IPC-Taut
proof
let p, q, r, s be Element of MC-wff ; ::_thesis: (p => (q => r)) => ((s => q) => (p => (s => r))) in IPC-Taut
A1: (((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r))) in IPC-Taut by Lm4;
((((q => r) => (s => r)) => (p => (s => r))) => ((s => q) => (p => (s => r)))) => ((p => (q => r)) => ((s => q) => (p => (s => r)))) in IPC-Taut by Lm4;
hence (p => (q => r)) => ((s => q) => (p => (s => r))) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem :: INTPRO_1:28
for p, q, r being Element of MC-wff holds ((p => q) => r) => (q => r) in IPC-Taut
proof
let p, q, r be Element of MC-wff ; ::_thesis: ((p => q) => r) => (q => r) in IPC-Taut
A1: (q => (p => q)) => (((p => q) => r) => (q => r)) in IPC-Taut by Th24;
q => (p => q) in IPC-Taut by Def14;
hence ((p => q) => r) => (q => r) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem Th29: :: INTPRO_1:29
for p, q, r being Element of MC-wff holds (p => (q => r)) => (q => (p => r)) in IPC-Taut
proof
let p, q, r be Element of MC-wff ; ::_thesis: (p => (q => r)) => (q => (p => r)) in IPC-Taut
A1: q => (p => q) in IPC-Taut by Def14;
(p => (q => r)) => ((p => q) => (p => r)) in IPC-Taut by Def14;
then A2: (p => q) => ((p => (q => r)) => (p => r)) in IPC-Taut by Th23;
((p => q) => ((p => (q => r)) => (p => r))) => ((q => (p => q)) => (q => ((p => (q => r)) => (p => r)))) in IPC-Taut by Th22;
then (q => (p => q)) => (q => ((p => (q => r)) => (p => r))) in IPC-Taut by A2, Def14;
then q => ((p => (q => r)) => (p => r)) in IPC-Taut by A1, Def14;
hence (p => (q => r)) => (q => (p => r)) in IPC-Taut by Th23; ::_thesis: verum
end;
theorem Th30: :: INTPRO_1:30
for p, q being Element of MC-wff holds (p => (p => q)) => (p => q) in IPC-Taut
proof
let p, q be Element of MC-wff ; ::_thesis: (p => (p => q)) => (p => q) in IPC-Taut
(p => (p => q)) => ((p => p) => (p => q)) in IPC-Taut by Def14;
then A1: (p => p) => ((p => (p => q)) => (p => q)) in IPC-Taut by Th23;
p => p in IPC-Taut by Th17;
hence (p => (p => q)) => (p => q) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem :: INTPRO_1:31
for q, p being Element of MC-wff holds q => ((q => p) => p) in IPC-Taut
proof
let q, p be Element of MC-wff ; ::_thesis: q => ((q => p) => p) in IPC-Taut
A1: ((q => p) => (q => p)) => (q => ((q => p) => p)) in IPC-Taut by Th29;
(q => p) => (q => p) in IPC-Taut by Th17;
hence q => ((q => p) => p) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem Th32: :: INTPRO_1:32
for s, q, p being Element of MC-wff st s => (q => p) in IPC-Taut & q in IPC-Taut holds
s => p in IPC-Taut
proof
let s, q, p be Element of MC-wff ; ::_thesis: ( s => (q => p) in IPC-Taut & q in IPC-Taut implies s => p in IPC-Taut )
assume that
A1: s => (q => p) in IPC-Taut and
A2: q in IPC-Taut ; ::_thesis: s => p in IPC-Taut
(s => (q => p)) => (q => (s => p)) in IPC-Taut by Th29;
then q => (s => p) in IPC-Taut by A1, Def14;
hence s => p in IPC-Taut by A2, Def14; ::_thesis: verum
end;
begin
theorem Th33: :: INTPRO_1:33
for p being Element of MC-wff holds p => (p '&' p) in IPC-Taut
proof
let p be Element of MC-wff ; ::_thesis: p => (p '&' p) in IPC-Taut
A1: (p => (p => (p '&' p))) => (p => (p '&' p)) in IPC-Taut by Th30;
p => (p => (p '&' p)) in IPC-Taut by Def14;
hence p => (p '&' p) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem Th34: :: INTPRO_1:34
for p, q being Element of MC-wff holds
( p '&' q in IPC-Taut iff ( p in IPC-Taut & q in IPC-Taut ) )
proof
let p, q be Element of MC-wff ; ::_thesis: ( p '&' q in IPC-Taut iff ( p in IPC-Taut & q in IPC-Taut ) )
hereby ::_thesis: ( p in IPC-Taut & q in IPC-Taut implies p '&' q in IPC-Taut )
A1: (p '&' q) => q in IPC-Taut by Def14;
assume A2: p '&' q in IPC-Taut ; ::_thesis: ( p in IPC-Taut & q in IPC-Taut )
(p '&' q) => p in IPC-Taut by Def14;
hence ( p in IPC-Taut & q in IPC-Taut ) by A2, A1, Def14; ::_thesis: verum
end;
assume that
A3: p in IPC-Taut and
A4: q in IPC-Taut ; ::_thesis: p '&' q in IPC-Taut
p => (q => (p '&' q)) in IPC-Taut by Def14;
then q => (p '&' q) in IPC-Taut by A3, Def14;
hence p '&' q in IPC-Taut by A4, Def14; ::_thesis: verum
end;
theorem :: INTPRO_1:35
for p, q being Element of MC-wff holds
( p '&' q in IPC-Taut iff q '&' p in IPC-Taut )
proof
let p, q be Element of MC-wff ; ::_thesis: ( p '&' q in IPC-Taut iff q '&' p in IPC-Taut )
hereby ::_thesis: ( q '&' p in IPC-Taut implies p '&' q in IPC-Taut )
assume A1: p '&' q in IPC-Taut ; ::_thesis: q '&' p in IPC-Taut
then A2: q in IPC-Taut by Th34;
p in IPC-Taut by A1, Th34;
hence q '&' p in IPC-Taut by A2, Th34; ::_thesis: verum
end;
assume A3: q '&' p in IPC-Taut ; ::_thesis: p '&' q in IPC-Taut
then A4: p in IPC-Taut by Th34;
q in IPC-Taut by A3, Th34;
hence p '&' q in IPC-Taut by A4, Th34; ::_thesis: verum
end;
theorem Th36: :: INTPRO_1:36
for p, q, r being Element of MC-wff holds ((p '&' q) => r) => (p => (q => r)) in IPC-Taut
proof
let p, q, r be Element of MC-wff ; ::_thesis: ((p '&' q) => r) => (p => (q => r)) in IPC-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 IPC-Taut by Def14;
A2: p => (q => (p '&' q)) in IPC-Taut by Def14;
p => ((q => (p '&' q)) => (((p '&' q) => r) => (q => r))) in IPC-Taut by Th18, Th24;
then (p => (q => (p '&' q))) => (p => (((p '&' q) => r) => (q => r))) in IPC-Taut by A1, Def14;
then A3: p => (((p '&' q) => r) => (q => r)) in IPC-Taut by A2, Def14;
(p => (((p '&' q) => r) => (q => r))) => (((p '&' q) => r) => (p => (q => r))) in IPC-Taut by Th29;
hence ((p '&' q) => r) => (p => (q => r)) in IPC-Taut by A3, Def14; ::_thesis: verum
end;
theorem Th37: :: INTPRO_1:37
for p, q, r being Element of MC-wff holds (p => (q => r)) => ((p '&' q) => r) in IPC-Taut
proof
let p, q, r be Element of MC-wff ; ::_thesis: (p => (q => r)) => ((p '&' q) => r) in IPC-Taut
A1: ((p '&' q) => q) => ((q => r) => ((p '&' q) => r)) in IPC-Taut by Th24;
(p '&' q) => q in IPC-Taut by Def14;
then (q => r) => ((p '&' q) => r) in IPC-Taut by A1, Def14;
then A2: p => ((q => r) => ((p '&' q) => r)) in IPC-Taut by Th18;
A3: (p => ((p '&' q) => r)) => ((p '&' q) => (p => r)) in IPC-Taut by Th29;
(p => ((q => r) => ((p '&' q) => r))) => ((p => (q => r)) => (p => ((p '&' q) => r))) in IPC-Taut by Def14;
then (p => (q => r)) => (p => ((p '&' q) => r)) in IPC-Taut by A2, Def14;
then A4: (p => (q => r)) => ((p '&' q) => (p => r)) in IPC-Taut by A3, Th26;
A5: (p '&' q) => p in IPC-Taut by Def14;
((p '&' q) => (p => r)) => (((p '&' q) => p) => ((p '&' q) => r)) in IPC-Taut by Def14;
then ((p '&' q) => (p => r)) => ((p '&' q) => r) in IPC-Taut by A5, Th32;
hence (p => (q => r)) => ((p '&' q) => r) in IPC-Taut by A4, Th26; ::_thesis: verum
end;
theorem Th38: :: INTPRO_1:38
for r, p, q being Element of MC-wff holds (r => p) => ((r => q) => (r => (p '&' q))) in IPC-Taut
proof
let r, p, q be Element of MC-wff ; ::_thesis: (r => p) => ((r => q) => (r => (p '&' q))) in IPC-Taut
A1: (r => (q => (p '&' q))) => ((r => q) => (r => (p '&' q))) in IPC-Taut by Def14;
p => (q => (p '&' q)) in IPC-Taut by Def14;
then A2: r => (p => (q => (p '&' q))) in IPC-Taut by Th18;
(r => (p => (q => (p '&' q)))) => ((r => p) => (r => (q => (p '&' q)))) in IPC-Taut by Def14;
then (r => p) => (r => (q => (p '&' q))) in IPC-Taut by A2, Def14;
hence (r => p) => ((r => q) => (r => (p '&' q))) in IPC-Taut by A1, Th26; ::_thesis: verum
end;
theorem Th39: :: INTPRO_1:39
for p, q being Element of MC-wff holds ((p => q) '&' p) => q in IPC-Taut
proof
let p, q be Element of MC-wff ; ::_thesis: ((p => q) '&' p) => q in IPC-Taut
set P = p => q;
A1: (p => q) => (p => q) in IPC-Taut by Th17;
((p => q) => (p => q)) => (((p => q) '&' p) => q) in IPC-Taut by Th37;
hence ((p => q) '&' p) => q in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem :: INTPRO_1:40
for p, q, s being Element of MC-wff holds (((p => q) '&' p) '&' s) => q in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (((p => q) '&' p) '&' s) => q in IPC-Taut
set P = (p => q) '&' p;
A1: ((p => q) '&' p) => q in IPC-Taut by Th39;
(((p => q) '&' p) '&' s) => ((p => q) '&' p) in IPC-Taut by Def14;
hence (((p => q) '&' p) '&' s) => q in IPC-Taut by A1, Th26; ::_thesis: verum
end;
theorem :: INTPRO_1:41
for q, s, p being Element of MC-wff holds (q => s) => ((p '&' q) => s) in IPC-Taut
proof
let q, s, p be Element of MC-wff ; ::_thesis: (q => s) => ((p '&' q) => s) in IPC-Taut
set P = p '&' q;
A1: (p '&' q) => q in IPC-Taut by Def14;
((p '&' q) => q) => ((q => s) => ((p '&' q) => s)) in IPC-Taut by Th24;
hence (q => s) => ((p '&' q) => s) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem Th42: :: INTPRO_1:42
for q, s, p being Element of MC-wff holds (q => s) => ((q '&' p) => s) in IPC-Taut
proof
let q, s, p be Element of MC-wff ; ::_thesis: (q => s) => ((q '&' p) => s) in IPC-Taut
set P = q '&' p;
A1: (q '&' p) => q in IPC-Taut by Def14;
((q '&' p) => q) => ((q => s) => ((q '&' p) => s)) in IPC-Taut by Th24;
hence (q => s) => ((q '&' p) => s) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem Th43: :: INTPRO_1:43
for p, s, q being Element of MC-wff holds ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in IPC-Taut
proof
let p, s, q be Element of MC-wff ; ::_thesis: ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in IPC-Taut
set P = p '&' s;
A1: ((p '&' s) => q) => (((p '&' s) => s) => ((p '&' s) => (q '&' s))) in IPC-Taut by Th38;
(p '&' s) => s in IPC-Taut by Def14;
hence ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in IPC-Taut by A1, Th32; ::_thesis: verum
end;
theorem Th44: :: INTPRO_1:44
for p, q, s being Element of MC-wff holds (p => q) => ((p '&' s) => (q '&' s)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p => q) => ((p '&' s) => (q '&' s)) in IPC-Taut
A1: ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in IPC-Taut by Th43;
(p => q) => ((p '&' s) => q) in IPC-Taut by Th42;
hence (p => q) => ((p '&' s) => (q '&' s)) in IPC-Taut by A1, Th26; ::_thesis: verum
end;
theorem Th45: :: INTPRO_1:45
for p, q, s being Element of MC-wff holds ((p => q) '&' (p '&' s)) => (q '&' s) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p => q) '&' (p '&' s)) => (q '&' s) in IPC-Taut
set P = p => q;
set Q = p '&' s;
set S = q '&' s;
A1: (p => q) => ((p '&' s) => (q '&' s)) in IPC-Taut by Th44;
((p => q) => ((p '&' s) => (q '&' s))) => (((p => q) '&' (p '&' s)) => (q '&' s)) in IPC-Taut by Th37;
hence ((p => q) '&' (p '&' s)) => (q '&' s) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem Th46: :: INTPRO_1:46
for p, q being Element of MC-wff holds (p '&' q) => (q '&' p) in IPC-Taut
proof
let p, q be Element of MC-wff ; ::_thesis: (p '&' q) => (q '&' p) in IPC-Taut
set P = p '&' q;
A1: (p '&' q) => q in IPC-Taut by Def14;
A2: (p '&' q) => p in IPC-Taut by Def14;
((p '&' q) => q) => (((p '&' q) => p) => ((p '&' q) => (q '&' p))) in IPC-Taut by Th38;
then ((p '&' q) => p) => ((p '&' q) => (q '&' p)) in IPC-Taut by A1, Def14;
hence (p '&' q) => (q '&' p) in IPC-Taut by A2, Def14; ::_thesis: verum
end;
theorem Th47: :: INTPRO_1:47
for p, q, s being Element of MC-wff holds ((p => q) '&' (p '&' s)) => (s '&' q) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p => q) '&' (p '&' s)) => (s '&' q) in IPC-Taut
A1: (q '&' s) => (s '&' q) in IPC-Taut by Th46;
((p => q) '&' (p '&' s)) => (q '&' s) in IPC-Taut by Th45;
hence ((p => q) '&' (p '&' s)) => (s '&' q) in IPC-Taut by A1, Th26; ::_thesis: verum
end;
theorem Th48: :: INTPRO_1:48
for p, q, s being Element of MC-wff holds (p => q) => ((p '&' s) => (s '&' q)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p => q) => ((p '&' s) => (s '&' q)) in IPC-Taut
set P = p => q;
set Q = p '&' s;
set S = s '&' q;
A1: ((p => q) '&' (p '&' s)) => (s '&' q) in IPC-Taut by Th47;
(((p => q) '&' (p '&' s)) => (s '&' q)) => ((p => q) => ((p '&' s) => (s '&' q))) in IPC-Taut by Th36;
hence (p => q) => ((p '&' s) => (s '&' q)) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem Th49: :: INTPRO_1:49
for p, q, s being Element of MC-wff holds (p => q) => ((s '&' p) => (s '&' q)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p => q) => ((s '&' p) => (s '&' q)) in IPC-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 IPC-Taut by Th48;
A2: (s '&' p) => (p '&' s) in IPC-Taut by Th46;
((p => q) => ((p '&' s) => (s '&' q))) => (((s '&' p) => (p '&' s)) => ((p => q) => ((s '&' p) => (s '&' q)))) in IPC-Taut by Th27;
then ((s '&' p) => (p '&' s)) => ((p => q) => ((s '&' p) => (s '&' q))) in IPC-Taut by A1, Def14;
hence (p => q) => ((s '&' p) => (s '&' q)) in IPC-Taut by A2, Def14; ::_thesis: verum
end;
theorem :: INTPRO_1:50
for p, s, q being Element of MC-wff holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut
proof
let p, s, q be Element of MC-wff ; ::_thesis: (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut
set P = s '&' q;
set Q = q '&' s;
A1: (s '&' q) => (q '&' s) in IPC-Taut by Th46;
((s '&' q) => (q '&' s)) => ((p '&' (s '&' q)) => (p '&' (q '&' s))) in IPC-Taut by Th49;
hence (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem :: INTPRO_1:51
for p, q, s being Element of MC-wff holds ((p => q) '&' (p => s)) => (p => (q '&' s)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p => q) '&' (p => s)) => (p => (q '&' s)) in IPC-Taut
set P = p => q;
set Q = p => s;
set S = p => (q '&' s);
A1: (p => q) => ((p => s) => (p => (q '&' s))) in IPC-Taut by Th38;
((p => q) => ((p => s) => (p => (q '&' s)))) => (((p => q) '&' (p => s)) => (p => (q '&' s))) in IPC-Taut by Th37;
hence ((p => q) '&' (p => s)) => (p => (q '&' s)) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
Lm5: for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => q in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p '&' q) '&' s) => q in IPC-Taut
A1: (p '&' q) => q in IPC-Taut by Def14;
((p '&' q) '&' s) => (p '&' q) in IPC-Taut by Def14;
hence ((p '&' q) '&' s) => q in IPC-Taut by A1, Th26; ::_thesis: verum
end;
Lm6: for p, q, s being Element of MC-wff holds (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in IPC-Taut
set P = (p '&' q) '&' s;
A1: ((p '&' q) '&' s) => q in IPC-Taut by Lm5;
(((p '&' q) '&' s) => q) => ((((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q)) in IPC-Taut by Th49;
hence (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
Lm7: for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in IPC-Taut
A1: (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in IPC-Taut by Lm6;
((p '&' q) '&' s) => (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) in IPC-Taut by Th33;
hence ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in IPC-Taut by A1, Th26; ::_thesis: verum
end;
Lm8: for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (p '&' s) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p '&' q) '&' s) => (p '&' s) in IPC-Taut
set P = p '&' q;
A1: (p '&' q) => p in IPC-Taut by Def14;
((p '&' q) => p) => (((p '&' q) '&' s) => (p '&' s)) in IPC-Taut by Th44;
hence ((p '&' q) '&' s) => (p '&' s) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
Lm9: for p, q, s being Element of MC-wff holds (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in IPC-Taut
set P = (p '&' q) '&' s;
set Q = p '&' s;
A1: ((p '&' q) '&' s) => (p '&' s) in IPC-Taut by Lm8;
(((p '&' q) '&' s) => (p '&' s)) => ((((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q)) in IPC-Taut by Th44;
hence (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
Lm10: for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((p '&' s) '&' q) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p '&' q) '&' s) => ((p '&' s) '&' q) in IPC-Taut
A1: (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in IPC-Taut by Lm9;
((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in IPC-Taut by Lm7;
hence ((p '&' q) '&' s) => ((p '&' s) '&' q) in IPC-Taut by A1, Th26; ::_thesis: verum
end;
Lm11: for p, s, q being Element of MC-wff holds ((p '&' s) '&' q) => ((s '&' p) '&' q) in IPC-Taut
proof
let p, s, q be Element of MC-wff ; ::_thesis: ((p '&' s) '&' q) => ((s '&' p) '&' q) in IPC-Taut
set P = p '&' s;
set Q = s '&' p;
A1: (p '&' s) => (s '&' p) in IPC-Taut by Th46;
((p '&' s) => (s '&' p)) => (((p '&' s) '&' q) => ((s '&' p) '&' q)) in IPC-Taut by Th44;
hence ((p '&' s) '&' q) => ((s '&' p) '&' q) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
Lm12: for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((s '&' p) '&' q) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p '&' q) '&' s) => ((s '&' p) '&' q) in IPC-Taut
A1: ((p '&' s) '&' q) => ((s '&' p) '&' q) in IPC-Taut by Lm11;
((p '&' q) '&' s) => ((p '&' s) '&' q) in IPC-Taut by Lm10;
hence ((p '&' q) '&' s) => ((s '&' p) '&' q) in IPC-Taut by A1, Th26; ::_thesis: verum
end;
Lm13: for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((s '&' q) '&' p) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p '&' q) '&' s) => ((s '&' q) '&' p) in IPC-Taut
A1: ((s '&' p) '&' q) => ((s '&' q) '&' p) in IPC-Taut by Lm10;
((p '&' q) '&' s) => ((s '&' p) '&' q) in IPC-Taut by Lm12;
hence ((p '&' q) '&' s) => ((s '&' q) '&' p) in IPC-Taut by A1, Th26; ::_thesis: verum
end;
Lm14: for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (p '&' (s '&' q)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p '&' q) '&' s) => (p '&' (s '&' q)) in IPC-Taut
A1: ((s '&' q) '&' p) => (p '&' (s '&' q)) in IPC-Taut by Th46;
((p '&' q) '&' s) => ((s '&' q) '&' p) in IPC-Taut by Lm13;
hence ((p '&' q) '&' s) => (p '&' (s '&' q)) in IPC-Taut by A1, Th26; ::_thesis: verum
end;
Lm15: for p, s, q being Element of MC-wff holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut
proof
let p, s, q be Element of MC-wff ; ::_thesis: (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut
set P = s '&' q;
set Q = q '&' s;
A1: (s '&' q) => (q '&' s) in IPC-Taut by Th46;
((s '&' q) => (q '&' s)) => ((p '&' (s '&' q)) => (p '&' (q '&' s))) in IPC-Taut by Th49;
hence (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem :: INTPRO_1:52
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (p '&' (q '&' s)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p '&' q) '&' s) => (p '&' (q '&' s)) in IPC-Taut
A1: (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut by Lm15;
((p '&' q) '&' s) => (p '&' (s '&' q)) in IPC-Taut by Lm14;
hence ((p '&' q) '&' s) => (p '&' (q '&' s)) in IPC-Taut by A1, Th26; ::_thesis: verum
end;
Lm16: for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((s '&' q) '&' p) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p '&' (q '&' s)) => ((s '&' q) '&' p) in IPC-Taut
A1: (p '&' (s '&' q)) => ((s '&' q) '&' p) in IPC-Taut by Th46;
(p '&' (q '&' s)) => (p '&' (s '&' q)) in IPC-Taut by Lm15;
hence (p '&' (q '&' s)) => ((s '&' q) '&' p) in IPC-Taut by A1, Th26; ::_thesis: verum
end;
Lm17: for s, q, p being Element of MC-wff holds ((s '&' q) '&' p) => ((q '&' s) '&' p) in IPC-Taut
proof
let s, q, p be Element of MC-wff ; ::_thesis: ((s '&' q) '&' p) => ((q '&' s) '&' p) in IPC-Taut
set P = s '&' q;
set Q = q '&' s;
A1: (s '&' q) => (q '&' s) in IPC-Taut by Th46;
((s '&' q) => (q '&' s)) => (((s '&' q) '&' p) => ((q '&' s) '&' p)) in IPC-Taut by Th44;
hence ((s '&' q) '&' p) => ((q '&' s) '&' p) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
Lm18: for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((q '&' s) '&' p) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p '&' (q '&' s)) => ((q '&' s) '&' p) in IPC-Taut
A1: ((s '&' q) '&' p) => ((q '&' s) '&' p) in IPC-Taut by Lm17;
(p '&' (q '&' s)) => ((s '&' q) '&' p) in IPC-Taut by Lm16;
hence (p '&' (q '&' s)) => ((q '&' s) '&' p) in IPC-Taut by A1, Th26; ::_thesis: verum
end;
Lm19: for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((p '&' s) '&' q) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p '&' (q '&' s)) => ((p '&' s) '&' q) in IPC-Taut
A1: ((q '&' s) '&' p) => ((p '&' s) '&' q) in IPC-Taut by Lm13;
(p '&' (q '&' s)) => ((q '&' s) '&' p) in IPC-Taut by Lm18;
hence (p '&' (q '&' s)) => ((p '&' s) '&' q) in IPC-Taut by A1, Th26; ::_thesis: verum
end;
Lm20: for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => (p '&' (s '&' q)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p '&' (q '&' s)) => (p '&' (s '&' q)) in IPC-Taut
set P = q '&' s;
set Q = s '&' q;
A1: (q '&' s) => (s '&' q) in IPC-Taut by Th46;
((q '&' s) => (s '&' q)) => ((p '&' (q '&' s)) => (p '&' (s '&' q))) in IPC-Taut by Th49;
hence (p '&' (q '&' s)) => (p '&' (s '&' q)) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem :: INTPRO_1:53
for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((p '&' q) '&' s) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p '&' (q '&' s)) => ((p '&' q) '&' s) in IPC-Taut
A1: (p '&' (s '&' q)) => ((p '&' q) '&' s) in IPC-Taut by Lm19;
(p '&' (q '&' s)) => (p '&' (s '&' q)) in IPC-Taut by Lm20;
hence (p '&' (q '&' s)) => ((p '&' q) '&' s) in IPC-Taut by A1, Th26; ::_thesis: verum
end;
begin
theorem Th54: :: INTPRO_1:54
for p being Element of MC-wff holds (p 'or' p) => p in IPC-Taut
proof
let p be Element of MC-wff ; ::_thesis: (p 'or' p) => p in IPC-Taut
A1: p => p in IPC-Taut by Th17;
(p => p) => ((p => p) => ((p 'or' p) => p)) in IPC-Taut by Def14;
then (p => p) => ((p 'or' p) => p) in IPC-Taut by A1, Def14;
hence (p 'or' p) => p in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem :: INTPRO_1:55
for p, q being Element of MC-wff st ( p in IPC-Taut or q in IPC-Taut ) holds
p 'or' q in IPC-Taut
proof
let p, q be Element of MC-wff ; ::_thesis: ( ( p in IPC-Taut or q in IPC-Taut ) implies p 'or' q in IPC-Taut )
assume A1: ( p in IPC-Taut or q in IPC-Taut ) ; ::_thesis: p 'or' q in IPC-Taut
now__::_thesis:_(_(_p_in_IPC-Taut_&_p_'or'_q_in_IPC-Taut_)_or_(_q_in_IPC-Taut_&_p_'or'_q_in_IPC-Taut_)_)
percases ( p in IPC-Taut or q in IPC-Taut ) by A1;
caseA2: p in IPC-Taut ; ::_thesis: p 'or' q in IPC-Taut
p => (p 'or' q) in IPC-Taut by Def14;
hence p 'or' q in IPC-Taut by A2, Def14; ::_thesis: verum
end;
caseA3: q in IPC-Taut ; ::_thesis: p 'or' q in IPC-Taut
q => (p 'or' q) in IPC-Taut by Def14;
hence p 'or' q in IPC-Taut by A3, Def14; ::_thesis: verum
end;
end;
end;
hence p 'or' q in IPC-Taut ; ::_thesis: verum
end;
theorem Th56: :: INTPRO_1:56
for p, q being Element of MC-wff holds (p 'or' q) => (q 'or' p) in IPC-Taut
proof
let p, q be Element of MC-wff ; ::_thesis: (p 'or' q) => (q 'or' p) in IPC-Taut
A1: p => (q 'or' p) in IPC-Taut by Def14;
A2: q => (q 'or' p) in IPC-Taut by Def14;
(p => (q 'or' p)) => ((q => (q 'or' p)) => ((p 'or' q) => (q 'or' p))) in IPC-Taut by Def14;
then (q => (q 'or' p)) => ((p 'or' q) => (q 'or' p)) in IPC-Taut by A1, Def14;
hence (p 'or' q) => (q 'or' p) in IPC-Taut by A2, Def14; ::_thesis: verum
end;
theorem :: INTPRO_1:57
for p, q being Element of MC-wff holds
( p 'or' q in IPC-Taut iff q 'or' p in IPC-Taut )
proof
let p, q be Element of MC-wff ; ::_thesis: ( p 'or' q in IPC-Taut iff q 'or' p in IPC-Taut )
hereby ::_thesis: ( q 'or' p in IPC-Taut implies p 'or' q in IPC-Taut )
assume A1: p 'or' q in IPC-Taut ; ::_thesis: q 'or' p in IPC-Taut
(p 'or' q) => (q 'or' p) in IPC-Taut by Th56;
hence q 'or' p in IPC-Taut by A1, Def14; ::_thesis: verum
end;
assume A2: q 'or' p in IPC-Taut ; ::_thesis: p 'or' q in IPC-Taut
(q 'or' p) => (p 'or' q) in IPC-Taut by Th56;
hence p 'or' q in IPC-Taut by A2, Def14; ::_thesis: verum
end;
theorem Th58: :: INTPRO_1:58
for p, q, s being Element of MC-wff holds (p => q) => (p => (q 'or' s)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p => q) => (p => (q 'or' s)) in IPC-Taut
A1: (q => (q 'or' s)) => ((p => q) => (p => (q 'or' s))) in IPC-Taut by Th22;
q => (q 'or' s) in IPC-Taut by Def14;
hence (p => q) => (p => (q 'or' s)) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem Th59: :: INTPRO_1:59
for p, q, s being Element of MC-wff holds (p => q) => (p => (s 'or' q)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p => q) => (p => (s 'or' q)) in IPC-Taut
A1: (q => (s 'or' q)) => ((p => q) => (p => (s 'or' q))) in IPC-Taut by Th22;
q => (s 'or' q) in IPC-Taut by Def14;
hence (p => q) => (p => (s 'or' q)) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem Th60: :: INTPRO_1:60
for p, q, s being Element of MC-wff holds (p => q) => ((p 'or' s) => (q 'or' s)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p => q) => ((p 'or' s) => (q 'or' s)) in IPC-Taut
set P = p 'or' s;
set Q = q 'or' s;
A1: (p => q) => (p => (q 'or' s)) in IPC-Taut by Th58;
(p => (q 'or' s)) => ((s => (q 'or' s)) => ((p 'or' s) => (q 'or' s))) in IPC-Taut by Def14;
then A2: (s => (q 'or' s)) => ((p => (q 'or' s)) => ((p 'or' s) => (q 'or' s))) in IPC-Taut by Th23;
s => (q 'or' s) in IPC-Taut by Def14;
then (p => (q 'or' s)) => ((p 'or' s) => (q 'or' s)) in IPC-Taut by A2, Def14;
hence (p => q) => ((p 'or' s) => (q 'or' s)) in IPC-Taut by A1, Th26; ::_thesis: verum
end;
theorem Th61: :: INTPRO_1:61
for p, q, s being Element of MC-wff st p => q in IPC-Taut holds
(p 'or' s) => (q 'or' s) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ( p => q in IPC-Taut implies (p 'or' s) => (q 'or' s) in IPC-Taut )
assume A1: p => q in IPC-Taut ; ::_thesis: (p 'or' s) => (q 'or' s) in IPC-Taut
(p => q) => ((p 'or' s) => (q 'or' s)) in IPC-Taut by Th60;
hence (p 'or' s) => (q 'or' s) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem Th62: :: INTPRO_1:62
for p, q, s being Element of MC-wff holds (p => q) => ((s 'or' p) => (s 'or' q)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p => q) => ((s 'or' p) => (s 'or' q)) in IPC-Taut
set P = s 'or' p;
set Q = s 'or' q;
A1: s => (s 'or' q) in IPC-Taut by Def14;
A2: (p => q) => (p => (s 'or' q)) in IPC-Taut by Th59;
(s => (s 'or' q)) => ((p => (s 'or' q)) => ((s 'or' p) => (s 'or' q))) in IPC-Taut by Def14;
then (p => (s 'or' q)) => ((s 'or' p) => (s 'or' q)) in IPC-Taut by A1, Def14;
hence (p => q) => ((s 'or' p) => (s 'or' q)) in IPC-Taut by A2, Th26; ::_thesis: verum
end;
theorem Th63: :: INTPRO_1:63
for p, q, s being Element of MC-wff st p => q in IPC-Taut holds
(s 'or' p) => (s 'or' q) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ( p => q in IPC-Taut implies (s 'or' p) => (s 'or' q) in IPC-Taut )
assume A1: p => q in IPC-Taut ; ::_thesis: (s 'or' p) => (s 'or' q) in IPC-Taut
(p => q) => ((s 'or' p) => (s 'or' q)) in IPC-Taut by Th62;
hence (s 'or' p) => (s 'or' q) in IPC-Taut by A1, Def14; ::_thesis: verum
end;
theorem Th64: :: INTPRO_1:64
for p, q, s being Element of MC-wff holds (p 'or' (q 'or' s)) => (q 'or' (p 'or' s)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p 'or' (q 'or' s)) => (q 'or' (p 'or' s)) in IPC-Taut
set P = p 'or' s;
set Q = q 'or' s;
A1: (p 'or' s) => (q 'or' (p 'or' s)) in IPC-Taut by Def14;
p => (p 'or' s) in IPC-Taut by Def14;
then p => (q 'or' (p 'or' s)) in IPC-Taut by A1, Th26;
then A2: ((q 'or' (p 'or' s)) 'or' p) => ((q 'or' (p 'or' s)) 'or' (q 'or' (p 'or' s))) in IPC-Taut by Th63;
((q 'or' (p 'or' s)) 'or' (q 'or' (p 'or' s))) => (q 'or' (p 'or' s)) in IPC-Taut by Th54;
then A3: ((q 'or' (p 'or' s)) 'or' p) => (q 'or' (p 'or' s)) in IPC-Taut by A2, Th26;
s => (p 'or' s) in IPC-Taut by Def14;
then (q 'or' s) => (q 'or' (p 'or' s)) in IPC-Taut by Th63;
then A4: (p 'or' (q 'or' s)) => (p 'or' (q 'or' (p 'or' s))) in IPC-Taut by Th63;
(p 'or' (q 'or' (p 'or' s))) => ((q 'or' (p 'or' s)) 'or' p) in IPC-Taut by Th56;
then (p 'or' (q 'or' s)) => ((q 'or' (p 'or' s)) 'or' p) in IPC-Taut by A4, Th26;
hence (p 'or' (q 'or' s)) => (q 'or' (p 'or' s)) in IPC-Taut by A3, Th26; ::_thesis: verum
end;
theorem :: INTPRO_1:65
for p, q, s being Element of MC-wff holds (p 'or' (q 'or' s)) => ((p 'or' q) 'or' s) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: (p 'or' (q 'or' s)) => ((p 'or' q) 'or' s) in IPC-Taut
A1: (s 'or' (p 'or' q)) => ((p 'or' q) 'or' s) in IPC-Taut by Th56;
(q 'or' s) => (s 'or' q) in IPC-Taut by Th56;
then A2: (p 'or' (q 'or' s)) => (p 'or' (s 'or' q)) in IPC-Taut by Th63;
(p 'or' (s 'or' q)) => (s 'or' (p 'or' q)) in IPC-Taut by Th64;
then (p 'or' (q 'or' s)) => (s 'or' (p 'or' q)) in IPC-Taut by A2, Th26;
hence (p 'or' (q 'or' s)) => ((p 'or' q) 'or' s) in IPC-Taut by A1, Th26; ::_thesis: verum
end;
theorem :: INTPRO_1:66
for p, q, s being Element of MC-wff holds ((p 'or' q) 'or' s) => (p 'or' (q 'or' s)) in IPC-Taut
proof
let p, q, s be Element of MC-wff ; ::_thesis: ((p 'or' q) 'or' s) => (p 'or' (q 'or' s)) in IPC-Taut
(p 'or' q) => (q 'or' p) in IPC-Taut by Th56;
then A1: ((p 'or' q) 'or' s) => ((q 'or' p) 'or' s) in IPC-Taut by Th61;
(q 'or' p) => (p 'or' q) in IPC-Taut by Th56;
then A2: (s 'or' (q 'or' p)) => (s 'or' (p 'or' q)) in IPC-Taut by Th63;
((q 'or' p) 'or' s) => (s 'or' (q 'or' p)) in IPC-Taut by Th56;
then ((p 'or' q) 'or' s) => (s 'or' (q 'or' p)) in IPC-Taut by A1, Th26;
then A3: ((p 'or' q) 'or' s) => (s 'or' (p 'or' q)) in IPC-Taut by A2, Th26;
(s 'or' q) => (q 'or' s) in IPC-Taut by Th56;
then A4: (p 'or' (s 'or' q)) => (p 'or' (q 'or' s)) in IPC-Taut by Th63;
(s 'or' (p 'or' q)) => (p 'or' (s 'or' q)) in IPC-Taut by Th64;
then ((p 'or' q) 'or' s) => (p 'or' (s 'or' q)) in IPC-Taut by A3, Th26;
hence ((p 'or' q) 'or' s) => (p 'or' (q 'or' s)) in IPC-Taut by A4, Th26; ::_thesis: verum
end;
begin
definition
let T be Subset of MC-wff;
attrT is CPC_theory means :Def19: :: INTPRO_1:def 19
for p, q, r being Element of MC-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 => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & p 'or' (p => FALSUM) in T & ( p in T & p => q in T implies q in T ) );
correctness
;
end;
:: deftheorem Def19 defines CPC_theory INTPRO_1:def_19_:_
for T being Subset of MC-wff holds
( T is CPC_theory iff for p, q, r being Element of MC-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 => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & p 'or' (p => FALSUM) in T & ( p in T & p => q in T implies q in T ) ) );
theorem Th67: :: INTPRO_1:67
for T being Subset of MC-wff st T is CPC_theory holds
T is IPC_theory
proof
let T be Subset of MC-wff; ::_thesis: ( T is CPC_theory implies T is IPC_theory )
assume A1: T is CPC_theory ; ::_thesis: T is IPC_theory
let p, q, r be Element of MC-wff ; :: according to INTPRO_1:def_14 ::_thesis: ( 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 => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & ( p in T & p => q in T implies q in T ) )
thus ( 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 => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & ( p in T & p => q in T implies q in T ) ) by A1, Def19; ::_thesis: verum
end;
definition
let X be Subset of MC-wff;
func CnCPC X -> Subset of MC-wff means :Def20: :: INTPRO_1:def 20
for r being Element of MC-wff holds
( r in it iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T );
existence
ex b1 being Subset of MC-wff st
for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T )
proof
defpred S1[ set ] means for T being Subset of MC-wff st T is CPC_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 MC-wff & S1[a] ) ) from XBOOLE_0:sch_1();
Y c= MC-wff
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in MC-wff )
assume a in Y ; ::_thesis: a in MC-wff
hence a in MC-wff by A1; ::_thesis: verum
end;
then reconsider Z = Y as Subset of MC-wff ;
take Z ; ::_thesis: for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T )
thus for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of MC-wff st ( for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) ) & ( for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) ) holds
b1 = b2
proof
let Y, Z be Subset of MC-wff; ::_thesis: ( ( for r being Element of MC-wff holds
( r in Y iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) ) & ( for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) ) implies Y = Z )
assume that
A2: for r being Element of MC-wff holds
( r in Y iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) and
A3: for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is CPC_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 MC-wff ;
for T being Subset of MC-wff st T is CPC_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 MC-wff ;
for T being Subset of MC-wff st T is CPC_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 Def20 defines CnCPC INTPRO_1:def_20_:_
for X, b2 being Subset of MC-wff holds
( b2 = CnCPC X iff for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) );
definition
func CPC-Taut -> Subset of MC-wff equals :: INTPRO_1:def 21
CnCPC ({} MC-wff);
correctness
coherence
CnCPC ({} MC-wff) is Subset of MC-wff;
;
end;
:: deftheorem defines CPC-Taut INTPRO_1:def_21_:_
CPC-Taut = CnCPC ({} MC-wff);
theorem Th68: :: INTPRO_1:68
for X being Subset of MC-wff holds CnIPC X c= CnCPC X
proof
let X be Subset of MC-wff; ::_thesis: CnIPC X c= CnCPC X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnIPC X or a in CnCPC X )
assume A1: a in CnIPC X ; ::_thesis: a in CnCPC X
then reconsider r = a as Element of MC-wff ;
for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is CPC_theory & X c= T implies r in T )
assume that
A2: T is CPC_theory and
A3: X c= T ; ::_thesis: r in T
T is IPC_theory by A2, Th67;
hence r in T by A1, A3, Def15; ::_thesis: verum
end;
hence a in CnCPC X by Def20; ::_thesis: verum
end;
theorem Th69: :: INTPRO_1:69
for X being Subset of MC-wff
for p, q, r being Element of MC-wff holds
( p => (q => p) in CnCPC X & (p => (q => r)) => ((p => q) => (p => r)) in CnCPC X & (p '&' q) => p in CnCPC X & (p '&' q) => q in CnCPC X & p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X )
proof
let X be Subset of MC-wff; ::_thesis: for p, q, r being Element of MC-wff holds
( p => (q => p) in CnCPC X & (p => (q => r)) => ((p => q) => (p => r)) in CnCPC X & (p '&' q) => p in CnCPC X & (p '&' q) => q in CnCPC X & p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X )
let p, q, r be Element of MC-wff ; ::_thesis: ( p => (q => p) in CnCPC X & (p => (q => r)) => ((p => q) => (p => r)) in CnCPC X & (p '&' q) => p in CnCPC X & (p '&' q) => q in CnCPC X & p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X )
A1: CnIPC X c= CnCPC X by Th68;
p => (q => p) in CnIPC X by Th1;
hence p => (q => p) in CnCPC X by A1; ::_thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in CnCPC X & (p '&' q) => p in CnCPC X & (p '&' q) => q in CnCPC X & p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X )
A2: CnIPC X c= CnCPC X by Th68;
(p => (q => r)) => ((p => q) => (p => r)) in CnIPC X by Th2;
hence (p => (q => r)) => ((p => q) => (p => r)) in CnCPC X by A2; ::_thesis: ( (p '&' q) => p in CnCPC X & (p '&' q) => q in CnCPC X & p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X )
A3: CnIPC X c= CnCPC X by Th68;
(p '&' q) => p in CnIPC X by Th3;
hence (p '&' q) => p in CnCPC X by A3; ::_thesis: ( (p '&' q) => q in CnCPC X & p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X )
A4: CnIPC X c= CnCPC X by Th68;
(p '&' q) => q in CnIPC X by Th4;
hence (p '&' q) => q in CnCPC X by A4; ::_thesis: ( p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X )
A5: CnIPC X c= CnCPC X by Th68;
p => (q => (p '&' q)) in CnIPC X by Th5;
hence p => (q => (p '&' q)) in CnCPC X by A5; ::_thesis: ( p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X )
A6: CnIPC X c= CnCPC X by Th68;
p => (p 'or' q) in CnIPC X by Th6;
hence p => (p 'or' q) in CnCPC X by A6; ::_thesis: ( q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X )
A7: CnIPC X c= CnCPC X by Th68;
q => (p 'or' q) in CnIPC X by Th7;
hence q => (p 'or' q) in CnCPC X by A7; ::_thesis: ( (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X )
A8: CnIPC X c= CnCPC X by Th68;
(p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X by Th8;
hence (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X by A8; ::_thesis: ( FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X )
A9: CnIPC X c= CnCPC X by Th68;
FALSUM => p in CnIPC X by Th9;
hence FALSUM => p in CnCPC X by A9; ::_thesis: p 'or' (p => FALSUM) in CnCPC X
for T being Subset of MC-wff st T is CPC_theory & X c= T holds
p 'or' (p => FALSUM) in T by Def19;
hence p 'or' (p => FALSUM) in CnCPC X by Def20; ::_thesis: verum
end;
theorem Th70: :: INTPRO_1:70
for X being Subset of MC-wff
for p, q being Element of MC-wff st p in CnCPC X & p => q in CnCPC X holds
q in CnCPC X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff st p in CnCPC X & p => q in CnCPC X holds
q in CnCPC X
let p, q be Element of MC-wff ; ::_thesis: ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X )
assume that
A1: p in CnCPC X and
A2: p => q in CnCPC X ; ::_thesis: q in CnCPC X
for T being Subset of MC-wff st T is CPC_theory & X c= T holds
q in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is CPC_theory & X c= T implies q in T )
assume that
A3: T is CPC_theory and
A4: X c= T ; ::_thesis: q in T
A5: p => q in T by A2, A3, A4, Def20;
p in T by A1, A3, A4, Def20;
hence q in T by A3, A5, Def19; ::_thesis: verum
end;
hence q in CnCPC X by Def20; ::_thesis: verum
end;
theorem Th71: :: INTPRO_1:71
for T, X being Subset of MC-wff st T is CPC_theory & X c= T holds
CnCPC X c= T
proof
let T, X be Subset of MC-wff; ::_thesis: ( T is CPC_theory & X c= T implies CnCPC X c= T )
assume that
A1: T is CPC_theory and
A2: X c= T ; ::_thesis: CnCPC X c= T
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnCPC X or a in T )
thus ( not a in CnCPC X or a in T ) by A1, A2, Def20; ::_thesis: verum
end;
theorem Th72: :: INTPRO_1:72
for X being Subset of MC-wff holds X c= CnCPC X
proof
let X be Subset of MC-wff; ::_thesis: X c= CnCPC X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in CnCPC X )
assume A1: a in X ; ::_thesis: a in CnCPC X
then reconsider t = a as Element of MC-wff ;
for T being Subset of MC-wff st T is CPC_theory & X c= T holds
t in T by A1;
hence a in CnCPC X by Def20; ::_thesis: verum
end;
theorem Th73: :: INTPRO_1:73
for X, Y being Subset of MC-wff st X c= Y holds
CnCPC X c= CnCPC Y
proof
let X, Y be Subset of MC-wff; ::_thesis: ( X c= Y implies CnCPC X c= CnCPC Y )
assume A1: X c= Y ; ::_thesis: CnCPC X c= CnCPC Y
thus CnCPC X c= CnCPC Y ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnCPC X or a in CnCPC Y )
assume A2: a in CnCPC X ; ::_thesis: a in CnCPC Y
then reconsider t = a as Element of MC-wff ;
for T being Subset of MC-wff st T is CPC_theory & Y c= T holds
t in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is CPC_theory & Y c= T implies t in T )
assume that
A3: T is CPC_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, Def20; ::_thesis: verum
end;
hence a in CnCPC Y by Def20; ::_thesis: verum
end;
end;
Lm21: for X being Subset of MC-wff holds CnCPC (CnCPC X) c= CnCPC X
proof
let X be Subset of MC-wff; ::_thesis: CnCPC (CnCPC X) c= CnCPC X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnCPC (CnCPC X) or a in CnCPC X )
assume A1: a in CnCPC (CnCPC X) ; ::_thesis: a in CnCPC X
then reconsider t = a as Element of MC-wff ;
for T being Subset of MC-wff st T is CPC_theory & X c= T holds
t in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is CPC_theory & X c= T implies t in T )
assume that
A2: T is CPC_theory and
A3: X c= T ; ::_thesis: t in T
CnCPC X c= T by A2, A3, Th71;
hence t in T by A1, A2, Def20; ::_thesis: verum
end;
hence a in CnCPC X by Def20; ::_thesis: verum
end;
theorem :: INTPRO_1:74
for X being Subset of MC-wff holds CnCPC (CnCPC X) = CnCPC X
proof
let X be Subset of MC-wff; ::_thesis: CnCPC (CnCPC X) = CnCPC X
A1: CnCPC X c= CnCPC (CnCPC X) by Th72;
CnCPC (CnCPC X) c= CnCPC X by Lm21;
hence CnCPC (CnCPC X) = CnCPC X by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm22: for X being Subset of MC-wff holds CnCPC X is CPC_theory
proof
let X be Subset of MC-wff; ::_thesis: CnCPC X is CPC_theory
let p be Element of MC-wff ; :: according to INTPRO_1:def_19 ::_thesis: for q, r being Element of MC-wff holds
( p => (q => p) in CnCPC X & (p => (q => r)) => ((p => q) => (p => r)) in CnCPC X & (p '&' q) => p in CnCPC X & (p '&' q) => q in CnCPC X & p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
let q, r be Element of MC-wff ; ::_thesis: ( p => (q => p) in CnCPC X & (p => (q => r)) => ((p => q) => (p => r)) in CnCPC X & (p '&' q) => p in CnCPC X & (p '&' q) => q in CnCPC X & p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus p => (q => p) in CnCPC X by Th69; ::_thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in CnCPC X & (p '&' q) => p in CnCPC X & (p '&' q) => q in CnCPC X & p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus (p => (q => r)) => ((p => q) => (p => r)) in CnCPC X by Th69; ::_thesis: ( (p '&' q) => p in CnCPC X & (p '&' q) => q in CnCPC X & p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus (p '&' q) => p in CnCPC X by Th69; ::_thesis: ( (p '&' q) => q in CnCPC X & p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus (p '&' q) => q in CnCPC X by Th69; ::_thesis: ( p => (q => (p '&' q)) in CnCPC X & p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus p => (q => (p '&' q)) in CnCPC X by Th69; ::_thesis: ( p => (p 'or' q) in CnCPC X & q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus p => (p 'or' q) in CnCPC X by Th69; ::_thesis: ( q => (p 'or' q) in CnCPC X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus q => (p 'or' q) in CnCPC X by Th69; ::_thesis: ( (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X & FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC X by Th69; ::_thesis: ( FALSUM => p in CnCPC X & p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus FALSUM => p in CnCPC X by Th69; ::_thesis: ( p 'or' (p => FALSUM) in CnCPC X & ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) )
thus p 'or' (p => FALSUM) in CnCPC X by Th69; ::_thesis: ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X )
thus ( p in CnCPC X & p => q in CnCPC X implies q in CnCPC X ) by Th70; ::_thesis: verum
end;
registration
let X be Subset of MC-wff;
cluster CnCPC X -> CPC_theory ;
coherence
CnCPC X is CPC_theory by Lm22;
end;
theorem Th75: :: INTPRO_1:75
for T being Subset of MC-wff holds
( T is CPC_theory iff CnCPC T = T )
proof
let T be Subset of MC-wff; ::_thesis: ( T is CPC_theory iff CnCPC T = T )
hereby ::_thesis: ( CnCPC T = T implies T is CPC_theory )
assume A1: T is CPC_theory ; ::_thesis: CnCPC T = T
A2: CnCPC T c= T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnCPC T or a in T )
assume a in CnCPC T ; ::_thesis: a in T
hence a in T by A1, Def20; ::_thesis: verum
end;
T c= CnCPC T by Th72;
hence CnCPC T = T by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
thus ( CnCPC T = T implies T is CPC_theory ) ; ::_thesis: verum
end;
theorem :: INTPRO_1:76
for T being Subset of MC-wff st T is CPC_theory holds
CPC-Taut c= T
proof
let T be Subset of MC-wff; ::_thesis: ( T is CPC_theory implies CPC-Taut c= T )
assume A1: T is CPC_theory ; ::_thesis: CPC-Taut c= T
CPC-Taut c= CnCPC T by Th73, XBOOLE_1:2;
hence CPC-Taut c= T by A1, Th75; ::_thesis: verum
end;
registration
cluster CPC-Taut -> CPC_theory ;
coherence
CPC-Taut is CPC_theory ;
end;
theorem :: INTPRO_1:77
IPC-Taut c= CPC-Taut by Th68;
begin
definition
let T be Subset of MC-wff;
attrT is S4_theory means :Def22: :: INTPRO_1:def 22
for p, q, r being Element of MC-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 => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & p 'or' (p => FALSUM) in T & (Nes (p => q)) => ((Nes p) => (Nes q)) in T & (Nes p) => p in T & (Nes p) => (Nes (Nes p)) in T & ( p in T & p => q in T implies q in T ) & ( p in T implies Nes p in T ) );
correctness
;
end;
:: deftheorem Def22 defines S4_theory INTPRO_1:def_22_:_
for T being Subset of MC-wff holds
( T is S4_theory iff for p, q, r being Element of MC-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 => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & p 'or' (p => FALSUM) in T & (Nes (p => q)) => ((Nes p) => (Nes q)) in T & (Nes p) => p in T & (Nes p) => (Nes (Nes p)) in T & ( p in T & p => q in T implies q in T ) & ( p in T implies Nes p in T ) ) );
theorem Th78: :: INTPRO_1:78
for T being Subset of MC-wff st T is S4_theory holds
T is CPC_theory
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory implies T is CPC_theory )
assume A1: T is S4_theory ; ::_thesis: T is CPC_theory
let p, q, r be Element of MC-wff ; :: according to INTPRO_1:def_19 ::_thesis: ( 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 => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & p 'or' (p => FALSUM) in T & ( p in T & p => q in T implies q in T ) )
thus ( 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 => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & p 'or' (p => FALSUM) in T & ( p in T & p => q in T implies q in T ) ) by A1, Def22; ::_thesis: verum
end;
theorem :: INTPRO_1:79
for T being Subset of MC-wff st T is S4_theory holds
T is IPC_theory
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory implies T is IPC_theory )
assume A1: T is S4_theory ; ::_thesis: T is IPC_theory
let p, q, r be Element of MC-wff ; :: according to INTPRO_1:def_14 ::_thesis: ( 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 => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & ( p in T & p => q in T implies q in T ) )
thus ( 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 => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & ( p in T & p => q in T implies q in T ) ) by A1, Def22; ::_thesis: verum
end;
definition
let X be Subset of MC-wff;
func CnS4 X -> Subset of MC-wff means :Def23: :: INTPRO_1:def 23
for r being Element of MC-wff holds
( r in it iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T );
existence
ex b1 being Subset of MC-wff st
for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T )
proof
defpred S1[ set ] means for T being Subset of MC-wff st T is S4_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 MC-wff & S1[a] ) ) from XBOOLE_0:sch_1();
Y c= MC-wff
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in MC-wff )
assume a in Y ; ::_thesis: a in MC-wff
hence a in MC-wff by A1; ::_thesis: verum
end;
then reconsider Z = Y as Subset of MC-wff ;
take Z ; ::_thesis: for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T )
thus for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of MC-wff st ( for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) ) & ( for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) ) holds
b1 = b2
proof
let Y, Z be Subset of MC-wff; ::_thesis: ( ( for r being Element of MC-wff holds
( r in Y iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) ) & ( for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) ) implies Y = Z )
assume that
A2: for r being Element of MC-wff holds
( r in Y iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) and
A3: for r being Element of MC-wff holds
( r in Z iff for T being Subset of MC-wff st T is S4_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 MC-wff ;
for T being Subset of MC-wff st T is S4_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 MC-wff ;
for T being Subset of MC-wff st T is S4_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 Def23 defines CnS4 INTPRO_1:def_23_:_
for X, b2 being Subset of MC-wff holds
( b2 = CnS4 X iff for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) );
definition
func S4-Taut -> Subset of MC-wff equals :: INTPRO_1:def 24
CnS4 ({} MC-wff);
correctness
coherence
CnS4 ({} MC-wff) is Subset of MC-wff;
;
end;
:: deftheorem defines S4-Taut INTPRO_1:def_24_:_
S4-Taut = CnS4 ({} MC-wff);
theorem Th80: :: INTPRO_1:80
for X being Subset of MC-wff holds CnCPC X c= CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: CnCPC X c= CnS4 X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnCPC X or a in CnS4 X )
assume A1: a in CnCPC X ; ::_thesis: a in CnS4 X
then reconsider r = a as Element of MC-wff ;
for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory & X c= T implies r in T )
assume that
A2: T is S4_theory and
A3: X c= T ; ::_thesis: r in T
T is CPC_theory by A2, Th78;
hence r in T by A1, A3, Def20; ::_thesis: verum
end;
hence a in CnS4 X by Def23; ::_thesis: verum
end;
theorem Th81: :: INTPRO_1:81
for X being Subset of MC-wff holds CnIPC X c= CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: CnIPC X c= CnS4 X
A1: CnCPC X c= CnS4 X by Th80;
CnIPC X c= CnCPC X by Th68;
hence CnIPC X c= CnS4 X by A1, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th82: :: INTPRO_1:82
for X being Subset of MC-wff
for p, q, r being Element of MC-wff holds
( p => (q => p) in CnS4 X & (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X & (p '&' q) => p in CnS4 X & (p '&' q) => q in CnS4 X & p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
proof
let X be Subset of MC-wff; ::_thesis: for p, q, r being Element of MC-wff holds
( p => (q => p) in CnS4 X & (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X & (p '&' q) => p in CnS4 X & (p '&' q) => q in CnS4 X & p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
let p, q, r be Element of MC-wff ; ::_thesis: ( p => (q => p) in CnS4 X & (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X & (p '&' q) => p in CnS4 X & (p '&' q) => q in CnS4 X & p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A1: CnIPC X c= CnS4 X by Th81;
p => (q => p) in CnIPC X by Th1;
hence p => (q => p) in CnS4 X by A1; ::_thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X & (p '&' q) => p in CnS4 X & (p '&' q) => q in CnS4 X & p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A2: CnIPC X c= CnS4 X by Th81;
(p => (q => r)) => ((p => q) => (p => r)) in CnIPC X by Th2;
hence (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X by A2; ::_thesis: ( (p '&' q) => p in CnS4 X & (p '&' q) => q in CnS4 X & p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A3: CnIPC X c= CnS4 X by Th81;
(p '&' q) => p in CnIPC X by Th3;
hence (p '&' q) => p in CnS4 X by A3; ::_thesis: ( (p '&' q) => q in CnS4 X & p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A4: CnIPC X c= CnS4 X by Th81;
(p '&' q) => q in CnIPC X by Th4;
hence (p '&' q) => q in CnS4 X by A4; ::_thesis: ( p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A5: CnIPC X c= CnS4 X by Th81;
p => (q => (p '&' q)) in CnIPC X by Th5;
hence p => (q => (p '&' q)) in CnS4 X by A5; ::_thesis: ( p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A6: CnIPC X c= CnS4 X by Th81;
p => (p 'or' q) in CnIPC X by Th6;
hence p => (p 'or' q) in CnS4 X by A6; ::_thesis: ( q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A7: CnIPC X c= CnS4 X by Th81;
q => (p 'or' q) in CnIPC X by Th7;
hence q => (p 'or' q) in CnS4 X by A7; ::_thesis: ( (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A8: CnIPC X c= CnS4 X by Th81;
(p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X by Th8;
hence (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X by A8; ::_thesis: ( FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X )
A9: CnIPC X c= CnS4 X by Th81;
FALSUM => p in CnIPC X by Th9;
hence FALSUM => p in CnS4 X by A9; ::_thesis: p 'or' (p => FALSUM) in CnS4 X
for T being Subset of MC-wff st T is S4_theory & X c= T holds
p 'or' (p => FALSUM) in T by Def22;
hence p 'or' (p => FALSUM) in CnS4 X by Def23; ::_thesis: verum
end;
theorem Th83: :: INTPRO_1:83
for X being Subset of MC-wff
for p, q being Element of MC-wff st p in CnS4 X & p => q in CnS4 X holds
q in CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff st p in CnS4 X & p => q in CnS4 X holds
q in CnS4 X
let p, q be Element of MC-wff ; ::_thesis: ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X )
assume that
A1: p in CnS4 X and
A2: p => q in CnS4 X ; ::_thesis: q in CnS4 X
for T being Subset of MC-wff st T is S4_theory & X c= T holds
q in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory & X c= T implies q in T )
assume that
A3: T is S4_theory and
A4: X c= T ; ::_thesis: q in T
A5: p => q in T by A2, A3, A4, Def23;
p in T by A1, A3, A4, Def23;
hence q in T by A3, A5, Def22; ::_thesis: verum
end;
hence q in CnS4 X by Def23; ::_thesis: verum
end;
theorem Th84: :: INTPRO_1:84
for X being Subset of MC-wff
for p, q being Element of MC-wff holds (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: for p, q being Element of MC-wff holds (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X
let p, q be Element of MC-wff ; ::_thesis: (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X
for T being Subset of MC-wff st T is S4_theory & X c= T holds
(Nes (p => q)) => ((Nes p) => (Nes q)) in T by Def22;
hence (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X by Def23; ::_thesis: verum
end;
theorem Th85: :: INTPRO_1:85
for X being Subset of MC-wff
for p being Element of MC-wff holds (Nes p) => p in CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: for p being Element of MC-wff holds (Nes p) => p in CnS4 X
let p be Element of MC-wff ; ::_thesis: (Nes p) => p in CnS4 X
for T being Subset of MC-wff st T is S4_theory & X c= T holds
(Nes p) => p in T by Def22;
hence (Nes p) => p in CnS4 X by Def23; ::_thesis: verum
end;
theorem Th86: :: INTPRO_1:86
for X being Subset of MC-wff
for p being Element of MC-wff holds (Nes p) => (Nes (Nes p)) in CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: for p being Element of MC-wff holds (Nes p) => (Nes (Nes p)) in CnS4 X
let p be Element of MC-wff ; ::_thesis: (Nes p) => (Nes (Nes p)) in CnS4 X
for T being Subset of MC-wff st T is S4_theory & X c= T holds
(Nes p) => (Nes (Nes p)) in T by Def22;
hence (Nes p) => (Nes (Nes p)) in CnS4 X by Def23; ::_thesis: verum
end;
theorem Th87: :: INTPRO_1:87
for X being Subset of MC-wff
for p being Element of MC-wff st p in CnS4 X holds
Nes p in CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: for p being Element of MC-wff st p in CnS4 X holds
Nes p in CnS4 X
let p be Element of MC-wff ; ::_thesis: ( p in CnS4 X implies Nes p in CnS4 X )
assume A1: p in CnS4 X ; ::_thesis: Nes p in CnS4 X
for T being Subset of MC-wff st T is S4_theory & X c= T holds
Nes p in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory & X c= T implies Nes p in T )
assume that
A2: T is S4_theory and
A3: X c= T ; ::_thesis: Nes p in T
p in T by A1, A2, A3, Def23;
hence Nes p in T by A2, Def22; ::_thesis: verum
end;
hence Nes p in CnS4 X by Def23; ::_thesis: verum
end;
theorem Th88: :: INTPRO_1:88
for T, X being Subset of MC-wff st T is S4_theory & X c= T holds
CnS4 X c= T
proof
let T, X be Subset of MC-wff; ::_thesis: ( T is S4_theory & X c= T implies CnS4 X c= T )
assume that
A1: T is S4_theory and
A2: X c= T ; ::_thesis: CnS4 X c= T
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnS4 X or a in T )
thus ( not a in CnS4 X or a in T ) by A1, A2, Def23; ::_thesis: verum
end;
theorem Th89: :: INTPRO_1:89
for X being Subset of MC-wff holds X c= CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: X c= CnS4 X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in CnS4 X )
assume A1: a in X ; ::_thesis: a in CnS4 X
then reconsider t = a as Element of MC-wff ;
for T being Subset of MC-wff st T is S4_theory & X c= T holds
t in T by A1;
hence a in CnS4 X by Def23; ::_thesis: verum
end;
theorem Th90: :: INTPRO_1:90
for X, Y being Subset of MC-wff st X c= Y holds
CnS4 X c= CnS4 Y
proof
let X, Y be Subset of MC-wff; ::_thesis: ( X c= Y implies CnS4 X c= CnS4 Y )
assume A1: X c= Y ; ::_thesis: CnS4 X c= CnS4 Y
thus CnS4 X c= CnS4 Y ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnS4 X or a in CnS4 Y )
assume A2: a in CnS4 X ; ::_thesis: a in CnS4 Y
then reconsider t = a as Element of MC-wff ;
for T being Subset of MC-wff st T is S4_theory & Y c= T holds
t in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory & Y c= T implies t in T )
assume that
A3: T is S4_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, Def23; ::_thesis: verum
end;
hence a in CnS4 Y by Def23; ::_thesis: verum
end;
end;
Lm23: for X being Subset of MC-wff holds CnS4 (CnS4 X) c= CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: CnS4 (CnS4 X) c= CnS4 X
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnS4 (CnS4 X) or a in CnS4 X )
assume A1: a in CnS4 (CnS4 X) ; ::_thesis: a in CnS4 X
then reconsider t = a as Element of MC-wff ;
for T being Subset of MC-wff st T is S4_theory & X c= T holds
t in T
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory & X c= T implies t in T )
assume that
A2: T is S4_theory and
A3: X c= T ; ::_thesis: t in T
CnS4 X c= T by A2, A3, Th88;
hence t in T by A1, A2, Def23; ::_thesis: verum
end;
hence a in CnS4 X by Def23; ::_thesis: verum
end;
theorem :: INTPRO_1:91
for X being Subset of MC-wff holds CnS4 (CnS4 X) = CnS4 X
proof
let X be Subset of MC-wff; ::_thesis: CnS4 (CnS4 X) = CnS4 X
A1: CnS4 X c= CnS4 (CnS4 X) by Th89;
CnS4 (CnS4 X) c= CnS4 X by Lm23;
hence CnS4 (CnS4 X) = CnS4 X by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
Lm24: for X being Subset of MC-wff holds CnS4 X is S4_theory
proof
let X be Subset of MC-wff; ::_thesis: CnS4 X is S4_theory
let p be Element of MC-wff ; :: according to INTPRO_1:def_22 ::_thesis: for q, r being Element of MC-wff holds
( p => (q => p) in CnS4 X & (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X & (p '&' q) => p in CnS4 X & (p '&' q) => q in CnS4 X & p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
let q, r be Element of MC-wff ; ::_thesis: ( p => (q => p) in CnS4 X & (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X & (p '&' q) => p in CnS4 X & (p '&' q) => q in CnS4 X & p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus p => (q => p) in CnS4 X by Th82; ::_thesis: ( (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X & (p '&' q) => p in CnS4 X & (p '&' q) => q in CnS4 X & p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus (p => (q => r)) => ((p => q) => (p => r)) in CnS4 X by Th82; ::_thesis: ( (p '&' q) => p in CnS4 X & (p '&' q) => q in CnS4 X & p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus (p '&' q) => p in CnS4 X by Th82; ::_thesis: ( (p '&' q) => q in CnS4 X & p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus (p '&' q) => q in CnS4 X by Th82; ::_thesis: ( p => (q => (p '&' q)) in CnS4 X & p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus p => (q => (p '&' q)) in CnS4 X by Th82; ::_thesis: ( p => (p 'or' q) in CnS4 X & q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus p => (p 'or' q) in CnS4 X by Th82; ::_thesis: ( q => (p 'or' q) in CnS4 X & (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus q => (p 'or' q) in CnS4 X by Th82; ::_thesis: ( (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X & FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 X by Th82; ::_thesis: ( FALSUM => p in CnS4 X & p 'or' (p => FALSUM) in CnS4 X & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus FALSUM => p in CnS4 X by Th82; ::_thesis: ( p 'or' (p => FALSUM) in CnS4 X & (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus p 'or' (p => FALSUM) in CnS4 X by Th82; ::_thesis: ( (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X & (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X by Th84; ::_thesis: ( (Nes p) => p in CnS4 X & (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus (Nes p) => p in CnS4 X by Th85; ::_thesis: ( (Nes p) => (Nes (Nes p)) in CnS4 X & ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus (Nes p) => (Nes (Nes p)) in CnS4 X by Th86; ::_thesis: ( ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) & ( p in CnS4 X implies Nes p in CnS4 X ) )
thus ( p in CnS4 X & p => q in CnS4 X implies q in CnS4 X ) by Th83; ::_thesis: ( p in CnS4 X implies Nes p in CnS4 X )
thus ( p in CnS4 X implies Nes p in CnS4 X ) by Th87; ::_thesis: verum
end;
registration
let X be Subset of MC-wff;
cluster CnS4 X -> S4_theory ;
coherence
CnS4 X is S4_theory by Lm24;
end;
theorem Th92: :: INTPRO_1:92
for T being Subset of MC-wff holds
( T is S4_theory iff CnS4 T = T )
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory iff CnS4 T = T )
hereby ::_thesis: ( CnS4 T = T implies T is S4_theory )
assume A1: T is S4_theory ; ::_thesis: CnS4 T = T
A2: CnS4 T c= T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in CnS4 T or a in T )
assume a in CnS4 T ; ::_thesis: a in T
hence a in T by A1, Def23; ::_thesis: verum
end;
T c= CnS4 T by Th89;
hence CnS4 T = T by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
thus ( CnS4 T = T implies T is S4_theory ) ; ::_thesis: verum
end;
theorem :: INTPRO_1:93
for T being Subset of MC-wff st T is S4_theory holds
S4-Taut c= T
proof
let T be Subset of MC-wff; ::_thesis: ( T is S4_theory implies S4-Taut c= T )
assume A1: T is S4_theory ; ::_thesis: S4-Taut c= T
S4-Taut c= CnS4 T by Th90, XBOOLE_1:2;
hence S4-Taut c= T by A1, Th92; ::_thesis: verum
end;
registration
cluster S4-Taut -> S4_theory ;
coherence
S4-Taut is S4_theory ;
end;
theorem :: INTPRO_1:94
CPC-Taut c= S4-Taut by Th80;
theorem :: INTPRO_1:95
IPC-Taut c= S4-Taut by Th81;