:: Intuitionistic Propositional Calculus in the Extended Framework with Modal
:: Operator, Part I
:: by Takao Inou\'e
::
:: Received April 3, 2003
:: Copyright (c) 2003-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSEQ_1, CARD_1, ORDINAL4, SUBSET_1, NUMBERS, ARYTM_3, RELAT_1,
TARSKI, XBOOLE_0, FUNCT_1, QC_LANG2, XBOOLEAN, INTPRO_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1,
FUNCT_1, FINSEQ_1;
constructors NAT_1, FINSEQ_1, NUMBERS;
registrations SUBSET_1, ORDINAL1, FUNCT_1, FINSEQ_1, NAT_1, XCMPLX_0;
requirements NUMERALS, BOOLE, SUBSET;
begin :: Intuitionistic propositional calculus IPC in the extended
:: language with modal operator
definition
let E be set;
attr E is with_FALSUM means
:: INTPRO_1:def 1
<*0*>in E;
end;
definition
let E be set;
attr E is with_int_implication means
:: INTPRO_1:def 2
for p, q being FinSequence st p in E & q in E holds <*1*>^p^q in E;
end;
definition
let E be set;
attr E is with_int_conjunction means
:: INTPRO_1:def 3
for p, q being FinSequence st p in E & q in E holds <*2*>^p^q in E;
end;
definition
let E be set;
attr E is with_int_disjunction means
:: INTPRO_1:def 4
for p, q being FinSequence st p in E & q in E holds <*3*>^p^q in E;
end;
definition
let E be set;
attr E is with_int_propositional_variables means
:: INTPRO_1:def 5
for n being Element of NAT holds <* 5+2*n *> in E;
end;
definition
let E be set;
attr E is with_modal_operator means
:: INTPRO_1:def 6
for p being FinSequence st p in E holds <*6*>^p in E;
end;
:: We reserve <*4*> for verum for a possible formulation.
:: So do we <* 5+2*n+1 *> for every n >= 1 for introduction of a number of
:: other logical connectives (e.g. for polymodal logics,
:: hybrid logics, recent computer-oriented logics and so on).
definition
let E be set;
attr E is MC-closed means
:: INTPRO_1:def 7
E c= NAT* & E is with_FALSUM
with_int_implication with_int_conjunction with_int_disjunction
with_int_propositional_variables with_modal_operator;
end;
registration
cluster MC-closed -> with_FALSUM with_int_implication with_int_conjunction
with_int_disjunction with_int_propositional_variables with_modal_operator non
empty for set;
cluster with_FALSUM with_int_implication with_int_conjunction
with_int_disjunction with_int_propositional_variables with_modal_operator ->
MC-closed for Subset of NAT*;
end;
definition
func MC-wff -> set means
:: INTPRO_1:def 8
it is MC-closed & for E being set st E is MC-closed holds it c= E;
end;
registration
cluster MC-wff -> MC-closed;
end;
registration
cluster MC-closed non empty for set;
end;
registration
cluster MC-wff -> functional;
end;
registration
cluster -> FinSequence-like for Element of MC-wff;
end;
definition
mode MC-formula is Element of MC-wff;
end;
definition
func FALSUM -> MC-formula equals
:: INTPRO_1:def 9
<*0*>;
let p, q be Element of MC-wff;
func p => q -> MC-formula equals
:: INTPRO_1:def 10
<*1*>^p^q;
func p '&' q -> MC-formula equals
:: INTPRO_1:def 11
<*2*>^p^q;
func p 'or' q -> MC-formula equals
:: INTPRO_1:def 12
<*3*>^p^q;
end;
definition
let p be Element of MC-wff;
func Nes p -> MC-formula equals
:: INTPRO_1:def 13
<*6*>^p;
end;
reserve T, X, Y for Subset of MC-wff;
reserve p, q, r, s for Element of MC-wff;
definition
let T be Subset of MC-wff;
attr T is IPC_theory means
:: 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);
end;
definition
let X;
func CnIPC X -> Subset of MC-wff means
:: INTPRO_1:def 15
r in it iff for T st T is IPC_theory & X c= T holds r in T;
end;
definition
func IPC-Taut -> Subset of MC-wff equals
:: INTPRO_1:def 16
CnIPC({}(MC-wff));
end;
definition
let p be Element of MC-wff;
func neg p -> MC-formula equals
:: INTPRO_1:def 17
(p => FALSUM);
end;
definition
func IVERUM -> MC-formula equals
:: INTPRO_1:def 18
(FALSUM => FALSUM);
end;
theorem :: INTPRO_1:1
p => (q => p) in CnIPC (X);
theorem :: INTPRO_1:2
(p => (q => r)) => ((p => q) => (p => r)) in CnIPC (X);
theorem :: INTPRO_1:3
p '&' q => p in CnIPC(X);
theorem :: INTPRO_1:4
p '&' q => q in CnIPC(X);
theorem :: INTPRO_1:5
p => (q => (p '&' q)) in CnIPC (X);
theorem :: INTPRO_1:6
p => (p 'or' q) in CnIPC (X);
theorem :: INTPRO_1:7
q => (p 'or' q) in CnIPC (X);
theorem :: INTPRO_1:8
(p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC (X);
theorem :: INTPRO_1:9
FALSUM => p in CnIPC (X);
theorem :: INTPRO_1:10
p in CnIPC(X) & p => q in CnIPC(X) implies q in CnIPC(X);
theorem :: INTPRO_1:11
T is IPC_theory & X c= T implies CnIPC(X) c= T;
theorem :: INTPRO_1:12
X c= CnIPC(X);
theorem :: INTPRO_1:13
X c= Y implies CnIPC(X) c= CnIPC(Y);
theorem :: INTPRO_1:14
CnIPC(CnIPC(X)) = CnIPC(X);
registration
let X be Subset of MC-wff;
cluster CnIPC(X) -> IPC_theory;
end;
theorem :: INTPRO_1:15
T is IPC_theory iff CnIPC(T) = T;
theorem :: INTPRO_1:16
T is IPC_theory implies IPC-Taut c= T;
registration
cluster IPC-Taut -> IPC_theory;
end;
begin :: Formulas provable in IPC : implication
theorem :: INTPRO_1:17
p => p in IPC-Taut;
theorem :: INTPRO_1:18
q in IPC-Taut implies p => q in IPC-Taut;
theorem :: INTPRO_1:19
IVERUM in IPC-Taut;
theorem :: INTPRO_1:20
(p => q) => (p => p) in IPC-Taut;
theorem :: INTPRO_1:21
(q => p) => (p => p) in IPC-Taut;
theorem :: INTPRO_1:22
(q => r) => ((p => q) => (p => r)) in IPC-Taut;
theorem :: INTPRO_1:23
p => (q => r) in IPC-Taut implies q => (p => r) in IPC-Taut;
theorem :: INTPRO_1:24 :: Hypothetical syllogism
(p => q) => ((q => r) => (p => r)) in IPC-Taut;
theorem :: INTPRO_1:25
p => q in IPC-Taut implies (q => r) => (p => r) in IPC-Taut;
theorem :: INTPRO_1:26
p => q in IPC-Taut & q => r in IPC-Taut implies p => r in IPC-Taut;
theorem :: INTPRO_1:27
(p => (q => r)) => ((s => q) => (p => (s => r))) in IPC-Taut;
theorem :: INTPRO_1:28
((p => q) => r) => (q => r) in IPC-Taut;
theorem :: INTPRO_1:29 :: Contraposition
(p => (q => r)) => (q => (p => r)) in IPC-Taut;
theorem :: INTPRO_1:30 :: A Hilbert axiom
(p => (p => q)) => (p => q) in IPC-Taut;
theorem :: INTPRO_1:31 :: Modus ponendo ponens
q => ((q => p) => p) in IPC-Taut;
theorem :: INTPRO_1:32
s => (q => p) in IPC-Taut & q in IPC-Taut implies s => p in IPC-Taut;
begin :: Formulas provable in IPC : conjunction
theorem :: INTPRO_1:33
p => (p '&' p) in IPC-Taut;
theorem :: INTPRO_1:34
(p '&' q) in IPC-Taut iff p in IPC-Taut & q in IPC-Taut;
theorem :: INTPRO_1:35
(p '&' q) in IPC-Taut iff (q '&' p) in IPC-Taut;
theorem :: INTPRO_1:36
(( p '&' q ) => r ) => ( p => ( q => r )) in IPC-Taut;
theorem :: INTPRO_1:37
( p => ( q => r )) => (( p '&' q ) => r ) in IPC-Taut;
theorem :: INTPRO_1:38
( r => p ) => (( r => q ) => ( r => ( p '&' q ))) in IPC-Taut;
theorem :: INTPRO_1:39
( (p => q) '&' p ) => q in IPC-Taut;
theorem :: INTPRO_1:40
(( (p => q) '&' p ) '&' s ) => q in IPC-Taut;
theorem :: INTPRO_1:41
(q => s) => (( p '&' q ) => s) in IPC-Taut;
theorem :: INTPRO_1:42
(q => s) => (( q '&' p ) => s) in IPC-Taut;
theorem :: INTPRO_1:43
( (p '&' s) => q ) => ((p '&' s) => (q '&' s)) in IPC-Taut;
theorem :: INTPRO_1:44
( p => q ) => ((p '&' s) => (q '&' s)) in IPC-Taut;
theorem :: INTPRO_1:45
(( p => q ) '&' ( p '&' s )) => ( q '&' s ) in IPC-Taut;
theorem :: INTPRO_1:46
( p '&' q ) => ( q '&' p ) in IPC-Taut;
theorem :: INTPRO_1:47
( p => q ) '&' ( p '&' s ) => ( s '&' q ) in IPC-Taut;
theorem :: INTPRO_1:48
( p => q ) => (( p '&' s ) => ( s '&' q )) in IPC-Taut;
theorem :: INTPRO_1:49
( p => q ) => (( s '&' p ) => ( s '&' q )) in IPC-Taut;
theorem :: INTPRO_1:50
( p '&' (s '&' q) ) => ( p '&' (q '&' s) ) in IPC-Taut;
theorem :: INTPRO_1:51
( ( p => q ) '&' (p => s) ) => ( p => (q '&' s) ) in IPC-Taut;
theorem :: INTPRO_1:52
(p '&' q) '&' s => p '&' (q '&' s) in IPC-Taut;
theorem :: INTPRO_1:53
p '&' (q '&' s) => (p '&' q) '&' s in IPC-Taut;
begin :: Formulas provable in IPC: disjunction
theorem :: INTPRO_1:54
(p 'or' p) => p in IPC-Taut;
theorem :: INTPRO_1:55
p in IPC-Taut or q in IPC-Taut implies (p 'or' q) in IPC-Taut;
theorem :: INTPRO_1:56
(p 'or' q) => (q 'or' p) in IPC-Taut;
theorem :: INTPRO_1:57
(p 'or' q) in IPC-Taut iff (q 'or' p) in IPC-Taut;
theorem :: INTPRO_1:58
(p => q) => (p => (q 'or' s)) in IPC-Taut;
theorem :: INTPRO_1:59
(p => q) => (p => (s 'or' q)) in IPC-Taut;
theorem :: INTPRO_1:60
( p => q ) => ((p 'or' s) => (q 'or' s)) in IPC-Taut;
theorem :: INTPRO_1:61
p => q in IPC-Taut implies (p 'or' s) => (q 'or' s) in IPC-Taut;
theorem :: INTPRO_1:62
( p => q ) => (( s 'or' p ) => ( s 'or' q )) in IPC-Taut;
theorem :: INTPRO_1:63
p => q in IPC-Taut implies ( s 'or' p ) => ( s 'or' q ) in IPC-Taut;
theorem :: INTPRO_1:64
( p 'or' (q 'or' s) ) => ( q 'or' (p 'or' s) ) in IPC-Taut;
theorem :: INTPRO_1:65
( p 'or' (q 'or' s) ) => ( (p 'or' q) 'or' s ) in IPC-Taut;
theorem :: INTPRO_1:66
( (p 'or' q) 'or' s ) => ( p 'or' (q 'or' s) ) in IPC-Taut;
begin :: Classical propositional calculus CPC
reserve T, X, Y for Subset of MC-wff;
reserve p, q, r for Element of MC-wff;
definition
let T be Subset of MC-wff;
attr T is CPC_theory means
:: INTPRO_1:def 19
for p, q, r being Element of MC-wff holds
p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q)
=> p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q)
in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T
& FALSUM => p in T & p 'or' (p => FALSUM) in T & (p in T & p => q in T implies
q in T);
end;
theorem :: INTPRO_1:67
T is CPC_theory implies T is IPC_theory;
definition
let X;
func CnCPC X -> Subset of MC-wff means
:: INTPRO_1:def 20
r in it iff for T st T is CPC_theory & X c= T holds r in T;
end;
definition
func CPC-Taut -> Subset of MC-wff equals
:: INTPRO_1:def 21
CnCPC({}(MC-wff));
end;
theorem :: INTPRO_1:68
CnIPC (X) c= CnCPC (X);
theorem :: INTPRO_1:69
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);
theorem :: INTPRO_1:70
p in CnCPC(X) & p => q in CnCPC(X) implies q in CnCPC(X);
theorem :: INTPRO_1:71
T is CPC_theory & X c= T implies CnCPC(X) c= T;
theorem :: INTPRO_1:72
X c= CnCPC(X);
theorem :: INTPRO_1:73
X c= Y implies CnCPC(X) c= CnCPC(Y);
theorem :: INTPRO_1:74
CnCPC(CnCPC(X)) = CnCPC(X);
registration
let X be Subset of MC-wff;
cluster CnCPC(X) -> CPC_theory;
end;
theorem :: INTPRO_1:75
T is CPC_theory iff CnCPC(T) = T;
theorem :: INTPRO_1:76
T is CPC_theory implies CPC-Taut c= T;
registration
cluster CPC-Taut -> CPC_theory;
end;
theorem :: INTPRO_1:77
IPC-Taut c= CPC-Taut;
begin :: Modal calculus S4
reserve T, X, Y for Subset of MC-wff;
reserve p, q, r for Element of MC-wff;
definition
let T be Subset of MC-wff;
attr T is S4_theory means
:: INTPRO_1:def 22
for p, q, r being Element of MC-wff holds
p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q)
=> p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & p => (p 'or' q)
in T & q => (p 'or' q) in T & (p => r) => ((q => r) => ((p 'or' q) => r)) in T
& FALSUM => p in T & p 'or' (p => FALSUM) in T & (Nes (p => q)) => ((Nes p) =>
(Nes q)) in T & (Nes p) => p in T & (Nes p) => Nes (Nes p) in T & (p in T & p
=> q in T implies q in T) & (p in T implies Nes p in T);
end;
theorem :: INTPRO_1:78
T is S4_theory implies T is CPC_theory;
theorem :: INTPRO_1:79
T is S4_theory implies T is IPC_theory;
definition
let X;
func CnS4 X -> Subset of MC-wff means
:: INTPRO_1:def 23
r in it iff for T st T is S4_theory & X c= T holds r in T;
end;
definition
func S4-Taut -> Subset of MC-wff equals
:: INTPRO_1:def 24
CnS4({}(MC-wff));
end;
theorem :: INTPRO_1:80
CnCPC (X) c= CnS4 (X);
theorem :: INTPRO_1:81
CnIPC (X) c= CnS4 (X);
theorem :: INTPRO_1:82
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);
theorem :: INTPRO_1:83
p in CnS4 (X) & p => q in CnS4 (X) implies q in CnS4 (X);
theorem :: INTPRO_1:84
(Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 (X);
theorem :: INTPRO_1:85
(Nes p) => p in CnS4 (X);
theorem :: INTPRO_1:86
(Nes p) => Nes (Nes p) in CnS4 (X);
theorem :: INTPRO_1:87
p in CnS4 (X) implies Nes p in CnS4 (X);
theorem :: INTPRO_1:88
T is S4_theory & X c= T implies CnS4(X) c= T;
theorem :: INTPRO_1:89
X c= CnS4(X);
theorem :: INTPRO_1:90
X c= Y implies CnS4(X) c= CnS4(Y);
theorem :: INTPRO_1:91
CnS4(CnS4(X)) = CnS4(X);
registration
let X be Subset of MC-wff;
cluster CnS4(X) -> S4_theory;
end;
theorem :: INTPRO_1:92
T is S4_theory iff CnS4(T) = T;
theorem :: INTPRO_1:93
T is S4_theory implies S4-Taut c= T;
registration
cluster S4-Taut -> S4_theory;
end;
theorem :: INTPRO_1:94
CPC-Taut c= S4-Taut;
theorem :: INTPRO_1:95
IPC-Taut c= S4-Taut;