The abstract of the Mizar article:

Logical Equivalence of Formulae

by

Oleg Okhotnikov

Received January 24, 1995

MML identifier: CQC_THE3

[ Mizar article, MML identifier index ]

environ

 vocabulary CQC_LANG, QC_LANG1, QMAX_1, CQC_THE1, BOOLE, ZF_LANG, PRE_TOPC,
      FINSEQ_1, FUNCT_1, CAT_1, QC_LANG3, CQC_THE3;
 notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, DOMAIN_1, NAT_1, FUNCT_1,
      FINSEQ_1, QC_LANG1, QC_LANG3, CQC_LANG, CQC_THE1;
 constructors DOMAIN_1, NAT_1, QC_LANG3, CQC_THE1, XREAL_0, MEMBERED, XBOOLE_0;
 clusters RELSET_1, CQC_LANG, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

reserve p, q, r, s, p1, q1 for Element of CQC-WFF,
        X, Y, Z, X1, X2 for Subset of CQC-WFF,
        h for QC-formula,
        x, y for bound_QC-variable,
        n for Nat;

theorem :: CQC_THE3:1
  p in X implies X |- p;

theorem :: CQC_THE3:2
  X c= Cn(Y) implies Cn(X) c= Cn(Y);

theorem :: CQC_THE3:3
  X |- p & {p} |- q implies X |- q;

theorem :: CQC_THE3:4
  X |- p & X c= Y implies Y |- p;

definition
  let p, q be Element of CQC-WFF;
  pred p |- q means
:: CQC_THE3:def 1
{p} |- q;
end;

theorem :: CQC_THE3:5
  p |- p;

theorem :: CQC_THE3:6
  p |- q & q |- r implies p |- r;

definition
  let X, Y be Subset of CQC-WFF;
  pred X |- Y means
:: CQC_THE3:def 2
    for p being Element of CQC-WFF
      st p in Y holds X |- p;
end;

theorem :: CQC_THE3:7
  X |- Y iff Y c= Cn(X);

theorem :: CQC_THE3:8
    X |- X;

theorem :: CQC_THE3:9
  X |- Y & Y |- Z implies X |- Z;

theorem :: CQC_THE3:10
  X |- {p} iff X |- p;

theorem :: CQC_THE3:11
  {p} |- {q} iff p |- q;

theorem :: CQC_THE3:12
    X c= Y implies Y |- X;

theorem :: CQC_THE3:13
  X |- TAUT;

theorem :: CQC_THE3:14
  {}(CQC-WFF) |- TAUT;

definition
  let X be Subset of CQC-WFF;
  pred |- X means
:: CQC_THE3:def 3
    for p being Element of CQC-WFF
      st p in X holds |- p;
end;

theorem :: CQC_THE3:15
  |- X iff {}(CQC-WFF) |- X;

theorem :: CQC_THE3:16
    |- TAUT;

theorem :: CQC_THE3:17
    |- X iff X c= TAUT;

definition
  let X, Y;
  pred X |-| Y means
:: CQC_THE3:def 4
    for p holds (X |- p iff Y |- p);
  reflexivity;
  symmetry;
end;

theorem :: CQC_THE3:18
  X |-| Y iff (X |- Y & Y |- X);

theorem :: CQC_THE3:19
  X |-| Y & Y |-| Z implies X |-| Z;

theorem :: CQC_THE3:20
  X |-| Y iff Cn(X) = Cn(Y);

theorem :: CQC_THE3:21
  Cn(X) \/ Cn(Y) c= Cn(X \/ Y);

theorem :: CQC_THE3:22
  Cn(X \/ Y) = Cn(Cn(X) \/ Cn(Y));

theorem :: CQC_THE3:23
    X |-| Cn(X);

theorem :: CQC_THE3:24
    X \/ Y |-| Cn(X) \/ Cn(Y);

theorem :: CQC_THE3:25
  X1 |-| X2 implies X1 \/ Y |-| X2 \/ Y;

theorem :: CQC_THE3:26
  X1 |-| X2 & X1 \/ Y |- Z implies X2 \/ Y |- Z;

theorem :: CQC_THE3:27
  X1 |-| X2 & Y |- X1 implies Y |- X2;

definition
  let p, q be Element of CQC-WFF;
  pred p |-| q means
:: CQC_THE3:def 5
p |- q & q |- p;
  reflexivity;
  symmetry;
end;

theorem :: CQC_THE3:28
  p |-| q & q |-| r implies p |-| r;

theorem :: CQC_THE3:29
  p |-| q iff {p} |-| {q};

theorem :: CQC_THE3:30
    p |-| q & X |- p implies X |- q;

theorem :: CQC_THE3:31
  {p,q} |-| {p '&' q};

theorem :: CQC_THE3:32
    p '&' q |-| q '&' p;

theorem :: CQC_THE3:33
   X |- p '&' q iff (X |- p & X |- q);

theorem :: CQC_THE3:34
    p |-| q & r |-| s implies p '&' r |-| q '&' s;

theorem :: CQC_THE3:35
  X |- All(x,p) iff X |- p;

theorem :: CQC_THE3:36
  All(x,p) |-| p;

theorem :: CQC_THE3:37
    p |-| q implies All(x,p) |-| All(y,q);

definition let p, q be Element of CQC-WFF;
  pred p is_an_universal_closure_of q means
:: CQC_THE3:def 6
    p is closed &
    ex n being Nat st 1 <= n &
    ex L being FinSequence st len L = n & L.1 = q & L.n = p &
      for k being Nat st 1 <= k & k < n holds
        ex x being bound_QC-variable st
          ex r being Element of CQC-WFF st r = L.k & L.(k+1) = All(x,r);
end;

theorem :: CQC_THE3:38
  p is_an_universal_closure_of q implies p |-| q;

theorem :: CQC_THE3:39
  |- p => q implies p |- q;

theorem :: CQC_THE3:40
  X |- p => q implies X \/ {p} |- q;

theorem :: CQC_THE3:41
  p is closed & p |- q implies |- p => q;

theorem :: CQC_THE3:42
    p1 is_an_universal_closure_of p implies
    (X \/ {p} |- q iff X |- p1 => q);

theorem :: CQC_THE3:43
  p is closed & p |- q implies 'not' q |- 'not' p;

theorem :: CQC_THE3:44
    p is closed & X \/ {p} |- q implies X \/ {'not' q} |- 'not' p;

theorem :: CQC_THE3:45
  p is closed & 'not' p |- 'not' q implies q |- p;

theorem :: CQC_THE3:46
    p is closed & X \/ {'not' p} |- 'not' q implies X \/ {q} |- p;

theorem :: CQC_THE3:47
    p is closed & q is closed implies (p |- q iff 'not' q |- 'not' p);

theorem :: CQC_THE3:48
  p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q implies
    (p |- q iff 'not' q1 |- 'not' p1);

theorem :: CQC_THE3:49
    p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q implies
    (p |-| q iff 'not' p1 |-| 'not' q1);

definition
  let p, q be Element of CQC-WFF;
  pred p <==> q means
:: CQC_THE3:def 7
|- p <=> q;
  reflexivity;
  symmetry;
end;

theorem :: CQC_THE3:50
  p <==> q iff (|- p => q & |- q => p);

theorem :: CQC_THE3:51
    p <==> q & q <==> r implies p <==> r;

theorem :: CQC_THE3:52
    p <==> q implies p |-| q;

theorem :: CQC_THE3:53
   p <==> q iff 'not' p <==> 'not' q;

theorem :: CQC_THE3:54
  p <==> q & r <==> s implies p '&' r <==> q '&' s;

theorem :: CQC_THE3:55
  p <==> q & r <==> s implies p => r <==> q => s;

theorem :: CQC_THE3:56
    p <==> q & r <==> s implies p 'or' r <==> q 'or' s;

theorem :: CQC_THE3:57
    p <==> q & r <==> s implies p <=> r <==> q <=> s;

theorem :: CQC_THE3:58
  p <==> q implies All(x,p) <==> All(x,q);

theorem :: CQC_THE3:59
    p <==> q implies Ex(x,p) <==> Ex(x,q);

canceled;

theorem :: CQC_THE3:61
  for k being Nat, l being QC-variable_list of k,
  a being free_QC-variable, x being bound_QC-variable holds
  still_not-bound_in l c= still_not-bound_in Subst(l,a .--> x);

theorem :: CQC_THE3:62
  for k being Nat, l being QC-variable_list of k,
  a being free_QC-variable, x being bound_QC-variable holds
  still_not-bound_in Subst(l,a .--> x) c= still_not-bound_in l \/ {x};

theorem :: CQC_THE3:63
  for h holds still_not-bound_in h c= still_not-bound_in (h.x);

theorem :: CQC_THE3:64
  for h holds still_not-bound_in (h.x) c= still_not-bound_in h \/ {x};

theorem :: CQC_THE3:65
  p = h.x & x <> y & not y in still_not-bound_in h
    implies not y in still_not-bound_in p;

theorem :: CQC_THE3:66
    p = h.x & q = h.y &
    not x in still_not-bound_in h & not y in still_not-bound_in h
      implies All(x,p) <==> All(y,q);