:: Intuitionistic Propositional Calculus in the Extended Framework with Modal
:: Operator, Part I
::  by Takao Inou\'e
::
:: Received April 3, 2003
:: Copyright (c) 2003-2012 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, NUMBERS, ORDINAL1, NAT_1, FUNCT_1,
      FINSEQ_1;
 constructors NAT_1, FINSEQ_1;
 registrations SUBSET_1, ORDINAL1, FUNCT_1, FINSEQ_1;
 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 Element of 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;

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

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

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

registration
  cluster MC-wff -> functional;
  coherence
  proof
    MC-wff c= NAT* by Def7;
    hence thesis;
  end;
end;

registration
  cluster -> FinSequence-like for Element of MC-wff;
  coherence
  proof
    let p be Element of MC-wff;
    MC-wff c= NAT* by Def7;
    hence thesis;
  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 XBOOLE_0:
    sch 1;
    Y c= MC-wff
    proof
      let a be set;
      assume a in Y;
      hence thesis by A1;
    end;
    then reconsider Z = Y as Subset of MC-wff;
    take Z;
    thus thesis 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 thesis by A2;
    end;
    hence thesis by TARSKI:1;
  end;
end;

definition
  func IPC-Taut -> Subset of MC-wff equals
  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
  (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 that
A1: p in CnIPC(X) and
A2: p => q in CnIPC(X);
  T is IPC_theory & X c= T implies q in T
  proof
    assume that
A3: T is IPC_theory and
A4: X c= T;
A5: p => q in T by A2,A3,A4,Def15;
    p in T by A1,A3,A4,Def15;
    hence thesis by A3,A5,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 thesis 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 thesis 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 thesis by A1,A2,Def15;
  end;
  hence thesis by Def15;
end;

theorem
  CnIPC(CnIPC(X)) = CnIPC(X)
proof
A1: CnIPC(X) c= CnIPC(CnIPC(X)) by Th12;
  CnIPC(CnIPC(X)) c= CnIPC(X) by Lm2;
  hence thesis by A1,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 thesis by Th10;
end;

registration
  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: CnIPC(T) c= T
    proof
      let a be set;
      assume a in CnIPC(T);
      hence thesis by A1,Def15;
    end;
    T c= CnIPC(T) by Th12;
    hence CnIPC(T) = T by A2,XBOOLE_0:def 10;
  end;
  thus thesis;
end;

theorem
  T is IPC_theory implies IPC-Taut c= T
proof
  assume
A1: T is IPC_theory;
  IPC-Taut c= CnIPC(T) by Th13,XBOOLE_1:2;
  hence thesis by A1,Th15;
end;

registration
  cluster IPC-Taut -> IPC_theory;
  coherence;
end;

begin  :: Formulas provable in IPC : implication

theorem Th17:
  p => p in IPC-Taut
proof
A1: p => (p => p) in IPC-Taut by Def14;
A2: p => ((p => p) => p) in IPC-Taut by Def14;
  (p => ((p => p) => p)) => ((p => (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
  IVERUM in IPC-Taut by Def14;

theorem
  (p => q) => (p => p) in IPC-Taut by Th17,Th18;

theorem
  (q => p) => (p => p) in IPC-Taut by Th17,Th18;

theorem Th22:
  (q => r) => ((p => q) => (p => r)) in IPC-Taut
proof
A1: ((p => (q => r)) => ((p => q) => (p => r))) in IPC-Taut by Def14;
A2: ( (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;
  ((p => (q => r)) => ((p => q) => (p => r))) => ( (q => r) => ((p => (q
  => r)) => ((p => q) => (p => r)))) in IPC-Taut by Def14;
  then ( (q => r) => ((p => (q => r)) => ((p => q) => (p => r)))) in IPC-Taut
  by A1,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;
A2: ((p => q) => (p => r)) => ((q => (p => q)) => (q => (p => r))) in
  IPC-Taut by Th22;
  (p => (q => r)) => ((p => q) => (p => r)) in IPC-Taut by Def14;
  then ((p => q) => (p => r)) in IPC-Taut by A1,Def14;
  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 thesis 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 thesis 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))) in IPC-Taut by Lm4;
  ((((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;
  hence thesis by A1,Def14;
end;

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

theorem Th29: :: Contraposition
  (p => (q => r)) => (q => (p => r)) in IPC-Taut
proof
A1: q => (p => q) in IPC-Taut by Def14;
  (p => (q => r)) => ((p => q) => (p => r)) in IPC-Taut by Def14;
  then
A2: (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 (q => (p => q)) => (q => ((p => (q => r)) => (p => r))) in IPC-Taut by
A2,Def14;
  then (q => ((p => (q => r)) => (p => r))) in IPC-Taut by A1,Def14;
  hence thesis by Th23;
end;

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

theorem :: Modus ponendo ponens
  q => ((q => p) => p) in IPC-Taut
proof
A1: ((q => p) => (q => p)) => (q => ((q => p) => p)) in IPC-Taut by Th29;
  (q => p) => (q => p) in IPC-Taut by Th17;
  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 that
A1: s => (q => p) in IPC-Taut and
A2: 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 A2,Def14;
end;

begin :: Formulas provable in IPC : conjunction

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

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

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

theorem Th36:
  (( p '&' q ) => r ) => ( p => ( q => r )) in IPC-Taut
proof
  set qp = ( q => ( p '&' q ));
  set pr = (( p '&' q ) => r) => ( q => r );
A1: ( p => ( qp => pr )) => ( ( p => qp ) => ( p => pr )) in IPC-Taut by Def14;
A2: p => ( q => ( p '&' q )) in IPC-Taut by Def14;
  p => (( q => ( p '&' q )) => ((( p '&' q ) => r ) => ( q => r ))) in
  IPC-Taut by Th18,Th24;
  then ( ( p => qp ) => ( p => pr )) in IPC-Taut by A1,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) => (( q => r ) => (( p '&' q ) => r )) in IPC-Taut by
Th24;
  ( p '&' q ) => q in IPC-Taut by Def14;
  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;
A3: ( p => (( p '&' q ) => r )) => ((p '&' q ) => ( p => r )) in IPC-Taut by
Th29;
  p => (( q => r ) => (( p '&' q ) => r )) => ((p => ( q => r )) => ( p =>
  (( p '&' q ) => r ))) in IPC-Taut by Def14;
  then (p => ( q => r )) => ( p => (( p '&' q ) => r )) in IPC-Taut by A2,Def14
;
  then
A4: (p => ( q => r )) => ((p '&' q ) => ( p => r )) in IPC-Taut by A3,Th26;
A5: ( p '&' q ) => p in IPC-Taut by Def14;
  ((p '&' q ) => ( p => r )) => ((( p '&' q ) => p ) => (( p '&' q ) => r
  )) 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
A1: ( r => ( q => ( p '&' q ))) => (( r => q ) => ( r => ( p '&' q ))) in
  IPC-Taut by Def14;
  p => ( q => ( p '&' q )) in IPC-Taut by Def14;
  then
A2: 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 ( r => p ) => ( r => ( q => ( p '&' q ))) in IPC-Taut by A2,Def14;
  hence thesis by A1,Th26;
end;

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

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

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

theorem Th42:
  (q => s) => (( q '&' p ) => s) in IPC-Taut
proof
  set P = q '&' p;
A1: P => q in IPC-Taut by Def14;
  (P => q) => ((q => s) => (P => s)) in IPC-Taut by Th24;
  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 => q ) => (( P => s ) => ( P => ( q '&' s ))) in IPC-Taut by Th38;
  P => s in IPC-Taut by Def14;
  hence thesis by A1,Th32;
end;

theorem Th44:
  ( p => q ) => ((p '&' s) => (q '&' s)) in IPC-Taut
proof
A1: ( (p '&' s) => q ) => ((p '&' s) => (q '&' s)) in IPC-Taut by Th43;
  (p => q) => (( p '&' s ) => q) in IPC-Taut by Th42;
  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) in IPC-Taut by Th44;
  ( P => ( Q => S )) => (( P '&' Q ) => S ) in IPC-Taut by Th37;
  hence thesis by A1,Def14;
end;

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

theorem Th47:
  ( p => q ) '&' ( p '&' s ) => ( s '&' q ) in IPC-Taut
proof
A1: ( q '&' s ) => ( s '&' q ) in IPC-Taut by Th46;
  ( p => q ) '&' ( p '&' s ) => ( q '&' s ) in IPC-Taut by Th45;
  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 in IPC-Taut by Th47;
  (( P '&' Q ) => S ) => ( P => ( Q => S )) in IPC-Taut by Th36;
  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) in IPC-Taut by Th48;
A2: T => Q in IPC-Taut by Th46;
  (P => (Q => S)) => ((T => Q) => (P => (T => S))) in IPC-Taut by Th27;
  then (T => Q) => (P => (T => S)) in IPC-Taut by A1,Def14;
  hence thesis by A2,Def14;
end;

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

theorem
  ( ( 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) in IPC-Taut by Th38;
  ( P => ( Q => S )) => (( P '&' Q ) => S ) in IPC-Taut by Th37;
  hence thesis by A1,Def14;
end;

Lm5: ( (p '&' q) '&' s ) => q in IPC-Taut
proof
A1: (p '&' q) => q in IPC-Taut by Def14;
  ((p '&' q) '&' s) => (p '&' 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 in IPC-Taut by Lm5;
  ( P => q ) => (( P '&' P ) => ( P '&' q )) in IPC-Taut by Th49;
  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 ) '&' q
  in IPC-Taut by Lm6;
  ( (p '&' q) '&' s ) => ( (p '&' q) '&' s ) '&' ( (p '&' q) '&' s ) in
  IPC-Taut by Th33;
  hence thesis by A1,Th26;
end;

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

Lm10: (p '&' q) '&' s => (p '&' s) '&' q in IPC-Taut
proof
A1: (p '&' q) '&' s '&' q => (p '&' s) '&' q in IPC-Taut by Lm9;
  (p '&' q) '&' s => ((p '&' q) '&' s) '&' q in IPC-Taut by Lm7;
  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 in IPC-Taut by Th46;
  ( P => Q ) => ((P '&' q) => (Q '&' q)) in IPC-Taut by Th44;
  hence thesis by A1,Def14;
end;

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

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

Lm14: (p '&' q) '&' s => p '&' (s '&' q) in IPC-Taut
proof
A1: (s '&' q) '&' p => p '&' (s '&' q) in IPC-Taut by Th46;
  (p '&' q) '&' s => (s '&' q) '&' p in IPC-Taut by Lm13;
  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: s '&' q => q '&' s in IPC-Taut by Th46;
  ( P => Q ) => (( p '&' P ) => ( p '&' Q )) in IPC-Taut by Th49;
  hence thesis by A1,Def14;
end;

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

Lm16: p '&' (q '&' s) => (s '&' q) '&' p in IPC-Taut
proof
A1: p '&' (s '&' q) => (s '&' q) '&' p in IPC-Taut by Th46;
  p '&' (q '&' s) => p '&' (s '&' q) in IPC-Taut by Lm15;
  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: s '&' q => q '&' s in IPC-Taut by Th46;
  ( P => Q ) => ((P '&' p) => (Q '&' p)) in IPC-Taut by Th44;
  hence thesis by A1,Def14;
end;

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

Lm19: p '&' (q '&' s) => (p '&' s) '&' q in IPC-Taut
proof
A1: (q '&' s) '&' p => (p '&' s) '&' q in IPC-Taut by Lm13;
  p '&' (q '&' s) => (q '&' s) '&' p in IPC-Taut by Lm18;
  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: q '&' s => s '&' q in IPC-Taut by Th46;
  ( P => Q ) => (( p '&' P ) => ( p '&' Q )) in IPC-Taut by Th49;
  hence thesis by A1,Def14;
end;

theorem
  p '&' (q '&' s) => (p '&' q) '&' s in IPC-Taut
proof
A1: p '&' (s '&' q) => (p '&' q) '&' s in IPC-Taut by Lm19;
  p '&' (q '&' s) => p '&' (s '&' q) in IPC-Taut by Lm20;
  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
  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;
    end;
    case
A3:   q in IPC-Taut;
      q => (p 'or' q) in IPC-Taut by Def14;
      hence thesis by A3,Def14;
    end;
  end;
  hence thesis;
end;

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

theorem
  (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 thesis by A2,Def14;
end;

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

theorem Th59:
  (p => q) => (p => (s 'or' q)) in IPC-Taut
proof
A1: (q => (s 'or' q)) => ((p => q) => (p => (s 'or' q))) in IPC-Taut by Th22;
  q => (s 'or' q) in IPC-Taut by Def14;
  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;
A1: (p => q) => (p => Q) in IPC-Taut by Th58;
  (p => Q) => ((s => Q) => (P => Q)) in IPC-Taut by Def14;
  then
A2: (s => Q) => ((p => Q) => (P => Q)) in IPC-Taut by Th23;
  s => Q in IPC-Taut by Def14;
  then (p => Q) => (P => Q) in IPC-Taut by A2,Def14;
  hence thesis by A1,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 in IPC-Taut by Def14;
A2: (p => q) => (p => Q) in IPC-Taut by Th59;
  (s => Q) => ((p => Q) => (P => Q)) in IPC-Taut by Def14;
  then (p => Q) => (P => Q) in IPC-Taut by A1,Def14;
  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;
A1: P => (q 'or' P) in IPC-Taut by Def14;
  p => P in IPC-Taut by Def14;
  then p => (q 'or' P) in IPC-Taut by A1,Th26;
  then
A2: ((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
A3: ((q 'or' P) 'or' p) => (q 'or' P) in IPC-Taut by A2,Th26;
  s => P in IPC-Taut by Def14;
  then (q 'or' s) => (q 'or' P) in IPC-Taut by Th63;
  then
A4: (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 (p 'or' Q) => ((q 'or' P) 'or' p) in IPC-Taut by A4,Th26;
  hence thesis by A3,Th26;
end;

theorem
  ( p 'or' (q 'or' s) ) => ( (p 'or' q) 'or' s ) in IPC-Taut
proof
A1: (s 'or' (p 'or' q)) => ((p 'or' q) 'or' s) in IPC-Taut by Th56;
  (q 'or' s) => (s 'or' q) in IPC-Taut by Th56;
  then
A2: (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 (p 'or' (q 'or' s)) => (s 'or' (p 'or' q)) in IPC-Taut by A2,Th26;
  hence thesis by A1,Th26;
end;

theorem
  ( (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) => (p 'or' q) in IPC-Taut by Th56;
  then
A2: (s 'or' (q 'or' p)) => (s 'or' (p 'or' q)) in IPC-Taut by Th63;
  ((q 'or' p) 'or' s) => (s 'or' (q 'or' p)) in IPC-Taut by Th56;
  then ((p 'or' q) 'or' s) => (s 'or' (q 'or' p)) in IPC-Taut by A1,Th26;
  then
A3: ((p 'or' q) 'or' s) => (s 'or' (p 'or' q)) in IPC-Taut by A2,Th26;
  (s 'or' q) => (q 'or' s) in IPC-Taut by Th56;
  then
A4: (p 'or' (s 'or' q)) => (p 'or' (q 'or' s)) in IPC-Taut by Th63;
  (s 'or' (p 'or' q)) => (p 'or' (s 'or' q)) in IPC-Taut by Th64;
  then ((p 'or' q) 'or' s) => (p 'or' (s 'or' q)) in IPC-Taut by A3,Th26;
  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 XBOOLE_0:
    sch 1;
    Y c= MC-wff
    proof
      let a be set;
      assume a in Y;
      hence thesis by A1;
    end;
    then reconsider Z = Y as Subset of MC-wff;
    take Z;
    thus thesis 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 thesis by A2;
    end;
    hence thesis by TARSKI:1;
  end;
end;

definition
  func CPC-Taut -> Subset of MC-wff equals
  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 thesis 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
A1: CnIPC(X) c= CnCPC(X) by Th68;
  p => (q => p) in CnIPC (X) by Th1;
  hence p => (q => p) in CnCPC (X) by A1;
A2: CnIPC(X) c= CnCPC(X) by Th68;
  (p => (q => r)) => ((p => q) => (p => r)) in CnIPC (X) by Th2;
  hence (p => (q => r)) => ((p => q) => (p => r)) in CnCPC (X) by A2;
A3: CnIPC(X) c= CnCPC(X) by Th68;
  p '&' q => p in CnIPC (X) by Th3;
  hence p '&' q => p in CnCPC (X) by A3;
A4: CnIPC(X) c= CnCPC(X) by Th68;
  p '&' q => q in CnIPC (X) by Th4;
  hence p '&' q => q in CnCPC (X) by A4;
A5: CnIPC(X) c= CnCPC(X) by Th68;
  p => (q => (p '&' q)) in CnIPC (X) by Th5;
  hence p => (q => (p '&' q)) in CnCPC (X) by A5;
A6: CnIPC(X) c= CnCPC(X) by Th68;
  p => (p 'or' q) in CnIPC (X) by Th6;
  hence p => (p 'or' q) in CnCPC (X) by A6;
A7: CnIPC(X) c= CnCPC(X) by Th68;
  q => (p 'or' q) in CnIPC (X) by Th7;
  hence q => (p 'or' q) in CnCPC (X) by A7;
A8: CnIPC(X) c= CnCPC(X) by Th68;
  (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC (X) by Th8;
  hence (p => r) => ((q => r) => ((p 'or' q) => r)) in CnCPC (X) by A8;
A9: CnIPC(X) c= CnCPC(X) by Th68;
  FALSUM => p in CnIPC (X) by Th9;
  hence FALSUM => p in CnCPC (X) by A9;
  T is CPC_theory & X c= T implies p 'or' (p => FALSUM) in T by Def19;
  hence p 'or' (p => FALSUM) in CnCPC (X) by Def20;
end;

theorem Th70:
  p in CnCPC(X) & p => q in CnCPC(X) implies q in CnCPC(X)
proof
  assume that
A1: p in CnCPC(X) and
A2: p => q in CnCPC(X);
  T is CPC_theory & X c= T implies q in T
  proof
    assume that
A3: T is CPC_theory and
A4: X c= T;
A5: p => q in T by A2,A3,A4,Def20;
    p in T by A1,A3,A4,Def20;
    hence thesis by A3,A5,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 thesis 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 thesis 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 thesis by A1,A2,Def20;
  end;
  hence thesis by Def20;
end;

theorem
  CnCPC(CnCPC(X)) = CnCPC(X)
proof
A1: CnCPC(X) c= CnCPC(CnCPC(X)) by Th72;
  CnCPC(CnCPC(X)) c= CnCPC(X) by Lm21;
  hence thesis by A1,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 thesis by Th70;
end;

registration
  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: CnCPC(T) c= T
    proof
      let a be set;
      assume a in CnCPC(T);
      hence thesis by A1,Def20;
    end;
    T c= CnCPC(T) by Th72;
    hence CnCPC(T) = T by A2,XBOOLE_0:def 10;
  end;
  thus thesis;
end;

theorem
  T is CPC_theory implies CPC-Taut c= T
proof
  assume
A1: T is CPC_theory;
  CPC-Taut c= CnCPC(T) by Th73,XBOOLE_1:2;
  hence thesis by A1,Th75;
end;

registration
  cluster CPC-Taut -> CPC_theory;
  coherence;
end;

theorem
  IPC-Taut c= CPC-Taut by 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
  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 XBOOLE_0:
    sch 1;
    Y c= MC-wff
    proof
      let a be set;
      assume a in Y;
      hence thesis by A1;
    end;
    then reconsider Z = Y as Subset of MC-wff;
    take Z;
    thus thesis 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 thesis by A2;
    end;
    hence thesis by TARSKI:1;
  end;
end;

definition
  func S4-Taut -> Subset of MC-wff equals
  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: CnCPC (X) c= CnS4 (X) by Th80;
  CnIPC (X) c= CnCPC (X) by Th68;
  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
A1: CnIPC (X) c= CnS4 (X) by Th81;
  p => (q => p) in CnIPC (X) by Th1;
  hence p => (q => p) in CnS4 (X) by A1;
A2: CnIPC (X) c= CnS4 (X) by Th81;
  (p => (q => r)) => ((p => q) => (p => r)) in CnIPC (X) by Th2;
  hence (p => (q => r)) => ((p => q) => (p => r)) in CnS4 (X) by A2;
A3: CnIPC (X) c= CnS4 (X) by Th81;
  p '&' q => p in CnIPC (X) by Th3;
  hence p '&' q => p in CnS4 (X) by A3;
A4: CnIPC (X) c= CnS4 (X) by Th81;
  p '&' q => q in CnIPC (X) by Th4;
  hence p '&' q => q in CnS4 (X) by A4;
A5: CnIPC (X) c= CnS4 (X) by Th81;
  p => (q => (p '&' q)) in CnIPC (X) by Th5;
  hence p => (q => (p '&' q)) in CnS4 (X) by A5;
A6: CnIPC (X) c= CnS4 (X) by Th81;
  p => (p 'or' q) in CnIPC (X) by Th6;
  hence p => (p 'or' q) in CnS4 (X) by A6;
A7: CnIPC (X) c= CnS4 (X) by Th81;
  q => (p 'or' q) in CnIPC (X) by Th7;
  hence q => (p 'or' q) in CnS4 (X) by A7;
A8: CnIPC (X) c= CnS4 (X) by Th81;
  (p => r) => ((q => r) => ((p 'or' q) => r)) in CnIPC (X) by Th8;
  hence (p => r) => ((q => r) => ((p 'or' q) => r)) in CnS4 (X) by A8;
A9: CnIPC (X) c= CnS4 (X) by Th81;
  FALSUM => p in CnIPC (X) by Th9;
  hence FALSUM => p in CnS4 (X) by A9;
  T is S4_theory & X c= T implies p 'or' (p => FALSUM) in T by Def22;
  hence p 'or' (p => FALSUM) in CnS4 (X) by Def23;
end;

theorem Th83:
  p in CnS4 (X) & p => q in CnS4 (X) implies q in CnS4 (X)
proof
  assume that
A1: p in CnS4 (X) and
A2: p => q in CnS4 (X);
  T is S4_theory & X c= T implies q in T
  proof
    assume that
A3: T is S4_theory and
A4: X c= T;
A5: p => q in T by A2,A3,A4,Def23;
    p in T by A1,A3,A4,Def23;
    hence thesis by A3,A5,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 that
A2: T is S4_theory and
A3: X c= T;
    p in T by A1,A2,A3,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 thesis 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 thesis 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 thesis by A1,A2,Def23;
  end;
  hence thesis by Def23;
end;

theorem
  CnS4(CnS4(X)) = CnS4(X)
proof
A1: CnS4(X) c= CnS4(CnS4(X)) by Th89;
  CnS4(CnS4(X)) c= CnS4(X) by Lm23;
  hence thesis by A1,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 thesis by Th87;
end;

registration
  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: CnS4(T) c= T
    proof
      let a be set;
      assume a in CnS4(T);
      hence thesis by A1,Def23;
    end;
    T c= CnS4(T) by Th89;
    hence CnS4(T) = T by A2,XBOOLE_0:def 10;
  end;
  thus thesis;
end;

theorem
  T is S4_theory implies S4-Taut c= T
proof
  assume
A1: T is S4_theory;
  S4-Taut c= CnS4(T) by Th90,XBOOLE_1:2;
  hence thesis by A1,Th92;
end;

registration
  cluster S4-Taut -> S4_theory;
  coherence;
end;

theorem
  CPC-Taut c= S4-Taut by Th80;

theorem
  IPC-Taut c= S4-Taut by Th81;