:: INTPRO_1 semantic presentation

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 :

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 :

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 :

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 :

definition

let E be set ;
attr E is with_int_propositional_variables means :Def5: :: INTPRO_1:def 5
for n being Nat holds <*(5 + (2 * n))*> in E;

end;

:: deftheorem Def5 defines with_int_propositional_variables INTPRO_1:def 5 :

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 :

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 :

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 set ;
coherence by Def7, Lm1;
cluster with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator -> MC-closed Element of K40((NAT * ));
coherence 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines MC-wff INTPRO_1:def 8 :

registration

cluster MC-wff -> non empty with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator MC-closed ;
coherence by Def8;

end;

registration

cluster non empty with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator MC-closed set ;
existence

proof end;

end;

registration

cluster MC-wff -> non empty functional with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator MC-closed ;
coherence

proof end;

end;

registration

cluster -> FinSequence-like Element of MC-wff ;
coherence

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 by Def1;
let p, q be Element of MC-wff ;
func p => q -> MC-formula equals :: INTPRO_1:def 10
(<*1*> ^ p) ^ q;
correctness by Def2;
func p '&' q -> MC-formula equals :: INTPRO_1:def 11
(<*2*> ^ p) ^ q;
correctness by Def3;
func p 'or' q -> MC-formula equals :: INTPRO_1:def 12
(<*3*> ^ p) ^ q;
correctness by Def4;

end;

:: deftheorem defines FALSUM INTPRO_1:def 9 :

:: deftheorem defines => INTPRO_1:def 10 :

:: deftheorem defines '&' INTPRO_1:def 11 :

:: deftheorem defines 'or' INTPRO_1:def 12 :

definition

let p be Element of MC-wff ;
func Nes p -> MC-formula equals :: INTPRO_1:def 13
<*6*> ^ p;
correctness by Def6;

end;

:: deftheorem defines Nes INTPRO_1:def 13 :

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 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines CnIPC INTPRO_1:def 15 :

definition

func IPC-Taut -> Subset of MC-wff equals :: INTPRO_1:def 16
CnIPC ({} MC-wff );
correctness ;

end;

:: deftheorem defines IPC-Taut INTPRO_1:def 16 :

definition

let p be Element of MC-wff ;
func neg p -> MC-formula equals :: INTPRO_1:def 17
p => FALSUM ;
correctness ;

end;

:: deftheorem defines neg INTPRO_1:def 17 :

definition

func IVERUM -> MC-formula equals :: INTPRO_1:def 18
FALSUM => FALSUM ;
correctness ;

end;

:: deftheorem defines IVERUM INTPRO_1:def 18 :

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 q, p 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, r, q 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

proof end;

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

proof end;

registration

let X be Subset of MC-wff ;
cluster CnIPC X -> IPC_theory ;
coherence 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 ;

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 q, p 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

proof end;

theorem :: INTPRO_1:21

for q, p being Element of MC-wff holds (q => p) => (p => p) in IPC-Taut

proof end;

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 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 q, r, p, 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 q, p being Element of MC-wff holds q => ((q => p) => p) in IPC-Taut

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

proof 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 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 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, s, q 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, s, q 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, s, q 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 s, q, p 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 :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 :

theorem Th67: :: INTPRO_1:67

for T being Subset of MC-wff st T is CPC_theory holds
T is IPC_theory

proof 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines CnCPC INTPRO_1:def 20 :

definition

func CPC-Taut -> Subset of MC-wff equals :: INTPRO_1:def 21
CnCPC ({} MC-wff );
correctness ;

end;

:: deftheorem defines CPC-Taut INTPRO_1:def 21 :

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

proof end;

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

proof end;

registration

let X be Subset of MC-wff ;
cluster CnCPC X -> CPC_theory ;
coherence 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 ;

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

theorem Th78: :: INTPRO_1:78

for T being Subset of MC-wff st T is S4_theory holds
T is CPC_theory

proof end;

theorem :: INTPRO_1:79

for T being Subset of MC-wff st T is S4_theory holds
T is IPC_theory

proof 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def23 defines CnS4 INTPRO_1:def 23 :

definition

func S4-Taut -> Subset of MC-wff equals :: INTPRO_1:def 24
CnS4 ({} MC-wff );
correctness ;

end;

:: deftheorem defines S4-Taut INTPRO_1:def 24 :

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

proof end;

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

proof end;

registration

let X be Subset of MC-wff ;
cluster CnS4 X -> S4_theory ;
coherence 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 ;

end;

theorem :: INTPRO_1:94

CPC-Taut c= S4-Taut by Th80;

theorem :: INTPRO_1:95

IPC-Taut c= S4-Taut by Th81;