The Mizar article:

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

by
Takao Inoue

Received April 3, 2003

Copyright (c) 2003 Association of Mizar Users

MML identifier: INTPRO_1
[ 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;
 definitions TARSKI;
 theorems TARSKI, FINSEQ_1, XBOOLE_0, XBOOLE_1;
 schemes XBOOLE_0;

begin :: Intuitionistic propositional calculus IPC in the extended
      :: language with modal operator

definition let E be set;
  attr E is with_FALSUM means :Def1:
      <*0*>in E;
end;

definition let E be set;
  attr E is with_int_implication means :Def2:
  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 :Def3:
     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 :Def4:
     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 :Def5:
     for n being Nat holds <* 5+2*n *> in E;
end;

definition let E be set;
  attr E is with_modal_operator means :Def6:
  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 :Def7:
   E c= NAT* &
   E is with_FALSUM with_int_implication
        with_int_conjunction with_int_disjunction
        with_int_propositional_variables
        with_modal_operator;
end;

Lm1: for E be set st E is MC-closed holds E is non empty
proof
  let E be set;
  assume E is MC-closed;
  then E is with_FALSUM by Def7;
  hence thesis by Def1;
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;
  coherence by Def7,Lm1;
  cluster
      with_FALSUM with_int_implication
      with_int_conjunction with_int_disjunction
      with_int_propositional_variables
      with_modal_operator -> MC-closed Subset of NAT*;
  coherence by Def7;
end;

definition
  func MC-wff -> set means :Def8:
   it is MC-closed &
   for E being set st E is MC-closed holds it c= E;
existence
  proof
    defpred P[set] means
    for E being set st E is MC-closed holds $1 in E;
     consider E0 being set such that
A1:   for x being set holds x in E0 iff x in NAT* & P[x]
               from Separation;
  A2: <*0*> in NAT* by FINSEQ_1:def 11;
  A3: for E being set st E is MC-closed holds <*0*> in E
      proof
        let E be set; assume E is MC-closed;
        then E is with_FALSUM by Def7;
        hence thesis by Def1;
      end;
   then reconsider E0 as non empty set by A1,A2;
   take E0;
A4: E0 c= NAT*
   proof let x be set;
     thus thesis by A1;
   end;
     <*0*> in E0 by A1,A2,A3;
then A5:E0 is with_FALSUM by Def1;
     for n being Nat holds <* 5+2*n *> in E0
   proof let n be Nat;
     set p = 5+2*n;
     reconsider h = <*p*> as FinSequence of NAT;
A6:  h in NAT* by FINSEQ_1:def 11;
       for E being set st E is MC-closed holds <*p*> in E
     proof
       let E be set;
       assume E is MC-closed;
       then E is with_int_propositional_variables by Def7;
       hence thesis by Def5;
     end;
     hence thesis by A1,A6;
   end;
then A7: E0 is with_int_propositional_variables by Def5;
     for p, q being FinSequence
    st p in E0 & q in E0 holds <*1*>^p^q in E0
        proof
          let p, q be FinSequence such that
        A8: p in E0 & q in E0;
              p in NAT* & q in NAT* by A1,A8;
            then reconsider p'=p, q'=q as FinSequence of NAT by FINSEQ_1:def 11
;
       A9: <*1*>^p'^q' in NAT* by FINSEQ_1:def 11;
              for E being set
              st E is MC-closed holds <*1*>^p^q in E
                proof let E be set; assume
                A10:    E is MC-closed;
then A11:               E is with_int_implication by Def7;
                    p in E & q in E by A1,A8,A10;
                  hence thesis by A11,Def2;
                end;
           hence <*1*>^p^q in E0 by A1,A9;
        end;
then A12: E0 is with_int_implication by Def2;
     for p, q being FinSequence
    st p in E0 & q in E0 holds <*2*>^p^q in E0
         proof
          let p, q be FinSequence such that
        A13: p in E0 & q in E0;
              p in NAT* & q in NAT* by A1,A13;
            then reconsider p'=p, q'=q as FinSequence of NAT by FINSEQ_1:def 11
;
       A14: <*2*>^p'^q' in NAT* by FINSEQ_1:def 11;
              for E being set
              st E is MC-closed holds <*2*>^p^q in E
                proof let E be set; assume
                A15:    E is MC-closed;
then A16:              E is with_int_conjunction by Def7;
                    p in E & q in E by A1,A13,A15;
                  hence thesis by A16,Def3;
                end;
           hence <*2*>^p^q in E0 by A1,A14;
        end;
then A17: E0 is with_int_conjunction by Def3;
     for p, q being FinSequence
    st p in E0 & q in E0 holds <*3*>^p^q in E0
        proof
          let p, q be FinSequence such that
        A18: p in E0 & q in E0;
              p in NAT* & q in NAT* by A1,A18;
            then reconsider p'=p, q'=q as FinSequence of NAT by FINSEQ_1:def 11
;
       A19: <*3*>^p'^q' in NAT* by FINSEQ_1:def 11;
              for E being set
              st E is MC-closed holds <*3*>^p^q in E
                proof let E be set; assume
                A20:    E is MC-closed;
then A21:             E is with_int_disjunction by Def7;
                    p in E & q in E by A1,A18,A20;
                  hence thesis by A21,Def4;
                end;
           hence <*3*>^p^q in E0 by A1,A19;
        end;
then A22: E0 is with_int_disjunction by Def4;
     for p being FinSequence
    st p in E0 holds <*6*>^p in E0
        proof
          let p be FinSequence such that
        A23: p in E0;
              p in NAT* by A1,A23;
            then reconsider p'=p as FinSequence of NAT by FINSEQ_1:def 11;
        A24: <*6*>^p' in NAT* by FINSEQ_1:def 11;
              for E being set
              st E is MC-closed holds <*6*>^p in E
                proof let E be set; assume
                  A25:  E is MC-closed;
then A26:               E is with_modal_operator by Def7;
                    p in E by A1,A23,A25;
                  hence thesis by A26,Def6;
                end;
           hence <*6*>^p in E0 by A1,A24;
        end;
   then E0 is with_modal_operator by Def6;
  hence E0 is MC-closed by A4,A5,A7,A12,A17,A22,Def7;
   let E be set such that
A27:   E is MC-closed;
   let x be set; assume
     x in E0;
   hence thesis by A1,A27;
  end;
uniqueness
  proof
    let E1, E2 be set such that
A28:  E1 is MC-closed & for E being set
        st E is MC-closed holds E1 c= E and
A29:  E2 is MC-closed & for E being set
        st E is MC-closed holds E2 c= E;
      E1 c= E2 & E2 c= E1 by A28,A29;
  hence E1 = E2 by XBOOLE_0:def 10;
  end;
end;

definition
  cluster MC-wff -> MC-closed;
  coherence by Def8;
end;

definition
  cluster MC-closed non empty set;
  existence
  proof
    take MC-wff;
    thus thesis;
  end;
end;

definition
  cluster -> Relation-like Function-like Element of MC-wff;
coherence
   proof let p be Element of MC-wff;
       MC-wff c= NAT* & p in MC-wff by Def7;
     hence thesis by FINSEQ_1:def 11;
   end;
end;

definition
  cluster -> FinSequence-like Element of MC-wff;
coherence
   proof let p be Element of MC-wff;
       MC-wff c= NAT* & p in MC-wff by Def7;
     hence thesis by FINSEQ_1:def 11;
   end;
end;

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

definition
  func FALSUM -> MC-formula equals
    <*0*>;
correctness by Def1;

  let p, q be Element of MC-wff;
  func p => q -> MC-formula equals
    <*1*>^p^q;
correctness by Def2;

  func p '&' q -> MC-formula equals
    <*2*>^p^q;
correctness by Def3;

  func p 'or' q -> MC-formula equals
    <*3*>^p^q;
correctness by Def4;
end;

definition
let p be Element of MC-wff;
  func Nes p -> MC-formula equals
    <*6*>^p;
correctness by Def6;
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 :Def14:
    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;

definition let X;
  func CnIPC X -> Subset of MC-wff means :Def15:
  r in it iff for T st T is IPC_theory & X c= T holds r in T;
 existence
  proof
    defpred P[set] means
    for T st T is IPC_theory & X c= T holds $1 in T;
   consider Y being set such that
A1: for a being set holds a in Y iff
     a in MC-wff & P[a] from Separation;
      Y c= MC-wff
    proof
     let a be set; assume a in Y;
     hence a in MC-wff by A1;
    end;
   then reconsider Z = Y as Subset of MC-wff;
   take Z;
   thus r in Z iff for T st T is IPC_theory & X c= T holds r in T by A1;
  end;
 uniqueness
  proof
   let Y,Z be Subset of MC-wff such that
    A2: r in Y iff for T st T is IPC_theory & X c= T holds r in T and
    A3: r in Z iff for T st T is IPC_theory & X c= T holds r in T;
     for a being set holds a in Y iff a in Z
    proof
     let a be set;
     hereby assume A4: a in Y;
       then reconsider t=a as Element of MC-wff;
         for T st T is IPC_theory & X c= T holds t in T by A2,A4;
       hence a in Z by A3;
      end;
       assume A5: a in Z;
       then reconsider t=a as Element of MC-wff;
         for T st T is IPC_theory & X c= T holds t in T by A3,A5;
       hence a in Y by A2;
    end;
    hence thesis by TARSKI:2;
  end;
end;

definition
  func IPC-Taut -> Subset of MC-wff equals :Def16:
    CnIPC({}(MC-wff));
  correctness;
end;

definition
  let p be Element of MC-wff;
  func neg p -> MC-formula equals
        (p => FALSUM);
correctness;
end;

definition
  func IVERUM -> MC-formula equals :Def18:
  (FALSUM => FALSUM);
correctness;
end;

theorem Th1:
  p => (q => p) in CnIPC (X)
 proof
    T is IPC_theory & X c= T implies p => (q => p) in T by Def14;
  hence thesis by Def15;
 end;

theorem Th2:
  (p => (q => r)) => ((p => q) => (p => r)) in CnIPC (X)
 proof
    T is IPC_theory & X c= T implies
    (p => (q => r)) => ((p => q) => (p => r)) in T by Def14;
  hence thesis by Def15;
 end;

theorem Th3:
  p '&' q => p in CnIPC(X)
 proof
    T is IPC_theory & X c= T implies p '&' q => p in T by Def14;
  hence thesis by Def15;
 end;

theorem Th4:
  p '&' q => q in CnIPC(X)
 proof
    T is IPC_theory & X c= T implies p '&' q => q in T by Def14;
  hence thesis by Def15;
 end;

theorem Th5:
  p => (q => (p '&' q)) in CnIPC (X)
 proof
    T is IPC_theory & X c= T implies p => (q => (p '&' q)) in T by Def14;
  hence thesis by Def15;
 end;

theorem Th6:
  p => (p 'or' q) in CnIPC (X)
 proof
    T is IPC_theory & X c= T implies p => (p 'or' q) in T by Def14;
  hence thesis by Def15;
 end;

theorem Th7:
  q => (p 'or' q) in CnIPC (X)
 proof
    T is IPC_theory & X c= T implies q => (p 'or' q) in T by Def14;
  hence thesis by Def15;
 end;

theorem Th8:
  (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC (X)
 proof
    T is IPC_theory & X c= T
  implies (p => r) => ((q => r) => ((p 'or' q) => r)) in T by Def14;
  hence thesis by Def15;
 end;

theorem Th9:
  FALSUM => p in CnIPC (X)
 proof
    T is IPC_theory & X c= T implies FALSUM => p in T by Def14;
  hence thesis by Def15;
 end;

theorem Th10:
  p in CnIPC(X) & p => q in CnIPC(X) implies q in CnIPC(X)
 proof
  assume A1: p in CnIPC(X) & p => q in CnIPC(X);
    T is IPC_theory & X c= T implies q in T
  proof
    assume A2: T is IPC_theory & X c= T;
    then p in T & p => q in T by A1,Def15;
    hence thesis by A2,Def14;
  end;
  hence thesis by Def15;
 end;

theorem Th11: T is IPC_theory & X c= T implies CnIPC(X) c= T
 proof
  assume that A1:T is IPC_theory and A2: X c= T;
  let a be set;
  thus thesis by A1,A2,Def15;
 end;

theorem Th12:
  X c= CnIPC(X)
 proof
  let a be set;
  assume A1: a in X;
  then reconsider t = a as Element of MC-wff;
    for T st T is IPC_theory & X c= T holds t in T by A1;
  hence a in CnIPC(X) by Def15;
 end;

theorem Th13:
  X c= Y implies CnIPC(X) c= CnIPC(Y)
 proof
  assume A1: X c= Y;
  thus CnIPC(X) c= CnIPC(Y)
   proof
    let a be set; assume A2: a in CnIPC(X);
    then reconsider t = a as Element of MC-wff;
      for T st T is IPC_theory & Y c= T holds t in T
     proof
      let T such that A3: T is IPC_theory and A4: Y c= T;
        X c= T by A1,A4,XBOOLE_1:1;
      hence t in T by A2,A3,Def15;
     end;
    hence thesis by Def15;
   end;
 end;

Lm2: CnIPC(CnIPC(X)) c= CnIPC(X)
 proof
  let a be set; assume A1: a in CnIPC(CnIPC(X));
  then reconsider t = a as Element of MC-wff;
    for T st T is IPC_theory & X c= T holds t in T
   proof
    let T; assume that A2: T is IPC_theory and A3: X c= T;
      CnIPC(X) c= T by A2,A3,Th11;
    hence t in T by A1,A2,Def15;
   end;
  hence thesis by Def15;
 end;

theorem :: Th14:
    CnIPC(CnIPC(X)) = CnIPC(X)
 proof
    CnIPC(CnIPC(X)) c= CnIPC(X) & CnIPC(X) c= CnIPC(CnIPC(X)) by Lm2,Th12;
  hence thesis by XBOOLE_0:def 10;
 end;

Lm3:
CnIPC(X) is IPC_theory
 proof
  let p, q, r;
  thus p => (q => p) in CnIPC(X) by Th1;
  thus (p => (q => r)) => ((p => q) => (p => r)) in CnIPC(X) by Th2;
  thus (p '&' q) => p in CnIPC(X) by Th3;
  thus (p '&' q) => q in CnIPC(X) by Th4;
  thus p => (q => (p '&' q)) in CnIPC(X) by Th5;
  thus p => (p 'or' q) in CnIPC(X) by Th6;
  thus q => (p 'or' q) in CnIPC(X) by Th7;
  thus (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC(X) by Th8;
  thus FALSUM => p in CnIPC(X) by Th9;
  thus (p in CnIPC(X) & p => q in CnIPC(X) implies q in CnIPC(X)) by Th10;
 end;

definition let X be Subset of MC-wff;
  cluster CnIPC(X) -> IPC_theory;
  coherence by Lm3;
end;

theorem Th15:
  T is IPC_theory iff CnIPC(T) = T
 proof
   hereby assume A1: T is IPC_theory;
    A2: T c= CnIPC(T) by Th12;
      CnIPC(T) c= T
     proof
      let a be set; assume a in CnIPC(T);
      hence a in T by A1,Def15;
     end;
    hence CnIPC(T) = T by A2,XBOOLE_0:def 10;
   end;
  thus CnIPC(T) = T implies T is IPC_theory;
 end;

theorem :: Th16:
    T is IPC_theory implies IPC-Taut c= T
 proof
  assume A1: T is IPC_theory;
    {}(MC-wff) c= T by XBOOLE_1:2;
  then IPC-Taut c= CnIPC(T) by Def16,Th13;
  hence thesis by A1,Th15;
 end;

definition
  cluster IPC-Taut -> IPC_theory;
  coherence by Def16;
end;

begin  :: Formulas provable in IPC : implication

theorem Th17:  :: Identity law
  p => p in IPC-Taut
proof
A1:p => (p => p) in IPC-Taut by Def14;
A2:(p => ((p => p) => p))
      => ((p => (p => p)) => (p => p)) in IPC-Taut by Def14;
      p => ((p => p) => p) in IPC-Taut by Def14;
    then (p => (p => p)) => (p => p) in IPC-Taut by A2,Def14;
  hence thesis by A1,Def14;
end;

theorem Th18:
  q in IPC-Taut implies p => q in IPC-Taut
  proof
      q => (p => q) in IPC-Taut by Def14;
    hence thesis by Def14;
  end;

theorem :: Th19:
    IVERUM in IPC-Taut by Def14,Def18;

theorem :: Th20:
    (p => q) => (p => p) in IPC-Taut
proof
    (p => p) in IPC-Taut by Th17;
  hence thesis by Th18;
end;

theorem :: Th21:
    (q => p) => (p => p) in IPC-Taut
proof
    (p => p) in IPC-Taut by Th17;
  hence thesis by Th18;
end;

theorem Th22:
  (q => r) => ((p => q) => (p => r)) in IPC-Taut
proof
A1:((p => (q => r)) => ((p => q) => (p => r))) =>
     ( (q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) in IPC-Taut
         by Def14;
     ((p => (q => r)) => ((p => q) => (p => r))) in IPC-Taut by Def14;
then A2: ( (q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) in IPC-Taut
      by A1,Def14;
      ( (q => r) => ((p => (q => r)) => ((p => q) => (p => r))))
      => (((q => r) => (p => (q => r))) =>
    ((q => r) => ((p => q) => (p => r)))) in IPC-Taut
      by Def14;
then A3: ((q => r) => (p => (q => r))) =>
     ((q => r) => ((p => q) => (p => r))) in IPC-Taut
       by A2,Def14;
      (q => r) => (p => (q => r)) in IPC-Taut by Def14;
  hence thesis by A3,Def14;
end;

theorem Th23:
  p => (q => r) in IPC-Taut implies q => (p => r) in IPC-Taut
proof
  assume A1: p => (q => r) in IPC-Taut;
    (p => (q => r)) => ((p => q) => (p => r)) in IPC-Taut by Def14;
then A2:  ((p => q) => (p => r)) in IPC-Taut by A1,Def14;
    ((p => q) => (p => r)) => ((q => (p => q)) => (q => (p => r))) in IPC-Taut
    by Th22;
then A3:((q => (p => q)) => (q => (p => r))) in IPC-Taut by A2,Def14;
    q => (p => q) in IPC-Taut by Def14;
  hence thesis by A3,Def14;
end;

theorem Th24: :: Hypothetical syllogism
  (p => q) => ((q => r) => (p => r)) in IPC-Taut
proof
    (q => r) => ((p => q) => (p => r)) in IPC-Taut by Th22;
  hence thesis by Th23;
end;

theorem Th25:
  p => q in IPC-Taut implies (q => r) => (p => r) in IPC-Taut
 proof assume
A1: p => q in IPC-Taut;
     (p => q) => ((q => r) => (p => r)) in IPC-Taut by Th24;
  hence (q => r) => (p => r) in IPC-Taut by A1,Def14;
 end;

theorem Th26:
  p => q in IPC-Taut & q => r in IPC-Taut implies p => r in IPC-Taut
 proof assume that
A1: p => q in IPC-Taut and
A2: q => r in IPC-Taut;
     (p => q) => ((q => r) => (p => r)) in IPC-Taut by Th24;
   then (q => r) => (p => r) in IPC-Taut by A1,Def14;
  hence p => r in IPC-Taut by A2,Def14;
 end;

Lm4: (((q => r) => (p => r)) => s) => ((p => q) => s) in IPC-Taut
 proof
    (p => q) => ((q => r) => (p => r)) in IPC-Taut by Th24;
  hence thesis by Th25;
 end;

theorem Th27:
 (p => (q => r)) => ((s => q) => (p => (s => r))) in IPC-Taut
  proof
A1:  ((((q => r) => (s => r)) => (p => (s => r))) =>
     ((s => q) => (p => (s => r)))) =>
      ((p => (q => r)) => ((s => q) => (p => (s => r)))) in IPC-Taut by Lm4;
      (((q => r) => (s => r)) => (p => (s => r))) =>
    ((s => q) => (p => (s => r))) in IPC-Taut by Lm4;
   hence thesis by A1,Def14;
  end;

theorem :: Th28:
    ((p => q) => r) => (q => r) in IPC-Taut
proof
    q => (p => q) in IPC-Taut &
  (q => (p => q)) => (((p => q) => r) => (q => r)) in IPC-Taut
    by Def14,Th24;
 hence thesis by Def14;
end;

theorem Th29: :: Contraposition
  (p => (q => r)) => (q => (p => r)) in IPC-Taut
proof
    (p => (q => r)) => ((p => q) => (p => r)) in IPC-Taut by Def14;
then A1:(p => q) => ((p => (q => r)) => (p => r)) in IPC-Taut by Th23;
    ((p => q) => ((p => (q => r)) => (p => r))) =>
    ((q => (p => q)) => (q => ((p => (q => r)) => (p => r)))) in IPC-Taut
      by Th22;
then A2:(q => (p => q)) => (q => ((p => (q => r)) => (p => r))) in IPC-Taut
    by A1,Def14;
    q => (p => q) in IPC-Taut by Def14;
  then (q => ((p => (q => r)) => (p => r))) in IPC-Taut by A2,Def14;
  hence thesis by Th23;
end;

theorem Th30:  :: A Hilbert axiom
  (p => (p => q)) => (p => q) in IPC-Taut
proof
A1:p => p in IPC-Taut by Th17;
    (p => (p => q)) => ((p => p) => (p => q)) in IPC-Taut by Def14;
  then (p => p) => ((p => (p => q)) => (p => q)) in IPC-Taut by Th23;
  hence thesis by A1,Def14;
end;

theorem :: Th31: :: Modus ponendo ponens
    q => ((q => p) => p) in IPC-Taut
proof
A1:(q => p) => (q => p) in IPC-Taut by Th17;
    ((q => p) => (q => p)) => (q => ((q => p) => p)) in IPC-Taut by Th29;
  hence thesis by A1,Def14;
end;

theorem Th32:
  s => (q => p) in IPC-Taut & q in IPC-Taut implies s => p in IPC-Taut
proof
  assume A1: s => (q => p) in IPC-Taut & q in IPC-Taut;
    (s => (q => p)) => (q => (s => p)) in IPC-Taut by Th29;
  then q => (s => p) in IPC-Taut by A1,Def14;
  hence thesis by A1,Def14;
end;

begin :: Formulas provable in IPC : conjunction

theorem Th33:
  p => (p '&' p) in IPC-Taut
proof
A1:p => (p => (p '&' p)) in IPC-Taut by Def14;
    (p => (p => (p '&' p))) => (p => (p '&' p)) in IPC-Taut by Th30;
  hence thesis by A1,Def14;
end;

theorem Th34:
  (p '&' q) in IPC-Taut iff p in IPC-Taut & q in IPC-Taut
proof
  hereby assume A1: p '&' q in IPC-Taut;
      (p '&' q) => p in IPC-Taut & (p '&' q) => q in IPC-Taut by Def14;
    hence p in IPC-Taut & q in IPC-Taut by A1,Def14;
  end;
  assume A2: p in IPC-Taut & q in IPC-Taut;
    p => (q => (p '&' q)) in IPC-Taut by Def14;
  then q => (p '&' q) in IPC-Taut by A2,Def14;
  hence thesis by A2,Def14;
end;

theorem :: Th35:
    (p '&' q) in IPC-Taut iff (q '&' p) in IPC-Taut
proof
  hereby assume p '&' q in IPC-Taut;
    then p in IPC-Taut & q in IPC-Taut by Th34;
    hence q '&' p in IPC-Taut by Th34;
  end;
  assume q '&' p in IPC-Taut;
  then q in IPC-Taut & p in IPC-Taut by Th34;
  hence p '&' q in IPC-Taut by Th34;
end;

theorem Th36:
  (( p '&' q ) => r ) => ( p => ( q => r )) in IPC-Taut
proof
       ( q => ( p '&' q )) => ((( p '&' q ) => r ) => ( q => r )) in IPC-Taut
     by Th24;
then A1: p => (( q => ( p '&' q )) => ((( p '&' q ) => r ) => ( q => r )))
    in IPC-Taut by Th18;
    set qp = ( q => ( p '&' q ));
    set pr = (( p '&' q ) => r) => ( q => r );
      ( p => ( qp => pr )) => ( ( p => qp ) => ( p => pr )) in IPC-Taut by
Def14
;
    then A2: ( ( p => qp ) => ( p => pr )) in IPC-Taut by A1,Def14;
      p => ( q => ( p '&' q )) in IPC-Taut by Def14;
then A3: p => ((( p '&' q ) => r ) => ( q => r )) in IPC-Taut by A2,Def14;
       (p => ((( p '&' q ) => r ) => ( q => r ))) =>
     ((( p '&' q ) => r ) => ( p => ( q => r ))) in IPC-Taut by Th29;
     hence thesis by A3,Def14;
end;

theorem Th37:
  ( p => ( q => r )) => (( p '&' q ) => r ) in IPC-Taut
proof
  A1: ( p '&' q ) => q in IPC-Taut by Def14;
       (( p '&' q ) => q) => (( q => r ) => (( p '&' q ) => r )) in IPC-Taut
     by Th24;
     then ( q => r ) => (( p '&' q ) => r ) in IPC-Taut by A1,Def14;
  then A2: p => (( q => r ) => (( p '&' q ) => r )) in IPC-Taut by Th18;
       p => (( q => r ) => (( p '&' q ) => r )) =>
     ((p => ( q => r )) => ( p => (( p '&' q ) => r ))) in IPC-Taut
     by Def14;
  then A3: (p => ( q => r )) => ( p => (( p '&' q ) => r )) in IPC-Taut
     by A2,Def14;
       ( p => (( p '&' q ) => r )) => ((p '&' q ) => ( p => r )) in IPC-Taut
     by Th29;
  then A4: (p => ( q => r )) => ((p '&' q ) => ( p => r )) in IPC-Taut by A3,
Th26;
  A5: ((p '&' q ) => ( p => r )) => ((( p '&' q ) => p ) => (( p '&' q )
     => r )) in IPC-Taut by Def14;
       ( p '&' q ) => p in IPC-Taut by Def14;
     then ((p '&' q ) => ( p => r )) => (( p '&' q ) => r ) in IPC-Taut by A5,
Th32;
     hence thesis by A4,Th26;
end;

theorem Th38:
  ( r => p ) => (( r => q ) => ( r => ( p '&' q ))) in IPC-Taut
proof
       p => ( q => ( p '&' q )) in IPC-Taut by Def14;
  then A1: r => ( p => ( q => ( p '&' q ))) in IPC-Taut by Th18;
       (r => ( p => ( q => ( p '&' q )))) =>
     (( r => p ) => ( r => ( q => ( p '&' q )))) in IPC-Taut by Def14;
  then A2: ( r => p ) => ( r => ( q => ( p '&' q ))) in IPC-Taut by A1,Def14;
       ( r => ( q => ( p '&' q ))) => (( r => q ) => ( r => ( p '&' q )))
     in IPC-Taut by Def14;
     hence thesis by A2,Th26;
end;

theorem Th39:
  ( (p => q) '&' p ) => q in IPC-Taut
proof
  set P = p => q;
A1:( P => P ) => (( P '&' p ) => q ) in IPC-Taut by Th37;
    P => P in IPC-Taut by Th17;
  hence thesis by A1,Def14;
end;

theorem :: Th40:
    (( (p => q) '&' p ) '&' s ) => q in IPC-Taut
proof
  set P = (p => q) '&' p;
A1:(P '&' s) => P in IPC-Taut by Def14;
    P => q in IPC-Taut by Th39;
  hence thesis by A1,Th26;
end;

theorem :: Th41:
    (q => s) => (( p '&' q ) => s) in IPC-Taut
proof
  set P = p '&' q;
A1:(P => q) => ((q => s) => (P => s)) in IPC-Taut by Th24;
    P => q in IPC-Taut by Def14;
  hence thesis by A1,Def14;
end;

theorem Th42:
  (q => s) => (( q '&' p ) => s) in IPC-Taut
proof
  set P = q '&' p;
A1:(P => q) => ((q => s) => (P => s)) in IPC-Taut by Th24;
    P => q in IPC-Taut by Def14;
  hence thesis by A1,Def14;
end;

theorem Th43:
  ( (p '&' s) => q ) => ((p '&' s) => (q '&' s)) in IPC-Taut
proof
  set P = p '&' s;
A1:P => s in IPC-Taut by Def14;
    ( P => q ) => (( P => s ) => ( P => ( q '&' s ))) in IPC-Taut by Th38;
  hence thesis by A1,Th32;
end;

theorem Th44:
  ( p => q ) => ((p '&' s) => (q '&' s)) in IPC-Taut
proof
A1:(p => q) => (( p '&' s ) => q) in IPC-Taut by Th42;
    ( (p '&' s) => q ) => ((p '&' s) => (q '&' s)) in IPC-Taut by Th43;
  hence thesis by A1,Th26;
end;

theorem Th45:
  (( p => q ) '&' ( p '&' s )) => ( q '&' s ) in IPC-Taut
proof
  set P = p => q, Q = p '&' s, S = q '&' s;
A1:( P => ( Q => S )) => (( P '&' Q ) => S ) in IPC-Taut by Th37;
  P => (Q => S) in IPC-Taut by Th44;
  hence thesis by A1,Def14;
end;

theorem Th46:
  ( p '&' q ) => ( q '&' p ) in IPC-Taut
proof
  set P = p '&' q;
A1:( P => q ) => (( P => p ) => ( P => ( q '&' p ))) in IPC-Taut by Th38;
    P => q in IPC-Taut by Def14;
then A2:( P => p ) => ( P => ( q '&' p )) in IPC-Taut by A1,Def14;
    P => p in IPC-Taut by Def14;
  hence thesis by A2,Def14;
end;

theorem Th47:
  ( p => q ) '&' ( p '&' s ) => ( s '&' q ) in IPC-Taut
proof
A1:( p => q ) '&' ( p '&' s ) => ( q '&' s ) in IPC-Taut by Th45;
    ( q '&' s ) => ( s '&' q ) in IPC-Taut by Th46;
  hence thesis by A1,Th26;
end;

theorem Th48:
  ( p => q ) => (( p '&' s ) => ( s '&' q )) in IPC-Taut
proof
  set P = p => q, Q = p '&' s, S = s '&' q;
A1:(( P '&' Q ) => S ) => ( P => ( Q => S )) in IPC-Taut by Th36;
    P '&' Q => S in IPC-Taut by Th47;
  hence thesis by A1,Def14;
end;

theorem Th49:
  ( p => q ) => (( s '&' p ) => ( s '&' q )) in IPC-Taut
proof
  set P = p => q, Q = p '&' s, S = s '&' q, T = s '&' p;
A1:(P => (Q => S)) => ((T => Q) => (P => (T => S))) in IPC-Taut by Th27;
    P => (Q => S) in IPC-Taut by Th48;
then A2:(T => Q) => (P => (T => S)) in IPC-Taut by A1,Def14;
    T => Q in IPC-Taut by Th46;
  hence thesis by A2,Def14;
end;

theorem :: Th50:
    ( p '&' (s '&' q) ) => ( p '&' (q '&' s) ) in IPC-Taut
proof
  set P = s '&' q, Q = q '&' s;
A1:( P => Q ) => (( p '&' P ) => ( p '&' Q )) in IPC-Taut by Th49;
    P => Q in IPC-Taut by Th46;
  hence thesis by A1,Def14;
end;

theorem :: Th51:
    ( ( p => q ) '&' (p => s) ) => ( p => (q '&' s) ) in IPC-Taut
proof
  set P = p => q, Q = p => s, S = p => (q '&' s);
A1:( P => ( Q => S )) => (( P '&' Q ) => S ) in IPC-Taut by Th37;
    P => (Q => S) in IPC-Taut by Th38;
  hence thesis by A1,Def14;
end;

Lm5:
  ( (p '&' q) '&' s ) => q in IPC-Taut
proof
A1:((p '&' q) '&' s) => (p '&' q) in IPC-Taut by Def14;
    (p '&' q) => q in IPC-Taut by Def14;
  hence thesis by A1,Th26;
end;

Lm6:
  ( (p '&' q) '&' s ) '&' ( (p '&' q) '&' s ) => ( (p '&' q) '&' s ) '&' q
     in IPC-Taut
proof
  set P = (p '&' q) '&' s;
A1:( P => q ) => (( P '&' P ) => ( P '&' q )) in IPC-Taut by Th49;
    P => q in IPC-Taut by Lm5;
  hence thesis by A1,Def14;
end;

Lm7:
  (p '&' q) '&' s => ((p '&' q) '&' s) '&' q in IPC-Taut
proof
A1:( (p '&' q) '&' s ) => ( (p '&' q) '&' s ) '&' ( (p '&' q) '&' s )
    in IPC-Taut by Th33;
    ( (p '&' q) '&' s ) '&' ( (p '&' q) '&' s ) => ( (p '&' q) '&' s ) '&' q
     in IPC-Taut by Lm6;
  hence thesis by A1,Th26;
end;

Lm8:
  (p '&' q) '&' s => (p '&' s) in IPC-Taut
proof
  set P = p '&' q;
A1:( P => p ) => ((P '&' s) => (p '&' s)) in IPC-Taut by Th44;
    P => p in IPC-Taut by Def14;
  hence thesis by A1,Def14;
end;

Lm9:
  (p '&' q) '&' s '&' q => (p '&' s) '&' q in IPC-Taut
proof
  set P = p '&' q '&' s, Q = p '&' s;
A1:( P => Q ) => ((P '&' q) => (Q '&' q)) in IPC-Taut by Th44;
    P => Q in IPC-Taut by Lm8;
  hence thesis by A1,Def14;
end;

Lm10:
  (p '&' q) '&' s => (p '&' s) '&' q in IPC-Taut
proof
A1:(p '&' q) '&' s => ((p '&' q) '&' s) '&' q in IPC-Taut by Lm7;
    (p '&' q) '&' s '&' q => (p '&' s) '&' q in IPC-Taut by Lm9;
  hence thesis by A1,Th26;
end;

Lm11:
  (p '&' s) '&' q => (s '&' p) '&' q in IPC-Taut
proof
  set P = p '&' s, Q = s '&' p;
A1:( P => Q ) => ((P '&' q) => (Q '&' q)) in IPC-Taut by Th44;
    P => Q in IPC-Taut by Th46;
  hence thesis by A1,Def14;
end;

Lm12:
  (p '&' q) '&' s => (s '&' p) '&' q in IPC-Taut
proof
A1:(p '&' q) '&' s => (p '&' s) '&' q in IPC-Taut by Lm10;
    (p '&' s) '&' q => (s '&' p) '&' q in IPC-Taut by Lm11;
  hence thesis by A1,Th26;
end;

Lm13:
  (p '&' q) '&' s => (s '&' q) '&' p in IPC-Taut
proof
A1:(p '&' q) '&' s => (s '&' p) '&' q in IPC-Taut by Lm12;
    (s '&' p) '&' q => (s '&' q) '&' p in IPC-Taut by Lm10;
  hence thesis by A1,Th26;
end;

Lm14:
  (p '&' q) '&' s => p '&' (s '&' q) in IPC-Taut
proof
A1:(p '&' q) '&' s => (s '&' q) '&' p in IPC-Taut by Lm13;
    (s '&' q) '&' p => p '&' (s '&' q) in IPC-Taut by Th46;
  hence thesis by A1,Th26;
end;

Lm15:
  p '&' (s '&' q) => p '&' (q '&' s) in IPC-Taut
proof
  set P = s '&' q, Q = q '&' s;
A1:( P => Q ) => (( p '&' P ) => ( p '&' Q )) in IPC-Taut by Th49;
    s '&' q => q '&' s in IPC-Taut by Th46;
  hence thesis by A1,Def14;
end;

theorem :: Th52:
    (p '&' q) '&' s => p '&' (q '&' s) in IPC-Taut
proof
A1:(p '&' q) '&' s => p '&' (s '&' q) in IPC-Taut by Lm14;
    p '&' (s '&' q) => p '&' (q '&' s) in IPC-Taut by Lm15;
  hence thesis by A1,Th26;
end;

Lm16:
  p '&' (q '&' s) => (s '&' q) '&' p in IPC-Taut
proof
A1:p '&' (q '&' s) => p '&' (s '&' q) in IPC-Taut by Lm15;
    p '&' (s '&' q) => (s '&' q) '&' p in IPC-Taut by Th46;
  hence thesis by A1,Th26;
end;

Lm17:
  (s '&' q) '&' p => (q '&' s) '&' p in IPC-Taut
proof
  set P = s '&' q, Q = q '&' s;
A1:( P => Q ) => ((P '&' p) => (Q '&' p)) in IPC-Taut by Th44;
    s '&' q => q '&' s in IPC-Taut by Th46;
  hence thesis by A1,Def14;
end;

Lm18:
  p '&' (q '&' s) => (q '&' s) '&' p in IPC-Taut
proof
A1:p '&' (q '&' s) => (s '&' q) '&' p in IPC-Taut by Lm16;
    (s '&' q) '&' p => (q '&' s) '&' p in IPC-Taut by Lm17;
  hence thesis by A1,Th26;
end;

Lm19:
  p '&' (q '&' s) => (p '&' s) '&' q in IPC-Taut
proof
A1:p '&' (q '&' s) => (q '&' s) '&' p in IPC-Taut by Lm18;
    (q '&' s) '&' p => (p '&' s) '&' q in IPC-Taut by Lm13;
  hence thesis by A1,Th26;
end;

Lm20:
  p '&' (q '&' s) => p '&' (s '&' q) in IPC-Taut
proof
  set P = q '&' s, Q = s '&' q;
A1:( P => Q ) => (( p '&' P ) => ( p '&' Q )) in IPC-Taut by Th49;
    q '&' s => s '&' q in IPC-Taut by Th46;
  hence thesis by A1,Def14;
end;

theorem :: Th53:
    p '&' (q '&' s) => (p '&' q) '&' s in IPC-Taut
proof
A1:p '&' (q '&' s) => p '&' (s '&' q) in IPC-Taut by Lm20;
    p '&' (s '&' q) => (p '&' q) '&' s in IPC-Taut by Lm19;
  hence thesis by A1,Th26;
end;

begin :: Formulas provable in IPC: disjunction

theorem Th54:
  (p 'or' p) => p in IPC-Taut
proof
A1:p => p in IPC-Taut by Th17;
    (p => p) => ((p => p) => ((p 'or' p) => p)) in IPC-Taut by Def14;
  then (p => p) => ((p 'or' p) => p) in IPC-Taut by A1,Def14;
  hence thesis by A1,Def14;
end;

theorem :: Th55:
    p in IPC-Taut or q in IPC-Taut implies (p 'or' q) in IPC-Taut
proof
  assume A1: p in IPC-Taut or q in IPC-Taut;
    now per cases by A1;
   case A2: p in IPC-Taut;
       p => (p 'or' q) in IPC-Taut by Def14;
     hence thesis by A2,Def14;
   case A3: q in IPC-Taut;
       q => (p 'or' q) in IPC-Taut by Def14;
     hence thesis by A3,Def14;
  end;
hence thesis;
end;

theorem Th56:
  (p 'or' q) => (q 'or' p) in IPC-Taut
proof
A1: (p => (q 'or' p)) => ((q => (q 'or' p)) => ((p 'or' q) => (q 'or' p)))
                                in IPC-Taut by Def14;
A2: p => (q 'or' p) in IPC-Taut by Def14;
A3: q => (q 'or' p) in IPC-Taut by Def14;
  ((q => (q 'or' p)) => ((p 'or' q) => (q 'or' p)))
                                in IPC-Taut by A1,A2,Def14;
hence thesis by A3,Def14;
end;

theorem :: Th57:
    (p 'or' q) in IPC-Taut iff (q 'or' p) in IPC-Taut
proof
  hereby assume A1: p 'or' q in IPC-Taut;
      (p 'or' q) => (q 'or' p) in IPC-Taut by Th56;
    hence q 'or' p in IPC-Taut by A1,Def14;
  end;
  assume A2: q 'or' p in IPC-Taut;
      (q 'or' p) => (p 'or' q) in IPC-Taut by Th56;
    hence p 'or' q in IPC-Taut by A2,Def14;
end;

theorem Th58:
  (p => q) => (p => (q 'or' s)) in IPC-Taut
proof
  A1: q => (q 'or' s) in IPC-Taut by Def14;
    (q => (q 'or' s)) => ((p => q) => (p => (q 'or' s))) in IPC-Taut by Th22;
  hence thesis by A1,Def14;
end;

theorem Th59:
  (p => q) => (p => (s 'or' q)) in IPC-Taut
proof
  A1: q => (s 'or' q) in IPC-Taut by Def14;
    (q => (s 'or' q)) => ((p => q) => (p => (s 'or' q))) in IPC-Taut by Th22;
  hence thesis by A1,Def14;
end;

theorem Th60:
  ( p => q ) => ((p 'or' s) => (q 'or' s)) in IPC-Taut
proof
  set P = p 'or' s, Q = q 'or' s;
    (p => Q) => ((s => Q) => (P => Q)) in IPC-Taut by Def14;
  then A1: (s => Q) => ((p => Q) => (P => Q)) in IPC-Taut by Th23;
         s => Q in IPC-Taut by Def14;
  then A2: (p => Q) => (P => Q) in IPC-Taut by A1,Def14;
        (p => q) => (p => Q) in IPC-Taut by Th58;
  hence thesis by A2,Th26;
end;


theorem Th61:
  p => q in IPC-Taut implies (p 'or' s) => (q 'or' s) in IPC-Taut
proof
  assume A1: p => q in IPC-Taut;
    ( p => q ) => ((p 'or' s) => (q 'or' s)) in IPC-Taut by Th60;
  hence thesis by A1,Def14;
end;

theorem Th62:
  ( p => q ) => (( s 'or' p ) => ( s 'or' q )) in IPC-Taut
proof
  set P = s 'or' p, Q = s 'or' q;
  A1: (s => Q) => ((p => Q) => (P => Q)) in IPC-Taut by Def14;
         s => Q in IPC-Taut by Def14;
  then A2: (p => Q) => (P => Q) in IPC-Taut by A1,Def14;
        (p => q) => (p => Q) in IPC-Taut by Th59;
  hence thesis by A2,Th26;
end;

theorem Th63:
  p => q in IPC-Taut implies ( s 'or' p ) => ( s 'or' q ) in IPC-Taut
proof
  assume A1: p => q in IPC-Taut;
    ( p => q ) => (( s 'or' p ) => ( s 'or' q )) in IPC-Taut by Th62;
  hence thesis by A1,Def14;
end;

theorem Th64:
  ( p 'or' (q 'or' s) ) => ( q 'or' (p 'or' s) ) in IPC-Taut
proof
  set P = p 'or' s, Q = q 'or' s;
    s => P in IPC-Taut by Def14;
  then (q 'or' s) => (q 'or' P) in IPC-Taut by Th63;
  :: Q => (q 'or' P)  in IPC-Taut; then
  then A1: (p 'or' Q) => (p 'or' (q 'or' P)) in IPC-Taut by Th63;
    (p 'or' (q 'or' P)) => ((q 'or' P) 'or' p) in IPC-Taut by Th56;
  then A2: (p 'or' Q) => ((q 'or' P) 'or' p) in IPC-Taut by A1,Th26;
  A3: p => P in IPC-Taut by Def14;
    P => (q 'or' P) in IPC-Taut by Def14;
  then p => (q 'or' P) in IPC-Taut by A3,Th26;
  then A4: ((q 'or' P) 'or' p) => ((q 'or' P) 'or' (q 'or' P))
                     in IPC-Taut by Th63;
    ((q 'or' P) 'or' (q 'or' P)) => (q 'or' P) in IPC-Taut by Th54;
  then ((q 'or' P) 'or' p) => (q 'or' P) in IPC-Taut by A4,Th26;
  hence thesis by A2,Th26;
end;

theorem :: Th65:
    ( p 'or' (q 'or' s) ) => ( (p 'or' q) 'or' s ) in IPC-Taut
proof
     (q 'or' s) => (s 'or' q) in IPC-Taut by Th56;
  then A1: (p 'or' (q 'or' s)) => (p 'or' (s 'or' q)) in IPC-Taut by Th63;
     (p 'or' (s 'or' q)) => (s 'or' (p 'or' q)) in IPC-Taut by Th64;
  then A2: (p 'or' (q 'or' s)) => (s 'or' (p 'or' q))
                             in IPC-Taut by A1,Th26;
    (s 'or' (p 'or' q)) => ((p 'or' q) 'or' s) in IPC-Taut by Th56;
  hence thesis by A2,Th26;
end;

theorem :: Th66:
    ( (p 'or' q) 'or' s ) => ( p 'or' (q 'or' s) ) in IPC-Taut
proof
    (p 'or' q) => (q 'or' p) in IPC-Taut by Th56;
  then A1: ((p 'or' q) 'or' s) => ((q 'or' p) 'or' s) in IPC-Taut by Th61;
    ((q 'or' p) 'or' s) => (s 'or' (q 'or' p)) in IPC-Taut by Th56;
  then A2: ((p 'or' q) 'or' s) => (s 'or' (q 'or' p)) in IPC-Taut by A1,Th26;
    (q 'or' p) => (p 'or' q) in IPC-Taut by Th56;
  then (s 'or' (q 'or' p)) => (s 'or' (p 'or' q)) in IPC-Taut by Th63;
  then A3: ((p 'or' q) 'or' s) => (s 'or' (p 'or' q)) in IPC-Taut by A2,Th26;
    (s 'or' (p 'or' q)) => (p 'or' (s 'or' q)) in IPC-Taut by Th64;
  then A4: ((p 'or' q) 'or' s) => (p 'or' (s 'or' q)) in IPC-Taut by A3,Th26;
    (s 'or' q) => (q 'or' s) in IPC-Taut by Th56;
  then (p 'or' (s 'or' q)) => (p 'or' (q 'or' s)) in IPC-Taut by Th63;
   hence thesis by A4,Th26;
end;

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 :Def19:
    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;

theorem Th67:
T is CPC_theory implies T is IPC_theory
proof
assume A1: T is CPC_theory;
let p, q, r be Element of MC-wff;
thus thesis by A1,Def19;
end;

definition let X;
  func CnCPC X -> Subset of MC-wff means :Def20:
  r in it iff for T st T is CPC_theory & X c= T holds r in T;
 existence
  proof
    defpred P[set] means
    for T st T is CPC_theory & X c= T holds $1 in T;
   consider Y being set such that
A1: for a being set holds a in Y iff
     a in MC-wff & P[a] from Separation;
      Y c= MC-wff
    proof
     let a be set; assume a in Y;
     hence a in MC-wff by A1;
    end;
   then reconsider Z = Y as Subset of MC-wff;
   take Z;
   thus r in Z iff for T st T is CPC_theory & X c= T holds r in T by A1;
  end;
 uniqueness
  proof
   let Y,Z be Subset of MC-wff such that
    A2: r in Y iff for T st T is CPC_theory & X c= T holds r in T and
    A3: r in Z iff for T st T is CPC_theory & X c= T holds r in T;
     for a being set holds a in Y iff a in Z
    proof
     let a be set;
     hereby assume A4: a in Y;
       then reconsider t=a as Element of MC-wff;
         for T st T is CPC_theory & X c= T holds t in T by A2,A4;
       hence a in Z by A3;
      end;
       assume A5: a in Z;
       then reconsider t=a as Element of MC-wff;
         for T st T is CPC_theory & X c= T holds t in T by A3,A5;
       hence a in Y by A2;
    end;
    hence thesis by TARSKI:2;
  end;
end;

definition
  func CPC-Taut -> Subset of MC-wff equals :Def21:
    CnCPC({}(MC-wff));
  correctness;
end;

theorem Th68:
CnIPC (X) c= CnCPC (X)
proof
  let a be set;
  assume A1: a in CnIPC (X);
  then reconsider r = a as Element of MC-wff;
    for T st T is CPC_theory & X c= T holds r in T
      proof
        let T such that A2: T is CPC_theory and A3: X c= T;
          T is IPC_theory by A2,Th67;
        hence r in T by A1,A3,Def15;
      end;
  hence thesis by Def20;
end;

theorem Th69:
  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
thus p => (q => p) in CnCPC (X)
   proof
   A1: p => (q => p) in CnIPC (X) by Th1;
     CnIPC(X) c= CnCPC(X) by Th68;
   hence thesis by A1;
   end;

thus (p => (q => r)) => ((p => q) => (p => r)) in CnCPC (X)
   proof
   A2: (p => (q => r)) => ((p => q) => (p => r)) in CnIPC (X) by Th2;
     CnIPC(X) c= CnCPC(X) by Th68;
   hence thesis by A2;
   end;

thus p '&' q => p in CnCPC (X)
   proof
   A3: p '&' q => p in CnIPC (X) by Th3;
     CnIPC(X) c= CnCPC(X) by Th68;
   hence thesis by A3;
   end;

thus p '&' q => q in CnCPC (X)
   proof
   A4: p '&' q => q in CnIPC (X) by Th4;
     CnIPC(X) c= CnCPC(X) by Th68;
   hence thesis by A4;
   end;

thus p => (q => (p '&' q)) in CnCPC (X)
   proof
   A5: p => (q => (p '&' q)) in CnIPC (X) by Th5;
     CnIPC(X) c= CnCPC(X) by Th68;
   hence thesis by A5;
   end;

thus p => (p 'or' q) in CnCPC (X)
   proof
   A6: p => (p 'or' q) in CnIPC (X) by Th6;
     CnIPC(X) c= CnCPC(X) by Th68;
   hence thesis by A6;
   end;

thus q => (p 'or' q) in CnCPC (X)
   proof
   A7: q => (p 'or' q) in CnIPC (X) by Th7;
     CnIPC(X) c= CnCPC(X) by Th68;
   hence thesis by A7;
   end;

thus (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC (X)
   proof
   A8: (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC (X) by Th8;
     CnIPC(X) c= CnCPC(X) by Th68;
   hence thesis by A8;
   end;

thus FALSUM => p in CnCPC (X)
   proof
   A9: FALSUM => p in CnIPC (X) by Th9;
     CnIPC(X) c= CnCPC(X) by Th68;
   hence thesis by A9;
   end;

thus p 'or' (p => FALSUM) in CnCPC (X)
    proof
        T is CPC_theory & X c= T implies
                       p 'or' (p => FALSUM) in T by Def19;
      hence thesis by Def20;
    end;
end;

theorem Th70:
p in CnCPC(X) & p => q in CnCPC(X) implies q in CnCPC(X)
proof
  assume A1: p in CnCPC(X) & p => q in CnCPC(X);
    T is CPC_theory & X c= T implies q in T
    proof
      assume A2: T is CPC_theory & X c= T;
      then p in T & p => q in T by A1,Def20;
      hence thesis by A2,Def19;
    end;
  hence thesis by Def20;
end;


theorem Th71: T is CPC_theory & X c= T implies CnCPC(X) c= T
 proof
  assume that A1:T is CPC_theory and A2: X c= T;
  let a be set;
  thus thesis by A1,A2,Def20;
 end;

theorem Th72:
  X c= CnCPC(X)
 proof
  let a be set;
  assume A1: a in X;
  then reconsider t = a as Element of MC-wff;
    for T st T is CPC_theory & X c= T holds t in T by A1;
  hence a in CnCPC(X) by Def20;
 end;

theorem Th73:
  X c= Y implies CnCPC(X) c= CnCPC(Y)
 proof
  assume A1: X c= Y;
  thus CnCPC(X) c= CnCPC(Y)
   proof
    let a be set; assume A2: a in CnCPC(X);
    then reconsider t = a as Element of MC-wff;
      for T st T is CPC_theory & Y c= T holds t in T
     proof
      let T such that A3: T is CPC_theory and A4: Y c= T;
        X c= T by A1,A4,XBOOLE_1:1;
      hence t in T by A2,A3,Def20;
     end;
    hence thesis by Def20;
   end;
 end;

Lm21: CnCPC(CnCPC(X)) c= CnCPC(X)
 proof
  let a be set; assume A1: a in CnCPC(CnCPC(X));
  then reconsider t = a as Element of MC-wff;
    for T st T is CPC_theory & X c= T holds t in T
   proof
    let T; assume that A2: T is CPC_theory and A3: X c= T;
      CnCPC(X) c= T by A2,A3,Th71;
    hence t in T by A1,A2,Def20;
   end;
  hence thesis by Def20;
 end;

theorem :: Th6C:
    CnCPC(CnCPC(X)) = CnCPC(X)
 proof
    CnCPC(CnCPC(X)) c= CnCPC(X) & CnCPC(X) c= CnCPC(CnCPC(X)) by Lm21,Th72;
  hence thesis by XBOOLE_0:def 10;
 end;

Lm22:
CnCPC(X) is CPC_theory
 proof
  let p, q, r;
  thus p => (q => p) in CnCPC(X) by Th69;
  thus (p => (q => r)) => ((p => q) => (p => r)) in CnCPC(X) by Th69;
  thus (p '&' q) => p in CnCPC(X) by Th69;
  thus (p '&' q) => q in CnCPC(X) by Th69;
  thus p => (q => (p '&' q)) in CnCPC(X) by Th69;
  thus p => (p 'or' q) in CnCPC(X) by Th69;
  thus q => (p 'or' q) in CnCPC(X) by Th69;
  thus (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC(X) by Th69;
  thus FALSUM => p in CnCPC(X) by Th69;
  thus p 'or' (p => FALSUM) in CnCPC (X) by Th69;
  thus (p in CnCPC(X) & p => q in CnCPC(X) implies q in CnCPC(X)) by Th70;
 end;

definition let X be Subset of MC-wff;
  cluster CnCPC(X) -> CPC_theory;
  coherence by Lm22;
end;

theorem Th75:
  T is CPC_theory iff CnCPC(T) = T
 proof
   hereby assume A1: T is CPC_theory;
    A2: T c= CnCPC(T) by Th72;
      CnCPC(T) c= T
     proof
      let a be set; assume a in CnCPC(T);
      hence a in T by A1,Def20;
     end;
    hence CnCPC(T) = T by A2,XBOOLE_0:def 10;
   end;
  thus CnCPC(T) = T implies T is CPC_theory;
 end;

theorem :: Th8C:
    T is CPC_theory implies CPC-Taut c= T
 proof
  assume A1: T is CPC_theory;
    {}(MC-wff) c= T by XBOOLE_1:2;
  then CPC-Taut c= CnCPC(T) by Def21,Th73;
  hence thesis by A1,Th75;
 end;

definition
  cluster CPC-Taut -> CPC_theory;
  coherence by Def21;
end;

theorem :: CPCincIPC:
  IPC-Taut c= CPC-Taut by Def16,Def21,Th68;

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 :Def22:
    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;

theorem Th78:
T is S4_theory implies T is CPC_theory
proof
 assume A1: T is S4_theory;
 let p, q, r be Element of MC-wff;
 thus thesis by A1,Def22;
end;

theorem :: S4TincIPCT:
  T is S4_theory implies T is IPC_theory
proof
assume A1: T is S4_theory;
let p, q, r be Element of MC-wff;
thus thesis by A1,Def22;
end;

definition let X;
  func CnS4 X -> Subset of MC-wff means :Def23:
  r in it iff for T st T is S4_theory & X c= T holds r in T;
 existence
  proof
    defpred P[set] means
    for T st T is S4_theory & X c= T holds $1 in T;
   consider Y being set such that
A1: for a being set holds a in Y iff
     a in MC-wff & P[a] from Separation;
      Y c= MC-wff
    proof
     let a be set; assume a in Y;
     hence a in MC-wff by A1;
    end;
   then reconsider Z = Y as Subset of MC-wff;
   take Z;
   thus r in Z iff for T st T is S4_theory & X c= T holds r in T by A1;
  end;
 uniqueness
  proof
   let Y,Z be Subset of MC-wff such that
    A2: r in Y iff for T st T is S4_theory & X c= T holds r in T and
    A3: r in Z iff for T st T is S4_theory & X c= T holds r in T;
     for a being set holds a in Y iff a in Z
    proof
     let a be set;
     hereby assume A4: a in Y;
       then reconsider t=a as Element of MC-wff;
         for T st T is S4_theory & X c= T holds t in T by A2,A4;
       hence a in Z by A3;
      end;
       assume A5: a in Z;
       then reconsider t=a as Element of MC-wff;
         for T st T is S4_theory & X c= T holds t in T by A3,A5;
       hence a in Y by A2;
    end;
    hence thesis by TARSKI:2;
  end;
end;

definition
  func S4-Taut -> Subset of MC-wff equals :Def24:
    CnS4({}(MC-wff));
  correctness;
end;

theorem Th80:
CnCPC (X) c= CnS4 (X)
proof
  let a be set;
  assume A1: a in CnCPC (X);
  then reconsider r = a as Element of MC-wff;
    for T st T is S4_theory & X c= T holds r in T
      proof
        let T such that A2: T is S4_theory and A3: X c= T;
          T is CPC_theory by A2,Th78;
        hence thesis by A1,A3,Def20;
      end;
  hence thesis by Def23;
end;

theorem Th81:
CnIPC (X) c= CnS4 (X)
proof
A1: CnIPC (X) c= CnCPC (X) by Th68;
  CnCPC (X) c= CnS4 (X) by Th80;
hence thesis by A1,XBOOLE_1:1;
end;

theorem Th82:
  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
thus p => (q => p) in CnS4 (X)
   proof
   A1: p => (q => p) in CnIPC (X) by Th1;
     CnIPC (X) c= CnS4 (X) by Th81;
   hence thesis by A1;
   end;

thus (p => (q => r)) => ((p => q) => (p => r)) in CnS4 (X)
   proof
   A2: (p => (q => r)) => ((p => q) => (p => r)) in CnIPC (X) by Th2;
     CnIPC (X) c= CnS4 (X) by Th81;
   hence thesis by A2;
   end;

thus p '&' q => p in CnS4 (X)
   proof
   A3: p '&' q => p in CnIPC (X) by Th3;
     CnIPC (X) c= CnS4 (X) by Th81;
   hence thesis by A3;
   end;

thus p '&' q => q in CnS4 (X)
   proof
   A4: p '&' q => q in CnIPC (X) by Th4;
     CnIPC (X) c= CnS4 (X) by Th81;
   hence thesis by A4;
   end;

thus p => (q => (p '&' q)) in CnS4 (X)
   proof
   A5: p => (q => (p '&' q)) in CnIPC (X) by Th5;
     CnIPC (X) c= CnS4 (X) by Th81;
   hence thesis by A5;
   end;

thus p => (p 'or' q) in CnS4 (X)
   proof
   A6: p => (p 'or' q) in CnIPC (X) by Th6;
     CnIPC (X) c= CnS4 (X) by Th81;
   hence thesis by A6;
   end;

thus q => (p 'or' q) in CnS4 (X)
   proof
   A7: q => (p 'or' q) in CnIPC (X) by Th7;
     CnIPC (X) c= CnS4 (X) by Th81;
   hence thesis by A7;
   end;

thus (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 (X)
   proof
   A8: (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC (X) by Th8;
     CnIPC (X) c= CnS4 (X) by Th81;
   hence thesis by A8;
   end;

thus FALSUM => p in CnS4 (X)
   proof
   A9: FALSUM => p in CnIPC (X) by Th9;
     CnIPC (X) c= CnS4 (X) by Th81;
   hence thesis by A9;
   end;

thus p 'or' (p => FALSUM) in CnS4 (X)
    proof
        T is S4_theory & X c= T implies
                       p 'or' (p => FALSUM) in T by Def22;
      hence thesis by Def23;
    end;
end;

theorem Th83:
p in CnS4 (X) & p => q in CnS4 (X) implies q in CnS4 (X)
proof
  assume A1: p in CnS4 (X) & p => q in CnS4 (X);
    T is S4_theory & X c= T implies q in T
    proof
      assume A2: T is S4_theory & X c= T;
      then p in T & p => q in T by A1,Def23;
      hence thesis by A2,Def22;
    end;
  hence thesis by Def23;
end;

theorem Th84:
(Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4 (X)
 proof
    T is S4_theory & X c= T
         implies (Nes (p => q)) => ((Nes p) => (Nes q)) in T by Def22;
  hence thesis by Def23;
 end;

theorem Th85:
(Nes p) => p in CnS4 (X)
 proof
    T is S4_theory & X c= T implies (Nes p) => p in T by Def22;
  hence thesis by Def23;
 end;

theorem Th86:
(Nes p) => Nes (Nes p) in CnS4 (X)
 proof
    T is S4_theory & X c= T implies (Nes p) => Nes (Nes p) in T by Def22;
  hence thesis by Def23;
 end;

theorem Th87:
p in CnS4 (X) implies Nes p in CnS4 (X)
proof
  assume A1: p in CnS4 (X);
    T is S4_theory & X c= T implies Nes p in T
    proof
      assume A2: T is S4_theory & X c= T;
      then p in T by A1,Def23;
      hence thesis by A2,Def22;
    end;
  hence thesis by Def23;
end;

theorem Th88: T is S4_theory & X c= T implies CnS4(X) c= T
 proof
  assume that A1:T is S4_theory and A2: X c= T;
  let a be set;
  thus thesis by A1,A2,Def23;
 end;

theorem Th89:
  X c= CnS4(X)
 proof
  let a be set;
  assume A1: a in X;
  then reconsider t = a as Element of MC-wff;
    for T st T is S4_theory & X c= T holds t in T by A1;
  hence a in CnS4(X) by Def23;
 end;

theorem Th90:
  X c= Y implies CnS4(X) c= CnS4(Y)
 proof
  assume A1: X c= Y;
  thus CnS4(X) c= CnS4(Y)
   proof
    let a be set; assume A2: a in CnS4(X);
    then reconsider t = a as Element of MC-wff;
      for T st T is S4_theory & Y c= T holds t in T
     proof
      let T such that A3: T is S4_theory and A4: Y c= T;
        X c= T by A1,A4,XBOOLE_1:1;
      hence t in T by A2,A3,Def23;
     end;
    hence thesis by Def23;
   end;
 end;

Lm23: CnS4(CnS4(X)) c= CnS4(X)
 proof
  let a be set; assume A1: a in CnS4(CnS4(X));
  then reconsider t = a as Element of MC-wff;
    for T st T is S4_theory & X c= T holds t in T
   proof
    let T; assume that A2: T is S4_theory and A3: X c= T;
      CnS4(X) c= T by A2,A3,Th88;
    hence t in T by A1,A2,Def23;
   end;
  hence thesis by Def23;
 end;

theorem :: Th10M:
    CnS4(CnS4(X)) = CnS4(X)
 proof
    CnS4(CnS4(X)) c= CnS4(X) & CnS4(X) c= CnS4(CnS4(X)) by Lm23,Th89;
  hence thesis by XBOOLE_0:def 10;
 end;

Lm24:
CnS4(X) is S4_theory
 proof
  let p, q, r;
  thus p => (q => p) in CnS4(X) by Th82;
  thus (p => (q => r)) => ((p => q) => (p => r)) in CnS4(X) by Th82;
  thus (p '&' q) => p in CnS4(X) by Th82;
  thus (p '&' q) => q in CnS4(X) by Th82;
  thus p => (q => (p '&' q)) in CnS4(X) by Th82;
  thus p => (p 'or' q) in CnS4(X) by Th82;
  thus q => (p 'or' q) in CnS4(X) by Th82;
  thus (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4(X) by Th82;
  thus FALSUM => p in CnS4(X) by Th82;
  thus p 'or' (p => FALSUM) in CnS4 (X) by Th82;
  thus (Nes (p => q)) => ((Nes p) => (Nes q)) in CnS4(X) by Th84;
  thus (Nes p) => p in CnS4(X) by Th85;
  thus (Nes p) => Nes (Nes p) in CnS4(X) by Th86;
  thus p in CnS4(X) & p => q in CnS4(X) implies q in CnS4(X) by Th83;
  thus (p in CnS4(X) implies Nes p in CnS4(X)) by Th87;
 end;

definition let X be Subset of MC-wff;
  cluster CnS4(X) -> S4_theory;
  coherence by Lm24;
end;

theorem Th92:
  T is S4_theory iff CnS4(T) = T
 proof
   hereby assume A1: T is S4_theory;
    A2: T c= CnS4(T) by Th89;
      CnS4(T) c= T
     proof
      let a be set; assume a in CnS4(T);
      hence a in T by A1,Def23;
     end;
    hence CnS4(T) = T by A2,XBOOLE_0:def 10;
   end;
  thus CnS4(T) = T implies T is S4_theory;
 end;

theorem :: Th12M:
    T is S4_theory implies S4-Taut c= T
 proof
  assume A1: T is S4_theory;
    {}(MC-wff) c= T by XBOOLE_1:2;
  then S4-Taut c= CnS4(T) by Def24,Th90;
  hence thesis by A1,Th92;
 end;

definition
  cluster S4-Taut -> S4_theory;
  coherence by Def24;
end;

theorem :: S4incCPC:
  CPC-Taut c= S4-Taut by Def21,Def24,Th80;

theorem :: S4incIPC:
  IPC-Taut c= S4-Taut by Def16,Def24,Th81;

Back to top