:: by Takao Inou\'e

::

:: Received April 3, 2003

:: Copyright (c) 2003-2021 Association of Mizar Users

:: language with modal operator

:: deftheorem Def1 defines with_FALSUM INTPRO_1:def 1 :

for E being set holds

( E is with_FALSUM iff <*0*> in E );

for E being set holds

( E is with_FALSUM iff <*0*> in E );

definition

let E be set ;

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

for p, q being FinSequence st p in E & q in E holds

(<*1*> ^ p) ^ q in E;

:: deftheorem Def2 defines with_int_implication INTPRO_1:def 2 :

for E being set holds

( E is with_int_implication iff for p, q being FinSequence st p in E & q in E holds

(<*1*> ^ p) ^ q in E );

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 ;

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

for p, q being FinSequence st p in E & q in E holds

(<*2*> ^ p) ^ q in E;

:: deftheorem Def3 defines with_int_conjunction INTPRO_1:def 3 :

for E being set holds

( E is with_int_conjunction iff for p, q being FinSequence st p in E & q in E holds

(<*2*> ^ p) ^ q in E );

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 ;

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

for p, q being FinSequence st p in E & q in E holds

(<*3*> ^ p) ^ q in E;

:: deftheorem Def4 defines with_int_disjunction INTPRO_1:def 4 :

for E being set holds

( E is with_int_disjunction iff for p, q being FinSequence st p in E & q in E holds

(<*3*> ^ p) ^ q in E );

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 ;

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

for n being Element of NAT holds <*(5 + (2 * n))*> in E;

:: deftheorem Def5 defines with_int_propositional_variables INTPRO_1:def 5 :

for E being set holds

( E is with_int_propositional_variables iff for n being Element of NAT holds <*(5 + (2 * n))*> in E );

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 ;

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

for p being FinSequence st p in E holds

<*6*> ^ p in E;

:: deftheorem Def6 defines with_modal_operator INTPRO_1:def 6 :

for E being set holds

( E is with_modal_operator iff for p being FinSequence st p in E holds

<*6*> ^ p in E );

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).

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

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

( 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 );

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

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

for b_{1} being set st b_{1} is MC-closed holds

( b_{1} is with_FALSUM & b_{1} is with_int_implication & b_{1} is with_int_conjunction & b_{1} is with_int_disjunction & b_{1} is with_int_propositional_variables & b_{1} is with_modal_operator & not b_{1} is empty )
by Lm1;

for b_{1} being Subset of (NAT *) st b_{1} is with_FALSUM & b_{1} is with_int_implication & b_{1} is with_int_conjunction & b_{1} is with_int_disjunction & b_{1} is with_int_propositional_variables & b_{1} is with_modal_operator holds

b_{1} is MC-closed
;

end;

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

( b

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

b

definition

ex b_{1} being set st

( b_{1} is MC-closed & ( for E being set st E is MC-closed holds

b_{1} c= E ) )

for b_{1}, b_{2} being set st b_{1} is MC-closed & ( for E being set st E is MC-closed holds

b_{1} c= E ) & b_{2} is MC-closed & ( for E being set st E is MC-closed holds

b_{2} c= E ) holds

b_{1} = b_{2}
end;

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 ( it is MC-closed & ( for E being set st E is MC-closed holds

it c= E ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for b_{1} being set holds

( b_{1} = MC-wff iff ( b_{1} is MC-closed & ( for E being set st E is MC-closed holds

b_{1} c= E ) ) );

for b

( b

b

registration
end;

registration
end;

definition

correctness

coherence

<*0*> is MC-formula;

by Def1;

let p, q be Element of MC-wff ;

correctness

coherence

(<*1*> ^ p) ^ q is MC-formula;

by Def2;

correctness

coherence

(<*2*> ^ p) ^ q is MC-formula;

by Def3;

correctness

coherence

(<*3*> ^ p) ^ q is MC-formula;

by Def4;

end;
coherence

<*0*> is MC-formula;

by Def1;

let p, q be Element of MC-wff ;

correctness

coherence

(<*1*> ^ p) ^ q is MC-formula;

by Def2;

correctness

coherence

(<*2*> ^ p) ^ q is MC-formula;

by Def3;

correctness

coherence

(<*3*> ^ p) ^ q is MC-formula;

by Def4;

:: deftheorem defines => INTPRO_1:def 10 :

for p, q being Element of MC-wff holds p => q = (<*1*> ^ p) ^ q;

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;

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;

for p, q being Element of MC-wff holds p 'or' q = (<*3*> ^ p) ^ q;

definition

let T be Subset of MC-wff;

;

end;
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 for p, q, r being Element of MC-wff holds

( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & ( p in T & p => q in T implies q in T ) );

;

:: deftheorem 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 ) ) );

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;

ex b_{1} being Subset of MC-wff st

for r being Element of MC-wff holds

( r in b_{1} iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds

r in T )

for b_{1}, b_{2} being Subset of MC-wff st ( for r being Element of MC-wff holds

( r in b_{1} 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_{2} iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds

r in T ) ) holds

b_{1} = b_{2}

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

ex b

for r being Element of MC-wff holds

( r in b

r in T )

proof end;

uniqueness for b

( r in b

r in T ) ) & ( for r being Element of MC-wff holds

( r in b

r in T ) ) holds

b

proof end;

:: deftheorem Def15 defines CnIPC INTPRO_1:def 15 :

for X, b_{2} being Subset of MC-wff holds

( b_{2} = CnIPC X iff for r being Element of MC-wff holds

( r in b_{2} iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds

r in T ) );

for X, b

( b

( r in b

r in T ) );

:: deftheorem defines neg INTPRO_1:def 17 :

for p being Element of MC-wff holds neg p = p => FALSUM;

for p being Element of MC-wff holds neg p = p => FALSUM;

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

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

for p, q being Element of MC-wff holds p => (q => (p '&' 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

for p, q, r being Element of MC-wff holds (p => r) => ((q => r) => ((p 'or' q) => r)) 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

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;

Lm2: for X being Subset of MC-wff holds CnIPC (CnIPC X) c= 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
end;

theorem :: INTPRO_1:20

theorem :: INTPRO_1:21

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

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

s => 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 ) )

( p '&' q in IPC-Taut iff ( p in IPC-Taut & q 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;

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

(p 'or' s) => (q 'or' s) 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

(s 'or' p) => (s 'or' q) in IPC-Taut

proof end;

definition

let T be Subset of MC-wff;

;

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

;

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

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

definition

let X be Subset of MC-wff;

ex b_{1} being Subset of MC-wff st

for r being Element of MC-wff holds

( r in b_{1} iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds

r in T )

for b_{1}, b_{2} being Subset of MC-wff st ( for r being Element of MC-wff holds

( r in b_{1} 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_{2} iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds

r in T ) ) holds

b_{1} = b_{2}

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

ex b

for r being Element of MC-wff holds

( r in b

r in T )

proof end;

uniqueness for b

( r in b

r in T ) ) & ( for r being Element of MC-wff holds

( r in b

r in T ) ) holds

b

proof end;

:: deftheorem Def20 defines CnCPC INTPRO_1:def 20 :

for X, b_{2} being Subset of MC-wff holds

( b_{2} = CnCPC X iff for r being Element of MC-wff holds

( r in b_{2} iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds

r in T ) );

for X, b

( b

( r in b

r in T ) );

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 )

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

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;

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

proof end;

Lm22: for X being Subset of MC-wff holds CnCPC X is CPC_theory

by Th69, Th70;

registration
end;

definition

let T be Subset of MC-wff;

;

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

;

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

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

definition

let X be Subset of MC-wff;

ex b_{1} being Subset of MC-wff st

for r being Element of MC-wff holds

( r in b_{1} iff for T being Subset of MC-wff st T is S4_theory & X c= T holds

r in T )

for b_{1}, b_{2} being Subset of MC-wff st ( for r being Element of MC-wff holds

( r in b_{1} 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_{2} iff for T being Subset of MC-wff st T is S4_theory & X c= T holds

r in T ) ) holds

b_{1} = b_{2}

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

ex b

for r being Element of MC-wff holds

( r in b

r in T )

proof end;

uniqueness for b

( r in b

r in T ) ) & ( for r being Element of MC-wff holds

( r in b

r in T ) ) holds

b

proof end;

:: deftheorem Def23 defines CnS4 INTPRO_1:def 23 :

for X, b_{2} being Subset of MC-wff holds

( b_{2} = CnS4 X iff for r being Element of MC-wff holds

( r in b_{2} iff for T being Subset of MC-wff st T is S4_theory & X c= T holds

r in T ) );

for X, b

( b

( r in b

r in T ) );

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 )

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

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

for p, q being Element of MC-wff holds (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 X

proof end;

Lm23: for X being Subset of MC-wff holds CnS4 (CnS4 X) c= 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
end;