:: INTPRO_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

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 set ;
coherence
for b1 being set st b1 is MC-closed holds
( b1 is with_FALSUM & b1 is with_int_implication & b1 is with_int_conjunction & b1 is with_int_disjunction & b1 is with_int_propositional_variables & b1 is with_modal_operator & not b1 is empty )
by 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
for b1 being Subset of (NAT * ) st b1 is with_FALSUM & b1 is with_int_implication & b1 is with_int_conjunction & b1 is with_int_disjunction & b1 is with_int_propositional_variables & b1 is with_modal_operator holds
b1 is MC-closed
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
ex b1 being set st
( b1 is MC-closed & ( for E being set st E is MC-closed holds
b1 c= E ) )
proof end;
uniqueness
for b1, b2 being set st b1 is MC-closed & ( for E being set st E is MC-closed holds
b1 c= E ) & b2 is MC-closed & ( for E being set st E is MC-closed holds
b2 c= E ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines MC-wff INTPRO_1:def 8 :
for b1 being set holds
( b1 = MC-wff iff ( b1 is MC-closed & ( for E being set st E is MC-closed holds
b1 c= E ) ) );

registration
cluster MC-wff -> non empty with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator MC-closed ;
coherence
MC-wff is MC-closed
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
ex b1 being set st
( b1 is MC-closed & not b1 is empty )
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
MC-wff is functional
proof end;
end;

registration
cluster -> FinSequence-like Element of MC-wff ;
coherence
for b1 being Element of MC-wff holds b1 is FinSequence-like
proof end;
end;

definition
mode MC-formula is Element of MC-wff ;
end;

definition
func FALSUM -> MC-formula equals :: INTPRO_1:def 9
<*0*>;
correctness
coherence
<*0*> is MC-formula
;
by Def1;
let p, q be Element of MC-wff ;
func p => q -> MC-formula equals :: INTPRO_1:def 10
(<*1*> ^ p) ^ q;
correctness
coherence
(<*1*> ^ p) ^ q is MC-formula
;
by Def2;
func p '&' q -> MC-formula equals :: INTPRO_1:def 11
(<*2*> ^ p) ^ q;
correctness
coherence
(<*2*> ^ p) ^ q is MC-formula
;
by Def3;
func p 'or' q -> MC-formula equals :: INTPRO_1:def 12
(<*3*> ^ p) ^ q;
correctness
coherence
(<*3*> ^ p) ^ q is MC-formula
;
by Def4;
end;

:: deftheorem defines FALSUM INTPRO_1:def 9 :
FALSUM = <*0*>;

:: deftheorem defines => INTPRO_1:def 10 :
for p, q being Element of MC-wff holds p => q = (<*1*> ^ p) ^ q;

:: deftheorem defines '&' INTPRO_1:def 11 :
for p, q being Element of MC-wff holds p '&' q = (<*2*> ^ p) ^ q;

:: deftheorem defines 'or' INTPRO_1:def 12 :
for p, q being Element of MC-wff holds p 'or' q = (<*3*> ^ p) ^ q;

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

:: deftheorem defines Nes INTPRO_1:def 13 :
for p being Element of MC-wff holds Nes p = <*6*> ^ p;

definition
let T be Subset of MC-wff ;
attr T is IPC_theory means :Def14: :: INTPRO_1:def 14
for p, q, r being Element of MC-wff holds
( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & ( p in T & p => q in T implies q in T ) );
correctness
;
end;

:: deftheorem Def14 defines IPC_theory INTPRO_1:def 14 :
for T being Subset of MC-wff holds
( T is IPC_theory iff for p, q, r being Element of MC-wff holds
( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q) in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T & FALSUM => p in T & ( p in T & p => q in T implies q in T ) ) );

definition
let X be Subset of MC-wff ;
func CnIPC X -> Subset of MC-wff means :Def15: :: INTPRO_1:def 15
for r being Element of MC-wff holds
( r in it iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T );
existence
ex b1 being Subset of MC-wff st
for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T )
proof end;
uniqueness
for b1, b2 being Subset of MC-wff st ( for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) ) & ( for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines CnIPC INTPRO_1:def 15 :
for X, b2 being Subset of MC-wff holds
( b2 = CnIPC X iff for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is IPC_theory & X c= T holds
r in T ) );

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

:: deftheorem defines IPC-Taut INTPRO_1:def 16 :
IPC-Taut = CnIPC ({} MC-wff );

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

:: deftheorem defines neg INTPRO_1:def 17 :
for p being Element of MC-wff holds neg p = p => FALSUM ;

definition
func IVERUM -> MC-formula equals :: INTPRO_1:def 18
FALSUM => FALSUM ;
correctness
coherence
FALSUM => FALSUM is MC-formula
;
;
end;

:: deftheorem defines IVERUM INTPRO_1:def 18 :
IVERUM = FALSUM => FALSUM ;

theorem Th1: :: INTPRO_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of MC-wff holds X c= CnIPC X
proof end;

theorem Th13: :: INTPRO_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
CnIPC X is IPC_theory
by Lm3;
end;

theorem Th15: :: INTPRO_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Subset of MC-wff holds
( T is IPC_theory iff CnIPC T = T )
proof end;

theorem :: INTPRO_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of MC-wff holds p => p in IPC-Taut
proof end;

theorem Th18: :: INTPRO_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
IVERUM in IPC-Taut by Def14;

theorem :: INTPRO_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of MC-wff holds (p => q) => (p => p) in IPC-Taut
proof end;

theorem :: INTPRO_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, p being Element of MC-wff holds (q => p) => (p => p) in IPC-Taut
proof end;

theorem Th22: :: INTPRO_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of MC-wff holds (p => (p => q)) => (p => q) in IPC-Taut
proof end;

theorem :: INTPRO_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, p being Element of MC-wff holds q => ((q => p) => p) in IPC-Taut
proof end;

theorem Th32: :: INTPRO_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of MC-wff holds p => (p '&' p) in IPC-Taut
proof end;

theorem Th34: :: INTPRO_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of MC-wff holds ((p => q) '&' p) => q in IPC-Taut
proof end;

theorem :: INTPRO_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, s being Element of MC-wff holds (((p => q) '&' p) '&' s) => q in IPC-Taut
proof end;

theorem :: INTPRO_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of MC-wff holds (p '&' q) => (q '&' p) in IPC-Taut
proof end;

theorem Th47: :: INTPRO_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of MC-wff holds (p 'or' p) => p in IPC-Taut
proof end;

theorem :: INTPRO_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of MC-wff holds (p 'or' q) => (q 'or' p) in IPC-Taut
proof end;

theorem :: INTPRO_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
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 Th67: :: INTPRO_1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Subset of MC-wff st
for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T )
proof end;
uniqueness
for b1, b2 being Subset of MC-wff st ( for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) ) & ( for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines CnCPC INTPRO_1:def 20 :
for X, b2 being Subset of MC-wff holds
( b2 = CnCPC X iff for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is CPC_theory & X c= T holds
r in T ) );

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

:: deftheorem defines CPC-Taut INTPRO_1:def 21 :
CPC-Taut = CnCPC ({} MC-wff );

theorem Th68: :: INTPRO_1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of MC-wff holds CnIPC X c= CnCPC X
proof end;

theorem Th69: :: INTPRO_1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of MC-wff holds X c= CnCPC X
proof end;

theorem Th73: :: INTPRO_1:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
CnCPC X is CPC_theory
by Lm22;
end;

theorem Th75: :: INTPRO_1:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Subset of MC-wff holds
( T is CPC_theory iff CnCPC T = T )
proof end;

theorem :: INTPRO_1:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
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 Th78: :: INTPRO_1:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Subset of MC-wff st T is S4_theory holds
T is CPC_theory
proof end;

theorem :: INTPRO_1:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Subset of MC-wff st
for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T )
proof end;
uniqueness
for b1, b2 being Subset of MC-wff st ( for r being Element of MC-wff holds
( r in b1 iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) ) & ( for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def23 defines CnS4 INTPRO_1:def 23 :
for X, b2 being Subset of MC-wff holds
( b2 = CnS4 X iff for r being Element of MC-wff holds
( r in b2 iff for T being Subset of MC-wff st T is S4_theory & X c= T holds
r in T ) );

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

:: deftheorem defines S4-Taut INTPRO_1:def 24 :
S4-Taut = CnS4 ({} MC-wff );

theorem Th80: :: INTPRO_1:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of MC-wff holds CnCPC X c= CnS4 X
proof end;

theorem Th81: :: INTPRO_1:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of MC-wff holds CnIPC X c= CnS4 X
proof end;

theorem Th82: :: INTPRO_1:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of MC-wff holds X c= CnS4 X
proof end;

theorem Th90: :: INTPRO_1:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
CnS4 X is S4_theory
by Lm24;
end;

theorem Th92: :: INTPRO_1:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Subset of MC-wff holds
( T is S4_theory iff CnS4 T = T )
proof end;

theorem :: INTPRO_1:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
CPC-Taut c= S4-Taut by Th80;

theorem :: INTPRO_1:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
IPC-Taut c= S4-Taut by Th81;