INTPRO_2: Intuitionistic Propositional Calculus in the Extended Framework with Modal Operator, {P}art {II } (Negation, Deduction Theorem for IPC)

definition

let p, q be Element of MC-wff ;

func p 'equiv' q -> Element of MC-wff equals :: INTPRO_2:def 1
(p => q) '&' (q => p);

correctness ;

end;

:: deftheorem defines 'equiv' INTPRO_2:def 1 :

definition

func Proof_Step_Kinds_IPC -> set equals :: INTPRO_2:def 2
{ k where k is Nat : k <= 10 } ;

coherence ;

end;

:: deftheorem defines Proof_Step_Kinds_IPC INTPRO_2:def 2 :

registration

cluster Proof_Step_Kinds_IPC -> non empty ;

coherence by Th1;

end;

theorem Th3: :: INTPRO_2:2

for f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:]
for n being Nat st 1 <= n & n <= len f holds
not not (f . n) `2 = 0 & ... & not (f . n) `2 = 10

proof end;

definition

let PR be FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:];
let n be Nat;
let X be Subset of MC-wff;

pred PR,n is_a_correct_step_wrt_IPC X means :Def3: :: INTPRO_2:def 3
(PR . n) `1 in X if (PR . n) `2 = 0
ex p, q being Element of MC-wff st (PR . n) `1 = p => (q => p) if (PR . n) `2 = 1
ex p, q, r being Element of MC-wff st (PR . n) `1 = (p => (q => r)) => ((p => q) => (p => r)) if (PR . n) `2 = 2
ex p, q being Element of MC-wff st (PR . n) `1 = (p '&' q) => p if (PR . n) `2 = 3
ex p, q being Element of MC-wff st (PR . n) `1 = (p '&' q) => q if (PR . n) `2 = 4
ex p, q being Element of MC-wff st (PR . n) `1 = p => (q => (p '&' q)) if (PR . n) `2 = 5
ex p, q being Element of MC-wff st (PR . n) `1 = p => (p 'or' q) if (PR . n) `2 = 6
ex p, q being Element of MC-wff st (PR . n) `1 = q => (p 'or' q) if (PR . n) `2 = 7
ex p, q, r being Element of MC-wff st (PR . n) `1 = (p => r) => ((q => r) => ((p 'or' q) => r)) if (PR . n) `2 = 8
ex p being Element of MC-wff st (PR . n) `1 = FALSUM => p if (PR . n) `2 = 9
ex i, j being Nat ex p, q being Element of MC-wff st
( 1 <= i & i < n & 1 <= j & j < i & p = (PR . j) `1 & q = (PR . n) `1 & (PR . i) `1 = p => q ) if (PR . n) `2 = 10
;

consistency ;

end;

:: deftheorem Def3 defines is_a_correct_step_wrt_IPC INTPRO_2:def 3 :

definition

let X be Subset of MC-wff;
let f be FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:];

pred f is_a_proof_wrt_IPC X means :: INTPRO_2:def 4
( f <> {} & ( for n being Nat st 1 <= n & n <= len f holds
f,n is_a_correct_step_wrt_IPC X ) );

end;

:: deftheorem defines is_a_proof_wrt_IPC INTPRO_2:def 4 :

theorem Th5: :: INTPRO_2:4

for X being Subset of MC-wff
for f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st f is_a_proof_wrt_IPC X holds
1 <= len f

proof end;

theorem :: INTPRO_2:5

for X being Subset of MC-wff
for f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st f is_a_proof_wrt_IPC X holds
not not (f . 1) `2 = 0 & ... & not (f . 1) `2 = 10

proof end;

theorem Th7: :: INTPRO_2:6

for n being Nat
for X being Subset of MC-wff
for f, g being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st 1 <= n & n <= len f holds
( f,n is_a_correct_step_wrt_IPC X iff f ^ g,n is_a_correct_step_wrt_IPC X )

proof end;

theorem Th8: :: INTPRO_2:7

for n being Nat
for X being Subset of MC-wff
for f, g being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st 1 <= n & n <= len g & g,n is_a_correct_step_wrt_IPC X holds
f ^ g,n + (len f) is_a_correct_step_wrt_IPC X

proof end;

theorem Th9: :: INTPRO_2:8

for X being Subset of MC-wff
for f, g being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st f is_a_proof_wrt_IPC X & g is_a_proof_wrt_IPC X holds
f ^ g is_a_proof_wrt_IPC X

proof end;

theorem Th10: :: INTPRO_2:9

for X, Y being Subset of MC-wff
for f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st f is_a_proof_wrt_IPC X & X c= Y holds
f is_a_proof_wrt_IPC Y

proof end;

theorem Th11: :: INTPRO_2:10

for l being Nat
for X being Subset of MC-wff
for f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st f is_a_proof_wrt_IPC X & 1 <= l & l <= len f holds
(f . l) `1 in CnIPC X

proof end;

definition

let f be FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:];
assume A1: f <> {} ;

func Effect_IPC f -> Element of MC-wff equals :Def5: :: INTPRO_2:def 5
(f . (len f)) `1 ;

coherence

proof end;

end;

:: deftheorem Def5 defines Effect_IPC INTPRO_2:def 5 :

theorem Th12: :: INTPRO_2:11

for X being Subset of MC-wff
for f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st f is_a_proof_wrt_IPC X holds
Effect_IPC f in CnIPC X

proof end;

theorem Th13: :: INTPRO_2:12

for X being Subset of MC-wff holds X c= { F where F is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = F ) }

proof end;

theorem Th14: :: INTPRO_2:13

for Y, X being Subset of MC-wff st Y = { p where p is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = p ) } holds
Y is IPC_theory by Lm2, Lm3, Lm4, Lm5, Lm6, Lm7, Lm8, Lm9, Lm10, Lm11;

theorem Th15: :: INTPRO_2:14

for X being Subset of MC-wff holds { p where p is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = p ) } = CnIPC X

proof end;

theorem Th16: :: INTPRO_2:15

for X being Subset of MC-wff
for p being Element of MC-wff holds
( p in CnIPC X iff ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = p ) )

proof end;

theorem :: INTPRO_2:16

for X being Subset of MC-wff
for p being Element of MC-wff st p in CnIPC X holds
ex Y being Subset of MC-wff st
( Y c= X & Y is finite & p in CnIPC Y )

proof end;

definition

let X be Subset of MC-wff;
let s be MC-formula;

pred X |-_IPC s means :Def6: :: INTPRO_2:def 6
s in CnIPC X;

end;

:: deftheorem Def6 defines |-_IPC INTPRO_2:def 6 :

definition

let s be MC-formula;

pred |-_IPC s means :: INTPRO_2:def 7
{} MC-wff |-_IPC s;

end;

:: deftheorem defines |-_IPC INTPRO_2:def 7 :

theorem Th18: :: INTPRO_2:17

for X being Subset of MC-wff
for p, q being Element of MC-wff holds X |-_IPC p => (q => p) by INTPRO_1:1;

theorem Th19: :: INTPRO_2:18

for X being Subset of MC-wff
for p, q, r being Element of MC-wff holds X |-_IPC (p => (q => r)) => ((p => q) => (p => r)) by INTPRO_1:2;

theorem Th20: :: INTPRO_2:19

for X being Subset of MC-wff
for p, q being Element of MC-wff holds X |-_IPC (p '&' q) => p by INTPRO_1:3;

theorem Th21: :: INTPRO_2:20

for X being Subset of MC-wff
for p, q being Element of MC-wff holds X |-_IPC (p '&' q) => q by INTPRO_1:4;

theorem Th22: :: INTPRO_2:21

for X being Subset of MC-wff
for p, q being Element of MC-wff holds X |-_IPC p => (q => (p '&' q)) by INTPRO_1:5;

theorem Th23: :: INTPRO_2:22

for X being Subset of MC-wff
for p, q being Element of MC-wff holds X |-_IPC p => (p 'or' q) by INTPRO_1:6;

theorem Th24: :: INTPRO_2:23

for X being Subset of MC-wff
for p, q being Element of MC-wff holds X |-_IPC q => (p 'or' q) by INTPRO_1:7;

theorem Th25: :: INTPRO_2:24

for X being Subset of MC-wff
for p, q, r being Element of MC-wff holds X |-_IPC (p => r) => ((q => r) => ((p 'or' q) => r)) by INTPRO_1:8;

theorem Th26: :: INTPRO_2:25

for X being Subset of MC-wff
for p being Element of MC-wff holds X |-_IPC FALSUM => p by INTPRO_1:9;

theorem Th27: :: INTPRO_2:26

for X being Subset of MC-wff
for p, q being Element of MC-wff st X |-_IPC p & X |-_IPC p => q holds
X |-_IPC q by INTPRO_1:10;

theorem Th28: :: INTPRO_2:27

for p, q being Element of MC-wff holds |-_IPC p => (q => p) by Th18;

theorem Th29: :: INTPRO_2:28

for p, q, r being Element of MC-wff holds |-_IPC (p => (q => r)) => ((p => q) => (p => r)) by Th19;

theorem Th30: :: INTPRO_2:29

for p, q being Element of MC-wff holds |-_IPC (p '&' q) => p by Th20;

theorem Th31: :: INTPRO_2:30

for p, q being Element of MC-wff holds |-_IPC (p '&' q) => q by Th21;

theorem Th32: :: INTPRO_2:31

for p, q being Element of MC-wff holds |-_IPC p => (q => (p '&' q)) by Th22;

theorem :: INTPRO_2:32

for p, q being Element of MC-wff holds |-_IPC p => (p 'or' q) by Th23;

theorem :: INTPRO_2:33

for p, q being Element of MC-wff holds |-_IPC q => (p 'or' q) by Th24;

theorem Th35: :: INTPRO_2:34

for p, q, r being Element of MC-wff holds |-_IPC (p => r) => ((q => r) => ((p 'or' q) => r)) by Th25;

theorem Th36: :: INTPRO_2:35

for p being Element of MC-wff holds |-_IPC FALSUM => p by Th26;

theorem Th37: :: INTPRO_2:36

for p, q being Element of MC-wff st |-_IPC p & |-_IPC p => q holds
|-_IPC q by Th27;

definition

let s be MC-formula;

attr s is valid_IPC means :: INTPRO_2:def 8
{} MC-wff |-_IPC s;

end;

:: deftheorem defines valid_IPC INTPRO_2:def 8 :

definition

let s be MC-formula;

redefine attr s is valid_IPC means :: INTPRO_2:def 9
s in IPC-Taut ;

compatibility by Def6, INTPRO_1:def 16;

end;

:: deftheorem defines valid_IPC INTPRO_2:def 9 :

theorem :: INTPRO_2:37

for X being Subset of MC-wff
for p being Element of MC-wff st p is valid_IPC holds
X |-_IPC p

proof end;

theorem Th39: :: INTPRO_2:38

for p, q being Element of MC-wff holds p => (q => p) is valid_IPC

proof end;

theorem Th40: :: INTPRO_2:39

for p, q, r being Element of MC-wff holds (p => (q => r)) => ((p => q) => (p => r)) is valid_IPC

proof end;

theorem Th41: :: INTPRO_2:40

for p, q being Element of MC-wff holds (p '&' q) => p is valid_IPC

proof end;

theorem Th42: :: INTPRO_2:41

for p, q being Element of MC-wff holds (p '&' q) => q is valid_IPC

proof end;

theorem Th43: :: INTPRO_2:42

for p, q being Element of MC-wff holds p => (q => (p '&' q)) is valid_IPC

proof end;

theorem Th44: :: INTPRO_2:43

for p, q being Element of MC-wff holds p => (p 'or' q) is valid_IPC

proof end;

theorem Th45: :: INTPRO_2:44

for p, q being Element of MC-wff holds q => (p 'or' q) is valid_IPC

proof end;

theorem Th46: :: INTPRO_2:45

for p, q, r being Element of MC-wff holds (p => r) => ((q => r) => ((p 'or' q) => r)) is valid_IPC

proof end;

theorem Th47: :: INTPRO_2:46

for p being Element of MC-wff holds FALSUM => p is valid_IPC

proof end;

theorem :: INTPRO_2:47

for p, q being Element of MC-wff st p is valid_IPC & p => q is valid_IPC holds
q is valid_IPC

proof end;

theorem Th49: :: INTPRO_2:48

for X being Subset of MC-wff
for p being Element of MC-wff holds X |-_IPC p => p

proof end;

theorem :: INTPRO_2:49

for X being Subset of MC-wff holds X |-_IPC IVERUM by Th49, INTPRO_1:def 18;

theorem Th51: :: INTPRO_2:50

for X being Subset of MC-wff
for p, q being Element of MC-wff st X |-_IPC p holds
X |-_IPC q => p

proof end;

theorem Th52: :: INTPRO_2:51

for X being Subset of MC-wff
for p being Element of MC-wff st p is valid_IPC holds
X |-_IPC p

proof end;

theorem Th53: :: INTPRO_2:52

for X being Subset of MC-wff
for F, G being Element of MC-wff st X \/ {F} |-_IPC G holds
X |-_IPC F => G

proof end;

definition

let x1, x2, x3 be Element of MC-wff ;
:: original: {
redefine func {x1,x2,x3} -> Subset of MC-wff;
correctness

proof end;

end;

definition

let x1, x2, x3, x4 be Element of MC-wff ;
:: original: {
redefine func {x1,x2,x3,x4} -> Subset of MC-wff;
coherence

proof end;

end;

definition

let x1, x2, x3, x4, x5 be Element of MC-wff ;
:: original: {
redefine func {x1,x2,x3,x4,x5} -> Subset of MC-wff;
coherence

proof end;

end;

definition

let x1, x2, x3, x4, x5, x6 be Element of MC-wff ;
:: original: {
redefine func {x1,x2,x3,x4,x5,x6} -> Subset of MC-wff;
coherence

proof end;

end;

definition

let x1, x2, x3, x4, x5, x6, x7 be Element of MC-wff ;
:: original: {
redefine func {x1,x2,x3,x4,x5,x6,x7} -> Subset of MC-wff;
coherence

proof end;

end;

definition

let x1, x2, x3, x4, x5, x6, x7, x8 be Element of MC-wff ;
:: original: {
redefine func {x1,x2,x3,x4,x5,x6,x7,x8} -> Subset of MC-wff;
coherence

proof end;

end;

definition

let x1, x2, x3, x4, x5, x6, x7, x8, x9 be Element of MC-wff ;
:: original: {
redefine func {x1,x2,x3,x4,x5,x6,x7,x8,x9} -> Subset of MC-wff;
coherence

proof end;

end;

definition

let x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 be Element of MC-wff ;
:: original: {
redefine func {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} -> Subset of MC-wff;
coherence

proof end;

end;

theorem Th54: :: INTPRO_2:53

for F being Element of MC-wff
for G being MC-formula st {F} |-_IPC G holds
|-_IPC F => G

proof end;

theorem Th55: :: INTPRO_2:54

for F1, F2, G being MC-formula st {F1,F2} |-_IPC G holds
{F2} |-_IPC F1 => G

proof end;

theorem Th56: :: INTPRO_2:55

for F1, F2, F3, G being MC-formula st {F1,F2,F3} |-_IPC G holds
{F2,F3} |-_IPC F1 => G

proof end;

theorem Th57: :: INTPRO_2:56

for F1, F2, F3, F4, G being MC-formula st {F1,F2,F3,F4} |-_IPC G holds
{F2,F3,F4} |-_IPC F1 => G

proof end;

theorem :: INTPRO_2:57

for F1, F2, F3, F4, F5, G being MC-formula st {F1,F2,F3,F4,F5} |-_IPC G holds
{F2,F3,F4,F5} |-_IPC F1 => G

proof end;

theorem :: INTPRO_2:58

for F1, F2, F3, F4, F5, F6, G being MC-formula st {F1,F2,F3,F4,F5,F6} |-_IPC G holds
{F2,F3,F4,F5,F6} |-_IPC F1 => G

proof end;

theorem :: INTPRO_2:59

for F1, F2, F3, F4, F5, F6, F7, G being MC-formula st {F1,F2,F3,F4,F5,F6,F7} |-_IPC G holds
{F2,F3,F4,F5,F6,F7} |-_IPC F1 => G

proof end;

theorem :: INTPRO_2:60

for F1, F2, F3, F4, F5, F6, F7, F8, G being MC-formula st {F1,F2,F3,F4,F5,F6,F7,F8} |-_IPC G holds
{F2,F3,F4,F5,F6,F7,F8} |-_IPC F1 => G

proof end;

theorem :: INTPRO_2:61

for F1, F2, F3, F4, F5, F6, F7, F8, F9, G being MC-formula st {F1,F2,F3,F4,F5,F6,F7,F8,F9} |-_IPC G holds
{F2,F3,F4,F5,F6,F7,F8,F9} |-_IPC F1 => G

proof end;

theorem Th63: :: INTPRO_2:62

for x1, x2, x3, x4, x5, x6, x7, x8, x9, x10 being object holds {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} = {x2,x3,x4,x5,x6,x7,x8,x9,x10} \/ {x1}

proof end;

theorem :: INTPRO_2:63

for F1, F2, F3, F4, F5, F6, F7, F8, F9, F10, G being MC-formula st {F1,F2,F3,F4,F5,F6,F7,F8,F9,F10} |-_IPC G holds
{F2,F3,F4,F5,F6,F7,F8,F9,F10} |-_IPC F1 => G

proof end;

theorem Th65: :: INTPRO_2:64

for p being Element of MC-wff holds {p} |-_IPC p

proof end;

theorem Th66: :: INTPRO_2:65

for Y, X being Subset of MC-wff
for p being Element of MC-wff st X |-_IPC p & X c= Y holds
Y |-_IPC p

proof end;

theorem Th67: :: INTPRO_2:66

for X being Subset of MC-wff
for p being Element of MC-wff st p in X holds
X |-_IPC p

proof end;

theorem :: INTPRO_2:67

for X being Subset of MC-wff
for p being Element of MC-wff st p in X holds
p in CnIPC X

proof end;

theorem Th69: :: INTPRO_2:68

for p being Element of MC-wff st p in IPC-Taut holds
|-_IPC p by Def6, INTPRO_1:def 16;

theorem Th70: :: INTPRO_2:69

for p being Element of MC-wff st |-_IPC p holds
p in IPC-Taut by Def6, INTPRO_1:def 16;

theorem :: INTPRO_2:70

for p being Element of MC-wff holds
( p in IPC-Taut iff |-_IPC p ) by Th69, Th70;

theorem Th72: :: INTPRO_2:71

for p being Element of MC-wff holds |-_IPC p => ((p => FALSUM) => FALSUM)

proof end;

theorem Th73: :: INTPRO_2:72

for p, q being Element of MC-wff holds {(p '&' q)} |-_IPC p

proof end;

theorem Th74: :: INTPRO_2:73

for p, q being Element of MC-wff holds {(p '&' q)} |-_IPC q

proof end;

theorem Th75: :: INTPRO_2:74

for p, q being Element of MC-wff holds |-_IPC ((p => q) '&' (p => (q => FALSUM))) => (p => FALSUM)

proof end;

theorem Th76: :: INTPRO_2:75

for p, q being Element of MC-wff holds |-_IPC (p => FALSUM) => (p => q)

proof end;

theorem Th77: :: INTPRO_2:76

for p, q, r being Element of MC-wff holds |-_IPC ((p => r) '&' (q => r)) => ((p 'or' q) => r)

proof end;

theorem Th78: :: INTPRO_2:77

for p, q being Element of MC-wff holds |-_IPC (p '&' (p => q)) => q

proof end;

theorem Th79: :: INTPRO_2:78

for p being Element of MC-wff holds |-_IPC p => ((((p => FALSUM) => FALSUM) => FALSUM) => FALSUM)

proof end;

theorem Th80: :: INTPRO_2:79

for p, q being Element of MC-wff holds |-_IPC ((p => FALSUM) 'or' q) => (p => q)

proof end;

theorem Th81: :: INTPRO_2:80

for p, q being Element of MC-wff holds |-_IPC (p => q) => ((q => FALSUM) => (p => FALSUM)) by Th69, INTPRO_1:24;

theorem Th82: :: INTPRO_2:81

for p, q being Element of MC-wff holds |-_IPC ((p => FALSUM) 'or' (q => FALSUM)) => ((p '&' q) => FALSUM)

proof end;

theorem Th83: :: INTPRO_2:82

for p, q being MC-formula st |-_IPC p & |-_IPC q holds
|-_IPC p '&' q

proof end;

theorem Th84: :: INTPRO_2:83

for p, q being Element of MC-wff st |-_IPC p => q & |-_IPC q => p holds
|-_IPC p 'equiv' q by Th83;

theorem Th85: :: INTPRO_2:84

for p being Element of MC-wff holds |-_IPC p => p

proof end;

theorem :: INTPRO_2:85

for p being Element of MC-wff holds |-_IPC p 'equiv' p

proof end;

theorem Th87: :: INTPRO_2:86

for p, q being Element of MC-wff holds |-_IPC ((p '&' q) => FALSUM) => (p => (q => FALSUM))

proof end;

theorem Th88: :: INTPRO_2:87

for p, q being Element of MC-wff holds |-_IPC (p => (q => FALSUM)) => ((p '&' q) => FALSUM)

proof end;

theorem Th89: :: INTPRO_2:88

for p, q being Element of MC-wff holds |-_IPC ((p '&' q) => FALSUM) 'equiv' (p => (q => FALSUM))

proof end;

theorem Th90: :: INTPRO_2:89

for p, q being Element of MC-wff holds |-_IPC ((p '&' q) => FALSUM) => (q => (p => FALSUM))

proof end;

theorem Th91: :: INTPRO_2:90

for p, q being Element of MC-wff holds |-_IPC (q => (p => FALSUM)) => ((p '&' q) => FALSUM)

proof end;

theorem Th92: :: INTPRO_2:91

for p, q being Element of MC-wff holds |-_IPC (q => (p => FALSUM)) 'equiv' ((p '&' q) => FALSUM)

proof end;

theorem Th93: :: INTPRO_2:92

for p, q being Element of MC-wff holds |-_IPC p => (q => (((p '&' q) => FALSUM) => FALSUM))

proof end;

theorem Th94: :: INTPRO_2:93

for p, q being Element of MC-wff holds |-_IPC q => (p => (((p '&' q) => FALSUM) => FALSUM))

proof end;

theorem Th95: :: INTPRO_2:94

for p, q being Element of MC-wff holds |-_IPC p => (((p '&' q) => FALSUM) => (q => FALSUM))

proof end;

theorem Th96: :: INTPRO_2:95

for p, q being Element of MC-wff holds |-_IPC q => (((p '&' q) => FALSUM) => (p => FALSUM))

proof end;

theorem Th97: :: INTPRO_2:96

for p, q being Element of MC-wff holds |-_IPC ((p 'or' q) => FALSUM) => ((p => FALSUM) '&' (q => FALSUM))

proof end;

theorem Th98: :: INTPRO_2:97

for p, q being Element of MC-wff holds |-_IPC ((p => FALSUM) '&' (q => FALSUM)) => ((p 'or' q) => FALSUM) by Th77;

theorem Th99: :: INTPRO_2:98

for p, q being Element of MC-wff holds |-_IPC ((p 'or' q) => FALSUM) 'equiv' ((p => FALSUM) '&' (q => FALSUM))

proof end;

theorem Th100: :: INTPRO_2:99

for p being Element of MC-wff holds |-_IPC (p '&' (p => FALSUM)) => FALSUM by Th78;

theorem Th101: :: INTPRO_2:100

for p being Element of MC-wff holds |-_IPC FALSUM 'equiv' (p '&' (p => FALSUM))

proof end;

theorem Th102: :: INTPRO_2:101

for p being Element of MC-wff holds |-_IPC (p => FALSUM) => (((p => FALSUM) => FALSUM) => FALSUM) by Th72;

theorem Th103: :: INTPRO_2:102

for p being Element of MC-wff holds |-_IPC (((p => FALSUM) => FALSUM) => FALSUM) => (p => FALSUM)

proof end;

theorem Th104: :: INTPRO_2:103

for p being Element of MC-wff holds |-_IPC (p => FALSUM) 'equiv' (((p => FALSUM) => FALSUM) => FALSUM)

proof end;

theorem Th105: :: INTPRO_2:104

for p, q being Element of MC-wff holds |-_IPC ((p => FALSUM) => q) => ((((p => FALSUM) => FALSUM) => FALSUM) => q)

proof end;

theorem Th106: :: INTPRO_2:105

for p, q being Element of MC-wff holds |-_IPC (p => q) => (((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))

proof end;

theorem Th107: :: INTPRO_2:106

for p, q being Element of MC-wff holds |-_IPC (p '&' (q => FALSUM)) => ((p => q) => FALSUM)

proof end;

theorem Th108: :: INTPRO_2:107

for p, q being Element of MC-wff holds |-_IPC (((p => q) => FALSUM) => FALSUM) => (((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))

proof end;

theorem Th109: :: INTPRO_2:108

for p, q being Element of MC-wff holds |-_IPC (((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM)) => (((p => q) => FALSUM) => FALSUM)

proof end;

theorem Th110: :: INTPRO_2:109

for p, q being Element of MC-wff holds |-_IPC (((p => q) => FALSUM) => FALSUM) 'equiv' (((p => FALSUM) => FALSUM) => ((q => FALSUM) => FALSUM))

proof end;

theorem Th111: :: INTPRO_2:110

for p, q being Element of MC-wff holds |-_IPC (((p '&' q) => FALSUM) => FALSUM) => (((p => FALSUM) => FALSUM) '&' ((q => FALSUM) => FALSUM))

proof end;

theorem Th112: :: INTPRO_2:111

for p, q being Element of MC-wff holds |-_IPC (((p => FALSUM) => FALSUM) '&' ((q => FALSUM) => FALSUM)) => (((p '&' q) => FALSUM) => FALSUM)

proof end;

theorem Th113: :: INTPRO_2:112

for p, q being Element of MC-wff holds |-_IPC (((p '&' q) => FALSUM) => FALSUM) 'equiv' (((p => FALSUM) => FALSUM) '&' ((q => FALSUM) => FALSUM))

proof end;

theorem Th114: :: INTPRO_2:113

for p, q being Element of MC-wff holds |-_IPC (((p => q) => FALSUM) => FALSUM) => (p => ((q => FALSUM) => FALSUM))

proof end;

theorem :: INTPRO_2:114

for q, r being Element of MC-wff st |-_IPC r & {r} |-_IPC q holds
|-_IPC q

proof end;

theorem Th116: :: INTPRO_2:115

for X being Subset of MC-wff
for q, r being Element of MC-wff st X |-_IPC r & X \/ {r} |-_IPC q holds
X |-_IPC q

proof end;

theorem :: INTPRO_2:116

for Y, X being Subset of MC-wff
for q, r being Element of MC-wff st X |-_IPC r & Y \/ {r} |-_IPC q holds
X \/ Y |-_IPC q

proof end;

theorem :: INTPRO_2:117

for p, q, r being Element of MC-wff st |-_IPC p & {r} |-_IPC q holds
{(p => r)} |-_IPC q

proof end;

theorem Th119: :: INTPRO_2:118

for X being Subset of MC-wff
for p, q, r being Element of MC-wff st X |-_IPC p & X \/ {r} |-_IPC q holds
X \/ {(p => r)} |-_IPC q

proof end;

theorem Th120: :: INTPRO_2:119

for q, r being Element of MC-wff holds {q} |-_IPC q 'or' r

proof end;

theorem Th121: :: INTPRO_2:120

for q, r being Element of MC-wff holds {r} |-_IPC q 'or' r

proof end;

theorem :: INTPRO_2:121

for p, q, r being Element of MC-wff st {p} |-_IPC r & {q} |-_IPC r holds
{(p 'or' q)} |-_IPC r

proof end;

theorem Th123: :: INTPRO_2:122

for X being Subset of MC-wff
for p, q, r being Element of MC-wff st X \/ {p} |-_IPC r & X \/ {q} |-_IPC r holds
X \/ {(p 'or' q)} |-_IPC r

proof end;

theorem :: INTPRO_2:123

for Y, X being Subset of MC-wff
for p, q, r being Element of MC-wff st X \/ {p} |-_IPC r & Y \/ {q} |-_IPC r holds
(X \/ Y) \/ {(p 'or' q)} |-_IPC r

proof end;

theorem :: INTPRO_2:124

for p, q, r being Element of MC-wff holds |-_IPC (p => (q 'or' (p => r))) => (p => (q 'or' r))

proof end;

theorem Th126: :: INTPRO_2:125

for p, q being Element of MC-wff holds |-_IPC p => ((p => FALSUM) => q)

proof end;

theorem Th127: :: INTPRO_2:126

for p, q, r being Element of MC-wff holds |-_IPC (p => q) => (((q '&' r) => FALSUM) => ((p '&' r) => FALSUM))

proof end;

theorem Th128: :: INTPRO_2:127

for p, q, r being Element of MC-wff holds |-_IPC (p => q) => (((q 'or' r) => FALSUM) => ((p 'or' r) => FALSUM))

proof end;

definition

let p be Element of MC-wff ;

:: original: neg
redefine func neg p -> Element of MC-wff equals :: INTPRO_2:def 10
p => FALSUM;

correctness by INTPRO_1:def 17;

end;

:: deftheorem defines neg INTPRO_2:def 10 :

definition

let p be Element of MC-wff ;

func neg^2 p -> Element of MC-wff equals :: INTPRO_2:def 11
(p => FALSUM) => FALSUM;

correctness ;

end;

:: deftheorem defines neg^2 INTPRO_2:def 11 :

definition

let p be Element of MC-wff ;

func neg^3 p -> Element of MC-wff equals :: INTPRO_2:def 12
((p => FALSUM) => FALSUM) => FALSUM;

correctness ;

end;

:: deftheorem defines neg^3 INTPRO_2:def 12 :

definition

let p be Element of MC-wff ;

func neg^4 p -> Element of MC-wff equals :: INTPRO_2:def 13
(((p => FALSUM) => FALSUM) => FALSUM) => FALSUM;

correctness ;

end;

:: deftheorem defines neg^4 INTPRO_2:def 13 :

:: deftheorem defines neg^5 INTPRO_2:def 14 :

theorem :: INTPRO_2:128

for p being Element of MC-wff holds |-_IPC p => (neg (neg p)) by Th72;

theorem :: INTPRO_2:129

for p being Element of MC-wff holds |-_IPC p => (neg^2 p) by Th72;

theorem :: INTPRO_2:130

for p, q being Element of MC-wff holds |-_IPC ((p => q) '&' (p => (neg q))) => (neg p) by Th75;

theorem :: INTPRO_2:131

for p, q being Element of MC-wff holds |-_IPC (neg p) => (p => q) by Th76;

theorem :: INTPRO_2:132

for p being Element of MC-wff holds |-_IPC p => (neg (neg (neg (neg p)))) by Th79;

theorem :: INTPRO_2:133

for p, q being Element of MC-wff holds |-_IPC ((neg p) 'or' q) => (p => q) by Th80;

theorem :: INTPRO_2:134

for p, q being Element of MC-wff holds |-_IPC (p => q) => ((neg q) => (neg p)) by Th81;

theorem :: INTPRO_2:135

for p, q being Element of MC-wff holds |-_IPC ((neg p) 'or' (neg q)) => (neg (p '&' q)) by Th82;

theorem :: INTPRO_2:136

for p, q being Element of MC-wff holds |-_IPC (neg (p '&' q)) => (p => (neg q)) by Th87;

theorem :: INTPRO_2:137

for p, q being Element of MC-wff holds |-_IPC (p => (neg q)) => (neg (p '&' q)) by Th88;

theorem :: INTPRO_2:138

for p, q being Element of MC-wff holds |-_IPC (neg (p '&' q)) 'equiv' (p => (neg q)) by Th89;

theorem :: INTPRO_2:139

for p, q being Element of MC-wff holds |-_IPC (neg (p '&' q)) => (q => (neg p)) by Th90;

theorem :: INTPRO_2:140

for p, q being Element of MC-wff holds |-_IPC (q => (neg p)) => (neg (p '&' q)) by Th91;

theorem :: INTPRO_2:141

for p, q being Element of MC-wff holds |-_IPC (q => (neg p)) 'equiv' (neg (p '&' q)) by Th92;

theorem :: INTPRO_2:142

for p, q being Element of MC-wff holds |-_IPC p => (q => (neg (neg (p '&' q)))) by Th93;

theorem :: INTPRO_2:143

for p, q being Element of MC-wff holds |-_IPC q => (p => (neg (neg (p '&' q)))) by Th94;

theorem :: INTPRO_2:144

for p, q being Element of MC-wff holds |-_IPC p => ((neg (p '&' q)) => (neg q)) by Th95;

theorem :: INTPRO_2:145

for p, q being Element of MC-wff holds |-_IPC q => ((neg (p '&' q)) => (neg p)) by Th96;

theorem :: INTPRO_2:146

for p, q being Element of MC-wff holds |-_IPC (neg (p 'or' q)) => ((neg p) '&' (neg q)) by Th97;

theorem :: INTPRO_2:147

for p, q being Element of MC-wff holds |-_IPC ((neg p) '&' (neg q)) => (neg (p 'or' q)) by Th98;

theorem :: INTPRO_2:148

for p, q being Element of MC-wff holds |-_IPC (neg (p 'or' q)) 'equiv' ((neg p) '&' (neg q)) by Th99;

theorem :: INTPRO_2:149

for p being Element of MC-wff holds |-_IPC (p '&' (neg p)) => FALSUM by Th100;

theorem :: INTPRO_2:150

for p being Element of MC-wff holds |-_IPC FALSUM 'equiv' (p '&' (neg p)) by Th101;

theorem :: INTPRO_2:151

for p being Element of MC-wff holds |-_IPC (neg p) => (neg (neg (neg p))) by Th102;

theorem :: INTPRO_2:152

for p being Element of MC-wff holds |-_IPC (neg (neg (neg p))) => (neg p) by Th103;

theorem :: INTPRO_2:153

for p being Element of MC-wff holds |-_IPC (neg p) 'equiv' (neg (neg (neg p))) by Th104;

theorem :: INTPRO_2:154

for p, q being Element of MC-wff holds |-_IPC ((neg p) => q) => ((neg (neg (neg p))) => q) by Th105;

theorem :: INTPRO_2:155

for p, q being Element of MC-wff holds |-_IPC (p => q) => ((neg (neg p)) => (neg (neg q))) by Th106;

theorem :: INTPRO_2:156

for p, q being Element of MC-wff holds |-_IPC (p '&' (neg q)) => (neg (p => q)) by Th107;

theorem :: INTPRO_2:157

for p, q being Element of MC-wff holds |-_IPC (neg (neg (p => q))) => ((neg (neg p)) => (neg (neg q))) by Th108;

theorem :: INTPRO_2:158

for p, q being Element of MC-wff holds |-_IPC ((neg (neg p)) => (neg (neg q))) => (neg (neg (p => q))) by Th109;

theorem :: INTPRO_2:159

for p, q being Element of MC-wff holds |-_IPC (neg (neg (p => q))) 'equiv' ((neg (neg p)) => (neg (neg q))) by Th110;

theorem :: INTPRO_2:160

for p, q being Element of MC-wff holds |-_IPC (neg (neg (p '&' q))) => ((neg (neg p)) '&' (neg (neg q))) by Th111;

theorem :: INTPRO_2:161

for p, q being Element of MC-wff holds |-_IPC ((neg (neg p)) '&' (neg (neg q))) => (neg (neg (p '&' q))) by Th112;

theorem :: INTPRO_2:162

for p, q being Element of MC-wff holds |-_IPC (neg (neg (p '&' q))) 'equiv' ((neg (neg p)) '&' (neg (neg q))) by Th113;

theorem :: INTPRO_2:163

for p, q being Element of MC-wff holds |-_IPC (neg (neg (p => q))) => (p => (neg (neg q))) by Th114;