:: 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 b₁ being set st b₁ is MC-closed holds
( b₁ is with_FALSUM & b₁ is with_int_implication & b₁ is with_int_conjunction & b₁ is with_int_disjunction & b₁ is with_int_propositional_variables & b₁ is with_modal_operator & not b₁ 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 b₁ being Subset of (NAT *) st b₁ is with_FALSUM & b₁ is with_int_implication & b₁ is with_int_conjunction & b₁ is with_int_disjunction & b₁ is with_int_propositional_variables & b₁ is with_modal_operator holds
b₁ 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 b₁ being set st
( b₁ is MC-closed & ( for E being set st E is MC-closed holds
b₁ c= E ) )

proof end;

uniqueness
for b₁, b₂ being set st b₁ is MC-closed & ( for E being set st E is MC-closed holds
b₁ c= E ) & b₂ is MC-closed & ( for E being set st E is MC-closed holds
b₂ c= E ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines MC-wff INTPRO_1:def 8 :
for b₁ being set holds
( b₁ = MC-wff iff ( b₁ is MC-closed & ( for E being set st E is MC-closed holds
b₁ 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 b₁ being set st
( b₁ is MC-closed & not b₁ 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 b₁ being Element of MC-wff holds b₁ 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 b₁ being Subset of MC-wff st
for r being Element of MC-wff holds
( r in b₁ iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T )

proof end;

uniqueness
for b₁, b₂ being Subset of MC-wff st ( for r being Element of MC-wff holds
( r in b₁ 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 b₂ iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines CnIPC INTPRO_1:def 15 :
for X, b₂ being Subset of MC-wff holds
( b₂ = CnIPC X iff for r being Element of MC-wff holds
( r in b₂ 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 b₁ being Subset of MC-wff st
for r being Element of MC-wff holds
( r in b₁ iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T )

proof end;

uniqueness
for b₁, b₂ being Subset of MC-wff st ( for r being Element of MC-wff holds
( r in b₁ 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 b₂ iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines CnCPC INTPRO_1:def 20 :
for X, b₂ being Subset of MC-wff holds
( b₂ = CnCPC X iff for r being Element of MC-wff holds
( r in b₂ 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 b₁ being Subset of MC-wff st
for r being Element of MC-wff holds
( r in b₁ iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T )

proof end;

uniqueness
for b₁, b₂ being Subset of MC-wff st ( for r being Element of MC-wff holds
( r in b₁ 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 b₂ iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def23 defines CnS4 INTPRO_1:def 23 :
for X, b₂ being Subset of MC-wff holds
( b₂ = CnS4 X iff for r being Element of MC-wff holds
( r in b₂ 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;