:: 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;
definitions TARSKI;
expansions TARSKI;
theorems TARSKI, ZFMISC_1, CQC_THE1, CQC_THE2, LUKASI_1, NAT_1, QC_LANG1,
QC_LANG2, QC_LANG3, PROCAL_1, CQC_LANG, XBOOLE_0, XBOOLE_1;
schemes NAT_1, QC_LANG1;
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 Th1:
p in X implies X |- p
proof
X c= Cn(X) by CQC_THE1:17;
hence thesis by CQC_THE1:def 8;
end;
theorem Th2:
X c= Cn(Y) implies Cn(X) c= Cn(Y) by CQC_THE1:15,16;
theorem Th3:
X |- p & {p} |- q implies X |- q
proof
assume that
A1: X |- p and
A2: {p} |- q;
p in Cn(X) by A1,CQC_THE1:def 8;
then {p} c= Cn(X) by ZFMISC_1:31;
then
A3: Cn({p}) c= Cn(X) by CQC_THE1:15,16;
q in Cn({p}) by A2,CQC_THE1:def 8;
hence thesis by A3,CQC_THE1:def 8;
end;
theorem Th4:
X |- p & X c= Y implies Y |- p
proof
assume that
A1: X |- p and
A2: X c= Y;
A3: p in Cn(X) by A1,CQC_THE1:def 8;
Cn(X) c= Cn(Y) by A2,CQC_THE1:18;
hence thesis by A3,CQC_THE1:def 8;
end;
definition
let A;
let p, q be Element of CQC-WFF(A);
pred p |- q means
{p} |- q;
end;
theorem Th5:
p |- p
by CQC_THE2:87;
theorem Th6:
p |- q & q |- r implies p |- r
by Th3;
definition
let A;
let X, Y be Subset of CQC-WFF(A);
pred X |- Y means
for p being Element of CQC-WFF(A) st p in Y holds X |- p;
end;
theorem Th7:
X |- Y iff Y c= Cn(X)
proof
hereby
assume
A1: X |- Y;
now
let p be object;
assume
A2: p in Y;
then reconsider p9 = p as Element of CQC-WFF(A);
X |- p9 by A1,A2;
hence p in Cn(X) by CQC_THE1:def 8;
end;
hence Y c= Cn(X);
end;
thus thesis by CQC_THE1:def 8;
end;
theorem
X |- X
by Th1;
theorem Th9:
X |- Y & Y |- Z implies X |- Z
proof
assume that
A1: X |- Y and
A2: Y |- Z;
for p st p in Z holds X |- p
proof
let p;
assume p in Z;
then Y |- p by A2;
then
A3: p in Cn(Y) by CQC_THE1:def 8;
Y c= Cn(X) by A1,Th7;
then Cn(Y) c= Cn(X) by CQC_THE1:15,16;
hence thesis by A3,CQC_THE1:def 8;
end;
hence thesis;
end;
theorem Th10:
X |- {p} iff X |- p
proof
hereby
p in {p} by TARSKI:def 1;
hence X |- {p} implies X |- p;
end;
thus thesis by TARSKI:def 1;
end;
theorem Th11:
{p} |- {q} iff p |- q
by Th10;
theorem
X c= Y implies Y |- X
by Th1;
theorem Th13:
X |- TAUT(A)
proof
TAUT(A) c= Cn(X) by CQC_THE1:39;
hence thesis by Th7;
end;
theorem
{}(CQC-WFF(A)) |- TAUT(A) by Th13;
definition
let A;
let X be Subset of CQC-WFF(A);
pred |- X means
for p being Element of CQC-WFF(A) st p in X holds p is valid;
end;
theorem Th15:
|- X iff {}(CQC-WFF(A)) |- X
proof
hereby
assume
A1: |- X;
now
let p;
assume p in X;
then p is valid by A1;
hence {}(CQC-WFF(A)) |- p by CQC_THE1:def 9;
end;
hence {}(CQC-WFF(A)) |- X;
end;
thus thesis by CQC_THE1:def 9;
end;
theorem
|- TAUT(A)
proof
A1: |- TAUT(A) iff {}(CQC-WFF(A)) |- TAUT(A) by Th15;
{}(CQC-WFF(A)) |- TAUT(A) by Th13;
hence thesis by A1;
end;
theorem
|- X iff X c= TAUT(A)
proof
hereby
assume
A1: |- X;
now
let p;
assume p in X;
then p is valid by A1;
hence p in TAUT(A) by CQC_THE1:def 10;
end;
hence X c= TAUT(A);
end;
thus thesis by CQC_THE1:def 10;
end;
definition
let A, X, Y;
pred X |-| Y means
for p holds (X |- p iff Y |- p);
reflexivity;
symmetry;
end;
theorem Th18:
X |-| Y iff X |- Y & Y |- X
proof
thus X |-| Y implies X |- Y & Y |- X by Th1;
assume that
A1: X |- Y and
A2: Y |- X;
let p;
A3: now
assume Y |- p;
then Y |- {p} by Th10;
then X |- {p} by A1,Th9;
hence X |- p by Th10;
end;
now
assume X |- p;
then X |- {p} by Th10;
then Y |- {p} by A2,Th9;
hence Y |- p by Th10;
end;
hence X |- p iff Y |- p by A3;
end;
theorem
X |-| Y & Y |-| Z implies X |-| Z;
theorem Th20:
X |-| Y iff Cn(X) = Cn(Y)
proof
A1: now
assume
A2: X |-| Y;
then Y |- X by Th18;
then X c= Cn(Y) by Th7;
then
A3: Cn(X) c= Cn(Y) by CQC_THE1:15,16;
X |- Y by A2,Th18;
then Y c= Cn(X) by Th7;
then Cn(Y) c= Cn(X) by CQC_THE1:15,16;
hence Cn(X) = Cn(Y) by A3,XBOOLE_0:def 10;
end;
now
assume
A4: Cn(X) = Cn(Y);
X c= Cn(X) by CQC_THE1:17;
then
A5: Y |- X by A4,Th7;
Y c= Cn(Y) by CQC_THE1:17;
then X |- Y by A4,Th7;
hence X |-| Y by A5,Th18;
end;
hence thesis by A1;
end;
Lm1: X \/ Y c= Cn(X) \/ Cn(Y)
proof
A1: Y c= Cn(Y) by CQC_THE1:17;
X c= Cn(X) by CQC_THE1:17;
hence thesis by A1,XBOOLE_1:13;
end;
theorem Th21:
Cn(X) \/ Cn(Y) c= Cn(X \/ Y)
proof
A1: Cn(Y) c= Cn(X \/ Y) by CQC_THE1:18,XBOOLE_1:7;
Cn(X) c= Cn(X \/ Y) by CQC_THE1:18,XBOOLE_1:7;
hence thesis by A1,XBOOLE_1:8;
end;
theorem Th22:
Cn(X \/ Y) = Cn(Cn(X) \/ Cn(Y))
proof
A1: Cn(X \/ Y) c= Cn(Cn(X) \/ Cn(Y)) by Lm1,CQC_THE1:18;
Cn(Cn(X) \/ Cn(Y)) c= Cn(X \/ Y) by Th2,Th21;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem
X |-| Cn(X)
proof
Cn(X) = Cn(Cn(X)) by CQC_THE1:19;
hence thesis by Th20;
end;
theorem
X \/ Y |-| Cn(X) \/ Cn(Y)
proof
Cn(X \/ Y) = Cn(Cn(X) \/ Cn(Y)) by Th22;
hence thesis by Th20;
end;
theorem Th25:
X1 |-| X2 implies X1 \/ Y |-| X2 \/ Y
proof
assume X1 |-| X2;
then Cn(X1) = Cn(X2) by Th20;
then Cn(X1 \/ Y) = Cn(Cn(X2) \/ Cn(Y)) by Th22
.= Cn(X2 \/ Y) by Th22;
hence thesis by Th20;
end;
theorem Th26:
X1 |-| X2 & X1 \/ Y |- Z implies X2 \/ Y |- Z
proof
assume that
A1: X1 |-| X2 and
A2: X1 \/ Y |- Z;
X1 \/ Y |-| X2 \/ Y by A1,Th25;
then Cn(X1 \/ Y) = Cn(X2 \/ Y) by Th20;
then Z c= Cn(X2 \/ Y) by A2,Th7;
hence thesis by Th7;
end;
theorem Th27:
X1 |-| X2 & Y |- X1 implies Y |- X2
proof
assume that
A1: X1 |-| X2 and
A2: Y |- X1;
X1 |- X2 by A1,Th18;
hence thesis by A2,Th9;
end;
definition
let A;
let p, q be Element of CQC-WFF(A);
pred p |-| q means
p |- q & q |- p;
reflexivity by Th5;
symmetry;
end;
theorem Th28:
p |-| q & q |-| r implies p |-| r
by Th6;
theorem Th29:
p |-| q iff {p} |-| {q}
proof
A1: now
assume
A2: {p} |-| {q};
then {q} |- {p} by Th18;
then
A3: q |- p by Th11;
{p} |- {q} by A2,Th18;
then p |- q by Th11;
hence p |-| q by A3;
end;
now
assume
A4: p |-| q;
then q |- p;
then
A5: {q} |- {p} by Th11;
p |- q by A4;
then {p} |- {q} by Th11;
hence {p} |-| {q} by A5,Th18;
end;
hence thesis by A1;
end;
theorem
p |-| q & X |- p implies X |- q
proof
assume that
A1: p |-| q and
A2: X |- p;
A3: X |- {p} by A2,Th10;
{p} |-| {q} by A1,Th29;
then X |- {q} by A3,Th27;
hence thesis by Th10;
end;
theorem Th31:
{p,q} |-| {p '&' q}
by CQC_THE2:89;
theorem
p '&' q |-| q '&' p
proof
A1: {q,p} |-| {q '&' p} by Th31;
{p '&' q} |-| {q,p} by Th31;
then {p '&' q} |-| {q '&' p} by A1;
hence thesis by Th29;
end;
Lm2: X |- p & X |- q implies X |- p '&' q
proof
assume that
A1: X |- p and
A2: X |- q;
for r st r in {p,q} holds X |- r by A1,A2,TARSKI:def 2;
then X |- {p,q};
then X |- {p '&' q} by Th27,Th31;
hence thesis by Th10;
end;
Lm3: X |- p '&' q implies X |- p & X |- q
proof
assume X |- p '&' q;
then
A1: X |- {p '&' q} by Th10;
{p,q} |-| {p '&' q} by Th31;
then
A2: X |- {p,q} by A1,Th27;
p in {p,q} by TARSKI:def 2;
hence X |- p by A2;
q in {p,q} by TARSKI:def 2;
hence thesis by A2;
end;
theorem
X |- p '&' q iff X |- p & X |- q by Lm2,Lm3;
Lm4: p |-| q & r |-| s implies p '&' r |- q '&' s
proof
assume that
A1: p |-| q and
A2: r |-| s;
r |- s by A2;
then {r} |- s;
then
A3: {p,r} |- s by Th4,ZFMISC_1:7;
{p,r} |-| {p '&' r} by Th31;
then
A4: {p '&' r} |- {p,r} by Th18;
p |- q by A1;
then {p} |- q;
then {p,r} |- q by Th4,ZFMISC_1:7;
then {p,r} |- q '&' s by A3,Lm2;
then {p,r} |- {q '&' s} by Th10;
then {p '&' r} |- {q '&' s} by A4,Th9;
hence thesis by Th11;
end;
theorem
p |-| q & r |-| s implies p '&' r |-| q '&' s
by Lm4;
theorem Th35:
X |- All(x,p) iff X |- p
proof
thus X |- All(x,p) implies X |- p
proof
A1: X |- All(x,p) => p by CQC_THE1:56;
assume X |- All(x,p);
hence thesis by A1,CQC_THE1:55;
end;
thus thesis by CQC_THE2:90;
end;
theorem Th36:
All(x,p) |-| p
proof
{All(x,p)} |- All(x,p) => p by CQC_THE1:56;
then {All(x,p)} |- p by CQC_THE1:55,CQC_THE2:87;
hence All(x,p) |- p;
{p} |- p by CQC_THE2:87;
then {p} |- All(x,p) by Th35;
hence thesis;
end;
theorem
p |-| q implies All(x,p) |-| All(y,q)
proof
assume
A1: p |-| q;
A2: q |-| All(y,q) by Th36;
All(x,p) |-| p by Th36;
then All(x,p) |-| q by A1,Th28;
hence thesis by A2,Th28;
end;
definition
let A;
let p, q be Element of CQC-WFF(A);
pred p is_an_universal_closure_of q means
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 Th38:
p is_an_universal_closure_of q implies p |-| q
proof
assume p is_an_universal_closure_of q;
then consider n being Element of NAT such that
A1: 1 <= n and
A2: ex L being FinSequence st len L = n & L.1 = q & L.n = p &
for k being Nat st 1 <= k & k < n ex x, r st r = L.k & L.(k+1) = All(x,r);
consider L being FinSequence such that
len L = n and
A3: L.1 = q and
A4: L.n = p and
A5: for k being Nat st 1 <= k & k < n holds ex x, r st r = L.
k & L.(k+1) = All(x,r) by A2;
for k being Nat st 1 <= k & k <= n ex r st r = L.k & q |-| r
proof
defpred P[Nat] means 1 <= $1 & $1 <= n implies ex r st r = L.$1 & q |-| r;
A6: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A7: P[k];
now
assume that
1 <= k+1 and
A8: k+1 <= n;
per cases by A8,NAT_1:13,14;
case
A9: k = 0;
take p=q;
thus ex r st r = L.(k+1) & q |-| r by A3,A9;
end;
case
A10: 1 <= k & k < n;
then consider x, r such that
A11: r = L.k and
A12: L.(k+1) = All(x,r) by A5;
consider s such that
A13: s = All(x,r);
s |-| r by A13,Th36;
hence ex s st s = L.(k+1) & q |-| s by A7,A10,A11,A12,A13,Th28;
end;
end;
hence thesis;
end;
A14: P[0];
thus for k being Nat holds P[k] from NAT_1:sch 2(A14,A6 );
end;
then ex r st r = L.n & q |-| r by A1;
hence thesis by A4;
end;
theorem Th39:
p => q is valid implies p |- q
proof
assume p => q is valid;
then {p} |- p => q by CQC_THE1:59;
then {p} |- q by CQC_THE1:55,CQC_THE2:87;
hence thesis;
end;
theorem Th40:
X |- p => q implies X \/ {p} |- q
proof
p in {p} by TARSKI:def 1;
then p in X \/ {p} by XBOOLE_0:def 3;
then
A1: X \/ {p} |- p by Th1;
assume X |- p => q;
then X \/ {p} |- p => q by Th4,XBOOLE_1:7;
hence thesis by A1,CQC_THE1:55;
end;
theorem Th41:
p is closed & p |- q implies p => q is valid
proof
assume that
A1: p is closed and
A2: p |- q;
{}(CQC-WFF(A)) \/ {p} |- q by A2;
then {}(CQC-WFF(A)) |- p => q by A1,CQC_THE2:92;
hence thesis by CQC_THE1:def 9;
end;
theorem
p1 is_an_universal_closure_of p implies (X \/ {p} |- q iff X |- p1 => q)
proof
assume
A1: p1 is_an_universal_closure_of p;
now
assume X \/ {p} |- q;
then
A2: X \/ {p} |- {q} by Th10;
p |-| p1 by A1,Th38;
then {p} |-| {p1} by Th29;
then X \/ {p1} |- {q} by A2,Th26;
then
A3: X \/ {p1} |- q by Th10;
p1 is closed by A1;
hence X |- p1 => q by A3,CQC_THE2:92;
end;
hence X \/ {p} |- q implies X |- p1 => q;
now
assume X |- p1 => q;
then X \/ {p1} |- q by Th40;
then
A4: X \/ {p1} |- {q} by Th10;
p |-| p1 by A1,Th38;
then {p} |-| {p1} by Th29;
then X \/ {p} |- {q} by A4,Th26;
hence X \/ {p} |- q by Th10;
end;
hence thesis;
end;
theorem Th43:
p is closed & p |- q implies 'not' q |- 'not' p
proof
assume that
A1: p is closed and
A2: p |- q;
p => q is valid by A1,A2,Th41;
then 'not' q => 'not' p is valid by LUKASI_1:52;
hence thesis by Th39;
end;
theorem
p is closed & X \/ {p} |- q implies X \/ {'not' q} |- 'not' p
proof
assume that
A1: p is closed and
A2: X \/ {p} |- q;
X |- p => q by A1,A2,CQC_THE2:92;
then X |- 'not' q => 'not' p by LUKASI_1:69;
hence thesis by Th40;
end;
theorem Th45:
p is closed & 'not' p |- 'not' q implies q |- p
proof
assume that
A1: p is closed and
A2: 'not' p |- 'not' q;
'not' p is closed by A1,QC_LANG3:21;
then 'not' p => 'not' q is valid by A2,Th41;
then q => p is valid by LUKASI_1:52;
hence thesis by Th39;
end;
theorem
p is closed & X \/ {'not' p} |- 'not' q implies X \/ {q} |- p
proof
assume that
A1: p is closed and
A2: X \/ {'not' p} |- 'not' q;
'not' p is closed by A1,QC_LANG3:21;
then X |- 'not' p => 'not' q by A2,CQC_THE2:92;
then X |- q => p by LUKASI_1:69;
hence thesis by Th40;
end;
theorem
p is closed & q is closed implies (p |- q iff 'not' q |- 'not' p) by Th43
,Th45;
theorem Th48:
p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of
q implies (p |- q iff 'not' q1 |- 'not' p1)
proof
assume that
A1: p1 is_an_universal_closure_of p and
A2: q1 is_an_universal_closure_of q;
now
q |-| q1 by A2,Th38;
then
A3: q |- q1;
p1 |-| p by A1,Th38;
then
A4: p1 |- p;
assume p |- q;
then p1 |- q by A4,Th6;
then
A5: p1 |- q1 by A3,Th6;
p1 is closed by A1;
hence 'not' q1 |- 'not' p1 by A5,Th43;
end;
hence p |- q implies 'not' q1 |- 'not' p1;
now
q1 |-| q by A2,Th38;
then
A6: q1 |- q;
p1 |-| p by A1,Th38;
then
A7: p |- p1;
assume
A8: 'not' q1 |- 'not' p1;
q1 is closed by A2;
then p1 |- q1 by A8,Th45;
then p |- q1 by A7,Th6;
hence p |- q by A6,Th6;
end;
hence thesis;
end;
theorem
p1 is_an_universal_closure_of p & q1 is_an_universal_closure_of q
implies (p |-| q iff 'not' p1 |-| 'not' q1)
by Th48;
definition
let A;
let p, q be Element of CQC-WFF(A);
pred p <==> q means
p <=> q is valid;
reflexivity
proof
let p;
{}(CQC-WFF(A)) |- p => p by CQC_THE1:def 9;
then {}(CQC-WFF(A)) |- (p => p) '&' (p => p) by Lm2;
then (p => p) '&' (p => p) is valid by CQC_THE1:def 9;
hence thesis by QC_LANG2:def 4;
end;
symmetry
proof
let p, q;
assume p <=> q is valid;
then (p => q) '&' (q => p) is valid by QC_LANG2:def 4;
then
A1: {}(CQC-WFF(A)) |- (p => q) '&' (q => p) by CQC_THE1:def 9;
then
A2: {}(CQC-WFF(A)) |- q => p by Lm3;
{}(CQC-WFF(A)) |- p => q by A1,Lm3;
then {}(CQC-WFF(A)) |- (q => p) '&' (p => q) by A2,Lm2;
then (q => p) '&' (p => q) is valid by CQC_THE1:def 9;
hence thesis by QC_LANG2:def 4;
end;
end;
theorem Th50:
p <==> q iff p => q is valid & q => p is valid
proof
A1: now
assume that
A2: p => q is valid and
A3: q => p is valid;
A4: {}(CQC-WFF(A)) |- q => p by A3,CQC_THE1:def 9;
{}(CQC-WFF(A)) |- p => q by A2,CQC_THE1:def 9;
then {}(CQC-WFF(A)) |- (p => q) '&' (q => p) by A4,Lm2;
then (p => q) '&' (q => p) is valid by CQC_THE1:def 9;
then p <=> q is valid by QC_LANG2:def 4;
hence p <==> q;
end;
now
assume p <==> q;
then p <=> q is valid;
then (p => q) '&' (q => p) is valid by QC_LANG2:def 4;
then
A5: {}(CQC-WFF(A)) |- (p => q) '&' (q => p) by CQC_THE1:def 9;
then
A6: {}(CQC-WFF(A)) |- q => p by Lm3;
{}(CQC-WFF(A)) |- p => q by A5,Lm3;
hence p => q is valid & q => p is valid by A6,CQC_THE1:def 9;
end;
hence thesis by A1;
end;
theorem
p <==> q & q <==> r implies p <==> r
proof
assume that
A1: p <==> q and
A2: q <==> r;
A3: r => q is valid by A2,Th50;
q => p is valid by A1,Th50;
then
A4: r => p is valid by A3,LUKASI_1:42;
A5: q => r is valid by A2,Th50;
p => q is valid by A1,Th50;
then p => r is valid by A5,LUKASI_1:42;
hence thesis by A4,Th50;
end;
theorem
p <==> q implies p |-| q
proof
assume p <==> q;
then p <=> q is valid;
then (p => q) '&' (q => p) is valid by QC_LANG2:def 4;
then
A1: {}(CQC-WFF(A)) |- (p => q) '&' (q => p) by CQC_THE1:def 9;
then {}(CQC-WFF(A)) |- q => p by Lm3;
then
A2: q => p is valid by CQC_THE1:def 9;
{}(CQC-WFF(A)) |- p => q by A1,Lm3;
then p => q is valid by CQC_THE1:def 9;
hence p |- q & q |- p by A2,Th39;
end;
Lm5: p <==> q implies 'not' p <==> 'not' q
proof
assume
A1: p <==> q;
then q => p is valid by Th50;
then
A2: 'not' p => 'not' q is valid by LUKASI_1:52;
p => q is valid by A1,Th50;
then 'not' q => 'not' p is valid by LUKASI_1:52;
hence thesis by A2,Th50;
end;
Lm6: 'not' p <==> 'not' q implies p <==> q
proof
assume
A1: 'not' p <==> 'not' q;
then 'not' q => 'not' p is valid by Th50;
then
A2: p => q is valid by LUKASI_1:52;
'not' p => 'not' q is valid by A1,Th50;
then q => p is valid by LUKASI_1:52;
hence thesis by A2,Th50;
end;
theorem
p <==> q iff 'not' p <==> 'not' q by Lm5,Lm6;
theorem Th54:
p <==> q & r <==> s implies p '&' r <==> q '&' s
proof
assume that
A1: p <==> q and
A2: r <==> s;
s => r is valid by A2,Th50;
then
A3: s => r in TAUT(A) by CQC_THE1:def 10;
q => p is valid by A1,Th50;
then q => p in TAUT(A) by CQC_THE1:def 10;
then q '&' s => p '&' r in TAUT(A) by A3,PROCAL_1:56;
then
A4: q '&' s => p '&' r is valid by CQC_THE1:def 10;
r => s is valid by A2,Th50;
then
A5: r => s in TAUT(A) by CQC_THE1:def 10;
p => q is valid by A1,Th50;
then p => q in TAUT(A) by CQC_THE1:def 10;
then p '&' r => q '&' s in TAUT(A) by A5,PROCAL_1:56;
then p '&' r => q '&' s is valid by CQC_THE1:def 10;
hence thesis by A4,Th50;
end;
theorem Th55:
p <==> q & r <==> s implies p => r <==> q => s
proof
assume that
A1: p <==> q and
A2: r <==> s;
'not' r <==> 'not' s by A2,Lm5;
then p '&' 'not' r <==> q '&' 'not' s by A1,Th54;
then
A3: 'not' (p '&' 'not' r) <==> 'not' (q '&' 'not' s) by Lm5;
p => r = 'not' (p '&' 'not' r) by QC_LANG2:def 2;
hence thesis by A3,QC_LANG2:def 2;
end;
theorem
p <==> q & r <==> s implies p 'or' r <==> q 'or' s
proof
assume that
A1: p <==> q and
A2: r <==> s;
s => r is valid by A2,Th50;
then
A3: s => r in TAUT(A) by CQC_THE1:def 10;
q => p is valid by A1,Th50;
then q => p in TAUT(A) by CQC_THE1:def 10;
then q 'or' s => p 'or' r in TAUT(A) by A3,PROCAL_1:57;
then
A4: q 'or' s => p 'or' r is valid by CQC_THE1:def 10;
r => s is valid by A2,Th50;
then
A5: r => s in TAUT(A) by CQC_THE1:def 10;
p => q is valid by A1,Th50;
then p => q in TAUT(A) by CQC_THE1:def 10;
then p 'or' r => q 'or' s in TAUT(A) by A5,PROCAL_1:57;
then p 'or' r => q 'or' s is valid by CQC_THE1:def 10;
hence thesis by A4,Th50;
end;
theorem
p <==> q & r <==> s implies p <=> r <==> q <=> s
proof
assume that
A1: p <==> q and
A2: r <==> s;
A3: r => p <==> s => q by A1,A2,Th55;
A4: p <=> r = (p => r) '&' (r => p) by QC_LANG2:def 4;
p => r <==> q => s by A1,A2,Th55;
then (p => r) '&' (r => p) <==> (q => s) '&' (s => q) by A3,Th54;
hence thesis by A4,QC_LANG2:def 4;
end;
theorem Th58:
p <==> q implies All(x,p) <==> All(x,q)
proof
assume
A1: p <==> q;
then q => p is valid by Th50;
then All(x,q => p) is valid by CQC_THE2:23;
then
A2: All(x,q) => All(x,p) is valid by CQC_THE2:31;
p => q is valid by A1,Th50;
then All(x,p => q) is valid by CQC_THE2:23;
then All(x,p) => All(x,q) is valid by CQC_THE2:31;
hence thesis by A2,Th50;
end;
theorem
p <==> q implies Ex(x,p) <==> Ex(x,q)
proof
assume p <==> q;
then 'not' p <==> 'not' q by Lm5;
then All(x,'not' p) <==> All(x,'not' q) by Th58;
then
A1: 'not' All(x,'not' p) <==> 'not' All(x,'not' q) by Lm5;
Ex(x,p) = 'not' All(x,'not' p) by QC_LANG2:def 5;
hence thesis by A1,QC_LANG2:def 5;
end;
theorem Th60:
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)
proof
let k be Nat, l be QC-variable_list of k,A,
a be free_QC-variable of A,
x be bound_QC-variable of A;
let y be object;
A1: still_not-bound_in l = { l.n where n is Nat:
1 <= n & n <= len l & l.n in
bound_QC-variables A} by QC_LANG1:def 29;
assume
A2: y in still_not-bound_in l;
then reconsider y9 = y as Element of still_not-bound_in l;
A3: still_not-bound_in Subst(l,a .--> x)
= { Subst(l,a .--> x).n where n is Nat: 1 <= n
& n <= len Subst(l,a .--> x) & Subst(l,a .--> x).n in bound_QC-variables
A}
by QC_LANG1:def 29;
consider n being Nat such that
A4: y9 = l.n and
A5: 1 <= n and
A6: n <= len l and
A7: l.n in bound_QC-variables A by A1,A2;
l.n <> a by A7,QC_LANG3:34;
then
A8: l.n = Subst(l,a .--> x).n by A5,A6,CQC_LANG:3;
n <= len Subst(l,a .--> x) by A6,CQC_LANG:def 1;
hence y in still_not-bound_in Subst(l,a .--> x) by A3,A4,A5,A7,A8;
end;
theorem Th61:
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}
proof
let k be Nat, l be QC-variable_list of k,A,
a be free_QC-variable of A,
x be bound_QC-variable of A;
let y be object;
A1: still_not-bound_in l = { l.n where n is Nat:
1 <= n & n <= len l & l.n in
bound_QC-variables A} by QC_LANG1:def 29;
assume
A2: y in still_not-bound_in Subst(l,a .--> x);
then reconsider y9 = y as Element of still_not-bound_in Subst(l,a .--> x);
still_not-bound_in Subst(l,a .--> x)
= { Subst(l,a .--> x).n where n is Nat:
1 <= n &
n <= len Subst(l,a .--> x) & Subst(l,a .--> x).n in bound_QC-variables A}
by QC_LANG1:def 29;
then consider n being Nat such that
A3: y9 = Subst(l,a .--> x).n and
A4: 1 <= n and
A5: n <= len Subst(l,a .--> x) and
A6: Subst(l,a .--> x).n in bound_QC-variables A by A2;
A7: n <= len l by A5,CQC_LANG:def 1;
per cases;
suppose
l.n = a;
then y9 = x by A3,A4,A7,CQC_LANG:3;
then y9 in {x} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
l.n <> a;
then l.n = Subst(l,a .--> x).n by A4,A7,CQC_LANG:3;
then y9 in still_not-bound_in l by A1,A3,A4,A6,A7;
hence thesis by XBOOLE_0:def 3;
end;
end;
theorem Th62:
for h holds still_not-bound_in h c= still_not-bound_in (h.x)
proof
defpred P[QC-formula of A] means still_not-bound_in $1
c= still_not-bound_in ($1.x);
A1: for p being Element of QC-WFF(A) st P[p] holds P['not' p]
proof
let p be Element of QC-WFF(A);
still_not-bound_in (('not' p).x) = still_not-bound_in 'not' (p.x) by
CQC_LANG:19
.= still_not-bound_in(p.x) by QC_LANG3:7;
hence thesis by QC_LANG3:7;
end;
A2: for p, q being Element of QC-WFF(A) st P[p] & P[q] holds P[p '&' q]
proof
let p, q be Element of QC-WFF(A) such that
A3: P[p] and
A4: P[q];
A5: still_not-bound_in ((p '&' q).x) = still_not-bound_in ((p.x) '&' (q.x
)) by CQC_LANG:21
.= still_not-bound_in (p.x) \/ still_not-bound_in (q.x) by QC_LANG3:10;
still_not-bound_in (p '&' q) = still_not-bound_in p \/
still_not-bound_in q by QC_LANG3:10;
hence thesis by A3,A4,A5,XBOOLE_1:13;
end;
A6: for x being bound_QC-variable of A, p being Element of QC-WFF(A) st
P[p] holds
P[All(x, p)]
proof
let y be bound_QC-variable of A, p be Element of QC-WFF(A) such that
A7: P[p];
per cases;
suppose
y = x;
hence thesis by CQC_LANG:24;
end;
suppose
A8: y <> x;
A9: still_not-bound_in All(y,p) = still_not-bound_in p \ {y} by QC_LANG3:12;
still_not-bound_in (All(y,p).x) = still_not-bound_in All(y,p.x) by A8,
CQC_LANG:25
.= still_not-bound_in (p.x) \ {y} by QC_LANG3:12;
hence thesis by A7,A9,XBOOLE_1:33;
end;
end;
A10: for k being Nat, P being (QC-pred_symbol of k,A), ll being
QC-variable_list of k,A holds P[P!ll]
proof
let k be Nat, P be (QC-pred_symbol of k,A), ll be
QC-variable_list of k,A;
A11: still_not-bound_in ((P!ll).x) = still_not-bound_in
(P!Subst(ll,(A)a.0.-->
x)) by CQC_LANG:17
.= still_not-bound_in Subst(ll,(A)a.0.-->x) by QC_LANG3:5;
still_not-bound_in ll c= still_not-bound_in
Subst(ll,(A)a.0.-->x) by Th60;
hence thesis by A11,QC_LANG3:5;
end;
A12: P[VERUM(A)] by CQC_LANG:15;
thus for h holds P[h] from QC_LANG1:sch 1(A10,A12,A1,A2,A6);
end;
theorem Th63:
for h holds still_not-bound_in (h.x) c= still_not-bound_in h \/ {x}
proof
defpred P[QC-formula of A] means
still_not-bound_in ($1.x) c= still_not-bound_in $1 \/ {x};
A1: for p being Element of QC-WFF(A) st P[p] holds P['not' p]
proof
let p be Element of QC-WFF(A);
still_not-bound_in (('not' p).x) = still_not-bound_in 'not' (p.x) by
CQC_LANG:19
.= still_not-bound_in(p.x) by QC_LANG3:7;
hence thesis by QC_LANG3:7;
end;
A2: for p, q being Element of QC-WFF(A) st P[p] & P[q] holds P[p '&' q]
proof
let p, q be Element of QC-WFF(A) such that
A3: P[p] and
A4: P[q];
A5: still_not-bound_in ((p '&' q).x) = still_not-bound_in ((p.x) '&' (q.x
)) by CQC_LANG:21
.= still_not-bound_in (p.x) \/ still_not-bound_in (q.x) by QC_LANG3:10;
A6: still_not-bound_in p \/ {x} \/ (still_not-bound_in q \/ {x}) =
still_not-bound_in p \/ ({x} \/ still_not-bound_in q) \/ {x} by XBOOLE_1:4
.= still_not-bound_in p \/ still_not-bound_in q \/ {x} \/ {x} by
XBOOLE_1:4
.= still_not-bound_in p \/ still_not-bound_in q \/ ({x} \/ {x}) by
XBOOLE_1:4
.= still_not-bound_in p \/ still_not-bound_in q \/ {x};
still_not-bound_in (p.x) \/ still_not-bound_in (q.x) c=
still_not-bound_in p \/ {x} \/ (still_not-bound_in q \/ {x}) by A3,A4,
XBOOLE_1:13;
hence thesis by A5,A6,QC_LANG3:10;
end;
A7: for x being bound_QC-variable of A,
p being Element of QC-WFF(A) st P[p] holds
P[All(x, p)]
proof
let y be bound_QC-variable of A,
p be Element of QC-WFF(A) such that
A8: P[p];
per cases;
suppose
A9: y = x;
A10: (still_not-bound_in p) \ {x} c= still_not-bound_in p by XBOOLE_1:36;
A11: still_not-bound_in All(x,p) = (still_not-bound_in p) \ {x} by QC_LANG3:12
;
still_not-bound_in p c= still_not-bound_in (p.x) by Th62;
then
still_not-bound_in All(x,p) c= still_not-bound_in (p.x) by A11,A10;
then
A12: still_not-bound_in All(x,p) c= still_not-bound_in p \/ {x} by A8,
XBOOLE_1:1;
still_not-bound_in All(y,p) \/ {x} = ((still_not-bound_in p) \ {x})
\/ {x} by A9,QC_LANG3:12
.= still_not-bound_in p \/ {x} by XBOOLE_1:39;
hence thesis by A9,A12,CQC_LANG:24;
end;
suppose
A13: y <> x;
A14: still_not-bound_in All(y,p) \/ {x} = (still_not-bound_in p \ {y})
\/ {x} by QC_LANG3:12
.= (still_not-bound_in p \/ {x}) \ {y} by A13,XBOOLE_1:87,ZFMISC_1:11;
still_not-bound_in (All(y,p).x) = still_not-bound_in All(y,p.x) by A13,
CQC_LANG:25
.= still_not-bound_in (p.x) \ {y} by QC_LANG3:12;
hence thesis by A8,A14,XBOOLE_1:33;
end;
end;
A15: for k being Nat, P being (QC-pred_symbol of k,A), ll being
QC-variable_list of k,A holds P[P!ll]
proof
let k be Nat, P be (QC-pred_symbol of k,A), ll be
QC-variable_list of k,A;
A16: still_not-bound_in ((P!ll).x) = still_not-bound_in
(P!Subst(ll,(A)a.0.-->
x)) by CQC_LANG:17
.= still_not-bound_in Subst(ll,(A)a.0.-->x) by QC_LANG3:5;
still_not-bound_in Subst(ll,(A)a.0.-->x) c= still_not-bound_in ll \/ {x}
by Th61;
hence thesis by A16,QC_LANG3:5;
end;
A17: still_not-bound_in VERUM(A) = {} by QC_LANG3:3;
VERUM(A).x = VERUM(A) by CQC_LANG:15; then
still_not-bound_in ((VERUM(A)).x) = {} by A17; then
A18: still_not-bound_in ((VERUM(A)).x) c=
still_not-bound_in (VERUM(A)) \/ {x} by XBOOLE_1:2;
A19: P[VERUM(A)] by A18;
thus for h holds P[h] from QC_LANG1:sch 1(A15,A19,A1,A2,A7);
end;
theorem Th64:
p = h.x & x <> y & not y in still_not-bound_in h implies not y
in still_not-bound_in p
proof
assume that
A1: p = h.x and
A2: x <> y and
A3: not y in still_not-bound_in h and
A4: y in still_not-bound_in p;
A5: still_not-bound_in p c= still_not-bound_in h \/ {x} by A1,Th63;
per cases by A4,A5,XBOOLE_0:def 3;
suppose
y in still_not-bound_in h;
hence contradiction by A3;
end;
suppose
y in {x};
hence contradiction by A2,TARSKI:def 1;
end;
end;
theorem
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)
proof
assume that
A1: p = h.x and
A2: q = h.y and
A3: not x in still_not-bound_in h and
A4: not y in still_not-bound_in h;
per cases;
suppose
x = y;
hence thesis by A1,A2;
end;
suppose
A5: x <> y;
then not x in still_not-bound_in q by A2,A3,Th64;
then
A6: All(y,q) => All(x,p) is valid by A1,A2,A4,CQC_THE2:27;
not y in still_not-bound_in p by A1,A4,A5,Th64;
then All(x,p) => All(y,q) is valid by A1,A2,A3,CQC_THE2:27;
hence thesis by A6,Th50;
end;
end;