Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

### Logical Equivalence of Formulae

by
Oleg Okhotnikov

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);

```