:: INTPRO_1 semantic presentation

definition

let c₁ be set ;
attr a₁ is with_FALSUM means :Def1: :: INTPRO_1:def 1
<*0*> in a₁;

end;

:: deftheorem Def1 defines with_FALSUM INTPRO_1:def 1 :

definition

let c₁ be set ;
attr a₁ is with_int_implication means :Def2: :: INTPRO_1:def 2
for b₁, b₂ being FinSequence st b₁ in a₁ & b₂ in a₁ holds
(<*1*> ^ b₁) ^ b₂ in a₁;

end;

:: deftheorem Def2 defines with_int_implication INTPRO_1:def 2 :

definition

let c₁ be set ;
attr a₁ is with_int_conjunction means :Def3: :: INTPRO_1:def 3
for b₁, b₂ being FinSequence st b₁ in a₁ & b₂ in a₁ holds
(<*2*> ^ b₁) ^ b₂ in a₁;

end;

:: deftheorem Def3 defines with_int_conjunction INTPRO_1:def 3 :

definition

let c₁ be set ;
attr a₁ is with_int_disjunction means :Def4: :: INTPRO_1:def 4
for b₁, b₂ being FinSequence st b₁ in a₁ & b₂ in a₁ holds
(<*3*> ^ b₁) ^ b₂ in a₁;

end;

:: deftheorem Def4 defines with_int_disjunction INTPRO_1:def 4 :

definition

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

end;

:: deftheorem Def5 defines with_int_propositional_variables INTPRO_1:def 5 :

definition

let c₁ be set ;
attr a₁ is with_modal_operator means :Def6: :: INTPRO_1:def 6
for b₁ being FinSequence st b₁ in a₁ holds
<*6*> ^ b₁ in a₁;

end;

:: deftheorem Def6 defines with_modal_operator INTPRO_1:def 6 :

definition

let c₁ be set ;
attr a₁ is MC-closed means :Def7: :: INTPRO_1:def 7
( a₁ c= NAT * & a₁ is with_FALSUM & a₁ is with_int_implication & a₁ is with_int_conjunction & a₁ is with_int_disjunction & a₁ is with_int_propositional_variables & a₁ is with_modal_operator );

end;

:: deftheorem Def7 defines MC-closed INTPRO_1:def 7 :

Lemma8: for b₁ being set st b₁ is MC-closed holds
not b₁ 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, Lemma8;
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
( a₁ is MC-closed & ( for b₁ being set st b₁ is MC-closed holds
a₁ c= b₁ ) );
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 c₁, c₂ be Element of MC-wff ;
func c₁ => c₂ -> MC-formula equals :: INTPRO_1:def 10
(<*1*> ^ a₁) ^ a₂;
correctness by Def2;
func c₁ '&' c₂ -> MC-formula equals :: INTPRO_1:def 11
(<*2*> ^ a₁) ^ a₂;
correctness by Def3;
func c₁ 'or' c₂ -> MC-formula equals :: INTPRO_1:def 12
(<*3*> ^ a₁) ^ a₂;
correctness by Def4;

end;

:: deftheorem Def9 defines FALSUM INTPRO_1:def 9 :

:: deftheorem Def10 defines => INTPRO_1:def 10 :

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

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

definition

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

end;

:: deftheorem Def13 defines Nes INTPRO_1:def 13 :

definition

let c₁ be Subset of MC-wff ;
attr a₁ is IPC_theory means :Def14: :: INTPRO_1:def 14
for b₁, b₂, b₃ being Element of MC-wff holds
( b₁ => (b₂ => b₁) in a₁ & (b₁ => (b₂ => b₃)) => ((b₁ => b₂) => (b₁ => b₃)) in a₁ & (b₁ '&' b₂) => b₁ in a₁ & (b₁ '&' b₂) => b₂ in a₁ & b₁ => (b₂ => (b₁ '&' b₂)) in a₁ & b₁ => (b₁ 'or' b₂) in a₁ & b₂ => (b₁ 'or' b₂) in a₁ & (b₁ => b₃) => ((b₂ => b₃) => ((b₁ 'or' b₂) => b₃)) in a₁ & FALSUM => b₁ in a₁ & ( b₁ in a₁ & b₁ => b₂ in a₁ implies b₂ in a₁ ) );
correctness ;

end;

:: deftheorem Def14 defines IPC_theory INTPRO_1:def 14 :

definition

let c₁ be Subset of MC-wff ;
func CnIPC c₁ -> Subset of MC-wff means :Def15: :: INTPRO_1:def 15
for b₁ being Element of MC-wff holds
( b₁ in a₂ iff for b₂ being Subset of MC-wff st b₂ is IPC_theory & a₁ c= b₂ holds
b₁ in b₂ );
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 Def16 defines IPC-Taut INTPRO_1:def 16 :

definition

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

end;

:: deftheorem Def17 defines neg INTPRO_1:def 17 :

definition

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

end;

:: deftheorem Def18 defines IVERUM INTPRO_1:def 18 :

theorem Th1: :: INTPRO_1:1

for b₁ being Subset of MC-wff
for b₂, b₃ being Element of MC-wff holds b₂ => (b₃ => b₂) in CnIPC b₁

proof end;

theorem Th2: :: INTPRO_1:2

for b₁ being Subset of MC-wff
for b₂, b₃, b₄ being Element of MC-wff holds (b₂ => (b₃ => b₄)) => ((b₂ => b₃) => (b₂ => b₄)) in CnIPC b₁

proof end;

theorem Th3: :: INTPRO_1:3

for b₁ being Subset of MC-wff
for b₂, b₃ being Element of MC-wff holds (b₂ '&' b₃) => b₂ in CnIPC b₁

proof end;

theorem Th4: :: INTPRO_1:4

for b₁ being Subset of MC-wff
for b₂, b₃ being Element of MC-wff holds (b₂ '&' b₃) => b₃ in CnIPC b₁

proof end;

theorem Th5: :: INTPRO_1:5

for b₁ being Subset of MC-wff
for b₂, b₃ being Element of MC-wff holds b₂ => (b₃ => (b₂ '&' b₃)) in CnIPC b₁

proof end;

theorem Th6: :: INTPRO_1:6

for b₁ being Subset of MC-wff
for b₂, b₃ being Element of MC-wff holds b₂ => (b₂ 'or' b₃) in CnIPC b₁

proof end;

theorem Th7: :: INTPRO_1:7

for b₁ being Subset of MC-wff
for b₂, b₃ being Element of MC-wff holds b₂ => (b₃ 'or' b₂) in CnIPC b₁

proof end;

theorem Th8: :: INTPRO_1:8

for b₁ being Subset of MC-wff
for b₂, b₃, b₄ being Element of MC-wff holds (b₂ => b₃) => ((b₄ => b₃) => ((b₂ 'or' b₄) => b₃)) in CnIPC b₁

proof end;

theorem Th9: :: INTPRO_1:9

for b₁ being Subset of MC-wff
for b₂ being Element of MC-wff holds FALSUM => b₂ in CnIPC b₁

proof end;

theorem Th10: :: INTPRO_1:10

for b₁ being Subset of MC-wff
for b₂, b₃ being Element of MC-wff st b₂ in CnIPC b₁ & b₂ => b₃ in CnIPC b₁ holds
b₃ in CnIPC b₁

proof end;

theorem Th11: :: INTPRO_1:11

for b₁, b₂ being Subset of MC-wff st b₁ is IPC_theory & b₂ c= b₁ holds
CnIPC b₂ c= b₁

proof end;

theorem Th12: :: INTPRO_1:12

for b₁ being Subset of MC-wff holds b₁ c= CnIPC b₁

proof end;

theorem Th13: :: INTPRO_1:13

for b₁, b₂ being Subset of MC-wff st b₁ c= b₂ holds
CnIPC b₁ c= CnIPC b₂

proof end;

Lemma25: for b₁ being Subset of MC-wff holds CnIPC (CnIPC b₁) c= CnIPC b₁

proof end;

theorem Th14: :: INTPRO_1:14

for b₁ being Subset of MC-wff holds CnIPC (CnIPC b₁) = CnIPC b₁

proof end;

Lemma26: for b₁ being Subset of MC-wff holds CnIPC b₁ is IPC_theory

proof end;

registration

let c₁ be Subset of MC-wff ;
cluster CnIPC a₁ -> IPC_theory ;
coherence by Lemma26;

end;

theorem Th15: :: INTPRO_1:15

for b₁ being Subset of MC-wff holds
( b₁ is IPC_theory iff CnIPC b₁ = b₁ )

proof end;

theorem Th16: :: INTPRO_1:16

for b₁ being Subset of MC-wff st b₁ is IPC_theory holds
IPC-Taut c= b₁

proof end;

registration

cluster IPC-Taut -> IPC_theory ;
coherence ;

end;

theorem Th17: :: INTPRO_1:17

for b₁ being Element of MC-wff holds b₁ => b₁ in IPC-Taut

proof end;

theorem Th18: :: INTPRO_1:18

for b₁, b₂ being Element of MC-wff st b₁ in IPC-Taut holds
b₂ => b₁ in IPC-Taut

proof end;

theorem Th19: :: INTPRO_1:19

IVERUM in IPC-Taut by Def14;

theorem Th20: :: INTPRO_1:20

for b₁, b₂ being Element of MC-wff holds (b₁ => b₂) => (b₁ => b₁) in IPC-Taut

proof end;

theorem Th21: :: INTPRO_1:21

for b₁, b₂ being Element of MC-wff holds (b₁ => b₂) => (b₂ => b₂) in IPC-Taut

proof end;

theorem Th22: :: INTPRO_1:22

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ => b₂) => ((b₃ => b₁) => (b₃ => b₂)) in IPC-Taut

proof end;

theorem Th23: :: INTPRO_1:23

for b₁, b₂, b₃ being Element of MC-wff st b₁ => (b₂ => b₃) in IPC-Taut holds
b₂ => (b₁ => b₃) in IPC-Taut

proof end;

theorem Th24: :: INTPRO_1:24

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ => b₂) => ((b₂ => b₃) => (b₁ => b₃)) in IPC-Taut

proof end;

theorem Th25: :: INTPRO_1:25

for b₁, b₂, b₃ being Element of MC-wff st b₁ => b₂ in IPC-Taut holds
(b₂ => b₃) => (b₁ => b₃) in IPC-Taut

proof end;

theorem Th26: :: INTPRO_1:26

for b₁, b₂, b₃ being Element of MC-wff st b₁ => b₂ in IPC-Taut & b₂ => b₃ in IPC-Taut holds
b₁ => b₃ in IPC-Taut

proof end;

Lemma35: for b₁, b₂, b₃, b₄ being Element of MC-wff holds (((b₁ => b₂) => (b₃ => b₂)) => b₄) => ((b₃ => b₁) => b₄) in IPC-Taut

proof end;

theorem Th27: :: INTPRO_1:27

for b₁, b₂, b₃, b₄ being Element of MC-wff holds (b₁ => (b₂ => b₃)) => ((b₄ => b₂) => (b₁ => (b₄ => b₃))) in IPC-Taut

proof end;

theorem Th28: :: INTPRO_1:28

for b₁, b₂, b₃ being Element of MC-wff holds ((b₁ => b₂) => b₃) => (b₂ => b₃) in IPC-Taut

proof end;

theorem Th29: :: INTPRO_1:29

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ => (b₂ => b₃)) => (b₂ => (b₁ => b₃)) in IPC-Taut

proof end;

theorem Th30: :: INTPRO_1:30

for b₁, b₂ being Element of MC-wff holds (b₁ => (b₁ => b₂)) => (b₁ => b₂) in IPC-Taut

proof end;

theorem Th31: :: INTPRO_1:31

for b₁, b₂ being Element of MC-wff holds b₁ => ((b₁ => b₂) => b₂) in IPC-Taut

proof end;

theorem Th32: :: INTPRO_1:32

for b₁, b₂, b₃ being Element of MC-wff st b₁ => (b₂ => b₃) in IPC-Taut & b₂ in IPC-Taut holds
b₁ => b₃ in IPC-Taut

proof end;

theorem Th33: :: INTPRO_1:33

for b₁ being Element of MC-wff holds b₁ => (b₁ '&' b₁) in IPC-Taut

proof end;

theorem Th34: :: INTPRO_1:34

for b₁, b₂ being Element of MC-wff holds
( b₁ '&' b₂ in IPC-Taut iff ( b₁ in IPC-Taut & b₂ in IPC-Taut ) )

proof end;

theorem Th35: :: INTPRO_1:35

for b₁, b₂ being Element of MC-wff holds
( b₁ '&' b₂ in IPC-Taut iff b₂ '&' b₁ in IPC-Taut )

proof end;

theorem Th36: :: INTPRO_1:36

for b₁, b₂, b₃ being Element of MC-wff holds ((b₁ '&' b₂) => b₃) => (b₁ => (b₂ => b₃)) in IPC-Taut

proof end;

theorem Th37: :: INTPRO_1:37

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ => (b₂ => b₃)) => ((b₁ '&' b₂) => b₃) in IPC-Taut

proof end;

theorem Th38: :: INTPRO_1:38

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ => b₂) => ((b₁ => b₃) => (b₁ => (b₂ '&' b₃))) in IPC-Taut

proof end;

theorem Th39: :: INTPRO_1:39

for b₁, b₂ being Element of MC-wff holds ((b₁ => b₂) '&' b₁) => b₂ in IPC-Taut

proof end;

theorem Th40: :: INTPRO_1:40

for b₁, b₂, b₃ being Element of MC-wff holds (((b₁ => b₂) '&' b₁) '&' b₃) => b₂ in IPC-Taut

proof end;

theorem Th41: :: INTPRO_1:41

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ => b₂) => ((b₃ '&' b₁) => b₂) in IPC-Taut

proof end;

theorem Th42: :: INTPRO_1:42

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ => b₂) => ((b₁ '&' b₃) => b₂) in IPC-Taut

proof end;

theorem Th43: :: INTPRO_1:43

for b₁, b₂, b₃ being Element of MC-wff holds ((b₁ '&' b₂) => b₃) => ((b₁ '&' b₂) => (b₃ '&' b₂)) in IPC-Taut

proof end;

theorem Th44: :: INTPRO_1:44

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ => b₂) => ((b₁ '&' b₃) => (b₂ '&' b₃)) in IPC-Taut

proof end;

theorem Th45: :: INTPRO_1:45

for b₁, b₂, b₃ being Element of MC-wff holds ((b₁ => b₂) '&' (b₁ '&' b₃)) => (b₂ '&' b₃) in IPC-Taut

proof end;

theorem Th46: :: INTPRO_1:46

for b₁, b₂ being Element of MC-wff holds (b₁ '&' b₂) => (b₂ '&' b₁) in IPC-Taut

proof end;

theorem Th47: :: INTPRO_1:47

for b₁, b₂, b₃ being Element of MC-wff holds ((b₁ => b₂) '&' (b₁ '&' b₃)) => (b₃ '&' b₂) in IPC-Taut

proof end;

theorem Th48: :: INTPRO_1:48

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ => b₂) => ((b₁ '&' b₃) => (b₃ '&' b₂)) in IPC-Taut

proof end;

theorem Th49: :: INTPRO_1:49

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ => b₂) => ((b₃ '&' b₁) => (b₃ '&' b₂)) in IPC-Taut

proof end;

theorem Th50: :: INTPRO_1:50

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ '&' (b₂ '&' b₃)) => (b₁ '&' (b₃ '&' b₂)) in IPC-Taut

proof end;

theorem Th51: :: INTPRO_1:51

for b₁, b₂, b₃ being Element of MC-wff holds ((b₁ => b₂) '&' (b₁ => b₃)) => (b₁ => (b₂ '&' b₃)) in IPC-Taut

proof end;

Lemma54: for b₁, b₂, b₃ being Element of MC-wff holds ((b₁ '&' b₂) '&' b₃) => b₂ in IPC-Taut

proof end;

Lemma55: for b₁, b₂, b₃ being Element of MC-wff holds (((b₁ '&' b₂) '&' b₃) '&' ((b₁ '&' b₂) '&' b₃)) => (((b₁ '&' b₂) '&' b₃) '&' b₂) in IPC-Taut

proof end;

Lemma56: for b₁, b₂, b₃ being Element of MC-wff holds ((b₁ '&' b₂) '&' b₃) => (((b₁ '&' b₂) '&' b₃) '&' b₂) in IPC-Taut

proof end;

Lemma57: for b₁, b₂, b₃ being Element of MC-wff holds ((b₁ '&' b₂) '&' b₃) => (b₁ '&' b₃) in IPC-Taut

proof end;

Lemma58: for b₁, b₂, b₃ being Element of MC-wff holds (((b₁ '&' b₂) '&' b₃) '&' b₂) => ((b₁ '&' b₃) '&' b₂) in IPC-Taut

proof end;

Lemma59: for b₁, b₂, b₃ being Element of MC-wff holds ((b₁ '&' b₂) '&' b₃) => ((b₁ '&' b₃) '&' b₂) in IPC-Taut

proof end;

Lemma60: for b₁, b₂, b₃ being Element of MC-wff holds ((b₁ '&' b₂) '&' b₃) => ((b₂ '&' b₁) '&' b₃) in IPC-Taut

proof end;

Lemma61: for b₁, b₂, b₃ being Element of MC-wff holds ((b₁ '&' b₂) '&' b₃) => ((b₃ '&' b₁) '&' b₂) in IPC-Taut

proof end;

Lemma62: for b₁, b₂, b₃ being Element of MC-wff holds ((b₁ '&' b₂) '&' b₃) => ((b₃ '&' b₂) '&' b₁) in IPC-Taut

proof end;

Lemma63: for b₁, b₂, b₃ being Element of MC-wff holds ((b₁ '&' b₂) '&' b₃) => (b₁ '&' (b₃ '&' b₂)) in IPC-Taut

proof end;

Lemma64: for b₁, b₂, b₃ being Element of MC-wff holds (b₁ '&' (b₂ '&' b₃)) => (b₁ '&' (b₃ '&' b₂)) in IPC-Taut

proof end;

theorem Th52: :: INTPRO_1:52

for b₁, b₂, b₃ being Element of MC-wff holds ((b₁ '&' b₂) '&' b₃) => (b₁ '&' (b₂ '&' b₃)) in IPC-Taut

proof end;

Lemma65: for b₁, b₂, b₃ being Element of MC-wff holds (b₁ '&' (b₂ '&' b₃)) => ((b₃ '&' b₂) '&' b₁) in IPC-Taut

proof end;

Lemma66: for b₁, b₂, b₃ being Element of MC-wff holds ((b₁ '&' b₂) '&' b₃) => ((b₂ '&' b₁) '&' b₃) in IPC-Taut

proof end;

Lemma67: for b₁, b₂, b₃ being Element of MC-wff holds (b₁ '&' (b₂ '&' b₃)) => ((b₂ '&' b₃) '&' b₁) in IPC-Taut

proof end;

Lemma68: for b₁, b₂, b₃ being Element of MC-wff holds (b₁ '&' (b₂ '&' b₃)) => ((b₁ '&' b₃) '&' b₂) in IPC-Taut

proof end;

Lemma69: for b₁, b₂, b₃ being Element of MC-wff holds (b₁ '&' (b₂ '&' b₃)) => (b₁ '&' (b₃ '&' b₂)) in IPC-Taut

proof end;

theorem Th53: :: INTPRO_1:53

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ '&' (b₂ '&' b₃)) => ((b₁ '&' b₂) '&' b₃) in IPC-Taut

proof end;

theorem Th54: :: INTPRO_1:54

for b₁ being Element of MC-wff holds (b₁ 'or' b₁) => b₁ in IPC-Taut

proof end;

theorem Th55: :: INTPRO_1:55

for b₁, b₂ being Element of MC-wff st ( b₁ in IPC-Taut or b₂ in IPC-Taut ) holds
b₁ 'or' b₂ in IPC-Taut

proof end;

theorem Th56: :: INTPRO_1:56

for b₁, b₂ being Element of MC-wff holds (b₁ 'or' b₂) => (b₂ 'or' b₁) in IPC-Taut

proof end;

theorem Th57: :: INTPRO_1:57

for b₁, b₂ being Element of MC-wff holds
( b₁ 'or' b₂ in IPC-Taut iff b₂ 'or' b₁ in IPC-Taut )

proof end;

theorem Th58: :: INTPRO_1:58

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ => b₂) => (b₁ => (b₂ 'or' b₃)) in IPC-Taut

proof end;

theorem Th59: :: INTPRO_1:59

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ => b₂) => (b₁ => (b₃ 'or' b₂)) in IPC-Taut

proof end;

theorem Th60: :: INTPRO_1:60

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ => b₂) => ((b₁ 'or' b₃) => (b₂ 'or' b₃)) in IPC-Taut

proof end;

theorem Th61: :: INTPRO_1:61

for b₁, b₂, b₃ being Element of MC-wff st b₁ => b₂ in IPC-Taut holds
(b₁ 'or' b₃) => (b₂ 'or' b₃) in IPC-Taut

proof end;

theorem Th62: :: INTPRO_1:62

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ => b₂) => ((b₃ 'or' b₁) => (b₃ 'or' b₂)) in IPC-Taut

proof end;

theorem Th63: :: INTPRO_1:63

for b₁, b₂, b₃ being Element of MC-wff st b₁ => b₂ in IPC-Taut holds
(b₃ 'or' b₁) => (b₃ 'or' b₂) in IPC-Taut

proof end;

theorem Th64: :: INTPRO_1:64

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ 'or' (b₂ 'or' b₃)) => (b₂ 'or' (b₁ 'or' b₃)) in IPC-Taut

proof end;

theorem Th65: :: INTPRO_1:65

for b₁, b₂, b₃ being Element of MC-wff holds (b₁ 'or' (b₂ 'or' b₃)) => ((b₁ 'or' b₂) 'or' b₃) in IPC-Taut

proof end;

theorem Th66: :: INTPRO_1:66

for b₁, b₂, b₃ being Element of MC-wff holds ((b₁ 'or' b₂) 'or' b₃) => (b₁ 'or' (b₂ 'or' b₃)) in IPC-Taut

proof end;

definition

let c₁ be Subset of MC-wff ;
attr a₁ is CPC_theory means :Def19: :: INTPRO_1:def 19
for b₁, b₂, b₃ being Element of MC-wff holds
( b₁ => (b₂ => b₁) in a₁ & (b₁ => (b₂ => b₃)) => ((b₁ => b₂) => (b₁ => b₃)) in a₁ & (b₁ '&' b₂) => b₁ in a₁ & (b₁ '&' b₂) => b₂ in a₁ & b₁ => (b₂ => (b₁ '&' b₂)) in a₁ & b₁ => (b₁ 'or' b₂) in a₁ & b₂ => (b₁ 'or' b₂) in a₁ & (b₁ => b₃) => ((b₂ => b₃) => ((b₁ 'or' b₂) => b₃)) in a₁ & FALSUM => b₁ in a₁ & b₁ 'or' (b₁ => FALSUM ) in a₁ & ( b₁ in a₁ & b₁ => b₂ in a₁ implies b₂ in a₁ ) );
correctness ;

end;

:: deftheorem Def19 defines CPC_theory INTPRO_1:def 19 :

theorem Th67: :: INTPRO_1:67

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

proof end;

definition

let c₁ be Subset of MC-wff ;
func CnCPC c₁ -> Subset of MC-wff means :Def20: :: INTPRO_1:def 20
for b₁ being Element of MC-wff holds
( b₁ in a₂ iff for b₂ being Subset of MC-wff st b₂ is CPC_theory & a₁ c= b₂ holds
b₁ in b₂ );
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 Def21 defines CPC-Taut INTPRO_1:def 21 :

theorem Th68: :: INTPRO_1:68

for b₁ being Subset of MC-wff holds CnIPC b₁ c= CnCPC b₁

proof end;

theorem Th69: :: INTPRO_1:69

for b₁ being Subset of MC-wff
for b₂, b₃, b₄ being Element of MC-wff holds
( b₂ => (b₃ => b₂) in CnCPC b₁ & (b₂ => (b₃ => b₄)) => ((b₂ => b₃) => (b₂ => b₄)) in CnCPC b₁ & (b₂ '&' b₃) => b₂ in CnCPC b₁ & (b₂ '&' b₃) => b₃ in CnCPC b₁ & b₂ => (b₃ => (b₂ '&' b₃)) in CnCPC b₁ & b₂ => (b₂ 'or' b₃) in CnCPC b₁ & b₃ => (b₂ 'or' b₃) in CnCPC b₁ & (b₂ => b₄) => ((b₃ => b₄) => ((b₂ 'or' b₃) => b₄)) in CnCPC b₁ & FALSUM => b₂ in CnCPC b₁ & b₂ 'or' (b₂ => FALSUM ) in CnCPC b₁ )

proof end;

theorem Th70: :: INTPRO_1:70

for b₁ being Subset of MC-wff
for b₂, b₃ being Element of MC-wff st b₂ in CnCPC b₁ & b₂ => b₃ in CnCPC b₁ holds
b₃ in CnCPC b₁

proof end;

theorem Th71: :: INTPRO_1:71

for b₁, b₂ being Subset of MC-wff st b₁ is CPC_theory & b₂ c= b₁ holds
CnCPC b₂ c= b₁

proof end;

theorem Th72: :: INTPRO_1:72

for b₁ being Subset of MC-wff holds b₁ c= CnCPC b₁

proof end;

theorem Th73: :: INTPRO_1:73

for b₁, b₂ being Subset of MC-wff st b₁ c= b₂ holds
CnCPC b₁ c= CnCPC b₂

proof end;

Lemma88: for b₁ being Subset of MC-wff holds CnCPC (CnCPC b₁) c= CnCPC b₁

proof end;

theorem Th74: :: INTPRO_1:74

for b₁ being Subset of MC-wff holds CnCPC (CnCPC b₁) = CnCPC b₁

proof end;

Lemma89: for b₁ being Subset of MC-wff holds CnCPC b₁ is CPC_theory

proof end;

registration

let c₁ be Subset of MC-wff ;
cluster CnCPC a₁ -> CPC_theory ;
coherence by Lemma89;

end;

theorem Th75: :: INTPRO_1:75

for b₁ being Subset of MC-wff holds
( b₁ is CPC_theory iff CnCPC b₁ = b₁ )

proof end;

theorem Th76: :: INTPRO_1:76

for b₁ being Subset of MC-wff st b₁ is CPC_theory holds
CPC-Taut c= b₁

proof end;

registration

cluster CPC-Taut -> CPC_theory ;
coherence ;

end;

theorem Th77: :: INTPRO_1:77

IPC-Taut c= CPC-Taut by Th68;

definition

let c₁ be Subset of MC-wff ;
attr a₁ is S4_theory means :Def22: :: INTPRO_1:def 22
for b₁, b₂, b₃ being Element of MC-wff holds
( b₁ => (b₂ => b₁) in a₁ & (b₁ => (b₂ => b₃)) => ((b₁ => b₂) => (b₁ => b₃)) in a₁ & (b₁ '&' b₂) => b₁ in a₁ & (b₁ '&' b₂) => b₂ in a₁ & b₁ => (b₂ => (b₁ '&' b₂)) in a₁ & b₁ => (b₁ 'or' b₂) in a₁ & b₂ => (b₁ 'or' b₂) in a₁ & (b₁ => b₃) => ((b₂ => b₃) => ((b₁ 'or' b₂) => b₃)) in a₁ & FALSUM => b₁ in a₁ & b₁ 'or' (b₁ => FALSUM ) in a₁ & (Nes (b₁ => b₂)) => ((Nes b₁) => (Nes b₂)) in a₁ & (Nes b₁) => b₁ in a₁ & (Nes b₁) => (Nes (Nes b₁)) in a₁ & ( b₁ in a₁ & b₁ => b₂ in a₁ implies b₂ in a₁ ) & ( b₁ in a₁ implies Nes b₁ in a₁ ) );
correctness ;

end;

:: deftheorem Def22 defines S4_theory INTPRO_1:def 22 :

theorem Th78: :: INTPRO_1:78

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

proof end;

theorem Th79: :: INTPRO_1:79

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

proof end;

definition

let c₁ be Subset of MC-wff ;
func CnS4 c₁ -> Subset of MC-wff means :Def23: :: INTPRO_1:def 23
for b₁ being Element of MC-wff holds
( b₁ in a₂ iff for b₂ being Subset of MC-wff st b₂ is S4_theory & a₁ c= b₂ holds
b₁ in b₂ );
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 Def24 defines S4-Taut INTPRO_1:def 24 :

theorem Th80: :: INTPRO_1:80

for b₁ being Subset of MC-wff holds CnCPC b₁ c= CnS4 b₁

proof end;

theorem Th81: :: INTPRO_1:81

for b₁ being Subset of MC-wff holds CnIPC b₁ c= CnS4 b₁

proof end;

theorem Th82: :: INTPRO_1:82

for b₁ being Subset of MC-wff
for b₂, b₃, b₄ being Element of MC-wff holds
( b₂ => (b₃ => b₂) in CnS4 b₁ & (b₂ => (b₃ => b₄)) => ((b₂ => b₃) => (b₂ => b₄)) in CnS4 b₁ & (b₂ '&' b₃) => b₂ in CnS4 b₁ & (b₂ '&' b₃) => b₃ in CnS4 b₁ & b₂ => (b₃ => (b₂ '&' b₃)) in CnS4 b₁ & b₂ => (b₂ 'or' b₃) in CnS4 b₁ & b₃ => (b₂ 'or' b₃) in CnS4 b₁ & (b₂ => b₄) => ((b₃ => b₄) => ((b₂ 'or' b₃) => b₄)) in CnS4 b₁ & FALSUM => b₂ in CnS4 b₁ & b₂ 'or' (b₂ => FALSUM ) in CnS4 b₁ )

proof end;

theorem Th83: :: INTPRO_1:83

for b₁ being Subset of MC-wff
for b₂, b₃ being Element of MC-wff st b₂ in CnS4 b₁ & b₂ => b₃ in CnS4 b₁ holds
b₃ in CnS4 b₁

proof end;

theorem Th84: :: INTPRO_1:84

for b₁ being Subset of MC-wff
for b₂, b₃ being Element of MC-wff holds (Nes (b₂ => b₃)) => ((Nes b₂) => (Nes b₃)) in CnS4 b₁

proof end;

theorem Th85: :: INTPRO_1:85

for b₁ being Subset of MC-wff
for b₂ being Element of MC-wff holds (Nes b₂) => b₂ in CnS4 b₁

proof end;

theorem Th86: :: INTPRO_1:86

for b₁ being Subset of MC-wff
for b₂ being Element of MC-wff holds (Nes b₂) => (Nes (Nes b₂)) in CnS4 b₁

proof end;

theorem Th87: :: INTPRO_1:87

for b₁ being Subset of MC-wff
for b₂ being Element of MC-wff st b₂ in CnS4 b₁ holds
Nes b₂ in CnS4 b₁

proof end;

theorem Th88: :: INTPRO_1:88

for b₁, b₂ being Subset of MC-wff st b₁ is S4_theory & b₂ c= b₁ holds
CnS4 b₂ c= b₁

proof end;

theorem Th89: :: INTPRO_1:89

for b₁ being Subset of MC-wff holds b₁ c= CnS4 b₁

proof end;

theorem Th90: :: INTPRO_1:90

for b₁, b₂ being Subset of MC-wff st b₁ c= b₂ holds
CnS4 b₁ c= CnS4 b₂

proof end;

Lemma105: for b₁ being Subset of MC-wff holds CnS4 (CnS4 b₁) c= CnS4 b₁

proof end;

theorem Th91: :: INTPRO_1:91

for b₁ being Subset of MC-wff holds CnS4 (CnS4 b₁) = CnS4 b₁

proof end;

Lemma106: for b₁ being Subset of MC-wff holds CnS4 b₁ is S4_theory

proof end;

registration

let c₁ be Subset of MC-wff ;
cluster CnS4 a₁ -> S4_theory ;
coherence by Lemma106;

end;

theorem Th92: :: INTPRO_1:92

for b₁ being Subset of MC-wff holds
( b₁ is S4_theory iff CnS4 b₁ = b₁ )

proof end;

theorem Th93: :: INTPRO_1:93

for b₁ being Subset of MC-wff st b₁ is S4_theory holds
S4-Taut c= b₁

proof end;

registration

cluster S4-Taut -> S4_theory ;
coherence ;

end;

theorem Th94: :: INTPRO_1:94

CPC-Taut c= S4-Taut by Th80;

theorem Th95: :: INTPRO_1:95

IPC-Taut c= S4-Taut by Th81;