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