Volume 7, 1995

University of Bialystok

Copyright (c) 1995 Association of Mizar Users

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

Back to top