:: Calculus of Quantifiers. Deduction Theorem
:: by Agata Darmochwa\l
::
:: Received October 24, 1990
:: Copyright (c) 1990-2026 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 SUBSET_1, CQC_LANG, QC_LANG1, FINSEQ_1, ZFMISC_1, CQC_THE1,
NUMBERS, XBOOLEAN, BVFUNC_2, XBOOLE_0, FUNCT_1, TARSKI, RCOMP_1, MCART_1,
NAT_1, XXREAL_0, ARYTM_3, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, NAT_1,
FINSEQ_1, FUNCT_1, XTUPLE_0, MCART_1, DOMAIN_1, QC_LANG1, QC_LANG2,
CQC_LANG, CQC_THE1, XXREAL_0;
constructors DOMAIN_1, XXREAL_0, XREAL_0, CQC_THE1, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, RELSET_1, XREAL_0, CQC_LANG, ORDINAL1, LUKASI_1;
requirements NUMERALS, SUBSET, BOOLE, REAL;
definitions CQC_THE1;
expansions CQC_THE1;
theorems TARSKI, ZFMISC_1, LUKASI_1, CQC_LANG, CQC_THE1, ENUMSET1, QC_LANG1,
QC_LANG2, QC_LANG3, PROCAL_1, XBOOLE_0, XBOOLE_1, XXREAL_0;
schemes NAT_1;
begin
reserve A for QC-alphabet;
reserve X,T for Subset of CQC-WFF(A);
reserve F,G,H,p,q,r,t for Element of CQC-WFF(A);
reserve s,h for QC-formula of A;
reserve x,y for bound_QC-variable of A;
reserve f for FinSequence of [:CQC-WFF(A),Proof_Step_Kinds:];
reserve i,j for Element of NAT;
theorem Th1:
p => (q => r) is valid implies (p '&' q) => r is valid
proof
A1: (p => (q => r)) => ((p '&' q) => r) in TAUT(A) by PROCAL_1:32;
assume p => (q => r) in TAUT(A);
hence (p '&' q) => r in TAUT(A) by A1,CQC_THE1:46;
end;
theorem Th2:
p => (q => r) is valid implies (q '&' p) => r is valid
proof
assume p => (q => r) in TAUT(A);
then p => (q => r) is valid;
then (p '&' q) => r is valid by Th1;
then
A1: (p '&' q) => r in TAUT(A);
q '&' p => p '&' q in TAUT(A) by CQC_THE1:45;
hence (q '&' p) => r in TAUT(A) by A1,LUKASI_1:3;
end;
theorem Th3:
(p '&' q) => r is valid implies p => (q => r) is valid
proof
A1: ((p '&' q) => r) => (p => (q => r)) in TAUT(A) by PROCAL_1:31;
assume (p '&' q) => r in TAUT(A);
hence (p => (q => r)) in TAUT(A) by A1,CQC_THE1:46;
end;
theorem Th4:
(p '&' q) => r is valid implies q => (p => r) is valid
proof
A1: q '&' p => p '&' q in TAUT(A) by CQC_THE1:45;
assume (p '&' q) => r in TAUT(A);
then q '&' p => r in TAUT(A) by A1,LUKASI_1:3;
then q '&' p => r is valid;
then q => (p => r) is valid by Th3;
hence q => (p => r) in TAUT(A);
end;
Lm1: (p '&' q) => p is valid & (p '&' q) => q is valid
by PROCAL_1:19,PROCAL_1:21;
Lm2: p '&' q is valid implies p is valid & q is valid
proof
assume
A1: p '&' q is valid;
(p '&' q) => p is valid & (p '&' q) => q is valid by Lm1;
hence thesis by A1,CQC_THE1:65;
end;
Lm3: p => q is valid & p => r is valid implies p => q '&' r is valid
by PROCAL_1:52;
Lm4: p => q is valid & r => t is valid implies p 'or' r => q 'or' t is valid
by PROCAL_1:57;
Lm5: p => q is valid & r => t is valid implies p '&' r => q '&' t is valid
by PROCAL_1:56;
Lm6: p => p 'or' q is valid & p => q 'or' p is valid
by PROCAL_1:3,PROCAL_1:4;
Lm7: p => q is valid & r => q is valid implies (p 'or' r) => q is valid
by PROCAL_1:53;
Lm8: p is valid & q is valid implies p '&' q is valid
by PROCAL_1:47;
Lm9: p => q is valid implies r '&' p => r '&' q is valid
by PROCAL_1:50;
Lm10: p => q is valid implies p 'or' r => q 'or' r is valid
by PROCAL_1:48;
Lm11: p 'or' q => ('not' p => q) is valid
by PROCAL_1:5;
Lm12: ('not' p => q) => (p 'or' q) is valid
proof
'not' 'not' p => p in TAUT(A) by LUKASI_1:25;
then
('not' p => q) => ('not' 'not' p 'or' q) in TAUT(A) &
'not' 'not' p 'or' q
=> p 'or' q in TAUT(A) by PROCAL_1:14,48;
hence ('not' p => q) => (p 'or' q) in TAUT(A) by LUKASI_1:3;
end;
Lm13: p <=> p is valid
proof
(p => p) '&' (p => p) is valid by Lm8;
hence thesis by QC_LANG2:def 4;
end;
Lm14: p => q is valid & q => p is valid iff p <=> q is valid
proof
thus p => q is valid & q => p is valid implies p <=> q is valid
proof
assume p => q is valid & q => p is valid;
then (p => q) '&' (q => p) is valid by Lm8;
hence thesis by QC_LANG2:def 4;
end;
assume p <=> q is valid;
then (p => q) '&' (q => p) is valid by QC_LANG2:def 4;
hence thesis by Lm2;
end;
Lm15: p <=> q is valid implies ( p is valid iff q is valid)
proof
assume
A1: p <=> q in TAUT(A);
(p <=> q) => (p => q) in TAUT(A) by PROCAL_1:23;
then
A2: p => q in TAUT(A) by A1,CQC_THE1:46;
thus p is valid implies q is valid
by A2,CQC_THE1:46;
assume
A3: q in TAUT(A);
(p <=> q) => (q => p) in TAUT(A) by PROCAL_1:24;
then q => p in TAUT(A) by A1,CQC_THE1:46;
hence p in TAUT(A) by A3,CQC_THE1:46;
end;
Lm16: p => (q => r) is valid & r => t is valid implies p => (q => t) is valid
proof
assume that
A1: p => (q => r) is valid and
A2: r => t is valid;
(p '&' q) => r is valid by A1,Th1;
then (p '&' q) => t is valid by A2,LUKASI_1:42;
hence thesis by Th3;
end;
::------------------------------------------------
theorem Th5:
y in still_not-bound_in All(x,s) iff y in still_not-bound_in s & y <> x
proof
still_not-bound_in All(x,s) = still_not-bound_in s \ {x} by QC_LANG3:12;
hence thesis by ZFMISC_1:56;
end;
theorem Th6:
y in still_not-bound_in Ex(x,s) iff y in still_not-bound_in s & y <> x
proof
still_not-bound_in Ex(x,s) = still_not-bound_in s \ {x} by QC_LANG3:19;
hence thesis by ZFMISC_1:56;
end;
theorem Th7:
y in still_not-bound_in s => h iff y in still_not-bound_in s or y
in still_not-bound_in h
proof
still_not-bound_in s => h = still_not-bound_in s \/ still_not-bound_in h
by QC_LANG3:16;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th8:
y in still_not-bound_in s '&' h iff y in still_not-bound_in s or
y in still_not-bound_in h
proof
still_not-bound_in s '&' h = still_not-bound_in s \/ still_not-bound_in
h by QC_LANG3:10;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th9:
y in still_not-bound_in s 'or' h iff y in still_not-bound_in s
or y in still_not-bound_in h
proof
still_not-bound_in s 'or' h = still_not-bound_in s \/ still_not-bound_in
h by QC_LANG3:14;
hence thesis by XBOOLE_0:def 3;
end;
theorem
not x in still_not-bound_in All(x,y,s) & not y in still_not-bound_in
All(x,y,s)
proof
not y in still_not-bound_in All(y,s) by Th5;
then
A1: not y in still_not-bound_in All(x,All(y,s)) by Th5;
not x in still_not-bound_in All(x,All(y,s)) by Th5;
hence thesis by A1,QC_LANG2:14;
end;
theorem
not x in still_not-bound_in Ex(x,y,s) & not y in still_not-bound_in Ex
(x,y,s)
proof
not y in still_not-bound_in Ex(y,s) by Th6;
then
A1: not y in still_not-bound_in Ex(x,Ex(y,s)) by Th6;
not x in still_not-bound_in Ex(x,Ex(y,s)) by Th6;
hence thesis by A1,QC_LANG2:14;
end;
theorem Th12:
(s => h).x = (s.x) => (h.x)
proof
s => h = 'not'(s '&' 'not' h) by QC_LANG2:def 2;
hence (s => h).x = 'not'((s '&' 'not' h).x) by CQC_LANG:19
.= 'not'((s.x) '&' ('not' h).x) by CQC_LANG:21
.= 'not'((s.x) '&' 'not'(h.x)) by CQC_LANG:19
.= (s.x) => (h.x) by QC_LANG2:def 2;
end;
theorem
(s 'or' h).x = (s.x) 'or' (h.x)
proof
thus (s 'or' h).x = ('not'('not' s '&' 'not' h)).x by QC_LANG2:def 3
.= 'not'(('not' s '&' 'not' h).x) by CQC_LANG:19
.= 'not'((('not' s).x) '&' (('not' h).x)) by CQC_LANG:21
.= 'not'('not'(s.x) '&' (('not' h).x)) by CQC_LANG:19
.= 'not'('not'(s.x) '&' 'not'(h.x)) by CQC_LANG:19
.= (s.x) 'or' (h.x) by QC_LANG2:def 3;
end;
theorem
x<>y implies (Ex(x,p)).y = Ex(x,p.y)
proof
assume
A1: x<>y;
thus (Ex(x,p)).y = ('not' All(x,'not' p)).y by QC_LANG2:def 5
.= 'not'(All(x,'not' p).y) by CQC_LANG:19
.= 'not'(All(x,('not' p).y)) by A1,CQC_LANG:25
.= 'not' All(x,'not'(p.y)) by CQC_LANG:19
.= Ex(x,p.y) by QC_LANG2:def 5;
end;
::---------------------------------------------------------
theorem Th15:
p => Ex(x,p) is valid
proof
All(x,'not' p) => 'not' p is valid by CQC_THE1:66;
then 'not' 'not' p => 'not' All(x,'not' p) is valid by LUKASI_1:52;
then
A1: 'not' 'not' p => Ex(x,p) is valid by QC_LANG2:def 5;
('not' 'not' p => Ex(x,p)) => (p => Ex(x,p)) is valid;
hence thesis by A1,CQC_THE1:65;
end;
theorem Th16:
p is valid implies Ex(x,p) is valid
proof
assume
A1: p is valid;
p => Ex(x,p) is valid by Th15;
hence thesis by A1,CQC_THE1:65;
end;
theorem
All(x,p) => Ex(x,p) is valid
proof
All(x,p) => p is valid & p => Ex(x,p) is valid by Th15,CQC_THE1:66;
hence thesis by LUKASI_1:42;
end;
theorem
All(x,p) => Ex(y,p) is valid
proof
All(x,p) => p is valid & p => Ex(y,p) is valid by Th15,CQC_THE1:66;
hence thesis by LUKASI_1:42;
end;
theorem Th19:
p => q is valid & not x in still_not-bound_in q implies Ex(x,p) => q is valid
proof
assume p => q is valid & not x in still_not-bound_in q;
then 'not' q => 'not' p is valid & not x in still_not-bound_in 'not' q by
LUKASI_1:52,QC_LANG3:7;
then 'not' q => All(x,'not' p) is valid by CQC_THE1:67;
then 'not' All(x,'not' p) => 'not' 'not' q is valid by LUKASI_1:52;
then Ex(x,p) => 'not' 'not' q is valid by QC_LANG2:def 5;
hence thesis by LUKASI_1:55;
end;
theorem Th20:
not x in still_not-bound_in p implies Ex(x,p) => p is valid
proof
A1: p => p is valid;
assume not x in still_not-bound_in p;
hence thesis by A1,Th19;
end;
theorem
not x in still_not-bound_in p & Ex(x,p) is valid implies p is valid
proof
assume that
A1: not x in still_not-bound_in p and
A2: Ex(x,p) is valid;
Ex(x,p) => p is valid by A1,Th20;
hence thesis by A2,CQC_THE1:65;
end;
theorem Th22:
p=h.x & q=h.y & not y in still_not-bound_in h implies p => Ex(y, q) is valid
proof
assume that
A1: p=h.x and
A2: q=h.y and
A3: not y in still_not-bound_in h;
A4: (h => Ex(y,q)).x = (h.x) => (Ex(y,q).x) by Th12
.= p => Ex(y,q) by A1,CQC_LANG:27;
not y in still_not-bound_in Ex(y,q) by Th6;
then
A5: not y in still_not-bound_in h => Ex(y,q) by A3,Th7;
A6: q => Ex(y,q) is valid by Th15;
(h => Ex(y,q)).y = (h.y) => (Ex(y,q).y) by Th12
.= q => Ex(y,q) by A2,CQC_LANG:27;
hence thesis by A6,A4,A5,CQC_THE1:68;
end;
theorem Th23:
p is valid implies All(x,p) is valid
proof
A1: p => ((All(x,p) => All(x,p)) => p) is valid;
not x in still_not-bound_in All(x,p) by Th5;
then
A2: not x in still_not-bound_in All(x,p) => All(x,p) by Th7;
assume p is valid;
then (All(x,p) => All(x,p)) => p is valid by A1,CQC_THE1:65;
then (All(x,p) => All(x,p)) => All(x,p) is valid by A2,CQC_THE1:67;
hence thesis by CQC_THE1:65;
end;
theorem Th24:
not x in still_not-bound_in p implies p => All(x,p) is valid
proof
A1: p => p is valid;
assume not x in still_not-bound_in p;
hence thesis by A1,CQC_THE1:67;
end;
theorem Th25:
p=h.x & q=h.y & not x in still_not-bound_in h implies All(x,p) => q is valid
proof
assume that
A1: p=h.x and
A2: q=h.y and
A3: not x in still_not-bound_in h;
A4: (All(x,p) => h).y = (All(x,p).y) => q by A2,Th12
.= All(x,p) => q by CQC_LANG:27;
not x in still_not-bound_in All(x,p) by Th5;
then
A5: All(x,p) => p is valid & not x in still_not-bound_in All(x,p) => h by A3
,Th7,CQC_THE1:66;
(All(x,p) => h).x = (All(x,p).x) => p by A1,Th12
.= All(x,p) => p by CQC_LANG:27;
hence thesis by A4,A5,CQC_THE1:68;
end;
theorem
not y in still_not-bound_in p implies All(x,p) => All(y,p) is valid
proof
assume not y in still_not-bound_in p;
then All(x,p) => p is valid & not y in still_not-bound_in All(x,p) by Th5,
CQC_THE1:66;
hence thesis by CQC_THE1:67;
end;
theorem
p=h.x & q=h.y & not x in still_not-bound_in h & not y in
still_not-bound_in p implies All(x,p) => All(y,q) is valid
proof
assume p=h.x & q=h.y & not x in still_not-bound_in h & not y in
still_not-bound_in p;
then ( not y in still_not-bound_in All(x,p))& All(x,p) => q is valid by Th5
,Th25;
hence thesis by CQC_THE1:67;
end;
theorem
not x in still_not-bound_in p implies Ex(x,p) => Ex(y,p) is valid
proof
assume not x in still_not-bound_in p;
then
A1: not x in still_not-bound_in Ex(y,p) by Th6;
p => Ex(y,p) is valid by Th15;
hence thesis by A1,Th19;
end;
theorem
p=h.x & q=h.y & not x in still_not-bound_in q & not y in
still_not-bound_in h implies Ex(x,p) => Ex(y,q) is valid
proof
assume p=h.x & q=h.y & not x in still_not-bound_in q & not y in
still_not-bound_in h;
then ( not x in still_not-bound_in Ex(y,q))& p => Ex(y,q) is valid by Th6
,Th22;
hence thesis by Th19;
end;
theorem Th30:
All(x,p => q) => (All(x,p) => All(x,q)) is valid
proof
All(x,p => q) => (p => q) is valid by CQC_THE1:66;
then
A1: p => (All(x,p => q) => q) is valid by LUKASI_1:44;
All(x,p) => p is valid by CQC_THE1:66;
then All(x,p) => (All(x,p => q) => q) is valid by A1,LUKASI_1:42;
then
A2: (All(x,p => q) '&' All(x,p)) => q is valid by Th2;
( not x in still_not-bound_in All(x,p => q))& not x in
still_not-bound_in All( x,p) by Th5;
then not x in still_not-bound_in All(x,p => q) '&' All(x,p) by Th8;
then (All(x,p => q) '&' All(x,p)) => All(x,q) is valid by A2,CQC_THE1:67;
hence thesis by Th3;
end;
theorem Th31:
All(x,p => q) is valid implies All(x,p) => All(x,q) is valid
proof
assume
A1: All(x,p => q) is valid;
All(x,p => q) => (All(x,p) => All(x,q)) is valid by Th30;
hence thesis by A1,CQC_THE1:65;
end;
theorem Th32:
All(x,p <=> q) => (All(x,p) <=> All(x,q)) is valid
proof
A1: All(x,(p => q) '&' (q => p)) => ((p => q) '&' (q => p)) is valid by
CQC_THE1:66;
(p <=> q) => (p <=> q) is valid;
then (p <=> q) => ((p => q) '&' (q => p)) is valid by QC_LANG2:def 4;
then All(x,(p <=> q) => ((p => q) '&' (q => p))) is valid by Th23;
then
A2: All(x,p <=> q) => All(x,(p => q) '&' (q => p)) is valid by Th31;
All(x,p => q) => (All(x,p) => All(x,q)) is valid & All(x,q => p) => (
All(x,q ) => All(x,p)) is valid by Th30;
then
(All(x,p => q) '&' All(x,q => p)) => ((All(x,p) => All(x,q)) '&' (All(x
,q) => All(x,p))) is valid by Lm5;
then
A3: (All(x,p => q) '&' All(x,q => p)) => (All(x,p) <=> All(x,q)) is valid
by QC_LANG2:def 4;
A4: not x in still_not-bound_in All(x,(p => q) '&' (q => p)) by Th5;
((p => q) '&' (q => p)) => (q => p) is valid by Lm1;
then All(x,(p => q) '&' (q => p)) => (q => p) is valid by A1,LUKASI_1:42;
then
A5: All(x,(p => q) '&' (q => p)) => All(x,q => p) is valid by A4,CQC_THE1:67;
((p => q) '&' (q => p)) => (p => q) is valid by Lm1;
then All(x,(p => q) '&' (q => p)) => (p => q) is valid by A1,LUKASI_1:42;
then All(x,(p => q) '&' (q => p)) => All(x,p => q) is valid by A4,CQC_THE1:67
;
then All(x,(p => q) '&' (q => p)) => (All(x,p => q) '&' All(x,q => p)) is
valid by A5,Lm3;
then All(x,(p => q) '&' (q => p)) => (All(x,p) <=> All(x,q)) is valid by A3,
LUKASI_1:42;
hence thesis by A2,LUKASI_1:42;
end;
theorem
All(x,p <=> q) is valid implies All(x,p) <=> All(x,q) is valid
proof
assume
A1: All(x,p <=> q) is valid;
All(x,p <=> q) => (All(x,p) <=> All(x,q)) is valid by Th32;
hence thesis by A1,CQC_THE1:65;
end;
theorem Th34:
All(x,p => q) => (Ex(x,p) => Ex(x,q)) is valid
proof
All(x,p => q) => (p => q) is valid by CQC_THE1:66;
then
A1: (p '&' All(x,p => q)) => q is valid by Th2;
q => Ex(x,q) is valid by Th15;
then (p '&' All(x,p => q)) => Ex(x,q) is valid by A1,LUKASI_1:42;
then
A2: p => (All(x,p => q) => Ex(x,q)) is valid by Th3;
( not x in still_not-bound_in All(x,p => q))& not x in
still_not-bound_in Ex(x,q) by Th5,Th6;
then not x in still_not-bound_in All(x,p => q) => Ex(x,q) by Th7;
then Ex(x,p) => (All(x,p => q) => Ex(x,q)) is valid by A2,Th19;
hence thesis by LUKASI_1:44;
end;
theorem Th35:
All(x,p => q) is valid implies Ex(x,p) => Ex(x,q) is valid
proof
assume
A1: All(x,p => q) is valid;
All(x,p => q) => (Ex(x,p) => Ex(x,q)) is valid by Th34;
hence thesis by A1,CQC_THE1:65;
end;
theorem Th36:
All(x,p '&' q) => (All(x,p) '&' All(x,q)) is valid & (All(x,p)
'&' All(x,q)) => All(x,p '&' q) is valid
proof
All(x,p) => p is valid & All(x,q) => q is valid by CQC_THE1:66;
then
A1: (All(x,p) '&' All(x,q)) => (p '&' q) is valid by Lm5;
All(x,p '&'q => q) is valid & All(x,p '&' q => q) => (All(x,p '&' q) =>
All( x,q)) is valid by Lm1,Th23,Th30;
then
A2: All(x,p '&' q) => All(x,q) is valid by CQC_THE1:65;
All(x,p '&' q => p) is valid & All(x,p '&' q => p) => (All(x,p '&' q) =>
All (x,p)) is valid by Lm1,Th23,Th30;
then All(x,p '&' q) => All(x,p) is valid by CQC_THE1:65;
hence All(x,p '&' q) => (All(x,p) '&' All(x,q)) is valid by A2,Lm3;
( not x in still_not-bound_in All(x,p))& not x in still_not-bound_in
All( x, q ) by Th5;
then not x in still_not-bound_in All(x,p) '&' All(x,q) by Th8;
hence thesis by A1,CQC_THE1:67;
end;
theorem Th37:
All(x,p '&' q) <=> (All(x,p) '&' All(x,q)) is valid
proof
All(x,p '&' q) => (All(x,p) '&' All(x,q)) is valid & (All(x,p) '&' All(x
,q)) => All(x,p '&' q) is valid by Th36;
hence thesis by Lm14;
end;
theorem
All(x,p '&' q) is valid iff All(x,p) '&' All(x,q) is valid
proof
All(x,p '&' q) <=> (All(x,p) '&' All(x,q)) is valid by Th37;
hence thesis by Lm15;
end;
theorem Th39:
(All(x,p) 'or' All(x,q)) => All(x,p 'or' q) is valid
proof
All(x,q => p 'or' q) is valid & All(x,q => p 'or' q) => (All(x,q) => All
(x,p 'or' q)) is valid by Lm6,Th23,Th30;
then
A1: All(x,q) => All(x,p 'or' q) is valid by CQC_THE1:65;
All(x,p => p 'or' q) is valid & All(x,p => p 'or' q) => (All(x,p) => All
(x,p 'or' q)) is valid by Lm6,Th23,Th30;
then All(x,p) => All(x,p 'or' q) is valid by CQC_THE1:65;
hence thesis by A1,Lm7;
end;
theorem Th40:
Ex(x,p 'or' q) => (Ex(x,p) 'or' Ex(x,q)) is valid & (Ex(x,p)
'or' Ex(x,q)) => Ex(x,p 'or' q) is valid
proof
( not x in still_not-bound_in Ex(x,p))& not x in still_not-bound_in Ex(x
,q) by Th6;
then
A1: not x in still_not-bound_in Ex(x,p) 'or' Ex(x,q) by Th9;
p => Ex(x,p) is valid & q => Ex(x,q) is valid by Th15;
then (p 'or' q) => (Ex(x,p) 'or' Ex(x,q)) is valid by Lm4;
hence Ex(x,(p 'or' q)) => (Ex(x,p) 'or' Ex(x,q)) is valid by A1,Th19;
All(x,q => p 'or' q) is valid & All(x,q => p 'or' q) => (Ex(x,q) => Ex(
x,p 'or' q)) is valid by Lm6,Th23,Th34;
then
A2: Ex(x,q) => Ex(x,p 'or' q) is valid by CQC_THE1:65;
All(x,p => p 'or' q) is valid & All(x,p => p 'or' q) => (Ex(x,p) => Ex(
x,p 'or' q)) is valid by Lm6,Th23,Th34;
then Ex(x,p) => Ex(x,p 'or' q) is valid by CQC_THE1:65;
hence thesis by A2,Lm7;
end;
theorem Th41:
Ex(x,p 'or' q) <=> (Ex(x,p) 'or' Ex(x,q)) is valid
proof
Ex(x,p 'or' q) => (Ex(x,p) 'or' Ex(x,q)) is valid & (Ex(x,p) 'or' Ex(x,q
)) => Ex(x,p 'or' q) is valid by Th40;
hence thesis by Lm14;
end;
theorem
Ex(x,p 'or' q) is valid iff Ex(x,p) 'or' Ex(x,q) is valid
proof
Ex(x,p 'or' q) <=> (Ex(x,p) 'or' Ex(x,q)) is valid by Th41;
hence thesis by Lm15;
end;
theorem Th43:
Ex(x,p '&' q) => (Ex(x,p) '&' Ex(x,q)) is valid
proof
All(x,p '&' q => q) is valid by Lm1,Th23;
then
A1: Ex(x,p '&' q) => Ex(x,q) is valid by Th35;
All(x,p '&' q => p) is valid by Lm1,Th23;
then Ex(x,p '&' q) => Ex(x,p) is valid by Th35;
hence thesis by A1,Lm3;
end;
theorem
Ex(x,p '&' q) is valid implies Ex(x,p) '&' Ex(x,q) is valid
proof
assume
A1: Ex(x,p '&' q) is valid;
Ex(x,p '&' q) => (Ex(x,p) '&' Ex(x,q)) is valid by Th43;
hence thesis by A1,CQC_THE1:65;
end;
theorem Th45:
All(x,'not' 'not' p) => All(x,p) is valid & All(x,p) => All(x,
'not' 'not' p) is valid
proof
All(x,'not' 'not' p => p) is valid & All(x,p => 'not' 'not' p) is valid
by Th23;
hence thesis by Th31;
end;
theorem
All(x,'not' 'not' p) <=> All(x,p) is valid
proof
All(x,'not' 'not' p) => All(x,p) is valid & All(x,p) => All(x,'not'
'not' p) is valid by Th45;
hence thesis by Lm14;
end;
theorem Th47:
Ex(x,'not' 'not' p) => Ex(x,p) is valid & Ex(x,p) => Ex(x,'not'
'not' p) is valid
proof
All(x,'not' 'not' p => p) is valid & All(x,p => 'not' 'not' p) is valid
by Th23;
hence thesis by Th35;
end;
theorem
Ex(x,'not' 'not' p) <=> Ex(x,p) is valid
proof
Ex(x,'not' 'not' p) => Ex(x,p) is valid & Ex(x,p) => Ex(x,'not' 'not' p)
is valid by Th47;
hence thesis by Lm14;
end;
theorem Th49:
'not' Ex(x,'not' p) => All(x,p) is valid & All(x,p) => 'not' Ex(
x,'not' p) is valid
proof
A1: All(x,'not' 'not' p) => All(x,p) is valid by Th45;
A2: 'not' Ex(x,'not' p) = 'not' 'not' All(x,'not' 'not' p) by QC_LANG2:def 5;
then 'not' Ex(x,'not' p) => All(x,'not' 'not' p) is valid;
hence 'not' Ex(x,'not' p) => All(x,p) is valid by A1,LUKASI_1:42;
All(x,p) => All(x,'not' 'not' p) is valid & All(x,'not' 'not' p) =>
'not' 'not' All(x,'not' 'not' p) is valid by Th45;
hence thesis by A2,LUKASI_1:42;
end;
theorem
'not' Ex(x,'not' p) <=> All(x,p) is valid
proof
'not' Ex(x,'not' p) => All(x,p) is valid & All(x,p) => 'not' Ex(x,'not'
p) is valid by Th49;
hence thesis by Lm14;
end;
theorem Th51:
'not' All(x,p) => Ex(x,'not' p) is valid & Ex(x,'not' p) =>
'not' All(x,p) is valid
proof
A1: Ex(x,'not' p) = 'not' All(x,'not' 'not' p) by QC_LANG2:def 5;
All(x,'not' 'not' p) => All(x,p) is valid by Th45;
hence 'not' All(x,p) => Ex(x,'not' p) is valid by A1,LUKASI_1:52;
All(x,p) => All(x,'not' 'not' p) is valid by Th45;
hence thesis by A1,LUKASI_1:52;
end;
theorem
'not' All(x,p) <=> Ex(x,'not' p) is valid
proof
'not' All(x,p) => Ex(x,'not' p) is valid & Ex(x,'not' p) => 'not' All(x,
p) is valid by Th51;
hence thesis by Lm14;
end;
theorem
'not' Ex(x,p) => All(x,'not' p) is valid & All(x,'not' p) => 'not' Ex(
x, p ) is valid
proof
A1: 'not' Ex(x,p) = 'not' 'not' All(x,'not' p) by QC_LANG2:def 5;
hence 'not' Ex(x,p) => All(x,'not' p) is valid;
thus thesis by A1;
end;
theorem Th54:
All(x,'not' p) <=> 'not' Ex(x,p) is valid
proof
'not' 'not' All(x,'not' p) => All(x,'not' p) is valid;
then
A1: 'not' Ex(x,p) => All(x,'not' p) is valid by QC_LANG2:def 5;
All(x,'not' p) => 'not' 'not' All(x,'not' p) is valid;
then All(x,'not' p) => 'not' Ex(x,p) is valid by QC_LANG2:def 5;
hence thesis by A1,Lm14;
end;
theorem
All(x,All(y,p)) => All(y,All(x,p)) is valid & All(x,y,p) => All(y,x,p)
is valid
proof
not y in still_not-bound_in All(y,p) by Th5;
then
A1: not y in still_not-bound_in All(x,All(y,p)) by Th5;
All(x,All(y,p) => p) is valid & All(x,All(y,p) => p) => (All(x,All(y,p))
=> All(x,p)) is valid by Th23,Th30,CQC_THE1:66;
then All(x,All(y,p)) => All(x,p) is valid by CQC_THE1:65;
hence All(x,All(y,p)) => All(y,All(x,p)) is valid by A1,CQC_THE1:67;
then All(x,y,p) => All(y,All(x,p)) is valid by QC_LANG2:14;
hence thesis by QC_LANG2:14;
end;
theorem
p=h.x & q=h.y & not y in still_not-bound_in h implies All(x,All(y,q))
=> All(x,p) is valid
proof
assume p=h.x & q=h.y & not y in still_not-bound_in h;
then All(x,All(y,q) => p) is valid by Th23,Th25;
hence thesis by Th31;
end;
theorem
Ex(x,Ex(y,p)) => Ex(y,Ex(x,p)) is valid & Ex(x,y,p) => Ex(y,x,p) is valid
proof
not x in still_not-bound_in Ex(x,p) by Th6;
then
A1: not x in still_not-bound_in Ex(y,Ex(x,p)) by Th6;
All(y,p => Ex(x,p)) is valid & All(y,p => Ex(x,p)) => (Ex(y,p) => Ex(y,
Ex(x, p))) is valid by Th15,Th23,Th34;
then Ex(y,p) => Ex(y,Ex(x,p)) is valid by CQC_THE1:65;
hence Ex(x,Ex(y,p)) => Ex(y,Ex(x,p)) is valid by A1,Th19;
then Ex(x,y,p) => Ex(y,Ex(x,p)) is valid by QC_LANG2:14;
hence thesis by QC_LANG2:14;
end;
theorem
p=h.x & q=h.y & not y in still_not-bound_in h implies Ex(x,p) => Ex(x,
y,q) is valid
proof
assume p=h.x & q=h.y & not y in still_not-bound_in h;
then All(x,p => Ex(y,q)) is valid by Th22,Th23;
then Ex(x,p) => Ex(x,Ex(y,q)) is valid by Th35;
hence thesis by QC_LANG2:14;
end;
theorem
Ex(x,All(y,p)) => All(y,Ex(x,p)) is valid
proof
not x in still_not-bound_in Ex(x,p) by Th6;
then
A1: not x in still_not-bound_in All(y,Ex(x,p)) by Th5;
All(y,p => Ex(x,p)) is valid & All(y,p => Ex(x,p)) => (All(y,p) => All(y
,Ex( x,p))) is valid by Th15,Th23,Th30;
then All(y,p) => All(y,Ex(x,p)) is valid by CQC_THE1:65;
hence thesis by A1,Th19;
end;
theorem
Ex(x,p <=> p) is valid by Lm13,Th16;
theorem Th61:
Ex(x,p => q) => (All(x,p) => Ex(x,q)) is valid & (All(x,p) => Ex
(x,q)) => Ex(x,p => q) is valid
proof
All(x,p) => p is valid by CQC_THE1:66;
then
A1: (p => q) => (All(x,p) => q) is valid by LUKASI_1:41;
( not x in still_not-bound_in All(x,p))& not x in still_not-bound_in Ex(
x, q ) by Th5,Th6;
then
A2: not x in still_not-bound_in All(x,p) => Ex(x,q) by Th7;
q => Ex(x,q) is valid by Th15;
then (p => q) => (All(x,p) => Ex(x,q)) is valid by A1,Lm16;
hence Ex(x,p => q) => (All(x,p) => Ex(x,q)) is valid by A2,Th19;
All(x,p '&' 'not' q) => (All(x,p) '&' All(x,'not' q)) is valid by Th36;
then
A3: 'not'(All(x,p) '&' All(x,'not' q)) => 'not' All(x,p '&' 'not' q) is
valid by LUKASI_1:52;
'not' All(x,p '&' 'not' q) => Ex(x,'not'(p '&' 'not' q)) is valid by Th51;
then 'not'(All(x,p) '&' All(x,'not' q)) => Ex(x,'not'(p '&' 'not' q)) is
valid by A3,LUKASI_1:42;
then
A4: 'not'(All(x,p) '&' All(x,'not' q)) => Ex(x,p => q) is valid by
QC_LANG2:def 2;
All(x,'not' q) => 'not' 'not' All(x,'not' q) is valid;
then
A5: (All(x,p) '&' All(x,'not' q)) => (All(x,p) '&' 'not' 'not' All(x,'not'
q)) is valid by Lm9;
All(x,p) => Ex(x,q) = All(x,p) => 'not' All(x,'not' q) by QC_LANG2:def 5
.= 'not'(All(x,p) '&' 'not' 'not' All(x,'not' q)) by QC_LANG2:def 2;
then
(All(x,p) => Ex(x,q)) => 'not'(All(x,p) '&' All(x,'not' q)) is valid by A5,
LUKASI_1:52;
hence thesis by A4,LUKASI_1:42;
end;
theorem Th62:
Ex(x,p => q) <=> (All(x,p) => Ex(x,q)) is valid
proof
Ex(x,p => q) => (All(x,p) => Ex(x,q)) is valid & (All(x,p) => Ex(x,q))
=> Ex (x,p => q) is valid by Th61;
hence thesis by Lm14;
end;
theorem
Ex(x,p => q) is valid iff All(x,p) => Ex(x,q) is valid
proof
Ex(x,p => q) <=> (All(x,p) => Ex(x,q)) is valid by Th62;
hence thesis by Lm15;
end;
theorem Th64:
All(x,p '&' q) => (p '&' All(x,q)) is valid
proof
A1: All(x,p '&' q) => (p '&' q) is valid by CQC_THE1:66;
A2: not x in still_not-bound_in All(x,p '&' q) by Th5;
(p '&' q) => q is valid by Lm1;
then All(x,p '&' q) => q is valid by A1,LUKASI_1:42;
then
A3: All(x,p '&' q) => All(x,q) is valid by A2,CQC_THE1:67;
(p '&' q) => p is valid by Lm1;
then All(x,p '&' q) => p is valid by A1,LUKASI_1:42;
hence thesis by A3,Lm3;
end;
theorem Th65:
All(x,p '&' q) => (All(x,p) '&' q) is valid
proof
A1: (q '&' All(x,p)) => (All(x,p) '&' q) is valid by CQC_THE1:64;
All(x,(p '&' q) => (q '&' p)) is valid & All(x,(p '&' q) => (q '&' p))
=> ( All(x,p '&' q) => All(x,q '&' p)) is valid by Th23,Th30,CQC_THE1:64;
then
A2: All(x,p '&' q) => All(x,q '&' p) is valid by CQC_THE1:65;
All(x,q '&' p) => (q '&' All(x,p)) is valid by Th64;
then All(x,p '&' q) => (q '&' All(x,p)) is valid by A2,LUKASI_1:42;
hence thesis by A1,LUKASI_1:42;
end;
theorem Th66:
not x in still_not-bound_in p implies (p '&' All(x,q)) => All(x,
p '&' q) is valid
proof
assume
A1: not x in still_not-bound_in p;
All(x,q) => q is valid by CQC_THE1:66;
then
A2: p '&' All(x,q) => p '&' q is valid by Lm9;
not x in still_not-bound_in All(x,q) by Th5;
then not x in still_not-bound_in p '&' All(x,q) by A1,Th8;
hence thesis by A2,CQC_THE1:67;
end;
theorem
not x in still_not-bound_in p & p '&' All(x,q) is valid implies All(x,
p '&' q ) is valid
proof
assume that
A1: not x in still_not-bound_in p and
A2: p '&' All(x,q) is valid;
(p '&' All(x,q)) => All(x,p '&' q) is valid by A1,Th66;
hence thesis by A2,CQC_THE1:65;
end;
theorem Th68:
not x in still_not-bound_in p implies (p 'or' All(x,q)) => All(x
,p 'or' q) is valid & All(x,p 'or' q) => (p 'or' All(x,q)) is valid
proof
A1: not x in still_not-bound_in All(x,p 'or' q) by Th5;
All(x,p 'or' q) => (p 'or' q) is valid & (p 'or' q) => ('not' p => q) is
valid by Lm11,CQC_THE1:66;
then All(x,p 'or' q) => ('not' p => q) is valid by LUKASI_1:42;
then
A2: (All(x,p 'or' q) '&' 'not' p) => q is valid by Th1;
assume
A3: not x in still_not-bound_in p;
then not x in still_not-bound_in 'not' p by QC_LANG3:7;
then not x in still_not-bound_in All(x,p 'or' q) '&' 'not' p by A1,Th8;
then (All(x,p 'or' q) '&' 'not' p) => All(x,q) is valid by A2,CQC_THE1:67;
then
A4: All(x, p 'or' q) => ('not' p => All(x,q)) is valid by Th3;
p => p is valid;
then p => All(x,p) is valid by A3,CQC_THE1:67;
then
A5: (p 'or' All(x,q)) => (All(x,p) 'or' All(x,q)) is valid by Lm10;
(All(x,p) 'or' All(x,q)) => All(x,p 'or' q) is valid by Th39;
hence (p 'or' All(x,q)) => All(x,p 'or' q) is valid by A5,LUKASI_1:42;
('not' p => All(x,q)) => (p 'or' All(x,q)) is valid by Lm12;
hence thesis by A4,LUKASI_1:42;
end;
theorem Th69:
not x in still_not-bound_in p implies (p 'or' All(x,q)) <=> All(
x,p 'or' q) is valid
proof
assume not x in still_not-bound_in p;
then (p 'or' All(x,q)) => All(x,p 'or' q) is valid & All(x,p 'or' q) => (p
'or' All(x,q)) is valid by Th68;
hence thesis by Lm14;
end;
theorem
not x in still_not-bound_in p implies ( p 'or' All(x,q) is valid iff
All(x,p 'or' q) is valid)
proof
assume not x in still_not-bound_in p;
then (p 'or' All(x,q)) <=> All(x,p 'or' q) is valid by Th69;
hence thesis by Lm15;
end;
theorem Th71:
not x in still_not-bound_in p implies (p '&' Ex(x,q)) => Ex(x,p
'&' q) is valid & Ex(x,p '&' q) => (p '&' Ex(x,q)) is valid
proof
assume
A1: not x in still_not-bound_in p;
p '&' q => Ex(x,p '&' q) is valid by Th15;
then
A2: q => (p => Ex(x,p '&' q)) is valid by Th4;
not x in still_not-bound_in Ex(x,p '&' q) by Th6;
then not x in still_not-bound_in p => Ex(x,p '&' q) by A1,Th7;
then Ex(x,q) => (p => Ex(x,p '&' q)) is valid by A2,Th19;
hence (p '&' Ex(x,q)) => Ex(x,p '&' q) is valid by Th2;
q => Ex(x,q) is valid by Th15;
then
A3: p '&' q => p '&' Ex(x,q) is valid by Lm9;
not x in still_not-bound_in Ex(x,q) by Th6;
then not x in still_not-bound_in p '&' Ex(x,q) by A1,Th8;
hence thesis by A3,Th19;
end;
theorem Th72:
not x in still_not-bound_in p implies (p '&' Ex(x,q)) <=> Ex(x,p
'&' q) is valid
proof
assume not x in still_not-bound_in p;
then
(p '&' Ex(x,q)) => Ex(x,p '&' q) is valid & Ex(x,p '&' q) => (p '&' Ex(x
,q)) is valid by Th71;
hence thesis by Lm14;
end;
theorem
not x in still_not-bound_in p implies ( p '&' Ex(x,q) is valid iff Ex(
x,p '&' q ) is valid )
proof
assume not x in still_not-bound_in p;
then (p '&' Ex(x,q)) <=> Ex(x,p '&' q) is valid by Th72;
hence thesis by Lm15;
end;
Lm17: not x in still_not-bound_in p implies All(x,p => q) => (p => All(x,q))
is valid
proof
assume not x in still_not-bound_in p;
then
A1: p => All(x,p) is valid by Th24;
All(x,p => q) => (All(x,p) => All(x,q)) is valid by Th30;
then All(x,p) => (All(x,p => q) => All(x,q)) is valid by LUKASI_1:44;
then p => (All(x,p => q) => All(x,q)) is valid by A1,LUKASI_1:42;
hence thesis by LUKASI_1:44;
end;
theorem Th74:
not x in still_not-bound_in p implies All(x,p => q) => (p => All
(x,q)) is valid & (p => All(x,q)) => All(x,p => q) is valid
proof
assume
A1: not x in still_not-bound_in p;
hence All(x,p => q) => (p => All(x,q)) is valid by Lm17;
not x in still_not-bound_in All(x,q) by Th5;
then not x in still_not-bound_in p => All(x,q) by A1,Th7;
then
A2: All(x,(p => All(x,q)) => (p => q)) => ((p => All(x,q)) => All(x,p => q)
) is valid by Lm17;
All(x,(All(x,q) => q) => ((p => All(x,q)) => (p => q))) is valid & All(x
,( All(x,q) => q) => ((p => All(x,q)) => (p => q))) => (All(x,All(x,q) => q) =>
All(x,(p => All(x,q)) => (p => q))) is valid by Th23,Th30;
then
A3: All(x,All(x,q) => q) => All(x,(p => All(x,q)) => (p => q)) is valid by
CQC_THE1:65;
All(x,All(x,q) => q) is valid by Th23,CQC_THE1:66;
then All(x,(p => All(x,q)) => (p => q)) is valid by A3,CQC_THE1:65;
hence thesis by A2,CQC_THE1:65;
end;
theorem Th75:
not x in still_not-bound_in p implies (p => All(x,q)) <=> All(x,
p => q) is valid
proof
assume not x in still_not-bound_in p;
then
(p => All(x,q)) => All(x,p => q) is valid & All(x,p => q) => (p => All(x
,q)) is valid by Th74;
hence thesis by Lm14;
end;
theorem
not x in still_not-bound_in p implies ( All(x,p => q) is valid iff p
=> All(x, q ) is valid )
proof
assume not x in still_not-bound_in p;
then (p => All(x,q)) <=> All(x,p => q) is valid by Th75;
hence thesis by Lm15;
end;
theorem Th77:
not x in still_not-bound_in q implies Ex(x,p => q) => (All(x,p)
=> q) is valid
proof
assume
A1: not x in still_not-bound_in q;
not x in still_not-bound_in All(x,p) by Th5;
then not x in still_not-bound_in All(x,p) => q by A1,Th7;
then
A2: Ex(x,All(x,p) => q) => (All(x,p) => q) is valid by Th20;
All(x,p) => p is valid by CQC_THE1:66;
then
A3: All(x,(p => q) => (All(x,p) => q)) is valid by Th23,LUKASI_1:41;
All(x,(p => q) => (All(x,p) => q)) => (Ex(x,p => q) => Ex(x,All(x,p) =>
q)) is valid by Th34;
then Ex(x,p => q) => Ex(x,All(x,p) => q) is valid by A3,CQC_THE1:65;
hence thesis by A2,LUKASI_1:42;
end;
theorem Th78:
(All(x,p) => q) => Ex(x,p => q) is valid
proof
All(x,p '&' 'not' q) => All(x,p) '&' 'not' q is valid by Th65;
then 'not'(All(x,p) '&' 'not' q) => 'not' All(x,p '&' 'not' q) is valid by
LUKASI_1:52;
then
A1: (All(x,p) => q) => 'not' All(x,p '&' 'not' q) is valid by QC_LANG2:def 2;
All(x,'not' 'not'(p '&' 'not' q) => (p '&' 'not' q)) is valid & All(x,
'not' 'not'(p '&' 'not' q) => (p '&' 'not' q)) => (All(x,'not' 'not'(p '&'
'not' q)) => All(x,(p '&' 'not' q))) is valid by Th23,Th30;
then
All(x,'not' 'not'(p '&' 'not' q)) => All(x,(p '&' 'not' q)) is valid by
CQC_THE1:65;
then
'not' All(x,p '&' 'not' q) => 'not' All(x,'not' 'not'(p '&' 'not' q)) is
valid by LUKASI_1:52;
then (All(x,p) => q) => 'not' All(x,'not' 'not'(p '&' 'not' q)) is valid by
A1,LUKASI_1:42;
then (All(x,p) => q) => Ex(x,'not'(p '&' 'not' q)) is valid by QC_LANG2:def 5
;
hence thesis by QC_LANG2:def 2;
end;
theorem
not x in still_not-bound_in q implies ( All(x,p) => q is valid iff Ex(
x,p => q ) is valid )
proof
assume not x in still_not-bound_in q;
then
A1: Ex(x,p => q) => (All(x,p) => q ) is valid by Th77;
(All(x,p) => q) => Ex(x,p => q) is valid by Th78;
then (All(x,p) => q) <=> Ex(x,p => q) is valid by A1,Lm14;
hence thesis by Lm15;
end;
theorem Th80:
not x in still_not-bound_in q implies (Ex(x,p) => q) => All(x,p
=> q) is valid & All(x,p => q) => (Ex(x,p) => q) is valid
proof
assume
A1: not x in still_not-bound_in q;
p => Ex(x,p) is valid by Th15;
then
A2: (Ex(x,p) => q) => (p => q) is valid by LUKASI_1:41;
not x in still_not-bound_in Ex(x,p) by Th6;
then not x in still_not-bound_in Ex(x,p) => q by A1,Th7;
hence (Ex(x,p) => q) => All(x,p => q) is valid by A2,CQC_THE1:67;
All(x,p => q) => (Ex(x,p) => Ex(x,q)) is valid by Th34;
then
A3: (All(x,p => q) '&' Ex(x,p)) => Ex(x,q) is valid by Th1;
Ex(x,q) => q is valid by A1,Th20;
then (All(x,p => q) '&' Ex(x,p)) => q is valid by A3,LUKASI_1:42;
hence thesis by Th3;
end;
theorem Th81:
not x in still_not-bound_in q implies (Ex(x,p) => q) <=> All(x,p
=> q) is valid
proof
assume not x in still_not-bound_in q;
then
(Ex(x,p) => q) => All(x,p => q) is valid & All(x,p => q) => (Ex(x,p) =>
q ) is valid by Th80;
hence thesis by Lm14;
end;
theorem
not x in still_not-bound_in q implies ( Ex(x,p) => q is valid iff All(
x,p => q) is valid )
proof
assume not x in still_not-bound_in q;
then (Ex(x,p) => q) <=> All(x,p => q) is valid by Th81;
hence thesis by Lm15;
end;
theorem Th83:
not x in still_not-bound_in p implies Ex(x,p => q) => (p => Ex(x
,q)) is valid
proof
assume
A1: not x in still_not-bound_in p;
not x in still_not-bound_in Ex(x,q) by Th6;
then not x in still_not-bound_in p => Ex(x,q) by A1,Th7;
then
A2: Ex(x,p => Ex(x,q)) => (p => Ex(x,q)) is valid by Th20;
q => Ex(x,q) is valid by Th15;
then
A3: All(x,(p => q) => (p => Ex(x,q))) is valid by Th23,LUKASI_1:51;
All(x,(p => q) => (p => Ex(x,q))) => (Ex(x,p => q) => Ex(x,p => Ex(x,q))
) is valid by Th34;
then (Ex(x,p => q) => Ex(x,p => Ex(x,q))) is valid by A3,CQC_THE1:65;
hence thesis by A2,LUKASI_1:42;
end;
theorem Th84:
(p => Ex(x,q)) => Ex(x,p => q) is valid
proof
All(x,'not' 'not'(p '&' 'not' q) => (p '&' 'not' q)) is valid & All(x,
'not' 'not'(p '&' 'not' q) => (p '&' 'not' q)) => (All(x,'not' 'not'(p '&'
'not' q)) => All(x,p '&' 'not' q)) is valid by Th23,Th30;
then All(x,'not' 'not'(p '&' 'not' q)) => All(x,p '&' 'not' q) is valid by
CQC_THE1:65;
then
A1: 'not' All(x,p '&' 'not' q) => 'not' All(x,'not' 'not'(p '&' 'not' q))
is valid by LUKASI_1:52;
All(x,'not' q) <=> 'not' Ex(x,q) is valid by Th54;
then All(x,'not' q) => 'not' Ex(x,q) is valid by Lm14;
then (p '&' All(x,'not' q)) => (p '&' 'not' Ex(x,q)) is valid by Lm9;
then
A2: 'not'(p '&' 'not' Ex(x,q)) => 'not'(p '&' All(x,'not' q)) is valid by
LUKASI_1:52;
All(x,p '&' 'not' q) => (p '&' All(x,'not' q)) is valid by Th64;
then 'not'(p '&' All(x,'not' q)) => 'not' All(x,p '&' 'not' q) is valid by
LUKASI_1:52;
then 'not'(p '&' 'not' Ex(x,q)) => 'not' All(x,p '&' 'not' q) is valid by A2,
LUKASI_1:42;
then (p => Ex(x,q)) => 'not' All(x,p '&' 'not' q) is valid by QC_LANG2:def 2;
then (p => Ex(x,q)) => 'not' All(x,'not' 'not'(p '&' 'not' q)) is valid by A1
,LUKASI_1:42;
then (p => Ex(x,q)) => 'not' All(x,'not'(p => q)) is valid by QC_LANG2:def 2;
hence thesis by QC_LANG2:def 5;
end;
theorem Th85:
not x in still_not-bound_in p implies (p => Ex(x,q)) <=> Ex(x,p
=> q) is valid
proof
assume not x in still_not-bound_in p;
then
A1: Ex(x,p => q) => (p => Ex(x,q)) is valid by Th83;
(p => Ex(x,q)) => Ex(x,p => q) is valid by Th84;
hence thesis by A1,Lm14;
end;
theorem
not x in still_not-bound_in p implies ( p => Ex(x,q) is valid iff Ex(x
,p => q ) is valid )
proof
assume not x in still_not-bound_in p;
then (p => Ex(x,q)) <=> Ex(x,p => q) is valid by Th85;
hence thesis by Lm15;
end;
theorem
{p} |- p
proof
p in {p} & {p} c= Cn({p}) by CQC_THE1:17,TARSKI:def 1;
hence p in Cn({p});
end;
theorem Th88:
Cn({p} \/ {q}) = Cn({p '&' q})
proof
for t holds t in Cn({p} \/ {q}) iff for T st T is being_a_theory & {p
'&' q} c= T holds t in T
proof
let t;
thus t in Cn({p} \/ {q}) implies for T st T is being_a_theory & {p '&' q}
c= T holds t in T
proof
assume
A1: t in Cn({p} \/ {q});
let T;
assume that
A2: T is being_a_theory and
A3: {p '&' q} c= T;
A4: p '&' q in T & TAUT(A) c= T by A2,A3,CQC_THE1:38,ZFMISC_1:31;
p '&' q => q in TAUT(A) by PROCAL_1:21;
then q in T by A2,A4;
then
A5: {q} c= T by ZFMISC_1:31;
p '&' q => p in TAUT(A) by PROCAL_1:19;
then p in T by A2,A4;
then {p} c= T by ZFMISC_1:31;
then {p} \/ {q} c= T by A5,XBOOLE_1:8;
hence thesis by A1,A2,CQC_THE1:def 2;
end;
thus (for T st T is being_a_theory & {p '&' q} c= T holds t in T) implies
t in Cn({p} \/ {q})
proof
assume
A6: for T st T is being_a_theory & {p '&' q} c= T holds t in T;
for T st T is being_a_theory & {p} \/ {q} c= T holds t in T
proof
let T;
assume that
A7: T is being_a_theory and
A8: {p} \/ {q} c= T;
{p} c= {p} \/ {q} by XBOOLE_1:7;
then {p} c= T by A8,XBOOLE_1:1;
then
A9: p in T by ZFMISC_1:31;
{q} c= {p} \/ {q} by XBOOLE_1:7;
then {q} c= T by A8,XBOOLE_1:1;
then
A10: q in T by ZFMISC_1:31;
p => (q => p '&' q) in TAUT(A) & TAUT(A) c= T
by A7,CQC_THE1:38,PROCAL_1:28;
then (q => p '&' q) in T by A7,A9;
then p '&' q in T by A7,A10;
then {p '&' q} c= T by ZFMISC_1:31;
hence thesis by A6,A7;
end;
hence thesis by CQC_THE1:def 2;
end;
end;
hence thesis by CQC_THE1:def 2;
end;
theorem
{p,q} |- r iff {p '&' q} |- r
proof
thus {p,q} |- r implies {p '&' q} |- r
proof
assume r in Cn({p,q});
then r in Cn({p} \/ {q}) by ENUMSET1:1;
hence r in Cn({p '&' q}) by Th88;
end;
assume r in Cn({p '&' q});
then r in Cn({p} \/ {q}) by Th88;
hence r in Cn({p,q}) by ENUMSET1:1;
end;
theorem Th90:
X|- p implies X|- All(x,p)
proof
A1: X|- p => ((All(x,p) => All(x,p)) => p) by CQC_THE1:59;
not x in still_not-bound_in All(x,p) by Th5;
then
A2: not x in still_not-bound_in All(x,p) => All(x,p) by Th7;
assume X|- p;
then X|- (All(x,p) => All(x,p)) => p by A1,CQC_THE1:55;
then
A3: X|- (All(x,p) => All(x,p)) => All(x,p) by A2,CQC_THE1:57;
X|- All(x,p) => All(x,p) by CQC_THE1:59;
hence thesis by A3,CQC_THE1:55;
end;
theorem
not x in still_not-bound_in p implies X|- All(x,p => q) => (p => All(x
,q)) by Th74,CQC_THE1:59;
::$N Deduction Theorem
theorem
F is closed & (X \/ {F})|- G implies X |- F => G
proof
assume that
A1: F is closed and
A2: (X \/ {F}) |- G;
G in Cn(X \/ {F}) by A2;
then consider f such that
A3: f is_a_proof_wrt (X \/ {F}) and
A4: Effect f = G by CQC_THE1:36;
f <> {} by A3;
then
A5: G = (f.len f)`1 by A4,CQC_THE1:def 6;
defpred P[Nat] means 1 <= $1 & $1 <= len f implies for H st H = (f.$1)`1
holds X|- F => H;
A6: for n being Nat st for k being Nat st k < n holds P[k] holds P[n]
proof
let n be Nat such that
A7: for k being Nat st k < n holds 1 <= k & k <= len f implies for H
st H = (f.k)`1 holds X|- F => H;
assume that
A8: 1 <= n and
A9: n <= len f;
A10: f,n is_a_correct_step_wrt (X \/ {F}) by A3,A8,A9;
let H such that
A11: H = (f.n)`1;
now
(f.n)`2 = 0 or ... or (f.n)`2 = 9 by A8,A9,CQC_THE1:23;
then per cases;
suppose
(f.n)`2 = 0;
then H in X \/ {F} by A11,A10,CQC_THE1:def 4;
then
A12: H in X or H in {F} by XBOOLE_0:def 3;
now
per cases by A12,TARSKI:def 1;
suppose
A13: H in X;
X c= Cn(X) by CQC_THE1:17;
then
A14: X|- H by A13;
X|- H => (F => H) by CQC_THE1:59;
hence thesis by A14,CQC_THE1:55;
end;
suppose
H = F;
hence thesis by CQC_THE1:59;
end;
end;
hence thesis;
end;
suppose
(f.n)`2 = 1;
then H = VERUM(A) by A11,A10,CQC_THE1:def 4;
hence thesis by CQC_THE1:59,LUKASI_1:46;
end;
suppose
(f.n)`2 = 2;
then ex p st H = ('not' p => p) => p by A11,A10,CQC_THE1:def 4;
then H is valid by CQC_THE1:61;
hence thesis by CQC_THE1:59,LUKASI_1:61;
end;
suppose
(f.n)`2 = 3;
then ex p,q st H = p => ('not' p => q) by A11,A10,CQC_THE1:def 4;
then H is valid by CQC_THE1:62;
hence thesis by CQC_THE1:59,LUKASI_1:61;
end;
suppose
(f.n)`2 = 4;
then
ex p,q,r st H = (p => q) => ('not'(q '&' r) => 'not'(p '&' r)) by A11
,A10,CQC_THE1:def 4;
then H is valid by CQC_THE1:63;
hence thesis by CQC_THE1:59,LUKASI_1:61;
end;
suppose
(f.n)`2 = 5;
then ex p,q st H = p '&' q => q '&' p by A11,A10,CQC_THE1:def 4;
then H is valid by CQC_THE1:64;
hence thesis by CQC_THE1:59,LUKASI_1:61;
end;
suppose
(f.n)`2 = 6;
then ex p,x st H = All(x,p) => p by A11,A10,CQC_THE1:def 4;
then H is valid by CQC_THE1:66;
hence thesis by CQC_THE1:59,LUKASI_1:61;
end;
suppose
(f.n)`2 = 7;
then consider i,j being Nat, p,q such that
A15: 1 <= i and
A16: i < n and
A17: 1 <= j and
A18: j < i and
A19: p = (f.j)`1 and
A20: q = H and
A21: (f.i)`1 = p => q by A11,A10,CQC_THE1:def 4;
i <= len f by A9,A16,XXREAL_0:2;
then
A22: X|- F => (p => q) by A7,A15,A16,A21;
X|- (F => (p => q)) => ((F => p) => (F => q)) by CQC_THE1:59;
then
A23: X|- (F => p) => (F => q) by A22,CQC_THE1:55;
j < n by A16,A18,XXREAL_0:2;
then
A24: j <= len f by A9,XXREAL_0:2;
j < n by A16,A18,XXREAL_0:2;
then X|- F => p by A7,A17,A19,A24;
hence thesis by A20,A23,CQC_THE1:55;
end;
suppose
(f.n)`2 = 8;
then consider i being Nat,p,q,x such that
A25: 1 <= i and
A26: i < n and
A27: (f.i)`1 = p => q and
A28: not x in still_not-bound_in p and
A29: H = p => All(x,q) by A11,A10,CQC_THE1:def 4;
A30: X|- All(x,p => q) => (p => All(x,q)) by A28,Th74,CQC_THE1:59;
not x in still_not-bound_in F by A1,QC_LANG1:def 31;
then
A31: X|- All(x,F => (p => q)) => (F => All(x,p => q)) by Th74,CQC_THE1:59;
i <= len f by A9,A26,XXREAL_0:2;
then X|- All(x,F => (p => q)) by A7,A25,A26,A27,Th90;
then X|- F => All(x,p => q) by A31,CQC_THE1:55;
hence thesis by A29,A30,LUKASI_1:59;
end;
suppose
(f.n)`2 = 9;
then consider i being Nat,x,y,s such that
A32: 1 <= i and
A33: i < n and
A34: s.x in CQC-WFF(A) & s.y in CQC-WFF(A) and
A35: not x in still_not-bound_in s and
A36: s.x = (f.i)`1 and
A37: H = s.y by A11,A10,CQC_THE1:def 4;
reconsider s1 = s.x, s2 = s.y as Element of CQC-WFF(A) by A34;
A38: X|- All(x,s1) => s2 by A35,Th25,CQC_THE1:59;
not x in still_not-bound_in F by A1,QC_LANG1:def 31;
then
A39: X|- All(x,F => s1) => (F => All(x,s1)) by Th74,CQC_THE1:59;
i <= len f by A9,A33,XXREAL_0:2;
then X|- All(x,F => s1) by A7,A32,A33,A36,Th90;
then X |- F => All(x,s1) by A39,CQC_THE1:55;
hence thesis by A37,A38,LUKASI_1:59;
end;
end;
hence thesis;
end;
A40: for n be Nat holds P[n] from NAT_1:sch 4(A6);
1 <= len f by A3,CQC_THE1:25;
hence thesis by A40,A5;
end;