:: Logical Equivalence of Formulae :: by Oleg Okhotnikov :: :: Received January 24, 1995 :: Copyright (c) 1995-2021 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 NUMBERS, SUBSET_1, CQC_LANG, QC_LANG1, CQC_THE1, TARSKI, XBOOLE_0, XBOOLEAN, BVFUNC_2, RCOMP_1, XXREAL_0, FINSEQ_1, FUNCT_1, ARYTM_3, CARD_1, ZFREFLE1, FUNCOP_1, REALSET1, QC_LANG3, CQC_THE3, NAT_1; notations TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, FUNCT_1, FINSEQ_1, QC_LANG1, QC_LANG3, CQC_LANG, CQC_THE1, XXREAL_0; constructors DOMAIN_1, XXREAL_0, NAT_1, MEMBERED, QC_LANG3, CQC_THE1, NUMBERS; registrations SUBSET_1, RELSET_1, MEMBERED, CQC_LANG, LUKASI_1, XXREAL_0; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin reserve A for QC-alphabet; reserve p, q, r, s, p1, q1 for Element of CQC-WFF(A), X, Y, Z, X1, X2 for Subset of CQC-WFF(A), h for QC-formula of A, x, y for bound_QC-variable of A, n for Element of 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 A; let p, q be Element of CQC-WFF(A); 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 A; let X, Y be Subset of CQC-WFF(A); pred X |- Y means :: CQC_THE3:def 2 for p being Element of CQC-WFF(A) 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(A); theorem :: CQC_THE3:14 {}(CQC-WFF(A)) |- TAUT(A); definition let A; let X be Subset of CQC-WFF(A); pred |- X means :: CQC_THE3:def 3 for p being Element of CQC-WFF(A) st p in X holds p is valid; end; theorem :: CQC_THE3:15 |- X iff {}(CQC-WFF(A)) |- X; theorem :: CQC_THE3:16 |- TAUT(A); theorem :: CQC_THE3:17 |- X iff X c= TAUT(A); definition let A, 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 A; let p, q be Element of CQC-WFF(A); 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 A; let p, q be Element of CQC-WFF(A); pred p is_an_universal_closure_of q means :: CQC_THE3:def 6 p is closed & ex n being Element of 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 of A st ex r being Element of CQC-WFF(A) 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 is valid 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 is valid; 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 A; let p, q be Element of CQC-WFF(A); pred p <==> q means :: CQC_THE3:def 7 p <=> q is valid; reflexivity; symmetry; end; theorem :: CQC_THE3:50 p <==> q iff p => q is valid & q => p is valid; 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); theorem :: CQC_THE3:60 for k being Nat, l being QC-variable_list of k,A, a being free_QC-variable of A, x being bound_QC-variable of A holds still_not-bound_in l c= still_not-bound_in Subst(l,a .--> x); theorem :: CQC_THE3:61 for k being Nat, l being QC-variable_list of k,A, a being free_QC-variable of A, x being bound_QC-variable of A holds still_not-bound_in Subst(l,a .--> x) c= still_not-bound_in l \/ {x}; theorem :: CQC_THE3:62 for h holds still_not-bound_in h c= still_not-bound_in (h.x); theorem :: CQC_THE3:63 for h holds still_not-bound_in (h.x) c= still_not-bound_in h \/ {x}; theorem :: CQC_THE3:64 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:65 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);