:: Intuitionistic Propositional Calculus in the Extended Framework with ModalOperator, Part I
:: by Takao Inou\'e
::
:: Received April 3, 2003
:: Copyright (c) 2003 Association of Mizar Users
:: deftheorem Def1 defines with_FALSUM INTPRO_1:def 1 :
:: deftheorem Def2 defines with_int_implication INTPRO_1:def 2 :
:: deftheorem Def3 defines with_int_conjunction INTPRO_1:def 3 :
:: deftheorem Def4 defines with_int_disjunction INTPRO_1:def 4 :
:: deftheorem Def5 defines with_int_propositional_variables INTPRO_1:def 5 :
:: deftheorem Def6 defines with_modal_operator INTPRO_1:def 6 :
:: deftheorem Def7 defines MC-closed INTPRO_1:def 7 :
Lm1:
for E being set st E is MC-closed holds
not E is empty
:: deftheorem Def8 defines MC-wff INTPRO_1:def 8 :
:: deftheorem defines FALSUM INTPRO_1:def 9 :
:: deftheorem defines => INTPRO_1:def 10 :
:: deftheorem defines '&' INTPRO_1:def 11 :
:: deftheorem defines 'or' INTPRO_1:def 12 :
:: deftheorem defines Nes INTPRO_1:def 13 :
:: deftheorem Def14 defines IPC_theory INTPRO_1:def 14 :
:: deftheorem Def15 defines CnIPC INTPRO_1:def 15 :
:: deftheorem defines IPC-Taut INTPRO_1:def 16 :
:: deftheorem defines neg INTPRO_1:def 17 :
:: deftheorem defines IVERUM INTPRO_1:def 18 :
theorem Th1: :: INTPRO_1:1
theorem Th2: :: INTPRO_1:2
theorem Th3: :: INTPRO_1:3
theorem Th4: :: INTPRO_1:4
theorem Th5: :: INTPRO_1:5
theorem Th6: :: INTPRO_1:6
theorem Th7: :: INTPRO_1:7
theorem Th8: :: INTPRO_1:8
theorem Th9: :: INTPRO_1:9
theorem Th10: :: INTPRO_1:10
theorem Th11: :: INTPRO_1:11
theorem Th12: :: INTPRO_1:12
theorem Th13: :: INTPRO_1:13
Lm2:
for X being Subset of MC-wff holds CnIPC (CnIPC X) c= CnIPC X
theorem :: INTPRO_1:14
Lm3:
for X being Subset of MC-wff holds CnIPC X is IPC_theory
theorem Th15: :: INTPRO_1:15
theorem :: INTPRO_1:16
theorem Th17: :: INTPRO_1:17
theorem Th18: :: INTPRO_1:18
theorem :: INTPRO_1:19
theorem :: INTPRO_1:20
theorem :: INTPRO_1:21
theorem Th22: :: INTPRO_1:22
theorem Th23: :: INTPRO_1:23
theorem Th24: :: INTPRO_1:24
theorem Th25: :: INTPRO_1:25
theorem Th26: :: INTPRO_1:26
Lm4:
for q, r, p, s being Element of MC-wff holds (((q => r) => (p => r)) => s) => ((p => q) => s) in IPC-Taut
theorem Th27: :: INTPRO_1:27
theorem :: INTPRO_1:28
theorem Th29: :: INTPRO_1:29
theorem Th30: :: INTPRO_1:30
theorem :: INTPRO_1:31
theorem Th32: :: INTPRO_1:32
theorem Th33: :: INTPRO_1:33
theorem Th34: :: INTPRO_1:34
theorem :: INTPRO_1:35
theorem Th36: :: INTPRO_1:36
theorem Th37: :: INTPRO_1:37
theorem Th38: :: INTPRO_1:38
theorem Th39: :: INTPRO_1:39
theorem :: INTPRO_1:40
theorem :: INTPRO_1:41
theorem Th42: :: INTPRO_1:42
theorem Th43: :: INTPRO_1:43
theorem Th44: :: INTPRO_1:44
theorem Th45: :: INTPRO_1:45
theorem Th46: :: INTPRO_1:46
theorem Th47: :: INTPRO_1:47
theorem Th48: :: INTPRO_1:48
theorem Th49: :: INTPRO_1:49
theorem :: INTPRO_1:50
theorem :: INTPRO_1:51
Lm5:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => q in IPC-Taut
Lm6:
for p, q, s being Element of MC-wff holds (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in IPC-Taut
Lm7:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in IPC-Taut
Lm8:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (p '&' s) in IPC-Taut
Lm9:
for p, q, s being Element of MC-wff holds (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in IPC-Taut
Lm10:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((p '&' s) '&' q) in IPC-Taut
Lm11:
for p, s, q being Element of MC-wff holds ((p '&' s) '&' q) => ((s '&' p) '&' q) in IPC-Taut
Lm12:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((s '&' p) '&' q) in IPC-Taut
Lm13:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => ((s '&' q) '&' p) in IPC-Taut
Lm14:
for p, q, s being Element of MC-wff holds ((p '&' q) '&' s) => (p '&' (s '&' q)) in IPC-Taut
Lm15:
for p, s, q being Element of MC-wff holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in IPC-Taut
theorem :: INTPRO_1:52
Lm16:
for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((s '&' q) '&' p) in IPC-Taut
Lm17:
for s, q, p being Element of MC-wff holds ((s '&' q) '&' p) => ((q '&' s) '&' p) in IPC-Taut
Lm18:
for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((q '&' s) '&' p) in IPC-Taut
Lm19:
for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => ((p '&' s) '&' q) in IPC-Taut
Lm20:
for p, q, s being Element of MC-wff holds (p '&' (q '&' s)) => (p '&' (s '&' q)) in IPC-Taut
theorem :: INTPRO_1:53
theorem Th54: :: INTPRO_1:54
theorem :: INTPRO_1:55
theorem Th56: :: INTPRO_1:56
theorem :: INTPRO_1:57
theorem Th58: :: INTPRO_1:58
theorem Th59: :: INTPRO_1:59
theorem Th60: :: INTPRO_1:60
theorem Th61: :: INTPRO_1:61
theorem Th62: :: INTPRO_1:62
theorem Th63: :: INTPRO_1:63
theorem Th64: :: INTPRO_1:64
theorem :: INTPRO_1:65
theorem :: INTPRO_1:66
:: deftheorem Def19 defines CPC_theory INTPRO_1:def 19 :
theorem Th67: :: INTPRO_1:67
:: deftheorem Def20 defines CnCPC INTPRO_1:def 20 :
:: deftheorem defines CPC-Taut INTPRO_1:def 21 :
theorem Th68: :: INTPRO_1:68
theorem Th69: :: INTPRO_1:69
theorem Th70: :: INTPRO_1:70
theorem Th71: :: INTPRO_1:71
theorem Th72: :: INTPRO_1:72
theorem Th73: :: INTPRO_1:73
Lm21:
for X being Subset of MC-wff holds CnCPC (CnCPC X) c= CnCPC X
theorem :: INTPRO_1:74
Lm22:
for X being Subset of MC-wff holds CnCPC X is CPC_theory
theorem Th75: :: INTPRO_1:75
theorem :: INTPRO_1:76
theorem :: INTPRO_1:77
:: deftheorem Def22 defines S4_theory INTPRO_1:def 22 :
theorem Th78: :: INTPRO_1:78
theorem :: INTPRO_1:79
:: deftheorem Def23 defines CnS4 INTPRO_1:def 23 :
:: deftheorem defines S4-Taut INTPRO_1:def 24 :
theorem Th80: :: INTPRO_1:80
theorem Th81: :: INTPRO_1:81
theorem Th82: :: INTPRO_1:82
theorem Th83: :: INTPRO_1:83
theorem Th84: :: INTPRO_1:84
theorem Th85: :: INTPRO_1:85
theorem Th86: :: INTPRO_1:86
theorem Th87: :: INTPRO_1:87
theorem Th88: :: INTPRO_1:88
theorem Th89: :: INTPRO_1:89
theorem Th90: :: INTPRO_1:90
Lm23:
for X being Subset of MC-wff holds CnS4 (CnS4 X) c= CnS4 X
theorem :: INTPRO_1:91
Lm24:
for X being Subset of MC-wff holds CnS4 X is S4_theory
theorem Th92: :: INTPRO_1:92
theorem :: INTPRO_1:93
theorem :: INTPRO_1:94
theorem :: INTPRO_1:95