:: The Axiomatization of Propositional Logic
::  by Mariusz Giero
::
:: Received October 18, 2016
:: Copyright (c) 2016-2019 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, TARSKI,
      RELAT_1, RELAT_2, XBOOLE_0, FUNCT_1, QC_LANG1, XBOOLEAN, HILBERT1,
      CQC_THE1, NAT_1, XXREAL_0, LTLAXIO1, ARYTM_1, ZF_LANG, PARTFUN1,
      WELLFND1, ORDERS_2, ORDINAL1, STRUCT_0, MARGREL1, HILBERT2, ZFMISC_1,
      ZF_MODEL, PBOOLE, GLIB_000, INTPRO_1, ABCMIZ_0, GROUP_4, WELLORD1,
      FINSET_1, QMAX_1, PL_AXIOM;
 notations TARSKI, XBOOLE_0, ZFMISC_1, DOMAIN_1, SUBSET_1, SETFAM_1, RELAT_1,
      RELAT_2, RELSET_1, PARTFUN1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1,
      XXREAL_0, NAT_D, FUNCT_1, WELLORD1, STRUCT_0, ORDERS_2, FUNCT_2,
      FINSET_1, WELLFND1, BINOP_1, FINSEQ_1, HILBERT1, HILBERT2, PBOOLE,
      XBOOLEAN, MARGREL1, INTPRO_1;
 constructors NAT_D, RELSET_1, AOFA_I00, HILBERT2, DOMAIN_1, WELLORD1,
      WELLFND1, SETFAM_1, INTPRO_1;
 registrations SUBSET_1, ORDINAL1, FUNCT_1, FINSEQ_1, NAT_1, XBOOLEAN,
      RELSET_1, MARGREL1, XBOOLE_0, XREAL_0, HILBERT1, STRUCT_0, FINSET_1,
      ORDERS_2;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
 definitions TARSKI, ORDINAL1, INTPRO_1, HILBERT1;
 equalities XBOOLEAN, HILBERT1, HILBERT2, FINSEQ_1;
 expansions TARSKI, INTPRO_1;
 theorems TARSKI, FINSEQ_1, XBOOLE_0, XBOOLE_1, XBOOLEAN, LTLAXIO5, NAT_1,
      XXREAL_0, XREAL_1, NAT_D, FUNCT_1, RELAT_2, HILBERT2, RELAT_1, WELLORD1,
      WELLORD2, ZFMISC_1, PARTFUN1, WELLFND1, PCOMPS_2, FUNCT_2, XTUPLE_0,
      FINSEQ_3, ORDINAL1, FINSET_1, MARGREL1, INTPRO_1, HILBERT1;
 schemes XFAMILY, NAT_1, FINSEQ_1, BINOP_1, WELLFND1, FRAENKEL, FUNCT_2,
      HILBERT2, XBOOLE_0;

begin

theorem rnginc:
  for f,g be Function holds
  (dom f c= dom g & for x be set st x in dom f holds f.x = g.x)
  implies rng f c= rng g
  proof
    let f,g be Function;
    assume that A2: dom f c= dom g and A2a: for x be set st x in dom f
    holds f.x = g.x;
    let x be object;assume x in rng f;then
    consider y be object such that A1: y in dom f & x = f.y by FUNCT_1:def 3;
    x = g.y by A2a,A1;
    hence x in rng g by FUNCT_1:3,A1,A2;
  end;

theorem th1:
  for p,q being boolean object holds (p '&' q) => p = TRUE
  proof
   let p,q be boolean object;
   p = TRUE or p = FALSE by XBOOLEAN:def 3;
   hence (p '&' q) => p = TRUE;
  end;

theorem th2:
  for p being boolean object holds ('not' 'not' p) <=> p = TRUE
  proof
   let p be boolean object;
   p = TRUE or p = FALSE by XBOOLEAN:def 3;
   hence ('not' 'not' p) <=> p = TRUE;
  end;

theorem th3:
  for p,q being boolean object holds
    'not' (p '&' q) <=> ('not' p) 'or' ('not' q) = TRUE
  proof
   let p,q be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
   q = TRUE or q = FALSE by XBOOLEAN:def 3;
   hence 'not' (p '&' q) <=> ('not' p) 'or' ('not' q) = TRUE by A1;
  end;

theorem th3a:
  for p,q being boolean object holds
   'not' (p 'or' q) <=> ('not' p) '&' ('not' q) = TRUE
  proof
   let p,q be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
   q = TRUE or q = FALSE by XBOOLEAN:def 3;
   hence 'not' (p 'or' q) <=> ('not' p) '&' ('not' q) = TRUE by A1;
  end;

theorem th4:
  for p,q be boolean object holds
    (p => q) => (('not' q) => 'not' p) = TRUE
  proof
    let p,q be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
    q = TRUE or q = FALSE by XBOOLEAN:def 3;
    hence (p => q) => (('not' q) => 'not' p) = TRUE by A1;
  end;

theorem th5:
  for p,q,r be boolean object holds
    p => q => (p => r => (p => (q '&' r))) = TRUE
  proof
    let p,q,r be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;
    r = TRUE or r = FALSE by XBOOLEAN:def 3;
    hence thesis by A1,A2;
  end;

theorem th5a:
  for p,q,r be boolean object holds
    p => r => (q => r => ((p 'or' q) => r)) = TRUE
  proof
    let p,q,r be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;
    r = TRUE or r = FALSE by XBOOLEAN:def 3;
    hence thesis by A1,A2;
  end;

theorem th6:
  for p,q be boolean object holds (p '&' q) <=> (q '&' p) = TRUE
  proof
    let p,q be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
    q = TRUE or q = FALSE by XBOOLEAN:def 3;
    hence (p '&' q) <=> (q '&' p) = TRUE by A1;
  end;

theorem th6a:
  for p,q be boolean object holds (p 'or' q) <=> (q 'or' p) = TRUE
  proof
    let p,q be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
    q = TRUE or q = FALSE by XBOOLEAN:def 3;
    hence (p 'or' q) <=> (q 'or' p) = TRUE by A1;
  end;

theorem th7:
  for p,q,r be boolean object holds
    (p '&' q '&' r) <=> (p '&' (q '&' r)) = TRUE
  proof
    let p,q,r be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;
    r= TRUE or r = FALSE by XBOOLEAN:def 3;
    hence thesis by A1,A2;
  end;

theorem th7a:
  for p,q,r be boolean object holds
    (p 'or' q 'or' r) <=> (p 'or' (q 'or' r)) = TRUE
  proof
    let p,q,r be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;
    r= TRUE or r = FALSE by XBOOLEAN:def 3;
    hence thesis by A1,A2;
  end;

theorem Th17a:
  for p,q be boolean object holds
    ('not' q => 'not' p) => (('not' q => p) => q) = TRUE
  proof
    let p,q be boolean object;
A1: p = FALSE or p = TRUE by XBOOLEAN:def 3;
    q = FALSE or q = TRUE by XBOOLEAN:def 3;
    hence thesis by A1;
  end;

theorem th8:
  for p,q,r be boolean object holds
    p '&' (q 'or' r) <=> ((p '&' q) 'or' (p '&' r)) = TRUE
  proof
    let p,q,r be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;
    r= TRUE or r = FALSE by XBOOLEAN:def 3;
    hence thesis by A1,A2;
  end;

theorem th8a:
  for p,q,r be boolean object holds
    p 'or' (q '&' r) <=> ((p 'or' q) '&' (p 'or' r)) = TRUE
  proof
    let p,q,r be boolean object;
A1: p = TRUE or p = FALSE by XBOOLEAN:def 3;
A2: q = TRUE or q = FALSE by XBOOLEAN:def 3;
    r= TRUE or r = FALSE by XBOOLEAN:def 3;
    hence thesis by A1,A2;
  end;

theorem uniolinf:
  for X be finite set,Y be set holds
    Y is c=-linear & X c= union Y & Y <> {} implies
      ex Z be set st X c= Z & Z in Y
  proof
    let X be finite set,Y be set;
    assume
A0: Y is c=-linear & X c= union Y & Y <> {};
      deffunc G(object) = {y where y is Element of Y: $1 in y};
      deffunc F(object) = the Element of G($1);
A18: for x be object holds x in X implies G(x) is non empty
    proof
      let x be object;
      assume x in X;then
      consider y be set such that
A11:  x in y & y in Y by TARSKI:def 4,A0;
      reconsider y as Element of Y by A11;
      y in G(x) by A11;
      hence G(x) is non empty;
    end;
    per cases;
    suppose
S1:   X is empty;
      consider Z be object such that
A15:  Z in Y by A0,XBOOLE_0:def 1;
      consider Z1 be set such that
A16:  Z1 in Y & not ex x be object st x in Y & x in Z1 by TARSKI:3,A15;
      X c= Z1 by S1;
      hence thesis by A16;
    end;
    suppose
S2:   not X is empty;
      set Y1 = {F(x) where x is Element of X: x in X};
A20:  X is finite;
A2:   Y1 is finite from FRAENKEL:sch 21(A20);
A19:  Y1 c= Y
      proof
        let x be object;
        assume x in Y1;then
        consider x1 be Element of X such that
A13:    x = the Element of G(x1) & x1 in X;
        G(x1) is non empty by A18,A13;then
        x in G(x1) by A13;then
        consider x2 be Element of Y such that
A14:    x2 = x & x1 in x2;
        thus x in Y by A0,A14;
      end;
      Y1 <> {}
      proof
        consider x be object such that
A15:    x in X by XBOOLE_0:def 1,S2;
        consider x1 be set such that
A16:    x1 in X & not ex x be object st x in X & x in x1 by TARSKI:3,A15;
        reconsider x1 as Element of X by A16;
        the Element of G(x1) in Y1 by A16;
        hence thesis;
      end;then
      consider Z being set such that
A1:   Z in Y1 & for y being set st y in Y1 holds y c= Z
        by FINSET_1:12,A0,A2,A19;
A4:   X c= Z
    proof
      let x be object;
      assume
A8:   x in X;then
      the Element of G(x) in Y1;then
A9:   the Element of G(x) c= Z by A1;
      G(x) is non empty by A8,A18;then
      the Element of G(x) in G(x);then
      consider y3 be Element of Y such that
A10:  y3 = the Element of G(x) & x in y3;
      thus x in Z by A10,A9;
    end;
    consider x be Element of X such that
A6: Z = the Element of G(x) & x in X by A1;
     G(x) is non empty by A6,A18;then
     Z in G(x) by A6;then
     consider y be Element of Y such that
U1:  y = Z & x in y;
     thus ex Z be set st X c= Z & Z in Y by A4,A0,U1;
   end;
 end;

begin

definition
  let D be set;
  attr D is with_propositional_variables means
  :Def4:
  for n being Element of NAT holds <*3+n*> in D;
end;

definition
  let D be set;
  attr D is PL-closed means
  :Def5:
  D c= NAT* & D is with_FALSUM
  with_implication with_propositional_variables;
end;

Lm1: for D be set st D is PL-closed holds D is non empty
proof
  let D be set;
  assume D is PL-closed;
  then D is with_FALSUM;
  hence thesis;
end;

registration
  cluster PL-closed -> with_FALSUM with_implication
    with_propositional_variables non empty for set;
  coherence by Lm1;
  cluster with_FALSUM with_implication
    with_propositional_variables -> PL-closed for Subset of NAT*;
  coherence;
end;

definition
  func PL-WFF -> set means
  :Def6:
  it is PL-closed & for D being set st D is PL-closed holds it c= D;
  existence
  proof
A1: <*0 qua Element of NAT *> in NAT* by FINSEQ_1:def 11;
    defpred P[set] means for D being set st D is PL-closed holds $1 in D;
    consider D0 being set such that
A2: for x being set holds x in D0 iff x in NAT* & P[x] from XFAMILY:
    sch 1;
A3: for D being set st D is PL-closed holds <*0*> in D by INTPRO_1:def 1;
    then reconsider D0 as non empty set by A2,A1;
    take D0;
A4: D0 c= NAT* by A2;
    for p, q being FinSequence st p in D0 & q in D0 holds <*1*>^p^q in D0
    proof
      let p, q be FinSequence such that
A5:   p in D0 and
A6:   q in D0;
A7:   q in NAT* by A2,A6;
A8:   for D being set st D is PL-closed holds <*1*>^p^q in D
      proof
        let D be set;
        assume
A9:     D is PL-closed;
        then
A10:    q in D by A2,A6;
        p in D by A2,A5,A9;
        hence thesis by A9,A10,HILBERT1:def 2;
      end;
      p in NAT* by A2,A5;
      then reconsider p9=p, q9=q as FinSequence of NAT by A7,FINSEQ_1:def 11;
      <*1*>^p9^q9 in NAT* by FINSEQ_1:def 11;
      hence thesis by A2,A8;
    end;then
A11: D0 is with_implication by HILBERT1:def 2;
    for n being Element of NAT holds <*3+n*> in D0
    proof
      let n be Element of NAT;
      set p = 3+n;
      reconsider h = <*p*> as FinSequence of NAT;
A19:  h in NAT* by FINSEQ_1:def 11;
      for D being set st D is PL-closed holds <*p*> in D by Def4;
      hence thesis by A2,A19;
    end;
    then
A20: D0 is with_propositional_variables;
D0 is with_FALSUM by A2,A1,A3;
    hence D0 is PL-closed by A4,A20,A11;
    let D be set such that
A21: D is PL-closed;
    let x be object;
    assume x in D0;
    hence thesis by A2,A21;
  end;
  uniqueness
  proof
    let D1, D2 be set such that
A22: D1 is PL-closed and
A23: for D being set st D is PL-closed holds D1 c= D and
A24: D2 is PL-closed and
A25: for D being set st D is PL-closed holds D2 c= D;
A26: D2 c= D1 by A22,A25;
    D1 c= D2 by A23,A24;
    hence thesis by A26,XBOOLE_0:def 10;
  end;
end;

registration
  cluster PL-WFF -> PL-closed;
  coherence by Def6;
end;

registration
  cluster PL-closed non empty for set;
  existence
  proof
    take PL-WFF;
    thus thesis;
  end;
end;

registration
  cluster PL-WFF -> functional;
  coherence
  proof
    PL-WFF c= NAT* by Def5;
    hence thesis;
  end;
end;

registration
  cluster -> FinSequence-like for Element of PL-WFF;
  coherence
  proof
    let p be Element of PL-WFF;
    PL-WFF c= NAT* by Def5;
    hence thesis;
  end;
end;

definition
  func FaLSUM -> Element of PL-WFF equals
  <*0*>;
  correctness by INTPRO_1:def 1;
  let p, q be Element of PL-WFF;
  func p => q -> Element of PL-WFF equals
  <*1*>^p^q;
  coherence by HILBERT1:def 2;
end;

definition
  let n be Element of NAT;
  func Prop n -> Element of PL-WFF equals
  <*(3 + n)*>;
  coherence by Def4;
end;

definition
  func props -> Subset of PL-WFF means :defprops:
  for x be set holds x in it iff ex n be Element of NAT st x=Prop n;
 existence
 proof
   defpred P1[object] means
   ex n be Element of NAT st$1=Prop n;
   consider X being set such that
A1: for x being object holds(x in X iff x in PL-WFF & P1[x])
    from XBOOLE_0:sch 1;
    X c=PL-WFF by A1;
  then reconsider X as Subset of PL-WFF;
  take X;
  thus for x being set holds (x in X iff ex n be Element of NAT st x=Prop n)
  by A1;
 end;
 uniqueness
 proof
  let A,B be Subset of PL-WFF such that
   A2: for x be set holds x in A iff ex n be Element of NAT st x=Prop n and
   A3: for x be set holds x in B iff ex n be Element of NAT st x=Prop n;
  A4: B c= A
  proof
   let x be object;
   assume x in B;
   then consider n be Element of NAT such that
    A5: x=Prop n by A3;
   thus x in A by A2,A5;
  end;
  A c= B
  proof
   let x be object;
   assume x in A;
   then consider n be Element of NAT such that
    A6: x=Prop n by A2;
   thus x in B by A3,A6;
  end;
  hence A=B by A4,XBOOLE_0:def 10;
 end;
end;

reserve p,q,r,s,A,B for Element of PL-WFF,
  F,G,H for Subset of PL-WFF,
  k,n for Element of NAT,
  f,f1,f2 for FinSequence of PL-WFF;

definition
  let D be Subset of PL-WFF;
  redefine attr D is with_implication means
  for p, q st p in D & q in D holds p => q in D;
  compatibility
  proof
    thus D is with_implication implies for p, q st p in D & q in D
    holds p => q in D by HILBERT1:def 2;
    assume
A1: for p, q st p in D & q in D holds p => q in D;
    let p, q be FinSequence;
    assume
A2: p in D & q in D;
    then reconsider p9 = p, q9 = q as Element of PL-WFF;
    p9 => q9 in D by A1,A2;
    hence thesis;
  end;
end;

scheme
  PLInd { P[set] }: for r holds P[r]
  provided
A1: P[FaLSUM] and
A2: for n holds P[Prop n] and
A3: for r,s st P[r] & P[s] holds P[r => s]
  proof
  set X = { p where p is Element of PL-WFF: P[p]};
  X c= PL-WFF
  proof
    let x be object;
    assume x in X;
    then ex p being Element of PL-WFF st x = p & P[p];
    hence thesis;
  end;
  then reconsider X as Subset of PL-WFF;
  let r;
A4: X is with_propositional_variables
  proof
    let n;
    P[Prop n] by A2;
    hence thesis;
  end;
A5: X is with_implication
  proof
    let p, q;
    assume p in X;
    then
A6: ex x being Element of PL-WFF st p = x & P[x];
    assume q in X;
    then ex x being Element of PL-WFF st q = x & P[x];
    then P[p => q] by A3,A6;
    hence thesis;
  end;
  PL-WFF c= NAT* by Def5;then
A8: X c= NAT*;
    X is with_FALSUM by A1;
  then PL-WFF c= X by A8,A5,A4,Def6;
  then r in X;
  then ex p being Element of PL-WFF st r = p & P[p];
  hence thesis;
end;

theorem plhp:
  PL-WFF c= HP-WFF
  proof
    let x be object;
    assume
A0: x in PL-WFF;
    defpred P[Element of PL-WFF] means $1 in HP-WFF;
    VERUM = FaLSUM;
    :: syntactically only,since represented by identical sequences
    then A1: P[FaLSUM];
A2: for n holds P[Prop n]
    proof
      let n;
      Prop n = prop n;
      hence thesis;
    end;
A3: for r,s st P[r] & P[s] holds P[r => s]
    proof
      let r,s;
      assume P[r] & P[s];then
      reconsider r1 = r, s1 = s as Element of HP-WFF;
      r1 => s1 in HP-WFF;
      hence P[r => s];
    end;
A4: for A holds P[A] from PLInd(A1,A2,A3);
    reconsider x1 = x as Element of PL-WFF by A0;
    x1 in HP-WFF by A4;
    hence x in HP-WFF;
  end;

definition let p;
  func 'not' p -> Element of PL-WFF equals
  p => FaLSUM;
  correctness;
end;

definition
  func VeRUM -> Element of PL-WFF equals
  'not' FaLSUM;
  correctness;
end;

definition let p,q;
  func p '&' q -> Element of PL-WFF equals
  'not' (p => 'not' q);
  coherence;
  func p 'or' q -> Element of PL-WFF equals
  ('not' p) => q;
  coherence;
end;

definition let p,q;
  func p <=> q -> Element of PL-WFF equals
  (p => q) '&' (q => p);
  correctness;
end;

begin

definition
  mode PLModel is Subset of props;
end;

reserve M for PLModel;

definition let M be PLModel;
  func SAT M -> Function of PL-WFF,BOOLEAN means :Def11:
  it.FaLSUM=0 &
  (for k holds it.Prop k=1 iff Prop k in M) &
  for p,q holds it.(p=>q)=(it.p)=>(it.q);
  existence
  proof
    defpred P1[Element of NAT,Element of BOOLEAN] means
    $2=1 iff Prop $1 in M;
A16: for x be Element of NAT
     ex y being Element of BOOLEAN st P1[x,y]
     proof
       let x be Element of NAT;
       defpred P2[Element of BOOLEAN] means
       $1=1 iff Prop x in M;
       per cases;
       suppose prop x in M;
         then P2[TRUE];
         hence ex y being Element of BOOLEAN st P1[x,y];
       end;
       suppose not prop x in M;
         then P2[FALSE];
         hence ex y being Element of BOOLEAN st P1[x,y];
       end;
     end;
     consider f1 be sequence of BOOLEAN such that
A19: for k holds P1[k,f1.k] from FUNCT_2:sch 3(A16);
     deffunc P(Element of NAT)=f1.$1;
     defpred C[Element of HP-WFF,Element of HP-WFF,set,set,set] means
     ex s5 be Element of BOOLEAN st $5=FALSE;
     defpred I[Element of HP-WFF,Element of HP-WFF,set,set,set] means
     ($3 is Element of BOOLEAN & $4 is Element of BOOLEAN implies ex s3,s4,s5
     be Element of BOOLEAN st s3=$3 & s4=$4 & s5=$5 & s5=s3=>s4)
     & (not($3 is Element of BOOLEAN & $4 is Element of BOOLEAN)
     implies $5=FALSE);
A1:  for p,q be Element of HP-WFF for a,b being set
     ex c being set st C[p,q,a,b,c];
A2:  for p,q be Element of HP-WFF for a,b being set
     ex d being set st I[p,q,a,b,d]
     proof
       let p,q be Element of HP-WFF,a,b be set;
       per cases;
       suppose a is Element of BOOLEAN & b is Element of BOOLEAN;
         then reconsider a1=a,b1=b as Element of BOOLEAN;
         reconsider ab = a1 => b1 as Element of BOOLEAN by MARGREL1:def 12;
         ab = a1 => b1;
         hence thesis;
       end;
       suppose not(a is Element of BOOLEAN & b is Element of BOOLEAN);
         hence thesis;
       end;
     end;
A3:  for p,q be Element of HP-WFF for a,b,c,d being set
     st C[p,q,a,b,c] & C[p,q,a,b,d] holds c = d;
A4:  for p,q be Element of HP-WFF for a,b,c,d being set
     st I[p,q,a,b,c] & I[p,q,a,b,d] holds c = d;
     consider sat being ManySortedSet of HP-WFF such that
A34: sat.VERUM=0 &
     (for n holds sat.(prop n)=P(n)) &
     for p,q be Element of HP-WFF holds C[p,q,sat.p,sat.q,sat.(p '&' q)] &
     I[p,q,sat.p,sat.q,sat.(p=>q)] from HILBERT2: sch 3(A1,A2,A3,A4);
A35: for x be object st x in HP-WFF holds sat.x in BOOLEAN
     proof
       let x be object;
       assume x in HP-WFF;
       then reconsider x1=x as Element of HP-WFF;
A42:   now
         let n;
         sat.(prop n)=f1.n by A34;
         hence sat.(prop n) in BOOLEAN;
       end;
       per cases by HILBERT2:9;
       suppose x1 = VERUM;
         hence sat.x in BOOLEAN by A34;
       end;
       suppose x1 is simple;then
         ex n be Element of NAT st x1=prop n by HILBERT2:def 8;
         hence sat.x in BOOLEAN by A42;
       end;
       suppose x1 is conjunctive;then
         consider A,B be Element of HP-WFF such that
E2:      x1=A '&' B by HILBERT2:def 6;
         consider s5 be Element of BOOLEAN such that
E3:      sat.(A '&' B)=FALSE by A34;
         thus sat.x in BOOLEAN by E3,E2;
       end;
       suppose x1 is conditional;then
         consider A,B be Element of HP-WFF such that
E1:      x1=A=>B by HILBERT2:def 7;
A37:     I[A,B,sat.A,sat.B,sat.(A=>B)] by A34;
         thus sat.x in BOOLEAN by A37,E1;
       end;
     end;
     dom sat=HP-WFF by PARTFUN1:def 2;then
     reconsider sat as
     Function of HP-WFF,BOOLEAN by A35,FUNCT_2:3;
     set satc = sat | PL-WFF;
     reconsider satc as Function of PL-WFF,BOOLEAN by FUNCT_2:32,plhp;
B1:  satc.FaLSUM = 0 by A34,FUNCT_1:49;
B2:  for k holds satc.Prop k=1 iff Prop k in M
     proof
       let k;
       hereby
         assume satc.Prop k=1;then
D2:      sat.Prop k = 1 by FUNCT_1:49;
         sat.prop k = f1.k by A34;
         hence Prop k in M by A19,D2;
       end;
       assume Prop k in M;then
D1:    f1.k = 1 by A19;
       sat.prop k = f1.k by A34;
       hence satc.Prop k=1 by D1,FUNCT_1:49;
     end;
     for p,q holds satc.(p=>q)=(satc.p)=>(satc.q)
     proof
       let p,q;
       reconsider p1=p,q1=q as Element of HP-WFF by plhp;
       consider s3,s4,s5 be Element of BOOLEAN such that
D4:    s3=sat.p1 & s4=sat.q1 & s5=sat.(p1=>q1) & s5=s3=>s4 by A34;
       thus satc.(p=>q)=sat.(p=>q) by FUNCT_1:49
       .= (satc.p)=>(sat.q) by FUNCT_1:49,D4
       .= (satc.p)=>(satc.q) by FUNCT_1:49;
     end;
     hence thesis by B1,B2;
  end;
  uniqueness
  proof
      let v1,v2 be Function of PL-WFF,BOOLEAN;
      assume
A65:  v1.FaLSUM=0 & (for k holds v1.
      Prop k=1 iff Prop k in M) & for p,q holds v1.(p=>q)=v1.p=>v1.q;
      assume
A66:  v2.FaLSUM=0 & (for k holds v2.
      Prop k=1 iff Prop k in M) & for p,q holds v2.(p=>q)=v2.p=>v2.q;
   defpred P1[Element of PL-WFF] means v1.$1=v2.$1;
   A67: P1[Prop n]
   proof
     per cases;
     suppose A68: Prop n in M;
       hence v1.Prop n=1 by A65
       .=v2.Prop n by A66,A68;
     end;
     suppose A69: not Prop n in M;
      then v1.Prop n=0 by XBOOLEAN:def 3,A65;
      hence v1.Prop n = v2.Prop n by XBOOLEAN:def 3,A66,A69;
    end;
   end;
   A70: for p,q st P1[p] & P1[q] holds P1[p=>q]
   proof
    let p,q;
    assume that
     A71: P1[p] and
     A72: P1[q];
     thus v1.(p=>q)=v1.p=>v1.q by A65
      .=v2.(p=>q) by A66,A72,A71;
   end;
   A83: P1[FaLSUM] by A66,A65;
   for A holds P1[A] from PLInd(A83,A67,A70); then
   A85: for x be Element of PL-WFF st x in dom v1 holds v1.x=v2.x;
   dom v1=PL-WFF by FUNCT_2:def 1
   .=dom v2 by FUNCT_2:def 1;
   hence thesis by A85,PARTFUN1:5;
 end;
end;

theorem
  (SAT M).(A => B) = 1 iff (SAT M).A = 0 or (SAT M).B = 1
  proof
A3:   (SAT M).B = TRUE or (SAT M).B = FALSE by XBOOLEAN:def 3;
      hereby
        assume (SAT M).(A => B) = 1;then
        (SAT M).A => (SAT M).B = 1 by Def11;
        hence (SAT M).A = 0 or (SAT M).B = 1 by A3;
      end;
      assume
A4:   (SAT M).A = 0 or (SAT M).B = 1;
      thus (SAT M).(A => B) = (SAT M).A => (SAT M).B by Def11
      .= 1 by A4;
    end;

theorem semnot2:
  (SAT M).('not' p) = 'not' (SAT M).p
  proof
    thus (SAT M).('not' p) = (SAT M).p => (SAT M).FaLSUM by Def11
    .= (SAT M).p => FALSE by Def11
    .= 'not' (SAT M).p;
  end;

theorem semnot:
  (SAT M).('not' A)=1 iff (SAT M).A=0
  proof
    hereby assume(SAT M).('not' A)=1;then
      'not' (SAT M).A = 1 by semnot2;
      hence (SAT M).A=0;
    end;
    assume A2: (SAT M).A=0;
    thus(SAT M).('not' A)= 'not' (SAT M).A by semnot2 .=1 by A2;
  end;

theorem semcon2:
  (SAT M).(A '&' B) = (SAT M).A '&' (SAT M).B
  proof
    thus (SAT M).(A '&' B) = 'not' (SAT M).(A => 'not' B) by semnot2
    .= 'not' ((SAT M).A => (SAT M).('not' B)) by Def11
    .= 'not' ((SAT M).A => 'not' (SAT M).B) by semnot2
    .= (SAT M).A '&' (SAT M).B;
  end;

theorem
  (SAT M).(A '&' B) = 1 iff (SAT M).A = 1 & (SAT M).B = 1
  proof
    hereby
      assume (SAT M).(A '&' B) = 1;then
      (SAT M).A '&' (SAT M).B = 1 by semcon2;
      hence (SAT M).A = 1 & (SAT M).B = 1 by XBOOLEAN:101;
    end;
    assume A3:(SAT M).A = 1 & (SAT M).B = 1;
    thus (SAT M).(A '&' B) = (SAT M).A '&' (SAT M).B by semcon2
    .= 1 by A3;
  end;

theorem semdis2:
  (SAT M).(A 'or' B) = (SAT M).A 'or' (SAT M).B
  proof
    thus (SAT M).(A 'or' B) = (SAT M).('not' A) => (SAT M).B by Def11
    .= (SAT M).A 'or' (SAT M).B by semnot2;
  end;

theorem
  (SAT M).(A 'or' B) = 1 iff (SAT M).A = 1 or (SAT M).B = 1
  proof
A2: (SAT M).B = TRUE or (SAT M).B = FALSE by XBOOLEAN:def 3;
    hereby
      assume (SAT M).(A 'or' B) = 1;then
      (SAT M).A 'or' (SAT M).B = 1 by semdis2;
      hence (SAT M).A = 1 or (SAT M).B = 1 by A2;
    end;
    assume A3:(SAT M).A = 1 or (SAT M).B = 1;
    thus (SAT M).(A 'or' B) = (SAT M).A 'or' (SAT M).B by semdis2
    .= 1 by A3;
  end;

theorem semequ2:
  (SAT M).(A <=> B) = (SAT M).A <=> (SAT M).B
  proof
    thus (SAT M).(A <=> B) = (SAT M).(A => B) '&' (SAT M).(B => A) by semcon2
    .= ((SAT M).A => (SAT M).B) '&' (SAT M).(B => A) by Def11
    .= (SAT M).A <=> (SAT M).B by Def11;
    end;

theorem
  (SAT M).(A <=> B) = 1 iff (SAT M).A = (SAT M).B
  proof
A2: (SAT M).B = TRUE or (SAT M).B = FALSE by XBOOLEAN:def 3;
    hereby
      assume (SAT M).(A <=> B) = 1;then
      (SAT M).A <=> (SAT M).B = 1 by semequ2;
      hence (SAT M).A = (SAT M).B by A2;
    end;
    assume A3:(SAT M).A = (SAT M).B;
    thus (SAT M).(A <=> B) = (SAT M).A <=> (SAT M).B by semequ2
    .=1 by A3,A2;
  end;

definition let M,p;
  pred M |= p means
  (SAT M).p=1;
end;

definition let M,F;
  pred M |= F means
  for p st p in F holds M|=p;
end;

definition let F,p;
  pred F |= p means
  for M st M |= F holds M |= p;
end;

definition let A;
  attr A is tautology means
  for M holds (SAT M).A=1;
end;

theorem tautsat:
  A is tautology iff {}PL-WFF |= A
  proof
    hereby
      assume A1: A is tautology;
      assume not {}PL-WFF |= A; then
      consider M such that
A3:   M |= {}PL-WFF & not M |= A;
      thus contradiction by A3,A1;
    end;
    assume
A4: {}PL-WFF |= A;
    assume not A is tautology;then
    consider M such that
A5: not (SAT M).A=1;
    M |= {}PL-WFF;then
    M |= A by A4;
    hence contradiction by A5;
  end;

theorem Th15:
  p => (q => p) is tautology
  proof
    let M;
    thus (SAT M).(p => (q => p)) = (SAT M).p => (SAT M).(q => p) by Def11
   .= (SAT M).p => ((SAT M).q => (SAT M).p) by Def11
   .= 1 by XBOOLEAN:104;
  end;

theorem Th16:
  (p => (q => r)) => ((p => q) => (p => r)) is tautology
  proof
   let M;
   thus (SAT M).((p => (q => r)) => ((p=>q)=>(p=>r)))
   = (SAT M).(p => (q => r)) => (SAT M).((p=>q)=>(p=>r)) by Def11
   .= ((SAT M).p => (SAT M).(q => r)) => (SAT M).((p=>q)=>(p=>r)) by Def11
   .= ((SAT M).p => ((SAT M).q => (SAT M).r))
   => (SAT M).((p=>q)=>(p=>r)) by Def11
   .= ((SAT M).p => ((SAT M).q => (SAT M).r))
   => ((SAT M).(p=>q)=>(SAT M).(p=>r)) by Def11
   .= ((SAT M).p => ((SAT M).q => (SAT M).r))
   => (((SAT M).p=>(SAT M).q)=>(SAT M).(p=>r)) by Def11
   .= ((SAT M).p => ((SAT M).q => (SAT M).r))
   => (((SAT M).p=>(SAT M).q)=>((SAT M).p=>(SAT M).r)) by Def11
   .= 1 by XBOOLEAN:109;
 end;

theorem Th17:
 ('not' q => 'not' p) => (('not' q => p) => q) is tautology
 proof
   let M;
   thus (SAT M).(('not' q => 'not' p) => (('not' q => p)=>q))
   = (SAT M).('not' q => 'not' p) => (SAT M).(('not' q => p)=>q) by Def11
   .= ((SAT M).('not' q) => (SAT M).('not' p)) =>
   (SAT M).(('not' q => p)=>q) by Def11
   .= (('not' (SAT M).q) => ((SAT M).('not' p))) =>
   (SAT M).(('not' q => p)=>q) by semnot2
   .= (('not' (SAT M).q) => ('not' (SAT M).p)) =>
   (SAT M).(('not' q => p)=>q) by semnot2
   .= (('not' (SAT M).q) => ('not' (SAT M).p)) =>
   ((SAT M).('not' q => p)=>(SAT M).q) by Def11
   .= (('not' (SAT M).q) => ('not' (SAT M).p)) =>
   (((SAT M).('not' q) => (SAT M).p)=>(SAT M).q) by Def11
   .= (('not' (SAT M).q) => ('not' (SAT M).p)) =>
   ((('not' (SAT M).q) => (SAT M).p)=>(SAT M).q) by semnot2
   .=1 by Th17a;
 end;

theorem
  (p => q) => (('not' q) => 'not' p) is tautology
 proof
   let M;
   thus (SAT M).((p => q) => (('not' q) => 'not' p)) =
   (SAT M).(p => q) => (SAT M).(('not' q) => 'not' p) by Def11
   .= ((SAT M).p => (SAT M).q) => (SAT M).(('not' q) => 'not' p) by Def11
   .= ((SAT M).p => (SAT M).q) => ((SAT M).('not' q) => (SAT M).('not' p))
   by Def11
   .= ((SAT M).p => (SAT M).q) => (('not' (SAT M).q) => (SAT M).('not' p))
   by semnot2
   .= ((SAT M).p => (SAT M).q) => (('not' (SAT M).q) => ('not' (SAT M).p))
   by semnot2
   .= 1 by th4;
 end;

theorem
  (p '&' q) => p is tautology
  proof
    let M;
    thus (SAT M).((p '&' q) => p) = (SAT M).(p '&' q) => (SAT M).p by Def11
    .= ((SAT M).p '&' (SAT M).q) => (SAT M).p by semcon2
    .= 1 by th1;
  end;

theorem
  (p '&' q) => q is tautology
  proof
    let M;
    thus (SAT M).((p '&' q) => q) = (SAT M).(p '&' q) => (SAT M).q by Def11
    .= ((SAT M).p '&' (SAT M).q) => (SAT M).q by semcon2
    .= 1 by th1;
  end;

theorem
  p => (p 'or' q) is tautology
  proof
    let M;
    thus (SAT M).(p => (p 'or' q)) = (SAT M).p => (SAT M).(p 'or' q) by Def11
    .= (SAT M).p => ((SAT M).p 'or' (SAT M).q) by semdis2
    .= 1 by XBOOLEAN:123;
  end;

theorem
  q => (p 'or' q) is tautology
  proof
    let M;
    thus (SAT M).(q => (p 'or' q)) = (SAT M).q => (SAT M).(p 'or' q) by Def11
    .= (SAT M).q => ((SAT M).p 'or' (SAT M).q) by semdis2
    .= 1 by XBOOLEAN:123;
  end;

theorem
  (p '&' q) <=> (q '&' p) is tautology
  proof
    let M;
    thus (SAT M).((p '&' q) <=> (q '&' p)) =
    (SAT M).(p '&' q) <=> (SAT M).(q '&' p) by semequ2
    .= ((SAT M).p '&' (SAT M).q) <=> (SAT M).(q '&' p) by semcon2
    .= ((SAT M).p '&' (SAT M).q) <=> ((SAT M).q '&' (SAT M).p) by semcon2
    .= 1 by th6;
  end;

theorem
  (p 'or' q) <=> (q 'or' p) is tautology
  proof
    let M;
    thus (SAT M).((p 'or' q) <=> (q 'or' p)) =
    (SAT M).(p 'or' q) <=> (SAT M).(q 'or' p) by semequ2
    .= ((SAT M).p 'or' (SAT M).q) <=> (SAT M).(q 'or' p) by semdis2
    .= ((SAT M).p 'or' (SAT M).q) <=> ((SAT M).q 'or' (SAT M).p) by semdis2
    .= 1 by th6a;
  end;

theorem
  (p '&' q '&' r) <=> (p '&' (q '&' r)) is tautology
  proof
    let M;
    thus (SAT M).((p '&' q '&' r) <=> (p '&' (q '&' r)))
    = (SAT M).(p '&' q '&' r) <=> (SAT M).(p '&' (q '&' r)) by semequ2
    .= (SAT M).(p '&' q) '&' (SAT M).r <=> (SAT M).(p '&' (q '&' r))
    by semcon2
    .= (SAT M).(p '&' q) '&' (SAT M).r
    <=> ((SAT M).p '&' (SAT M).(q '&' r)) by semcon2
    .= (SAT M).(p '&' q) '&' (SAT M).r
    <=> ((SAT M).p '&' ((SAT M).q '&' (SAT M).r)) by semcon2
    .= (SAT M).p '&' (SAT M).q '&' (SAT M).r
    <=> ((SAT M).p '&' ((SAT M).q '&' (SAT M).r)) by semcon2
    .= 1 by th7;
end;

theorem
  (p 'or' q 'or' r) <=> (p 'or' (q 'or' r)) is tautology
  proof
    let M;
    thus (SAT M).((p 'or' q 'or' r) <=> (p 'or' (q 'or' r)))
    = (SAT M).(p 'or' q 'or' r) <=> (SAT M).(p 'or' (q 'or' r)) by semequ2
    .= (SAT M).(p 'or' q) 'or' (SAT M).r <=> (SAT M).(p 'or' (q 'or' r))
    by semdis2
    .= (SAT M).(p 'or' q) 'or' (SAT M).r
    <=> ((SAT M).p 'or' (SAT M).(q 'or' r)) by semdis2
    .= (SAT M).(p 'or' q) 'or' (SAT M).r
    <=> ((SAT M).p 'or' ((SAT M).q 'or' (SAT M).r)) by semdis2
    .= (SAT M).p 'or' (SAT M).q 'or' (SAT M).r
    <=> ((SAT M).p 'or' ((SAT M).q 'or' (SAT M).r)) by semdis2
    .= 1 by th7a;
end;

theorem
  p '&' (q 'or' r) <=> ((p '&' q) 'or' (p '&' r)) is tautology
  proof
    let M;
    thus (SAT M).(p '&' (q 'or' r) <=> ((p '&' q) 'or' (p '&' r)))
    = (SAT M).(p '&' (q 'or' r)) <=>
    (SAT M).((p '&' q) 'or' (p '&' r)) by semequ2
    .= (SAT M).p '&' (SAT M).(q 'or' r) <=>
    (SAT M).((p '&' q) 'or' (p '&' r)) by semcon2
    .= (SAT M).p '&' ((SAT M).q 'or' (SAT M).r) <=>
    (SAT M).((p '&' q) 'or' (p '&' r)) by semdis2
    .= (SAT M).p '&' ((SAT M).q 'or' (SAT M).r) <=>
    ((SAT M).(p '&' q) 'or' (SAT M).(p '&' r)) by semdis2
    .= (SAT M).p '&' ((SAT M).q 'or' (SAT M).r) <=>
    ((SAT M).p '&' (SAT M).q 'or' (SAT M).(p '&' r)) by semcon2
    .= (SAT M).p '&' ((SAT M).q 'or' (SAT M).r) <=>
    ((SAT M).p '&' (SAT M).q 'or' ((SAT M).p '&' (SAT M).r)) by semcon2
    .= 1 by th8;
end;

theorem
  p 'or' (q '&' r) <=> ((p 'or' q) '&' (p 'or' r)) is tautology
  proof
    let M;
    thus (SAT M).(p 'or' (q '&' r) <=> ((p 'or' q) '&' (p 'or' r)))
    = (SAT M).(p 'or' (q '&' r)) <=>
    (SAT M).((p 'or' q) '&' (p 'or' r)) by semequ2
    .= (SAT M).p 'or' (SAT M).(q '&' r) <=>
    (SAT M).((p 'or' q) '&' (p 'or' r)) by semdis2
    .= (SAT M).p 'or' ((SAT M).q '&' (SAT M).r) <=>
    (SAT M).((p 'or' q) '&' (p 'or' r)) by semcon2
    .= (SAT M).p 'or' ((SAT M).q '&' (SAT M).r) <=>
    ((SAT M).(p 'or' q) '&' (SAT M).(p 'or' r)) by semcon2
    .= (SAT M).p 'or' ((SAT M).q '&' (SAT M).r) <=>
    (((SAT M).p 'or' (SAT M).q) '&' (SAT M).(p 'or' r)) by semdis2
    .= (SAT M).p 'or' ((SAT M).q '&' (SAT M).r) <=>
    (((SAT M).p 'or' (SAT M).q) '&' ((SAT M).p 'or' (SAT M).r)) by semdis2
    .= 1 by th8a;
end;

theorem
  ('not' 'not' p) <=> p is tautology
  proof
    let M;
    thus (SAT M).(('not' 'not' p) <=> p) =
    (SAT M).('not' 'not' p) <=> (SAT M).p by semequ2
    .= ('not' (SAT M).('not' p)) <=> (SAT M).p by semnot2
    .= ('not' 'not' (SAT M).p) <=> (SAT M).p by semnot2
    .=1 by th2;
  end;

theorem
  'not' (p '&' q) <=> ('not' p) 'or' ('not' q) is tautology
 proof
   let M;
   thus (SAT M).('not' (p '&' q) <=> ('not' p) 'or' ('not' q)) =
   (SAT M).('not' (p '&' q)) <=> (SAT M).(('not' p) 'or' ('not' q)) by semequ2
   .= ('not' (SAT M).(p '&' q)) <=>
   (SAT M).(('not' p) 'or' ('not' q)) by semnot2
   .= ('not' ((SAT M).p '&' (SAT M).q)) <=>
   (SAT M).(('not' p) 'or' ('not' q)) by semcon2
   .= ('not' ((SAT M).p '&' (SAT M).q)) <=>
   ((SAT M).('not' p) 'or' (SAT M).('not' q)) by semdis2
   .= ('not' ((SAT M).p '&' (SAT M).q)) <=>
   ('not' (SAT M).p 'or' (SAT M).('not' q)) by semnot2
   .= ('not' ((SAT M).p '&' (SAT M).q)) <=>
   ('not' (SAT M).p 'or' 'not' (SAT M).q) by semnot2
   .= 1 by th3;
end;

theorem
  'not' (p 'or' q) <=> ('not' p) '&' ('not' q) is tautology
 proof
   let M;
   thus (SAT M).('not' (p 'or' q) <=> ('not' p) '&' ('not' q)) =
   (SAT M).('not' (p 'or' q)) <=> (SAT M).(('not' p) '&' ('not' q)) by semequ2
   .= ('not' (SAT M).(p 'or' q)) <=>
   (SAT M).(('not' p) '&' ('not' q)) by semnot2
   .= ('not' ((SAT M).p 'or' (SAT M).q)) <=>
   (SAT M).(('not' p) '&' ('not' q)) by semdis2
   .= ('not' ((SAT M).p 'or' (SAT M).q)) <=>
   ((SAT M).('not' p) '&' (SAT M).('not' q)) by semcon2
   .= ('not' ((SAT M).p 'or' (SAT M).q)) <=>
   ('not' (SAT M).p '&' (SAT M).('not' q)) by semnot2
   .= ('not' ((SAT M).p 'or' (SAT M).q)) <=>
   ('not' (SAT M).p '&' 'not' (SAT M).q) by semnot2
   .= 1 by th3a;
end;

theorem
  p => q => (p => r => (p => (q '&' r))) is tautology
  proof
    let M;
    thus (SAT M).(p => q => (p => r => (p => (q '&' r))))
= (SAT M).(p =>q) => (SAT M).(p => r => (p => (q '&' r))) by Def11
.= (SAT M).p => (SAT M).q => ((SAT M).(p => r => (p => (q '&' r)))) by Def11
.= (SAT M).p => (SAT M).q
=> ((SAT M).(p => r) => (SAT M).(p => (q '&' r))) by Def11
.= (SAT M).p => (SAT M).q =>
((SAT M).p => (SAT M).r => (SAT M).(p => (q '&' r))) by Def11
.= (SAT M).p => (SAT M).q =>
((SAT M).p => (SAT M).r => ((SAT M).p => (SAT M).(q '&' r))) by Def11
.= (SAT M).p => (SAT M).q =>
((SAT M).p => (SAT M).r => ((SAT M).p => ((SAT M).q '&' (SAT M).r))) by semcon2
.= 1 by th5;
end;

theorem
  p => r => (q => r => ((p 'or' q) => r)) is tautology
  proof
    let M;
A3: (SAT M).(q => r => ((p 'or' q) => r))
    = (SAT M).(q => r) => (SAT M).((p 'or' q) => r) by Def11
    .= (SAT M).q => (SAT M).r => (SAT M).((p 'or' q) => r) by Def11
    .= (SAT M).q => (SAT M).r => ((SAT M).(p 'or' q) => (SAT M).r) by Def11
    .= (SAT M).q => (SAT M).r => (((SAT M).p 'or' (SAT M).q) => (SAT M).r)
    by semdis2;
    thus (SAT M).(p => r => (q => r => ((p 'or' q) => r)))
    = (SAT M).(p => r) => (SAT M).(q => r => ((p 'or' q) => r)) by Def11
    .= (SAT M).p => (SAT M).r => ((SAT M).q => (SAT M).r
    => (((SAT M).p 'or' (SAT M).q) => (SAT M).r)) by Def11,A3
    .= 1 by th5a;
  end;

theorem th24:
  F |= A & F |= A => B implies F |= B
  proof
    assume that
A1: F|=A and
A2: F|=A=>B;
    let M;
    assume
A3: M|=F;then
    M |= A=>B by A2;
    then A4: (SAT M).A=>(SAT M).B=1 by Def11;
    M |= A by A1,A3;
    hence (SAT M).B=1 by A4;
  end;

begin

definition let D be set;
  attr D is with_PL_axioms means :withplax:
  for p,q,r holds
  (p => (q => p) in D
  & (p => (q => r)) => ((p=>q)=>(p=>r)) in D
  & ('not' q => 'not' p) => (('not' q => p)=>q) in D);
end;

definition
  func PL_axioms -> Subset of PL-WFF means :defplax:
  it is with_PL_axioms &
  for D be Subset of PL-WFF st D is with_PL_axioms holds it c=D;
 existence
 proof
   defpred S1[object] means
   for D being set st D is with_PL_axioms holds$1 in D;
   consider D0 being set such that
A1: for x being object
    holds(x in D0 iff x in PL-WFF & S1[x]) from XBOOLE_0:sch 1;
    D0 c=PL-WFF by A1;
    then reconsider D0 as Subset of PL-WFF;
    take D0;
    thus D0 is with_PL_axioms
    proof
      let p,q,r be Element of PL-WFF;
      for D being set st D is with_PL_axioms holds p => (q => p) in D;
      hence p => (q => p) in D0 by A1;
      for D being set st D is with_PL_axioms holds
      (p => (q => r)) => ((p=>q)=>(p=>r)) in D;
      hence (p => (q => r)) => ((p=>q)=>(p=>r)) in D0 by A1;
      for D being set st D is with_PL_axioms holds
      ('not' q => 'not' p) => (('not' q => p)=>q) in D;
      hence ('not' q => 'not' p) => (('not' q => p)=>q) in D0 by A1;
    end;
    let D be Subset of PL-WFF;
    assume A2: D is with_PL_axioms;
    let x be object;
    assume x in D0;
    hence x in D by A1,A2;
  end;
  uniqueness
  proof
    let D1,D2 be Subset of PL-WFF;
    assume(D1 is with_PL_axioms) & (for D be Subset of PL-WFF st D is
    with_PL_axioms holds D1 c=D) & D2 is with_PL_axioms & for D be Subset of
    PL-WFF st D is with_PL_axioms holds D2 c=D;
    then D1 c=D2 & D2 c=D1;
    hence D1=D2 by XBOOLE_0:def 10;
  end;
end;

registration
  cluster PL_axioms -> with_PL_axioms;
  coherence by defplax;
end;

definition let p,q,r;
  pred p,q MP_rule r means
  q = p => r;
end;

registration
  cluster PL_axioms -> non empty;
  coherence by withplax;
end;

definition let A;
  attr A is axpl1 means :defaxpl1:
  ex p,q st A = p => (q => p);
  attr A is axpl2 means :defaxpl2:
  ex p,q,r st A = (p => (q => r)) => ((p=>q)=>(p=>r));
  attr A is axpl3 means :defaxpl3:
  ex p,q st A = ('not' q => 'not' p) => (('not' q => p)=>q);
end;

theorem Th36:
  for A be Element of PL_axioms holds
    (A is axpl1 or A is axpl2 or A is axpl3)
 proof
  defpred P1[Element of PL_axioms] means
  $1 is axpl1 or $1 is axpl2 or $1 is axpl3;
  set X={p where p is Element of PL_axioms:P1[p]};
  X c=PL-WFF
  proof
   let x be object;
   assume x in X;
   then ex p be Element of PL_axioms st x=p & P1[p];
   hence x in PL-WFF;
  end;
  then reconsider X as Subset of PL-WFF;
  let A be Element of PL_axioms;
  X is with_PL_axioms
  proof
   let p,q,r;
   thus p => (q => p) in X
   proof
    reconsider pp=p =>(q =>p) as Element of PL_axioms by withplax;
    P1[pp] by defaxpl1;
    hence thesis;
   end;
   thus (p => (q => r)) => ((p=>q)=>(p=>r)) in X
   proof
    reconsider pp=(p => (q => r)) => ((p=>q)=>(p=>r))
    as Element of PL_axioms by withplax;
    P1[pp] by defaxpl2;
    hence thesis;
   end;
   thus ('not' q => 'not' p) => (('not' q => p)=>q) in X
   proof
    reconsider pp=('not' q => 'not' p) => (('not' q => p)=>q)
    as Element of PL_axioms by withplax;
    P1[pp] by defaxpl3;
    hence thesis;
   end;
  end;
  then A in PL_axioms & PL_axioms c=X by defplax;
  then A in X;
  then ex p be Element of PL_axioms st A=p & P1[p];
  hence P1[A];
 end;

theorem Th37:
  A is axpl1 or A is axpl2 or A is axpl3 implies F |= A
 proof
  assume A1: A is axpl1 or A is axpl2 or A is axpl3;
  let M;
  assume M|=F;
  per cases by A1;
  suppose A is axpl1;
   then consider p,q be Element of PL-WFF such that
A2: A=p => (q => p);
    A is tautology by Th15,A2;
    hence thesis;
  end;
  suppose A is axpl2;
   then consider p,q,r be Element of PL-WFF such that
    A3: A=(p => (q => r)) => ((p=>q)=>(p=>r));
    A is tautology by Th16,A3;
    hence thesis;
  end;
  suppose A is axpl3;
   then consider p,q be Element of PL-WFF such that
    A4: A=('not' q => 'not' p) => (('not' q => p)=>q);
    A is tautology by Th17,A4;
    hence thesis;
  end;
 end;

definition let i be Nat,f,F;
  pred prc f,F,i means :defprc:
  f.i in PL_axioms or f.i in F or
  (ex j,k be Nat st 1<=j & j<i & 1<=k & k<i &
  (f/.j,f/.k MP_rule f/.i));
end;

definition let F,p;
  pred F |- p means
  ex f st f.len f=p & 1<=len f &
  for i be Nat st 1<=i & i<=len f holds prc f,F,i;
end;

theorem Th38:
  for i,n be Nat st
  n+len f<=len f2 & (for k be Nat st 1<=k & k<=len f holds f.k=f2.(k+n)) &
  1 <= i <= len f holds prc f,F,i implies prc f2,F,(i+n)
 proof
  let i,n be Nat;
  assume that
   A1: n+len f<=len f2 and
   A2: for k be Nat st 1<=k & k<=len f holds f.k=f2.(k+n) and
   A3: 1<=i and
   A4: i<=len f;
  i+n<=len f+n by A4,XREAL_1:6;
  then A5: i+n<=len f2 by A1,XXREAL_0:2;
  A6: f/.i=f.i by A3,A4,LTLAXIO5:1
   .=f2.(i+n) by A2,A3,A4
   .=f2/.(i+n) by A3,A5,LTLAXIO5:1,NAT_1:12;
  assume A7: prc f,F,i;
  per cases by A7;
  suppose f.i in PL_axioms;
   hence prc f2,F,i+n by A2,A3,A4;
  end;
  suppose f.i in F;
   hence prc f2,F,i+n by A2,A3,A4;
  end;
  suppose ex j,k be Nat st 1<=j & j<i & 1<=k & k<i & f/.j,f/.k MP_rule f/.i;
   then consider j,k be Nat such that
    A8: 1<=j and
    A9: j<i and
    A10: 1<=k and
    A11: k<i and
    A12: f/.j,f/.k MP_rule f/.i;
   A13: 1<=j+n & j+n<i+n by A8,A9,NAT_1:12,XREAL_1:8;
   A14: k<=len f by A4,A11,XXREAL_0:2;
   then k+n<=len f+n by XREAL_1:6;
   then A15: k+n<=len f2 by A1,XXREAL_0:2;
   A16: j<=len f by A4,A9,XXREAL_0:2;
   then j+n<=len f+n by XREAL_1:6;
   then A17: j+n<=len f2 by A1,XXREAL_0:2;
   A18: f/.k=f.k by A10,A14,LTLAXIO5:1
    .=f2.(k+n) by A2,A10,A14
    .=f2/.(k+n) by A10,A15,LTLAXIO5:1,NAT_1:12;
   A19: 1<=k+n & k+n<i+n by A10,A11,NAT_1:12,XREAL_1:8;
   f/.j=f.j by A8,A16,LTLAXIO5:1
    .=f2.(j+n) by A2,A8,A16
    .=f2/.(j+n) by A8,A17,LTLAXIO5:1,NAT_1:12;
   hence prc f2,F,i+n by A6,A12,A13,A19,A18;
  end;
 end;

theorem Th39:
  f2=f^f1 & 1<=len f & 1<=len f1 &
  (for i be Nat st 1<=i & i<=len f holds prc f,F,i) &
  (for i be Nat st 1<=i & i<=len f1 holds prc f1,F,i) implies
  for i be Nat st 1<=i & i<=len f2 holds prc f2,F,i
 proof
  assume that
   A1: f2=f^f1 and
   1<=len f and
   1<=len f1 and
   A2: for i be Nat st 1<=i & i<=len f holds prc f,F,i and
   A3: for i be Nat st 1<=i & i<=len f1 holds prc f1,F,i;
  A4: len f2=len f+len f1 by A1,FINSEQ_1:22;
  A5: for k be Nat st 1<=k & k<=len f1 holds f1.k=f2.(k+len f)
    by A1,FINSEQ_1:65;
  let i be Nat;
  assume that
   A6: 1<=i and
   A7: i<=len f2;
  per cases by NAT_1:13;
  suppose A8: i<=len f;
   then A9: f/.i=f.i by A6,LTLAXIO5:1
    .=f2.i by A1,A6,A8,FINSEQ_1:64
    .=f2/.i by A6,A7,LTLAXIO5:1;
   per cases by A2,A6,A8,defprc;
   suppose f.i in PL_axioms;
    hence prc f2,F,i by A1,A6,A8,FINSEQ_1:64;
   end;
   suppose f.i in F;
    hence prc f2,F,i by A1,A6,A8,FINSEQ_1:64;
   end;
   suppose ex j,k be Nat st 1<=j & j<i & 1<=k & k<i & f/.j,f/.k MP_rule f/.i;
    then consider j,k be Nat such that
     A10: 1<=j and
     A11: j<i and
     A12: 1<=k and
     A13: k<i and
     A14: f/.j,f/.k MP_rule f/.i;
    A15: k<=len f by A8,A13,XXREAL_0:2;
    then A16: k<=len f2 by A4,NAT_1:12;
    A17: f/.k=f.k by A12,A15,LTLAXIO5:1
     .=f2.k by A1,A12,A15,FINSEQ_1:64
     .=f2/.k by A12,A16,LTLAXIO5:1;
    A18: j<=len f by A8,A11,XXREAL_0:2;
    then A19: j<=len f2 by A4,NAT_1:12;
    f/.j=f.j by A10,A18,LTLAXIO5:1
     .=f2.j by A1,A10,A18,FINSEQ_1:64
     .=f2/.j by A10,A19,LTLAXIO5:1;
    hence prc f2,F,i by A9,A10,A11,A12,A13,A14,A17;
   end;
  end;
  suppose A25: len f+1<=i;
   set i1=i-' len f;
   i<=len f+len f1 by A1,A7,FINSEQ_1:22;
   then i-' len f<=len f+len f1-' len f by NAT_D:42;
   then A26: i1<=len f1 by NAT_D:34;
   1<=i1 by A25,NAT_D:55;
   then prc f2,F,i1+len f by A3,A4,A5,A26,Th38;
   hence prc f2,F,i by A25,NAT_D:43,55;
  end;
 end;

theorem Th40:
  (f=f1^<*p*> & 1<=len f1 &
  for i be Nat st 1<=i & i<=len f1 holds prc f1,F,i) &
  prc f,F,len f implies (for i be Nat st 1<=i & i<=len f holds prc f,F,i) &
  F|-p
 proof
   assume that
   A1: f=f1^<*p*> and
   1<=len f1 and
   A2: for i be Nat st 1<=i & i<=len f1 holds prc f1,F,i;
  A3: len f=(len f1+len<*p*>) by A1,FINSEQ_1:22
   .=len f1+1 by FINSEQ_1:39;
  assume A4: prc f,F,len f;
  A5: 0+len f1<=len f by A3,NAT_1:12;
  A6: now let i be Nat;
   assume that
    A7: 1<=i and
    A8: i<=len f;
   A9: i<len f1+1 or i=len f1+1 by A3,A8,XXREAL_0:1;
   A10: for k be Nat st 1<=k & k<=len f1 holds f1.k=f.(k+0) by A1,FINSEQ_1:64;
   per cases by A3,A9,NAT_1:13;
   suppose i<=len f1;
    then prc f,F,(i+0) by A2,A5,A7,A10,Th38;
    hence prc f,F,i;
   end;
   suppose i=len f;
    hence prc f,F,i by A4;
   end;
  end;
  hence for i be Nat st 1<=i & i<=len f holds prc f,F,i;
  f.len f=f.(len f1+len<*p*>) by A1,FINSEQ_1:22
   .=f.(len f1+1) by FINSEQ_1:39
   .=p by A1,FINSEQ_1:42;
  hence F|-p by A3,XREAL_1:31,A6;
 end;

theorem th42:
  p in PL_axioms or p in F implies F |- p
 proof
  defpred P1[set,set] means $2=p;
  A1: for k being Nat st k in Seg 1 holds ex x being Element of
  PL-WFF st P1[k,x];
  consider f such that
   A2: dom f=Seg 1 & for k being Nat st k in Seg 1 holds P1[k,f.k]
   from FINSEQ_1:sch 5(A1);
  A3: len f=1 by A2,FINSEQ_1:def 3;
  1 in Seg 1;
  then A4: f.1=p by A2;
  assume A5: p in PL_axioms or p in F;
  for j be Nat st 1<=j & j<=len f holds prc f,F,j
  proof
   let j be Nat;
   assume A6: 1<=j & j<=len f;
   per cases by A5;
   suppose p in PL_axioms;
    hence thesis by A3,A4,A6,XXREAL_0:1;
   end;
   suppose p in F;
    hence thesis by A3,A4,A6,XXREAL_0:1;
   end;
  end;
  hence F|-p by A3,A4;
 end;

theorem th43:
  F |- p & F |- p => q implies F |- q
 proof
  assume F|-p;
  then consider f such that
   A1: f.len f=p and
   A2: 1<=len f and
   A3: for i be Nat st 1<=i & i<=len f holds prc f,F,i;
  set j=len f;
  assume F|-p=>q;
  then consider f1 such that
   A4: f1.len f1=p=>q and
   A5: 1<=len f1 and
   A6: for i be Nat st 1<=i & i<=len f1 holds prc f1,F,i;
  A7: 1<=len f+len f1 by A2,NAT_1:12;
  set g=f^f1^<*q*>;
  A8: g=f^(f1^<*q*>) by FINSEQ_1:32;
  A9: for i be Nat st 1<=i & i<=len f1 holds g.(len f+i)=f1.i
  proof
   let i be Nat;
   assume that
    A10: 1<=i and
    A11: i<=len f1;
   len(f1^<*q*>)=len f1+len<*q*> by FINSEQ_1:22
    .=len f1+1 by FINSEQ_1:39;
   then i<=len(f1^<*q*>) by A11,NAT_1:12;
   hence g.(len f+i)=(f1^<*q*>).i by A8,A10,FINSEQ_1:65
    .=f1.i by A10,A11,FINSEQ_1:64;
  end;
  A12: len g=len(f^f1)+len<*q*> by FINSEQ_1:22
   .=len(f^f1)+1 by FINSEQ_1:39;
  then A13: len g=len f+len f1+1 by FINSEQ_1:22;
  then len g=len f+(len f1+1);
  then A14: j<len g by NAT_1:16;
  then A15: g/.j=g.j by A2,LTLAXIO5:1
   .=p by A1,A2,A8,FINSEQ_1:64;
  set k=len f+len f1;
  A16: 1<=k by A2,NAT_1:12;
U1: g.len g=q & 1<=len g by A12,FINSEQ_1:42,NAT_1:11;
  A18: k<len g by A13,NAT_1:16;
  then g/.k=g.k by A2,LTLAXIO5:1,NAT_1:12
   .=p=>q by A4,A5,A9;
  then g/.j,g/.k MP_rule g/.len g by A15,LTLAXIO5:1,U1;
  then A19: len(f^f1)=len f+len f1 & prc g,F,len g by A2,A14,A16,A18,
FINSEQ_1:22;
  for i be Nat st 1<=i & i<=len(f^f1) holds prc f^f1,F,i by A2,A3,A5,A6,Th39;
  hence F|-q by A7,A19,Th40;
 end;

theorem monmp:
  F c= G implies (F |- p implies G |- p)
  proof
    assume Z0: F c= G;
    assume F |- p;then
    consider f such that C1: f.len f = p & 1<=len f &
    for k be Nat st 1<=k<=len f holds prc f,F,k;
C17: len f in dom f by C1,FINSEQ_3:25;
     defpred P3[Nat] means 1 <= $1 <= len f implies G |- f/.$1;
C2:  now
       let s be Nat;
       assume C5: for n being Nat st n < s holds P3[n];
       per cases by NAT_1:14;
       suppose s = 0;
        hence P3[s];
       end;
       suppose not s < 1;
         assume C7: 1 <= s <= len f;then
C3:      prc f,F,s by C1;
C16:     s in dom f by C7,FINSEQ_3:25;
         thus G |- f/.s
          proof
            per cases by C3;
            suppose f.s in PL_axioms;then
              f/.s in PL_axioms by C16,PARTFUN1:def 6;
              hence G |- f/.s by th42;
            end;
            suppose f.s in F;then
              f/.s in F by C16,PARTFUN1:def 6;
              hence G |- f/.s by th42,Z0;
            end;
            suppose ex j,k be Nat st 1<=j & j<s & 1<=k & k<s &
              (f/.j,f/.k MP_rule f/.s);then
              consider j,k be Nat such that
              C4: 1<=j & j<s & 1<=k & k<s & (f/.j,f/.k MP_rule f/.s);
              C6: P3[j] by C5,C4;
              P3[k] by C4,C5;
              hence G |- f/.s by th43,C7,XXREAL_0:2,C4,C6;
            end;
          end;
        end;
      end;
      for k be Nat holds P3[k] from NAT_1:sch 4(C2);then
      G |- f/.(len f) by C1;
      hence G |- p by C1,C17,PARTFUN1:def 6;
  end;

begin

::#INSERT: Soundness theorem
theorem sth:
  F |- A implies F |= A
 proof
  assume F|-A;
  then consider f such that
   A1: f.len f=A and
   A2: 1<=len f and
   A3: for i be Nat st 1<=i & i<=len f holds prc f,F,i;
  defpred P[Nat] means
   1<=$1 & $1<=len f implies F|=f/.$1;
  A4: for i being Nat st for j being Nat st j<i holds P[j] holds P[i]
  proof
   let i be Nat;
   assume A5: for j being Nat st j<i holds P[j];
   per cases by NAT_1:14;
   suppose i=0;
    hence P[i];
   end;
   suppose not i<1;
    assume that
     A6: 1<=i and
     A7: i<=len f;
    per cases by A3,A6,A7,defprc;
    suppose f.i in PL_axioms;
     then f/.i in PL_axioms by A6,A7,LTLAXIO5:1;then
     f/.i is axpl1 or f/.i is axpl2 or f/.i is axpl3 by Th36;
     hence F|=f/.i by Th37;
    end;
    suppose f.i in F;
     then A9: f/.i in F by A6,A7,LTLAXIO5:1;
     thus F|=f/.i
     proof
      let M;
      assume M|=F;
      hence M|=f/.i by A9;
     end;
    end;
    suppose ex j,k be Nat st 1<=j & j<i & 1<=k & k<i & f/.j,f/.k MP_rule f/.i;
     then consider j,k be Nat such that
      A10: 1<=j and
      A11: j<i and
      A12: 1<=k and
      A13: k<i and
      A14: f/.j,f/.k MP_rule f/.i;
U1:   k<=len f by A7,A13,XXREAL_0:2;
     A16: j<=len f by A7,A11,XXREAL_0:2;
     F|=f/.j=>f/.i by A5,A12,A13,A14,U1;
      hence F|=f/.i by A5,A10,A11,A16,th24;
    end;
   end;
  end;
  A22: for i be Nat holds P[i] from NAT_1:sch 4(A4);
  f/.len f=A by A1,A2,LTLAXIO5:1;
  hence F|=A by A2,A22;
 end;

theorem thaa:
  F |- A => A
  proof
    A=>((A=>A)=>A) in PL_axioms by withplax;then
A1: F |- A=>((A=>A)=>A) by th42;
    A=>(A=>A) in PL_axioms by withplax;then
A2: F |- A=>(A=>A) by th42;
    (A=>((A=>A)=>A)) => ((A=>(A=>A))=>(A=>A)) in PL_axioms by withplax;then
    F |- (A=>((A=>A)=>A)) => ((A=>(A=>A))=>(A=>A)) by th42;then
    F |- (A=>(A=>A))=>(A=>A) by th43,A1;
    hence F|- A=>A by th43,A2;
end;

::$N Deduction theorem
theorem ded:
  F \/ {A} |- B implies F |- A => B
proof
  assume F \/ {A} |- B;then
  consider f such that
A1: f.len f = B and
A2: 1<=len f and
A3: for i be Nat st 1<=i & i<=len f holds prc f,F \/ {A},i;
    defpred P[Nat] means
    1<=$1 & $1<=len f implies F |- A => f/.$1;
A4: for i being Nat st for j being Nat st j<i holds P[j] holds P[i]
    proof
      let i be Nat;
      assume A5: for j be Nat st j<i holds P[j];
      per cases by NAT_1:14;
      suppose i=0;
        hence P[i];
      end;
      suppose not i<1;
        assume that
A6:     1<=i and
A7:     i<=len f;
        per cases by A3,A6,A7,defprc;
        suppose A8: f.i in PL_axioms;
          f/.i => (A=>f/.i) in  PL_axioms by withplax;then
A9:       F |- f/.i => (A=>f/.i) by th42;
          f/.i in PL_axioms by A6,A7,A8,LTLAXIO5:1;then
          F |- f/.i by th42;
          hence thesis by th43,A9;
        end;
        suppose A10: f.i in F \/ {A};
          per cases by A10,XBOOLE_0:def 3;
          suppose A11: f.i in F;
            f/.i => (A=>f/.i) in  PL_axioms by withplax;then
            A12: F |- f/.i=>(A=>f/.i) by th42;
            f/.i in F by A6,A7,A11,LTLAXIO5:1;then
            F |- f/.i by th42;
            hence thesis by th43,A12;
          end;
          suppose f.i in {A};then
            f.i=A by TARSKI:def 1;then
            f/.i=A by A6,A7,LTLAXIO5:1;
            hence thesis by thaa;
          end;
        end;
        suppose ex j,k be Nat st 1<=j & j<i & 1<=k & k<i &
          f/.j,f/.k MP_rule f/.i;
          then consider j,k be Nat such that
A15:      1<=j and
A16:      j<i and
A17:      1<=k and
A18:      k<i and
A19:      f/.j,f/.k MP_rule f/.i;
          j<=len f by A7,A16,XXREAL_0:2;then
A20:      F|- A => f/.j by A5,A15,A16;
          k<=len f by A7,A18,XXREAL_0:2;then
A21:      F|- A => f/.k by A5,A17,A18;
          (A=>(f/.j=>f/.i))=>((A=>f/.j)=>(A=>f/.i)) in PL_axioms
          by withplax;then
A23:      F |- (A=>(f/.j=>f/.i))=>((A=>f/.j)=>(A=>f/.i)) by th42;
            F|- (A=>f/.j)=>(A=>f/.i) by A23,th43,A21,A19;
            hence F |- A => f/.i by A20,th43;
        end;
      end;
    end;
A37: for i be Nat holds P[i] from NAT_1:sch 4(A4);
     B = f/.len f by A1,A2,LTLAXIO5:1;
     hence F |- A => B by A2,A37;
   end;

theorem
  F |- A => B implies F \/ {A} |- B
 proof
    A in {A} by TARSKI:def 1;
    then A in F\/{A} by XBOOLE_0:def 3;
    then A1: F\/{A}|-A by th42;
    assume F|-A=>B;
    then F\/{A}|-A=>B by monmp,XBOOLE_1:7;
    hence F\/{A}|-B by A1,th43;
  end;

theorem naab:
  F |- ('not' A) => (A => B)
 proof
   set f = F \/ {'not' A} \/ {A};
   A in f by ZFMISC_1:31,XBOOLE_1:11;then
A1: f |- A by th42;
    f = F \/  {A} \/ {'not' A} by XBOOLE_1:4;then
    'not' A in f by ZFMISC_1:31,XBOOLE_1:11;then
A2: f |- 'not' A by th42;
    A => ('not' B => A) in PL_axioms by withplax;then
    f |- A => ('not' B => A) by th42;then
A4: f |- ('not' B => A) by th43,A1;
    'not' A => ('not' B => 'not' A) in PL_axioms by withplax;then
    f |- 'not' A => ('not' B => 'not' A) by th42;then
A3: f |- 'not' B => 'not' A by th43,A2;
    ('not' B => 'not' A) => (('not' B => A)=>B) in PL_axioms by withplax;
    then f |- ('not' B => 'not' A) => (('not' B => A)=>B) by th42;then
    f |- ('not' B => A)=>B by th43,A3;then
    f |- B by th43,A4;then
    F \/ {'not' A} |- A => B by ded;
    hence thesis by ded;
  end;

theorem naa:
  F |- ('not' A => A) => A
  proof
    'not' A => 'not' A => (('not' A => A)=>A) in PL_axioms by withplax;then
A1: F |- ('not' A => 'not' A) => (('not' A => A)=>A) by th42;
    F |- 'not' A => 'not' A by thaa;
    hence thesis by A1,th43;
  end;

begin

definition
  let F;
  attr F is consistent means
  not ex p st (F |- p & F |- 'not' p);
end;

theorem conco:
  F is consistent iff ex A st not F |- A
  proof
    hereby assume
A0:   F is consistent;
      assume
A1:   for A holds F |- A;then
A2:   F |- Prop 0;
      F |- 'not' Prop 0 by A1;
      hence contradiction by A2,A0;
    end;
    assume
A4: ex A st not F |- A;
    assume not F is consistent;then
    consider A such that
A3: F |- A & F |- 'not' A;
    now
      let B;
      F |- 'not' A => (A => B) by naab;then
      F|- A => B by A3,th43;
      hence F |- B by A3,th43;
    end;
    hence contradiction by A4;
  end;

theorem th34:
  not F |- A implies F \/ {'not' A} is consistent
  proof
    assume Z1: not F |- A;
    assume not F \/ {'not' A} is consistent;then
A2: F |- 'not'A => A by ded,conco;
    F |- ('not' A => A) => A by naa;
    hence contradiction by Z1,A2,th43;
  end;

theorem exfin:
  for F,A holds
  F |- A iff ex G st G c= F & G is finite & G |- A
  proof
    let F,A;
    hereby
      assume F |- A;then
      consider f such that
A1:   f.len f=A & 1<=len f &
      for i be Nat st 1<=i & i<=len f holds prc f,F,i;
      deffunc h(Nat) = f.$1;
      set w2 = {i where i is Element of NAT: 1<=i & i<=len f};
      set G = {h(i) where i is Element of NAT: i in w2};
F1:   w2 c= Seg len f
      proof
        let x be object;
        assume x in w2;then
        consider i be Element of NAT such that
F2:     i = x & 1<=i<=len f;
        reconsider i1 = i as Nat;
        thus x in Seg len f by F2;
      end;
A8:   w2 is finite by F1;
A4:   G c= PL-WFF
      proof
        let x be object;
        assume x in G;then
        consider i be Element of NAT such that
A6:     x = h(i) & i in w2;
        consider j be Element of NAT such that
A9:     j = i & 1<=j & j<=len f by A6;
        i in dom f by FINSEQ_3:25,A9;then
A7:     x in rng f by A6,FUNCT_1:def 3;
        rng f c= PL-WFF by FINSEQ_1:def 4;
        hence x in PL-WFF by A7;
      end;
      G is finite from FRAENKEL:sch 21(A8);then
      reconsider G as finite Subset of PL-WFF by A4;
      now
        let i be Nat;
        assume
A6:     1<=i<=len f;then
        prc f,F,i by A1;then
        per cases;
        suppose f.i in PL_axioms;
          hence prc f,F/\G,i;
        end;
        suppose
A5:       f.i in F;
          reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
          i1 in w2 by A6;then
          f.i in G;
          hence prc f,F/\G,i by A5,XBOOLE_0:def 4;
        end;
        suppose ex j,k be Nat
          st 1<=j & j<i & 1<=k & k<i & (f/.j,f/.k MP_rule f/.i);
          hence prc f,F/\G,i;
        end;
      end; then
      F /\ G |- A by A1;
      hence ex G st G c= F & G is finite & G |- A by XBOOLE_1:17;
    end;
    given G such that
A1: G c= F & G is finite & G |- A;
    thus F |- A by A1,monmp;
  end;

theorem finin:
  for F st not F is consistent
  ex G st G is finite & not G is consistent & G c= F
  proof
    let F;
    assume not F is consistent;then
    consider A such that
A1: F |- A & F |- 'not' A;
    consider G such that
A2: G c= F & G is finite & G |- A by exfin,A1;
    consider H such that
A2a: H c= F & H is finite & H |- 'not' A by exfin,A1;
A5: G \/ H |- A by A2,monmp,XBOOLE_1:11;
    G \/ H |- 'not' A by A2a,XBOOLE_1:11,monmp;then
    not G \/ H is consistent by A5;
    hence thesis by XBOOLE_1:8,A2,A2a;
  end;

definition
  let F;
  attr F is maximal means
  for p holds (p in F or 'not' p in F);
end;

theorem incsub:
  F c= G & not F is consistent implies not G is consistent
  proof
    assume A2: F c= G & not F is consistent;then
    consider p such that A1: F |- p & F |- 'not' p;
    G |- p & G |- 'not' p by monmp,A1,A2;
    hence not G is consistent;
  end;

theorem onecon:
  F is consistent & not F \/ {A} is consistent implies
    F \/ {'not' A} is consistent
  proof
    assume A1: F is consistent & not F \/ {A} is consistent;
    assume not F \/ {'not' A} is consistent;then
    A2: F |- ('not'A) => A by ded,conco;
    F |- (('not' A) => A) => A by naa;then
    A6: F |- A by A2,th43;
    F |- 'not' A by A1,conco,ded;
    hence contradiction by A6,A1;
  end;

reserve x,y for set;

::$N Lindenbaum's lemma
theorem th37:
  for F st F is consistent ex G st F c= G & G is consistent & G is maximal
  proof
    let F;
    assume Z0: F is consistent;
    set L = PL-WFF;
    consider R be Relation such that
    A3: R well_orders L by WELLORD2:17;
    R /\ [:L,L:]c=[:L,L:] by XBOOLE_1:17;
    then reconsider R2 = R |_2 L as Relation of L by WELLORD1:def 6;
    R2 well_orders L by A3,PCOMPS_2:1;then
    A76: R2 is_connected_in L by WELLORD1:def 5;
    reconsider RS = RelStr(#L,R2#) as non empty RelStr;
    set cRS = the carrier of RS;
    defpred H[object,object,object] means
    for p for f be PartFunc of cRS,bool L st $1=p & $2=f holds
    ((union(rng (f qua bool L -valued Relation)) \/ F \/ {p} is consistent
    implies $3=union (rng f) \/ F \/ {p}) &
    (not union(rng (f qua bool L -valued Relation)) \/ F \/ {p} is consistent
    implies $3=union (rng f) \/ F));
    A4: for x,y be object st x in cRS & y in PFuncs(cRS, bool L)
    ex z be object st z in bool L &
    H[x,y,z]
    proof
      let x,y be object;
      assume A6: x in cRS & y in PFuncs(cRS, bool L);
      reconsider x1 = x as Element of L by A6;
      reconsider y1 = y as PartFunc of cRS,bool L by A6,PARTFUN1:46;
      per cases;
      suppose
A7: union(rng (y1 qua bool L -valued Relation)) \/ F \/ {x1} is consistent;
        take union(rng y1) \/ F \/ {x1};
        thus thesis by A7;
      end;
      suppose
A7a:not union(rng (y1 qua bool L -valued Relation)) \/ F \/ {x1} is consistent;
        take union(rng y1) \/ F;
        thus thesis by A7a;
      end;
    end;
    consider h be Function of [:cRS,PFuncs(cRS, bool L):],bool L such that
A9: for x,y be object st x in cRS & y in PFuncs(cRS, bool L)
    holds H[x,y,h.(x,y)] from BINOP_1:sch 1(A4);
    R2 well_orders L by A3,PCOMPS_2:1;then
    R2 is_well_founded_in L by WELLORD1:def 5;then
A11: RS is well_founded by WELLFND1:def 2;then
     consider f be Function of cRS, bool L such that
A12: f is_recursively_expressed_by h by WELLFND1:11;
A73: dom f = cRS by FUNCT_2:def 1;
     reconsider G=union (rng (f qua bool L -valued Relation))
       as Subset of PL-WFF;
     set iRS = the InternalRel of RS;
    F6: field R2 = L by A3,PCOMPS_2:1;
A17: for A,B holds [A,B] in R2 implies f.A c= f.B
    proof
      let A,B;assume F3: [A,B] in R2;
      per cases;
      suppose A = B;
        hence thesis;
      end;
      suppose S2: A <> B;
        set frA = f|iRS-Seg A;
        set frB = f|iRS-Seg B;
        iRS is well-ordering by A3,PCOMPS_2:1,WELLORD1:4,F6;then
        F12: iRS-Seg A c= iRS-Seg B by F3,WELLORD1:29,F6;
        iRS-Seg B c= field iRS by WELLORD1:9;then
        F21: frB is Function of iRS-Seg B,bool L by FUNCT_2:32,F6;
        iRS-Seg A c= field iRS by WELLORD1:9;then
        frA is Function of iRS-Seg A,bool L by FUNCT_2:32,F6;then
        F11: dom frA = iRS-Seg A by FUNCT_2:def 1;
        F13: dom frB = iRS-Seg B by FUNCT_2:def 1,F21;
        F18:
        now
          let x;assume F19: x in dom frA;
          thus frA.x = f.x by F19,FUNCT_1:47
            .= frB.x by F13,FUNCT_1:47,F12,F11,F19;
        end;
E1:  union rng frA c= union rng frB by ZFMISC_1:77,rnginc,F18,F11,F12,F13;then
F7:     union rng frA \/ F c= union rng frB \/ F by XBOOLE_1:9;
F15:    A in dom frB by F13,S2,F3,WELLORD1:1;
        frB.A = f.A by FUNCT_1:47,F13,S2,F3,WELLORD1:1;then
        F14: f.A c= union rng frB by ZFMISC_1:74,FUNCT_1:3,F15;
        F18: dom frA c= cRS;
        rng (frA qua bool L -valued Relation) c= bool L;then
E4:     frA in PFuncs(cRS, bool L) by PARTFUN1:def 3,F18;
        F18a: dom frB c= cRS;
        rng (frB qua bool L -valued Relation) c= bool L;then
E2:     frB in PFuncs(cRS, bool L) by PARTFUN1:def 3,F18a;
        per cases;
          suppose union(rng (frA qua bool L -valued Relation)) \/ F \/ {A}
            is consistent;
          per cases;
          suppose
F2a:        union(rng (frB qua bool L -valued Relation)) \/ F \/ {B}
              is consistent;
            F16: f.B = h.(B, frB) by WELLFND1:def 5,A12
            .= union (rng frB) \/ F \/ {B} by A9,E2,F2a;
            thus f.A c= f.B
            proof
              let x be object;assume x in f.A;then
              x in union (rng frB) \/ (F \/ {B}) by XBOOLE_0:def 3,F14;
              hence thesis by F16,XBOOLE_1:4;
            end;
          end;
          suppose
F2b:not union(rng (frB qua bool L -valued Relation)) \/ F \/ {B} is consistent;
            F16b: f.B = h.(B, frB) by WELLFND1:def 5,A12
            .= union (rng frB) \/ F by A9,E2,F2b;
            thus f.A c= f.B by F16b,XBOOLE_0:def 3,F14;
          end;
        end;
        suppose
F2:not union(rng (frA qua bool L -valued Relation)) \/ F \/ {A} is consistent;
          F8: f.A = h.(A, frA) by WELLFND1:def 5,A12
          .= union (rng frA) \/ F by A9,E4,F2;
          per cases;
          suppose F2a: union(rng (frB qua bool L -valued Relation)) \/ F \/ {B}
            is consistent;
            F9: f.B = h.(B, frB) by WELLFND1:def 5,A12
            .= union (rng frB) \/ F \/ {B} by A9,E2,F2a;
            thus f.A c= f.B by F8,F9,XBOOLE_1:10,F7;
          end;
          suppose F2b:
    not union(rng (frB qua bool L -valued Relation)) \/ F \/ {B} is consistent;
            f.B = h.(B, frB) by WELLFND1:def 5,A12
            .= union (rng frB) \/ F by A9,E2,F2b;
            hence f.A c= f.B by F8,XBOOLE_1:9,E1;
          end;
        end;
      end;
    end;
A54: rng f is c=-linear
    proof
      let x,y;assume B2: x in rng f & y in rng f;then
      consider x1 be object such that B3: x1 in dom f & f.x1 = x
        by FUNCT_1:def 3;
      consider y1 be object such that B4: y1 in dom f & f.y1 = y
        by FUNCT_1:def 3,B2;
      reconsider x1,y1 as Element of L by B3,B4;
      per cases;
      suppose x1 = y1;
        hence thesis by B3,B4;
      end;
      suppose B1: x1 <> y1;
        per cases by A76,RELAT_2:def 6,B1;
        suppose [x1,y1] in R2;then
          f.x1 c= f.y1 by A17;
          hence x,y are_c=-comparable by XBOOLE_0:def 9,B3,B4;
        end;
        suppose [y1,x1] in R2;then
          f.y1 c= f.x1 by A17;
          hence x,y are_c=-comparable by XBOOLE_0:def 9,B3,B4;
        end;
      end;
    end;
    defpred S[Element of RS] means f.$1 is consistent;
A26: now
      let x be Element of RS;
      A20: f.x = h.(x, f|iRS-Seg x) by WELLFND1:def 5,A12;
      f|iRS-Seg x in PFuncs(cRS, bool L) by PARTFUN1:45;
      hence H[x,f|iRS-Seg x,f.x] by A20,A9;
    end;
A27: now
      let x be Element of RS;
      reconsider x1 = {x} as Subset of L;
      set fr = f|iRS-Seg x;
      per cases;
      suppose union(rng (fr qua bool L -valued Relation)) \/ F \/ x1
        is consistent;then
        f.x = union(rng fr) \/ F \/ x1 by A26
        .= F \/ (union(rng fr) \/ x1) by XBOOLE_1:4;
        hence F c= f.x by XBOOLE_1:7;
      end;
      suppose not union(rng (fr qua bool L -valued Relation)) \/ F \/ x1
        is consistent;then
        f.x = F \/ union(rng fr) by A26;
        hence F c= f.x by XBOOLE_1:7;
      end;
    end;
A21: for x being Element of RS st
     for y being Element of RS st y <> x & [y,x] in iRS holds S[y] holds S[x]
    proof
      let x be Element of RS;
      assume A41: for y being Element of RS st y <> x & [y,x] in iRS
      holds S[y];
      set fr = f|iRS-Seg x;
      iRS-Seg x c= field iRS by WELLORD1:9; then
C2:   fr is Function of iRS-Seg x,bool L by FUNCT_2:32,F6; then
A39a: dom fr = iRS-Seg x by FUNCT_2:def 1;
      reconsider x1 = {x} as Subset of L;
      per cases;
      suppose union(rng (fr qua bool L -valued Relation)) \/ F \/ x1
        is consistent;
        hence S[x] by A26;
      end;
      suppose C1:not union(rng (fr qua bool L -valued Relation)) \/ F \/ x1
        is consistent;then
A22:    f.x = union(rng fr) \/ F by A26;
        per cases;
        suppose S4: for y be object holds (not [y,x] in iRS or y = x);
          iRS-Seg x = {}
          proof
            assume iRS-Seg x <> {};then
            consider y be object such that
F19:        y in iRS-Seg x by XBOOLE_0:7;
            y <> x & [y,x] in iRS by WELLORD1:1,F19;
            hence contradiction by S4;
          end;then
          dom fr = {} by FUNCT_2:def 1,C2;then
          rng fr = {} by RELAT_1:42;
          hence S[x] by Z0,ZFMISC_1:2,A26,C1;
        end;
        suppose A39: ex y be object st [y,x] in iRS & y <> x;
          assume A30: not S[x];
          consider y be object such that A29: [y,x] in iRS & y <> x by A39;
          y in dom iRS by A29,XTUPLE_0:def 12;then
          reconsider y as Element of RS;
          fr.y in rng fr by FUNCT_1:3,A39a,WELLORD1:1,A29;then
A37:      f.y in rng fr by WELLORD1:1,A29,A39a,FUNCT_1:47;
A37b:     rng fr <> {} by WELLORD1:1,A29,A39a,FUNCT_1:3;
A37a:     F c= f.y by A27;
          F c= union rng fr by TARSKI:def 4,A37,A37a;then
A23:      f.x = union(rng fr) by A22,XBOOLE_1:12;
          consider F such that
A31:      F is finite & not F is consistent & F c= f.x by A30,finin;
          rng fr c= rng f by RELAT_1:70;then
          consider z be set such that
A34:      F c= z & z in rng fr by uniolinf,A23,A31,A54,A37b;
          consider y be object such that
A36:      y in dom fr & fr.y = z by A34,FUNCT_1:def 3;
A42:      [y,x] in iRS by WELLORD1:1,A39a,A36;
A44:      y <> x by WELLORD1:1,A39a,A36;
          y in dom iRS by A42,XTUPLE_0:def 12;then
          reconsider y as Element of RS;
          f.y = fr.y by A36,FUNCT_1:47;
          hence contradiction by A36,A34,A31,incsub,A44,A42,A41;
        end;
      end;
    end;
    A13a: for A be Element of RS holds S[A] from WELLFND1:sch 3(A21,A11);
    take G;
    thus F c= G
    proof
      let y be object;assume A46: y in F;
      set z = the Element of RS;
A47:  F c= f.z by A27;
      f.z in rng f by FUNCT_1:3,A73;
      hence y in G by A46,A47,TARSKI:def 4;
    end;
    thus G is consistent
    proof
      assume not G is consistent;then
      consider F such that
A14:  F is finite & not F is consistent & F c= G by finin;
      consider z be set such that
A90:  F c= z & z in rng f by uniolinf,A14,A54,RELAT_1:42,A73;
      rng (f qua bool L -valued Relation) c= bool L;then
      reconsider z as Subset of PL-WFF by A90;
      consider x be object such that
A92:  x in dom f & f.x = z by A90,FUNCT_1:def 3;
      thus contradiction by A92,A13a,A90,A14,incsub;
    end;
    thus G is maximal
    proof
      given A such that A71: not A in G & not 'not' A in G;
      reconsider ARS = A as Element of RS;
      reconsider nA = 'not' A as Element of RS;
      set fA = f|iRS-Seg A;
      set fnA = f|iRS-Seg ('not' A);
      reconsider A1 = {A} as Subset of L;
      reconsider A1n = {'not' A} as Subset of L;
      A74: not union rng (fA qua bool L -valued Relation) \/ F \/ A1
      is consistent
      proof
        assume union rng (fA qua bool L -valued Relation) \/ F \/ A1
        is consistent;then
        A70: f.ARS = union rng fA \/ F \/ A1 by A26;
        ARS in A1 by TARSKI:def 1;then
C1:     ARS in union rng fA \/ F \/ A1 by XBOOLE_0:def 3;
        f.ARS in rng f by FUNCT_1:3,A73;
        hence contradiction by TARSKI:def 4,A71,A70,C1;
      end;
      A78: not union rng (fnA qua bool L -valued Relation) \/ F \/ A1n
      is consistent
      proof
        assume union rng (fnA qua bool L -valued Relation) \/ F \/ A1n
        is consistent;then
        A70a: f.nA = union rng fnA \/ F \/ A1n by A26;
        nA in A1n by TARSKI:def 1;then
        A72a: nA in f.nA by A70a,XBOOLE_0:def 3;
        f.nA in rng f by FUNCT_1:3,A73;
        hence contradiction by TARSKI:def 4,A71,A72a;
      end;then
      A80: f.nA = union rng fnA \/ F by A26;
      A79: f.A = union rng fA \/ F by A26,A74;
      reconsider AAA = A as Element of HP-WFF by plhp;
      reconsider fal=FaLSUM as Element of HP-WFF by plhp;
      AAA=>fal = A => FaLSUM;then
      len A <> len ('not' A) by HILBERT2:16;then
      per cases by A76,RELAT_2:def 6;
      suppose [A,'not' A] in R2;then
        f.A c= f.nA by A17;then
        not f.nA \/ A1 is consistent by A74,incsub,A79,XBOOLE_1:9;
        hence contradiction by A13a,onecon,A78,A80;
      end;
      suppose ['not' A,A] in R2;then
        f.nA c= f.A by A17;then
        not f.ARS \/ A1n is consistent by A78,incsub,A80,XBOOLE_1:9;
        hence contradiction by onecon,A74,A79,A13a;
      end;
    end;
  end;

theorem inder:
  F is maximal & F is consistent implies  for p holds F |- p iff p in F
  proof
    assume A1: F is maximal & F is consistent;
    let p;
    hereby
      assume A2: F |- p;
      assume not p in F;then
      'not' p in F by A1;then
      F |- 'not' p by th42;
      hence contradiction by A2,A1;
    end;
    assume p in F;
    hence F |- p by th42;
  end;

::#INSERT: Completeness theorem
theorem ct:
  F |= A implies F |- A
  proof
    assume
A0: F |= A & not F |- A;then
    consider G such that
A1: F \/ {'not' A} c= G and
A1a: G is consistent and
A1b: G is maximal by th37,th34;
    set M = {Prop n where n is Element of NAT: Prop n in G};
    M c= props
    proof
      let a be object;
      assume a in M;then
      consider k such that
A7:   Prop k = a & Prop k in G;
      thus a in props by A7,defprops;
    end;then
    reconsider M as PLModel;
    defpred P[Element of PL-WFF] means ($1 in G iff M |= $1);
H0: P[FaLSUM]
    proof
      hereby assume FaLSUM in G;then
        G |- FaLSUM & G |- 'not' FaLSUM by thaa,th42;
        hence M |= FaLSUM by A1a;
      end;
      assume M |= FaLSUM;
      hence thesis by Def11;
    end;
H1: for n holds P[Prop n]
    proof
      let n;
      hereby assume Prop n in G;then
        Prop n in M;
        hence M |= Prop n by Def11;
      end;
      assume M |= Prop n;then
      Prop n in M by Def11;then
      consider k such that
A6:   Prop n = Prop k & Prop k in G;
      thus Prop n in G by A6;
    end;
H2: for r,s st P[r] & P[s] holds P[r => s]
    proof
      let r,s;
      assume
A10:  P[r] & P[s];
      per cases;
      suppose
S1:     r => s in G;
        hereby assume
A11:      r=>s in G;
          per cases;
          suppose r in G;then
A12:        G |- r by th42;
            G |- r=>s by A11,th42;then
            G |- s by A12,th43;then
            M |= s by A10,inder,A1a,A1b;then
            (SAT M).r => (SAT M).s = 1;
            hence M |= r=>s by Def11;
          end;
          suppose not r in G;then
            not M |= r by A10;then
            (SAT M).r = 0 by XBOOLEAN:def 3;then
            (SAT M).r => (SAT M).s = 1;
            hence M |= r=>s by Def11;
          end;
        end;
        assume M |= r=>s;
        thus r=>s in G by S1;
    end;
    suppose
S2:   not r => s in G;
        thus r=>s in G implies M |= r=>s by S2;
        assume
A14:    M |= r=>s;
        'not' (r=>s) in G by S2,A1b;then
A16:    G |- 'not' (r=>s) by th42;
        now
          assume s in G;then
A17:      G |- s by th42;
          s=> (r=>s) in PL_axioms by withplax;then
          G |- s=> (r=>s) by th42;then
          G |- (r=>s) by th43,A17;
          hence contradiction by A16,A1a;
        end;then
A13:    not M |= s by A10;
        now
          assume 'not' r in G;then
A15:      G |- 'not' r by th42;
          G |- 'not' r => (r =>s) by naab;then
          G |- r=>s by th43,A15;
          hence contradiction by A16,A1a;
        end;then
        M |= r by A10,A1b;then
        not (SAT M).r => (SAT M).s = 1 by A13;
        hence r=>s in G by A14,Def11;
    end;
    end;
A2: for B holds P[B] from PLInd(H0,H1,H2);
A4: F c= G by XBOOLE_1:11,A1;
A3: M |= F by A4,A2;
    {'not' A} c= G by A1,XBOOLE_1:11;then
    M |= 'not' A by A2,ZFMISC_1:31;then
    not M |= A by semnot;
    hence contradiction by A0,A3;
end;

theorem
  A is tautology iff {}PL-WFF |- A by tautsat,sth,ct;