:: Intuitionistic Propositional Calculus in the Extended Framework with Modal Operator, Part I
:: by Takao Inou\'e
::
:: Received April 3, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users


:: language with modal operator
definition
let E be set ;
attr E 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 ;
attr E 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 ;
attr E 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 ;
attr E 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 ;
attr E 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 ;
attr E 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 );

:: We reserve <*4*> for verum for a possible formulation.
:: So do we <* 5+2*n+1 *> for every n >= 1 for introduction of a number of
:: other logical connectives (e.g. for polymodal logics,
:: hybrid logics, recent computer-oriented logics and so on).
definition
let E be set ;
attr E 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 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 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 K16((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
;
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 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 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 end;
end;

registration
cluster MC-wff -> functional ;
coherence
MC-wff is functional
proof 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 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 ;
func p => q -> MC-formula equals :: INTPRO_1:def 10
(<*1*> ^ p) ^ q;
correctness
coherence
(<*1*> ^ p) ^ q is MC-formula
;
by Def2;
func p '&' q -> MC-formula equals :: INTPRO_1:def 11
(<*2*> ^ p) ^ q;
correctness
coherence
(<*2*> ^ p) ^ q is MC-formula
;
by Def3;
func p '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;
attr T 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 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 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 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 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 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 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 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 end;

theorem Th7: :: INTPRO_1:7
for X being Subset of MC-wff
for p, q being Element of MC-wff holds q => (p 'or' q) in CnIPC X
proof end;

theorem Th8: :: INTPRO_1:8
for X being Subset of MC-wff
for p, q, r being Element of MC-wff holds (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC X
proof 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 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 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 by Def15;

theorem Th12: :: INTPRO_1:12
for X being Subset of MC-wff holds X c= CnIPC X
proof 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 end;

Lm2: for X being Subset of MC-wff holds CnIPC (CnIPC X) c= CnIPC X
proof end;

theorem :: INTPRO_1:14
for X being Subset of MC-wff holds CnIPC (CnIPC X) = CnIPC X
proof end;

Lm3: for X being Subset of MC-wff holds CnIPC X is IPC_theory
by Th1, Th2, Th3, Th4, Th5, Th6, Th7, Th8, Th9, Th10;

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

theorem :: INTPRO_1:16
for T being Subset of MC-wff st T is IPC_theory holds
IPC-Taut c= T
proof end;

registration
cluster IPC-Taut -> IPC_theory ;
coherence
IPC-Taut is IPC_theory
;
end;

theorem Th17: :: INTPRO_1:17
for p being Element of MC-wff holds p => p in IPC-Taut
proof end;

theorem Th18: :: INTPRO_1:18
for p, q being Element of MC-wff st q in IPC-Taut holds
p => q in IPC-Taut
proof 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 p, q being Element of MC-wff holds (q => p) => (p => p) in IPC-Taut by Th17, Th18;

theorem Th22: :: INTPRO_1:22
for p, q, r being Element of MC-wff holds (q => r) => ((p => q) => (p => r)) in IPC-Taut
proof 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 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 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 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 end;

Lm4: for p, q, r, s being Element of MC-wff holds (((q => r) => (p => r)) => s) => ((p => q) => s) in IPC-Taut
proof 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 end;

theorem :: INTPRO_1:28
for p, q, r being Element of MC-wff holds ((p => q) => r) => (q => r) in IPC-Taut
proof 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 end;

theorem Th30: :: INTPRO_1:30
for p, q being Element of MC-wff holds (p => (p => q)) => (p => q) in IPC-Taut
proof end;

theorem :: INTPRO_1:31
for p, q being Element of MC-wff holds q => ((q => p) => p) in IPC-Taut
proof end;

theorem Th32: :: INTPRO_1:32
for p, q, s being Element of MC-wff st s => (q => p) in IPC-Taut & q in IPC-Taut holds
s => p in IPC-Taut
proof end;

theorem Th33: :: INTPRO_1:33
for p being Element of MC-wff holds p => (p '&' p) in IPC-Taut
proof 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 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 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 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 end;

theorem Th38: :: INTPRO_1:38
for p, q, r being Element of MC-wff holds (r => p) => ((r => q) => (r => (p '&' q))) in IPC-Taut
proof end;

theorem Th39: :: INTPRO_1:39
for p, q being Element of MC-wff holds ((p => q) '&' p) => q in IPC-Taut
proof end;

theorem :: INTPRO_1:40
for p, q, s being Element of MC-wff holds (((p => q) '&' p) '&' s) => q in IPC-Taut
proof end;

theorem :: INTPRO_1:41
for p, q, s being Element of MC-wff holds (q => s) => ((p '&' q) => s) in IPC-Taut
proof end;

theorem Th42: :: INTPRO_1:42
for p, q, s being Element of MC-wff holds (q => s) => ((q '&' p) => s) in IPC-Taut
proof end;

theorem Th43: :: INTPRO_1:43
for p, q, s being Element of MC-wff holds ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in IPC-Taut
proof 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 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 end;

theorem Th46: :: INTPRO_1:46
for p, q being Element of MC-wff holds (p '&' q) => (q '&' p) in IPC-Taut
proof 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 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 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 end;

theorem :: INTPRO_1:50
for p, q, s being Element of MC-wff holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut
proof 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 end;

Lm5: for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => q in IPC-Taut
proof 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 end;

Lm7: for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in IPC-Taut
proof end;

Lm8: for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (p '&' s) in IPC-Taut
proof end;

Lm9: for p, q, s being Element of MC-wff holds (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in IPC-Taut
proof end;

Lm10: for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((p '&' s) '&' q) in IPC-Taut
proof end;

Lm11: for p, q, s being Element of MC-wff holds ((p '&' s) '&' q) => ((s '&' p) '&' q) in IPC-Taut
proof end;

Lm12: for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((s '&' p) '&' q) in IPC-Taut
proof end;

Lm13: for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((s '&' q) '&' p) in IPC-Taut
proof end;

Lm14: for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (p '&' (s '&' q)) in IPC-Taut
proof end;

Lm15: for p, q, s being Element of MC-wff holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut
proof 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 end;

Lm16: for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((s '&' q) '&' p) in IPC-Taut
proof end;

Lm17: for p, q, s being Element of MC-wff holds ((s '&' q) '&' p) => ((q '&' s) '&' p) in IPC-Taut
proof end;

Lm18: for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((q '&' s) '&' p) in IPC-Taut
proof end;

Lm19: for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((p '&' s) '&' q) in IPC-Taut
proof end;

Lm20: for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => (p '&' (s '&' q)) in IPC-Taut
proof 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 end;

theorem Th54: :: INTPRO_1:54
for p being Element of MC-wff holds (p 'or' p) => p in IPC-Taut
proof 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 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 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 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 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 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 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 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 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 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 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 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 end;

definition
let T be Subset of MC-wff;
attr T is CPC_theory means :: 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 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 :: INTPRO_1:67
for T being Subset of MC-wff st T is CPC_theory holds
T is IPC_theory ;

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 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 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 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 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 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 by Def20;

theorem Th72: :: INTPRO_1:72
for X being Subset of MC-wff holds X c= CnCPC X
proof 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 end;

Lm21: for X being Subset of MC-wff holds CnCPC (CnCPC X) c= CnCPC X
proof end;

theorem :: INTPRO_1:74
for X being Subset of MC-wff holds CnCPC (CnCPC X) = CnCPC X
proof end;

Lm22: for X being Subset of MC-wff holds CnCPC X is CPC_theory
by Th69, Th70;

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

theorem :: INTPRO_1:76
for T being Subset of MC-wff st T is CPC_theory holds
CPC-Taut c= T
proof 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;

definition
let T be Subset of MC-wff;
attr T is S4_theory means :: 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 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 :: INTPRO_1:78
for T being Subset of MC-wff st T is S4_theory holds
T is CPC_theory ;

theorem :: INTPRO_1:79
for T being Subset of MC-wff st T is S4_theory holds
T is IPC_theory ;

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

theorem Th81: :: INTPRO_1:81
for X being Subset of MC-wff holds CnIPC X c= CnS4 X
proof 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 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 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 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 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 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 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 by Def23;

theorem Th89: :: INTPRO_1:89
for X being Subset of MC-wff holds X c= CnS4 X
proof 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 end;

Lm23: for X being Subset of MC-wff holds CnS4 (CnS4 X) c= CnS4 X
proof end;

theorem :: INTPRO_1:91
for X being Subset of MC-wff holds CnS4 (CnS4 X) = CnS4 X
proof end;

Lm24: for X being Subset of MC-wff holds CnS4 X is S4_theory
by Th82, Th84, Th85, Th86, Th83, Th87;

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

theorem :: INTPRO_1:93
for T being Subset of MC-wff st T is S4_theory holds
S4-Taut c= T
proof 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;