begin
:: deftheorem Def1 defines with_FALSUM INTPRO_1:def 1 :
for E being set holds
( E is with_FALSUM iff <*0 *> in E );
:: 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 );
:: 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 );
:: 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 );
:: 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 );
:: 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 );
:: 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
:: 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 ) ) );
:: 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;
:: deftheorem defines Nes INTPRO_1:def 13 :
for p being Element of MC-wff holds Nes p = <*6*> ^ p;
:: 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 ) ) );
:: 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 ) );
:: deftheorem defines IPC-Taut INTPRO_1:def 16 :
IPC-Taut = CnIPC ({} MC-wff );
:: deftheorem defines neg INTPRO_1:def 17 :
for p being Element of MC-wff holds neg p = p => FALSUM ;
:: deftheorem defines IVERUM INTPRO_1:def 18 :
IVERUM = FALSUM => FALSUM ;
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
Lm2:
for X being Subset of MC-wff holds CnIPC (CnIPC X) c= CnIPC X
theorem
Lm3:
for X being Subset of MC-wff holds CnIPC X is IPC_theory
theorem Th15:
theorem
begin
theorem Th17:
theorem Th18:
theorem
theorem
theorem
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
Lm4:
for q, r, p, s being Element of MC-wff holds (((q => r) => (p => r)) => s) => ((p => q) => s) in IPC-Taut
theorem Th27:
theorem
theorem Th29:
theorem Th30:
theorem
theorem Th32:
begin
theorem Th33:
theorem Th34:
theorem
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem
theorem
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem
theorem
Lm5:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => q in IPC-Taut
Lm6:
for p, q, s being Element of MC-wff holds (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in IPC-Taut
Lm7:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in IPC-Taut
Lm8:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (p '&' s) in IPC-Taut
Lm9:
for p, q, s being Element of MC-wff holds (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in IPC-Taut
Lm10:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((p '&' s) '&' q) in IPC-Taut
Lm11:
for p, s, q being Element of MC-wff holds ((p '&' s) '&' q) => ((s '&' p) '&' q) in IPC-Taut
Lm12:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((s '&' p) '&' q) in IPC-Taut
Lm13:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((s '&' q) '&' p) in IPC-Taut
Lm14:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (p '&' (s '&' q)) in IPC-Taut
Lm15:
for p, s, q being Element of MC-wff holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut
theorem
Lm16:
for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((s '&' q) '&' p) in IPC-Taut
Lm17:
for s, q, p being Element of MC-wff holds ((s '&' q) '&' p) => ((q '&' s) '&' p) in IPC-Taut
Lm18:
for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((q '&' s) '&' p) in IPC-Taut
Lm19:
for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((p '&' s) '&' q) in IPC-Taut
Lm20:
for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => (p '&' (s '&' q)) in IPC-Taut
theorem
begin
theorem Th54:
theorem
theorem Th56:
theorem
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem
theorem
begin
:: 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:
:: 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 ) );
:: deftheorem defines CPC-Taut INTPRO_1:def 21 :
CPC-Taut = CnCPC ({} MC-wff );
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
Lm21:
for X being Subset of MC-wff holds CnCPC (CnCPC X) c= CnCPC X
theorem
Lm22:
for X being Subset of MC-wff holds CnCPC X is CPC_theory
theorem Th75:
theorem
theorem
begin
:: 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:
theorem
:: 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 ) );
:: deftheorem defines S4-Taut INTPRO_1:def 24 :
S4-Taut = CnS4 ({} MC-wff );
theorem Th80:
theorem Th81:
theorem Th82:
theorem Th83:
theorem Th84:
theorem Th85:
theorem Th86:
theorem Th87:
theorem Th88:
theorem Th89:
theorem Th90:
Lm23:
for X being Subset of MC-wff holds CnS4 (CnS4 X) c= CnS4 X
theorem
Lm24:
for X being Subset of MC-wff holds CnS4 X is S4_theory
theorem Th92:
theorem
theorem
theorem