The abstract of the Mizar article:

Intuitionistic Propositional Calculus in the Extended Framework with Modal Operator. Part I

by

Takao Inoue

Received April 3, 2003

MML identifier: INTPRO_1

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, RELAT_1, FUNCT_1, ZF_LANG, BOOLE, INTPRO_1, QC_LANG2;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, RELAT_1, FUNCT_1, NAT_1,
      FINSEQ_1;
 constructors NAT_1, CQC_LANG, MEMBERED;
 clusters RELSET_1, MEMBERED, NUMBERS, ORDINAL2;
 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 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;

definition
  cluster MC-closed ->
     with_FALSUM with_int_implication
     with_int_conjunction with_int_disjunction
     with_int_propositional_variables
     with_modal_operator non empty set;
  cluster
      with_FALSUM with_int_implication
      with_int_conjunction with_int_disjunction
      with_int_propositional_variables
      with_modal_operator -> MC-closed 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;

definition
  cluster MC-wff -> MC-closed;
end;

definition
  cluster MC-closed non empty set;
end;

definition
  cluster -> Relation-like Function-like Element of MC-wff;
end;

definition
  cluster -> FinSequence-like 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 :: Th14:
    CnIPC(CnIPC(X)) = CnIPC(X);

definition 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 :: Th16:
    T is IPC_theory implies IPC-Taut c= T;

definition
  cluster IPC-Taut -> IPC_theory;
end;

begin  :: Formulas provable in IPC : implication

theorem :: INTPRO_1:17   :: Identity law
  p => p in IPC-Taut;

theorem :: INTPRO_1:18
  q in IPC-Taut implies p => q in IPC-Taut;

theorem :: INTPRO_1:19 :: Th19:
    IVERUM in IPC-Taut;

theorem :: INTPRO_1:20 :: Th20:
    (p => q) => (p => p) in IPC-Taut;

theorem :: INTPRO_1:21 :: Th21:
    (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 :: Th28:
    ((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 :: Th31: :: 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 :: Th35:
    (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 :: Th40:
    (( (p => q) '&' p ) '&' s ) => q in IPC-Taut;

theorem :: INTPRO_1:41 :: Th41:
    (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 :: Th50:
    ( p '&' (s '&' q) ) => ( p '&' (q '&' s) ) in IPC-Taut;

theorem :: INTPRO_1:51 :: Th51:
    ( ( p => q ) '&' (p => s) ) => ( p => (q '&' s) ) in IPC-Taut;

theorem :: INTPRO_1:52 :: Th52:
    (p '&' q) '&' s => p '&' (q '&' s) in IPC-Taut;

theorem :: INTPRO_1:53 :: Th53:
    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 :: Th55:
    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 :: Th57:
    (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 :: Th65:
    ( p 'or' (q 'or' s) ) => ( (p 'or' q) 'or' s ) in IPC-Taut;

theorem :: INTPRO_1:66 :: Th66:
    ( (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 :: Th6C:
    CnCPC(CnCPC(X)) = CnCPC(X);

definition 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 :: Th8C:
    T is CPC_theory implies CPC-Taut c= T;

definition
  cluster CPC-Taut -> CPC_theory;
end;

theorem :: INTPRO_1:77 :: CPCincIPC:
  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 :: S4TincIPCT:
  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 :: Th10M:
    CnS4(CnS4(X)) = CnS4(X);

definition 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 :: Th12M:
    T is S4_theory implies S4-Taut c= T;

definition
  cluster S4-Taut -> S4_theory;
end;

theorem :: INTPRO_1:94 :: S4incCPC:
  CPC-Taut c= S4-Taut;

theorem :: INTPRO_1:95 :: S4incIPC:
  IPC-Taut c= S4-Taut;