:: Logical Equivalence of Formulae
:: by Oleg Okhotnikov
::
:: Received January 24, 1995
:: Copyright (c) 1995-2018 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,
NAT_1;
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);