Copyright (c) 1990 Association of Mizar Users
environ
vocabulary CQC_LANG, QC_LANG1, FINSEQ_1, CQC_THE1, QMAX_1, ZF_LANG, BOOLE,
PRE_TOPC, FUNCT_1, MCART_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, NAT_1, FINSEQ_1,
FUNCT_1, MCART_1, DOMAIN_1, QC_LANG1, QC_LANG2, CQC_LANG, CQC_THE1;
constructors DOMAIN_1, CQC_THE1, XREAL_0, XCMPLX_0, MEMBERED, XBOOLE_0;
clusters RELSET_1, CQC_LANG, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, SUBSET, BOOLE;
definitions CQC_THE1;
theorems AXIOMS, TARSKI, ZFMISC_1, LUKASI_1, CQC_LANG, CQC_THE1, ENUMSET1,
QC_LANG1, QC_LANG2, QC_LANG3, PROCAL_1, XBOOLE_0, XBOOLE_1;
schemes NAT_1;
begin
reserve X,T for Subset of CQC-WFF;
reserve F,G,H,p,q,r,t for Element of CQC-WFF;
reserve s,h for QC-formula;
reserve x,y for bound_QC-variable;
reserve f for FinSequence of [:CQC-WFF,Proof_Step_Kinds:];
reserve i,j,k,n for Nat;
theorem
Th1: |- p => (q => r) implies |- (p '&' q) => r
proof
assume A1: p => (q => r) in TAUT;
(p => (q => r)) => ((p '&' q) => r) in TAUT by PROCAL_1:32;
hence (p '&' q) => r in TAUT by A1,CQC_THE1:82;
end;
theorem Th2: |- p => (q => r) implies |- (q '&' p) => r
proof
assume p => (q => r) in TAUT;
then |- p => (q => r) by CQC_THE1:def 11;
then |- (p '&' q) => r by Th1;
then (p '&' q) => r in TAUT & q '&' p => p '&' q in TAUT
by CQC_THE1:81,def 11;
hence (q '&' p) => r in TAUT by LUKASI_1:3;
end;
theorem Th3: |- (p '&' q) => r implies |- p => (q => r)
proof
assume A1: (p '&' q) => r in TAUT;
((p '&' q) => r) => (p => (q => r)) in TAUT by PROCAL_1:31;
hence (p => (q => r)) in TAUT by A1,CQC_THE1:82;
end;
theorem Th4: |- (p '&' q) => r implies |- q => (p => r)
proof
assume A1: (p '&' q) => r in TAUT;
q '&' p => p '&' q in TAUT by CQC_THE1:81;
then q '&' p => r in TAUT by A1,LUKASI_1:3;
then |- q '&' p => r by CQC_THE1:def 11;
then |- q => (p => r) by Th3;
hence q => (p => r) in TAUT by CQC_THE1:def 11;
end;
Lm1: |- (p '&' q) => p & |- (p '&' q) => q
proof
thus (p '&' q) => p in TAUT & (p '&' q) => q in TAUT
by PROCAL_1:19,21;
end;
Lm2: |- p '&' q implies |- p & |- q
proof
assume A1: |- p '&' q;
|- (p '&' q) => p & |- (p '&' q) => q by Lm1;
hence thesis by A1,CQC_THE1:104;
end;
Lm3: |- p => q & |- p => r implies |- p => q '&' r
proof
assume p => q in TAUT & p => r in TAUT;
hence p => q '&' r in TAUT by PROCAL_1:52;
end;
Lm4: |- p => q & |- r => t implies |- p 'or' r => q 'or' t
proof
assume p => q in TAUT & r => t in TAUT;
hence p 'or' r => q 'or' t in TAUT by PROCAL_1:57;
end;
Lm5: |- p => q & |- r => t implies |- p '&' r => q '&' t
proof
assume p => q in TAUT & r => t in TAUT;
hence p '&' r => q '&' t in TAUT by PROCAL_1:56;
end;
Lm6: |- p => p 'or' q & |- p => q 'or' p
proof
thus p => p 'or' q in TAUT & p => q 'or' p in TAUT
by PROCAL_1:3,4;
end;
Lm7: |- p => q & |- r => q implies |- (p 'or' r) => q
proof
assume p => q in TAUT & r => q in TAUT;
hence (p 'or' r) => q in TAUT by PROCAL_1:53;
end;
Lm8: |- p & |- q implies |- p '&' q
proof
assume p in TAUT & q in TAUT;
hence p '&' q in TAUT by PROCAL_1:47;
end;
Lm9: |- p => q implies |- r '&' p => r '&' q
proof
assume p => q in TAUT;
hence r '&' p => r '&' q in TAUT by PROCAL_1:50;
end;
Lm10: |- p => q implies |- p 'or' r => q 'or' r
proof
assume p => q in TAUT;
hence p 'or' r => q 'or' r in TAUT by PROCAL_1:48;
end;
Lm11: |- p 'or' q => ('not' p => q)
proof
thus ( p 'or' q ) => ( 'not' p => q ) in TAUT by PROCAL_1:5;
end;
Lm12: |- ('not' p => q) => (p 'or' q)
proof
A1: ('not' p => q) => ('not' 'not' p 'or' q) in TAUT by PROCAL_1:14;
'not' 'not' p => p in TAUT by LUKASI_1:25;
then 'not' 'not' p 'or' q => p 'or' q in TAUT by PROCAL_1:48;
hence ('not' p => q) => (p 'or' q) in TAUT by A1,LUKASI_1:3;
end;
Lm13: |- p <=> p
proof
|- p => p by LUKASI_1:44;
then |- (p => p) '&' (p => p) by Lm8;
hence thesis by QC_LANG2:def 4;
end;
Lm14: |- p => q & |- q => p iff |- p <=> q
proof
thus |- p => q & |- q => p implies |- p <=> q
proof
assume |- p => q & |- q => p;
then |- (p => q) '&' (q => p) by Lm8;
hence thesis by QC_LANG2:def 4;
end;
assume |- p <=> q;
then |- (p => q) '&' (q => p) by QC_LANG2:def 4;
hence thesis by Lm2;
end;
Lm15: |- p <=> q implies (|- p iff |- q)
proof
assume A1: p <=> q in TAUT;
(p <=> q) => (p => q) in TAUT & (p <=> q) => (q => p) in TAUT
by PROCAL_1:23,24;
then A2: p => q in TAUT & q => p in TAUT by A1,CQC_THE1:82;
thus |- p implies |- q
proof
assume p in TAUT;
hence q in TAUT by A2,CQC_THE1:82;
end;
assume q in TAUT;
hence p in TAUT by A2,CQC_THE1:82;
end;
Lm16:
|- p => (q => r) & |- r => t implies |- p => (q => t)
proof
assume |- p => (q => r) & |- r => t;
then |- (p '&' q) => r & |- r => t by Th1;
then |- (p '&' q) => t by LUKASI_1:43;
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:16;
hence thesis by ZFMISC_1:64;
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:23;
hence thesis by ZFMISC_1:64;
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:20;
hence thesis by XBOOLE_0:def 2;
end;
canceled;
theorem Th9: 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:14;
hence thesis by XBOOLE_0:def 2;
end;
theorem Th10: 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:18;
hence thesis by XBOOLE_0:def 2;
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 not x in still_not-bound_in All(x,All(y,s)) &
not y in still_not-bound_in All(x,All(y,s)) by Th5;
hence thesis by QC_LANG2:20;
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 not x in still_not-bound_in Ex(x,Ex(y,s)) &
not y in still_not-bound_in Ex(x,Ex(y,s)) by Th6;
hence thesis by QC_LANG2:20;
end;
canceled;
theorem Th14: (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:32
.= 'not'((s.x) '&' ('not' h.x)) by CQC_LANG:34
.= 'not'((s.x) '&' 'not'(h.x)) by CQC_LANG:32
.= (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:32
.= 'not'((('not' s).x) '&' (('not' h).x)) by CQC_LANG:34
.= 'not'('not'(s.x) '&' (('not' h).x)) by CQC_LANG:32
.= 'not'('not'(s.x) '&' 'not'(h.x)) by CQC_LANG:32
.= (s.x) 'or' (h.x) by QC_LANG2:def 3;
end;
canceled;
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:32
.= 'not'(All(x,('not' p).y)) by A1,CQC_LANG:38
.= 'not' All(x,'not'(p.y)) by CQC_LANG:32
.= Ex(x,p.y) by QC_LANG2:def 5;
end;
::---------------------------------------------------------
theorem Th18: |- p => Ex(x,p)
proof
|- All(x,'not' p) => 'not' p by CQC_THE1:105;
then |- 'not' 'not' p => 'not' All(x,'not' p) by LUKASI_1:63;
then |- 'not' 'not' p => Ex(x,p) & |- ('not' 'not'
p => Ex(x,p)) => (p => Ex(x,p))
by LUKASI_1:67,QC_LANG2:def 5;
hence thesis by CQC_THE1:104;
end;
theorem Th19: |- p implies |- Ex(x,p)
proof
assume A1: |- p;
|- p => Ex(x,p) by Th18;
hence thesis by A1,CQC_THE1:104;
end;
theorem |- All(x,p) => Ex(x,p)
proof
|- All(x,p) => p & |- p => Ex(x,p) by Th18,CQC_THE1:105;
hence thesis by LUKASI_1:43;
end;
theorem |- All(x,p) => Ex(y,p)
proof
|- All(x,p) => p & |- p => Ex(y,p) by Th18,CQC_THE1:105;
hence thesis by LUKASI_1:43;
end;
theorem Th22: |- p => q & not x in still_not-bound_in q implies
|- Ex(x,p) => q
proof
assume that A1: |- p => q and A2: not x in still_not-bound_in q;
|-
'not' q => 'not' p & not x in still_not-bound_in 'not'
q by A1,A2,LUKASI_1:63,QC_LANG3:11;
then |- 'not' q => All(x,'not' p) by CQC_THE1:106;
then |- 'not' All(x,'not' p) => 'not' 'not' q by LUKASI_1:63;
then |- Ex(x,p) => 'not' 'not' q by QC_LANG2:def 5;
hence thesis by LUKASI_1:70;
end;
theorem Th23: not x in still_not-bound_in p implies |- Ex(x,p) => p
proof
assume A1: not x in still_not-bound_in p;
|- p => p by LUKASI_1:44;
hence thesis by A1,Th22;
end;
theorem not x in still_not-bound_in p & |- Ex(x,p) implies |- p
proof
assume A1: not x in still_not-bound_in p & |- Ex(x,p);
then |- Ex(x,p) => p by Th23;
hence thesis by A1,CQC_THE1:104;
end;
theorem Th25: p=h.x & q=h.y & not y in still_not-bound_in h
implies |- p => Ex(y,q)
proof assume A1: p=h.x & q=h.y & not y in still_not-bound_in h;
A2: |- q => Ex(y,q) by Th18;
A3: (h => Ex(y,q)).y = (h.y) => (Ex(y,q).y) by Th14
.= q => Ex(y,q) by A1,CQC_LANG:40;
A4: (h => Ex(y,q)).x = (h.x) => (Ex(y,q).x) by Th14
.= p => Ex(y,q) by A1,CQC_LANG:40;
not y in still_not-bound_in Ex(y,q) & not y in
still_not-bound_in h by A1,Th6;
then not y in still_not-bound_in h => Ex(y,q) by Th7;
hence thesis by A2,A3,A4,CQC_THE1:107;
end;
theorem Th26: |- p implies |- All(x,p)
proof
assume A1: |- p;
|- p => ((All(x,p) => All(x,p)) => p) by LUKASI_1:45;
then A2: |- (All(x,p) => All(x,p)) => p by A1,CQC_THE1:104;
not x in still_not-bound_in All(x,p) by Th5;
then not x in still_not-bound_in All(x,p) => All(x,p) by Th7;
then |- (All(x,p) => All(x,p)) => All(x,p) &
|- All(x,p) => All(x,p) by A2,CQC_THE1:106,LUKASI_1:44;
hence thesis by CQC_THE1:104;
end;
theorem Th27: not x in still_not-bound_in p implies |- p => All(x,p)
proof
assume A1: not x in still_not-bound_in p;
|- p => p by LUKASI_1:44;
hence thesis by A1,CQC_THE1:106;
end;
theorem Th28: p=h.x & q=h.y & not x in still_not-bound_in h
implies |- All(x,p) => q
proof
assume A1: p=h.x & q=h.y & not x in still_not-bound_in h;
A2: |- All(x,p) => p by CQC_THE1:105;
A3: (All(x,p) => h).x = (All(x,p).x) => p by A1,Th14
.= All(x,p) => p by CQC_LANG:40;
A4: (All(x,p) => h).y = (All(x,p).y) => q by A1,Th14
.= All(x,p) => q by CQC_LANG:40;
not x in still_not-bound_in All(x,p) by Th5;
then not x in still_not-bound_in All(x,p) => h by A1,Th7;
hence thesis by A2,A3,A4,CQC_THE1:107;
end;
theorem
not y in still_not-bound_in p implies |- All(x,p) => All(y,p)
proof
assume not y in still_not-bound_in p;
then |- All(x,p) => p & not y in still_not-bound_in All(x,p)
by Th5,CQC_THE1:105;
hence thesis by CQC_THE1:106;
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)
proof assume
A1: p=h.x & q=h.y & not x in still_not-bound_in h &
not y in still_not-bound_in p;
then A2: not y in still_not-bound_in All(x,p) by Th5;
|- All(x,p) => q by A1,Th28;
hence thesis by A2,CQC_THE1:106;
end;
theorem
not x in still_not-bound_in p implies |- Ex(x,p) => Ex(y,p)
proof
assume not x in still_not-bound_in p;
then |- p => Ex(y,p) & not x in still_not-bound_in Ex(y,p) by Th6,Th18;
hence thesis by Th22;
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)
proof assume that
A1: p=h.x & q=h.y and
A2: not x in still_not-bound_in q and
A3: not y in still_not-bound_in h;
A4: not x in still_not-bound_in Ex(y,q) by A2,Th6;
|- p => Ex(y,q) by A1,A3,Th25;
hence thesis by A4,Th22;
end;
canceled;
theorem
Th34: |- All(x,p => q) => (All(x,p) => All(x,q))
proof
not x in still_not-bound_in All(x,p => q) &
not x in still_not-bound_in All(x,p) by Th5;
then A1: not x in still_not-bound_in All(x,p => q) '&' All(x,p) by Th9;
|- All(x,p => q) => (p => q) by CQC_THE1:105;
then |- p => (All(x,p => q) => q) & |- All(x,p) => p
by CQC_THE1:105,LUKASI_1:48;
then |- All(x,p) => (All(x,p => q) => q) by LUKASI_1:43;
then |- (All(x,p => q) '&' All(x,p)) => q by Th2;
then |- (All(x,p => q) '&' All(x,p)) => All(x,q) by A1,CQC_THE1:106;
hence |- All(x,p => q) => (All(x,p) => All(x,q)) by Th3;
end;
theorem
Th35: |- All(x,p => q) implies |- All(x,p) => All(x,q)
proof
assume A1:|- All(x,p => q);
|- All(x,p => q) => (All(x,p) => All(x,q)) by Th34;
hence thesis by A1,CQC_THE1:104;
end;
theorem Th36:
|- All(x,p <=> q) => (All(x,p) <=> All(x,q))
proof
|- (p <=> q) => (p <=> q) by LUKASI_1:44;
then |- (p <=> q) => ((p => q) '&' (q => p)) by QC_LANG2:def 4;
then |- All(x,(p <=> q) => ((p => q) '&' (q => p))) by Th26;
then A1: |- All(x,p <=> q) => All(x,(p => q) '&' (q => p)) by Th35;
|- All(x,(p => q) '&' (q => p)) => ((p => q) '&' (q => p))
& |- ((p => q) '&' (q => p)) => (p => q)
& |- ((p => q) '&' (q => p)) => (q => p) by Lm1,CQC_THE1:105;
then A2: |- All(x,(p => q) '&' (q => p)) => (p => q) &
|- All(x,(p => q) '&' (q => p)) => (q => p) by LUKASI_1:43;
not x in still_not-bound_in All(x,(p => q) '&' (q => p)) by Th5;
then |- All(x,(p => q) '&' (q => p)) => All(x,p => q) &
|- All(x,(p => q) '&' (q => p)) => All(x,q => p) by A2,CQC_THE1:106;
then A3: |-
All(x,(p => q) '&' (q => p)) => (All(x,p => q) '&' All(x,q => p))
by Lm3;
|- All(x,p => q) => (All(x,p) => All(x,q)) &
|- All(x,q => p) => (All(x,q) => All(x,p)) by Th34;
then |- (All(x,p => q) '&' All(x,q => p)) => ((All(x,p) => All(x,q)) '&'
(All(x,q) => All(x,p))) by Lm5;
then |- (All(x,p => q) '&' All(x,q => p)) => (All(x,p) <=> All(x,q))
by QC_LANG2:def 4;
then |- All(x,(p => q) '&' (q => p)) => (All(x,p) <=> All(x,q))
by A3,LUKASI_1:43;
hence thesis by A1,LUKASI_1:43;
end;
theorem
|- All(x,p <=> q) implies |- All(x,p) <=> All(x,q)
proof
assume A1: |- All(x,p <=> q);
|- All(x,p <=> q) => (All(x,p) <=> All(x,q)) by Th36;
hence thesis by A1,CQC_THE1:104;
end;
theorem
Th38: |- All(x,p => q) => (Ex(x,p) => Ex(x,q))
proof
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 A1: not x in still_not-bound_in All(x,p => q) => Ex(x,q) by Th7;
|- All(x,p => q) => (p => q) by CQC_THE1:105;
then |- (p '&' All(x,p => q)) => q & |- q => Ex(x,q) by Th2,Th18;
then |- (p '&' All(x,p => q)) => Ex(x,q) by LUKASI_1:43;
then |- p => (All(x,p => q) => Ex(x,q)) by Th3;
then |- Ex(x,p) => (All(x,p => q) => Ex(x,q)) by A1,Th22;
hence thesis by LUKASI_1:48;
end;
theorem Th39: |- All(x,p => q) implies |- Ex(x,p) => Ex(x,q)
proof
assume A1: |- All(x,p => q);
|- All(x,p => q) => (Ex(x,p) => Ex(x,q)) by Th38;
hence thesis by A1,CQC_THE1:104;
end;
theorem
Th40: |- All(x,p '&' q) => (All(x,p) '&' All(x,q)) &
|- (All(x,p) '&' All(x,q)) => All(x,p '&' q)
proof
|- p '&' q => p & |- p '&'q => q by Lm1;
then A1: |- All(x,p '&' q => p) & |- All(x,p '&'q => q) by Th26;
|- All(x,p '&' q => p) => (All(x,p '&' q) => All(x,p)) &
|- All(x,p '&' q => q) => (All(x,p '&' q) => All(x,q)) by Th34;
then |- All(x,p '&' q) => All(x,p) & |- All(x,p '&' q) => All(x,q)
by A1,CQC_THE1:104;
hence |- All(x,p '&' q) => (All(x,p) '&' All(x,q)) by Lm3;
|- All(x,p) => p & |- All(x,q) => q by CQC_THE1:105;
then A2: |- (All(x,p) '&' All(x,q)) => (p '&' q) by Lm5;
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 Th9;
hence thesis by A2,CQC_THE1:106;
end;
theorem
Th41: |- All(x,p '&' q) <=> (All(x,p) '&' All(x,q))
proof
|- All(x,p '&' q) => (All(x,p) '&' All(x,q)) &
|- (All(x,p) '&' All(x,q)) => All(x,p '&' q) by Th40;
hence thesis by Lm14;
end;
theorem |- All(x,p '&' q) iff |- All(x,p) '&' All(x,q)
proof
|- All(x,p '&' q) <=> (All(x,p) '&' All(x,q)) by Th41;
hence thesis by Lm15;
end;
theorem
Th43: |- (All(x,p) 'or' All(x,q)) => All(x,p 'or' q)
proof
|- p => p 'or' q & |- q => p 'or' q by Lm6;
then A1: |- All(x,p => p 'or' q) & |- All(x,q => p 'or' q) by Th26;
|- All(x,p => p 'or' q) => (All(x,p) => All(x,p 'or' q)) &
|- All(x,q => p 'or' q) => (All(x,q) => All(x,p 'or' q)) by Th34;
then |- All(x,p) => All(x,p 'or' q) & |- All(x,q) => All(x,p 'or' q)
by A1,CQC_THE1:104;
hence thesis by Lm7;
end;
theorem
Th44: |- Ex(x,p 'or' q) => (Ex(x,p) 'or' Ex(x,q)) &
|- (Ex(x,p) 'or' Ex(x,q)) => Ex(x,p 'or' q)
proof
|- p => Ex(x,p) & |- q => Ex(x,q) by Th18;
then A1: |- (p 'or' q) => (Ex(x,p) 'or' Ex(x,q)) by Lm4;
not x in still_not-bound_in Ex(x,p) &
not x in still_not-bound_in Ex(x,q) by Th6;
then not x in still_not-bound_in Ex(x,p) 'or' Ex(x,q) by Th10;
hence |- Ex(x,(p 'or' q)) => (Ex(x,p) 'or' Ex(x,q)) by A1,Th22;
|- p => p 'or' q & |- q => p 'or' q by Lm6;
then A2: |- All(x,p => p 'or' q) & |- All(x,q => p 'or' q) by Th26;
|- All(x,p => p 'or' q) => (Ex(x,p) => Ex(x,p 'or' q)) &
|- All(x,q => p 'or' q) => (Ex(x,q) => Ex(x,p 'or' q)) by Th38;
then |- Ex(x,p) => Ex(x,p 'or' q) & |- Ex(x,q) => Ex(x,p 'or' q)
by A2,CQC_THE1:104;
hence thesis by Lm7;
end;
theorem
Th45: |- Ex(x,p 'or' q) <=> (Ex(x,p) 'or' Ex(x,q))
proof
|- Ex(x,p 'or' q) => (Ex(x,p) 'or' Ex(x,q)) &
|- (Ex(x,p) 'or' Ex(x,q)) => Ex(x,p 'or' q) by Th44;
hence thesis by Lm14;
end;
theorem
|- Ex(x,p 'or' q) iff |- Ex(x,p) 'or' Ex(x,q)
proof
|- Ex(x,p 'or' q) <=> (Ex(x,p) 'or' Ex(x,q)) by Th45;
hence thesis by Lm15;
end;
theorem Th47:
|- Ex(x,p '&' q) => (Ex(x,p) '&' Ex(x,q))
proof
|- p '&' q => p & |- p '&' q => q by Lm1;
then |- All(x,p '&' q => p) & |- All(x,p '&' q => q) by Th26;
then |- Ex(x,p '&' q) => Ex(x,p) & |- Ex(x,p '&' q) => Ex(x,q) by Th39;
hence |- Ex(x,p '&' q) => (Ex(x,p) '&' Ex(x,q)) by Lm3;
end;
theorem
|- Ex(x,p '&' q) implies |- Ex(x,p) '&' Ex(x,q)
proof
assume A1: |- Ex(x,p '&' q);
|- Ex(x,p '&' q) => (Ex(x,p) '&' Ex(x,q)) by Th47;
hence thesis by A1,CQC_THE1:104;
end;
theorem Th49: |- All(x,'not' 'not' p) => All(x,p) & |- All(x,p) => All(x,'not'
'not' p)
proof
|- 'not' 'not' p => p & |- p => 'not' 'not' p by LUKASI_1:64,65;
then |- All(x,'not' 'not' p => p) & |- All(x,p => 'not' 'not' p) by Th26;
hence thesis by Th35;
end;
theorem |- All(x,'not' 'not' p) <=> All(x,p)
proof
|- All(x,'not' 'not' p) => All(x,p) & |- All(x,p) => All(x,'not' 'not'
p) by Th49;
hence thesis by Lm14;
end;
theorem Th51: |- Ex(x,'not' 'not' p) => Ex(x,p) &
|- Ex(x,p) => Ex(x,'not' 'not' p)
proof
|- 'not' 'not' p => p & |- p => 'not' 'not' p by LUKASI_1:64,65;
then |- All(x,'not' 'not' p => p) & |- All(x,p => 'not' 'not' p) by Th26;
hence thesis by Th39;
end;
theorem |- Ex(x,'not' 'not' p) <=> Ex(x,p)
proof
|- Ex(x,'not' 'not' p) => Ex(x,p) & |- Ex(x,p) => Ex(x,'not' 'not' p)
by Th51;
hence thesis by Lm14;
end;
theorem Th53:
|- 'not' Ex(x,'not' p) => All(x,p) & |- All(x,p) => 'not' Ex(x,'not' p)
proof
A1: '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) & |- All(x,'not' 'not'
p) => All(x,p)
by Th49,LUKASI_1:65;
hence |- 'not' Ex(x,'not' p) => All(x,p) by LUKASI_1:43;
|- All(x,p) => All(x,'not' 'not' p) & |-
All(x,'not' 'not' p) => 'not' 'not' All(x,'not' 'not' p) by Th49,LUKASI_1:64;
hence |- All(x,p) => 'not' Ex(x,'not' p) by A1,LUKASI_1:43;
end;
theorem |- 'not' Ex(x,'not' p) <=> All(x,p)
proof
|- 'not' Ex(x,'not' p) => All(x,p) &
|- All(x,p) => 'not' Ex(x,'not' p) by Th53;
hence thesis by Lm14;
end;
theorem Th55: |- 'not' All(x,p) => Ex(x,'not' p) & |- Ex(x,'not' p) => 'not'
All(x,p)
proof
A1: Ex(x,'not' p) = 'not' All(x,'not' 'not' p) by QC_LANG2:def 5;
then |- 'not' All(x,'not' 'not' p) => Ex(x,'not' p) & |- All(x,'not' 'not'
p) => All(x,p)
by Th49,LUKASI_1:44;
then |- 'not' All(x,'not' 'not' p) => Ex(x,'not' p) &
|- 'not' All(x,p) => 'not'
All(x,'not' 'not' p) by LUKASI_1:63;
hence |- 'not' All(x,p) => Ex(x,'not' p) by LUKASI_1:43;
|- Ex(x,'not' p) => 'not' All(x,'not' 'not' p) & |-
All(x,p) => All(x,'not' 'not' p) by A1,Th49,LUKASI_1:44;
then |- Ex(x,'not' p) => 'not' All(x,'not' 'not' p) &
|- 'not' All(x,'not' 'not'
p) => 'not' All(x,p) by LUKASI_1:63;
hence |- Ex(x,'not' p) => 'not' All(x,p) by LUKASI_1:43;
end;
theorem |- 'not' All(x,p) <=> Ex(x,'not' p)
proof
|- 'not' All(x,p) => Ex(x,'not' p) &
|- Ex(x,'not' p) => 'not' All(x,p) by Th55;
hence thesis by Lm14;
end;
theorem |- 'not' Ex(x,p) => All(x,'not' p) & |- All(x,'not' p) => 'not' Ex(x,
p
)
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) by LUKASI_1:65;
thus thesis by A1,LUKASI_1:64;
end;
theorem Th58: |- All(x,'not' p) <=> 'not' Ex(x,p)
proof
|- All(x,'not' p) => 'not' 'not' All(x,'not' p) by LUKASI_1:64;
then A1:|- All(x,'not' p) => 'not' Ex(x,p) by QC_LANG2:def 5;
|- 'not' 'not' All(x,'not' p) => All(x,'not' p) by LUKASI_1:65;
then |- 'not' Ex(x,p) => All(x,'not' p) by QC_LANG2:def 5;
hence thesis by A1,Lm14;
end;
theorem
|- All(x,All(y,p)) => All(y,All(x,p)) & |- All(x,y,p) => All(y,x,p)
proof
|- All(y,p) => p by CQC_THE1:105;
then A1: |- All(x,All(y,p) => p) by Th26;
|- All(x,All(y,p) => p) => (All(x,All(y,p)) => All(x,p)) by Th34;
then A2: |- All(x,All(y,p)) => All(x,p) by A1,CQC_THE1:104;
not y in still_not-bound_in All(y,p) by Th5;
then not y in still_not-bound_in All(x,All(y,p)) by Th5;
hence |- All(x,All(y,p)) => All(y,All(x,p)) by A2,CQC_THE1:106;
then |- All(x,y,p) => All(y,All(x,p)) by QC_LANG2:20;
hence thesis by QC_LANG2:20;
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)
proof assume p=h.x & q=h.y & not y in still_not-bound_in h;
then |- All(y,q) => p by Th28;
then |- All(x,All(y,q) => p) by Th26;
hence thesis by Th35;
end;
theorem
|- Ex(x,Ex(y,p)) => Ex(y,Ex(x,p)) & |- Ex(x,y,p) => Ex(y,x,p)
proof
|- p => Ex(x,p) by Th18;
then A1: |- All(y,p => Ex(x,p)) by Th26;
|- All(y,p => Ex(x,p)) => (Ex(y,p) => Ex(y,Ex(x,p))) by Th38;
then A2: |- Ex(y,p) => Ex(y,Ex(x,p)) by A1,CQC_THE1:104;
not x in still_not-bound_in Ex(x,p) by Th6;
then not x in still_not-bound_in Ex(y,Ex(x,p)) by Th6;
hence |- Ex(x,Ex(y,p)) => Ex(y,Ex(x,p)) by A2,Th22;
then |- Ex(x,y,p) => Ex(y,Ex(x,p)) by QC_LANG2:20;
hence thesis by QC_LANG2:20;
end;
theorem
p=h.x & q=h.y & not y in still_not-bound_in h implies
|- Ex(x,p) => Ex(x,y,q)
proof
assume p=h.x & q=h.y & not y in still_not-bound_in h;
then |- p => Ex(y,q) by Th25;
then |- All(x,p => Ex(y,q)) by Th26;
then |- Ex(x,p) => Ex(x,Ex(y,q)) by Th39;
hence thesis by QC_LANG2:20;
end;
theorem
|- Ex(x,All(y,p)) => All(y,Ex(x,p))
proof
|- p => Ex(x,p) by Th18;
then A1: |- All(y,p => Ex(x,p)) by Th26;
|- All(y,p => Ex(x,p)) => (All(y,p) => All(y,Ex(x,p))) by Th34;
then A2: |- All(y,p) => All(y,Ex(x,p)) by A1,CQC_THE1:104;
not x in still_not-bound_in Ex(x,p) by Th6;
then not x in still_not-bound_in All(y,Ex(x,p)) by Th5;
hence thesis by A2,Th22;
end;
theorem |- Ex(x,p <=> p)
proof
|- p <=> p by Lm13;
hence thesis by Th19;
end;
theorem Th65:
|- Ex(x,p => q) => (All(x,p) => Ex(x,q)) &
|- (All(x,p) => Ex(x,q)) => Ex(x,p => q)
proof
|- All(x,p) => p by CQC_THE1:105;
then |- (p => q) => (All(x,p) => q) & |- q => Ex(x,q) by Th18,LUKASI_1:42;
then A1: |- (p => q) => (All(x,p) => Ex(x,q)) by Lm16;
not x in still_not-bound_in All(x,p) & not x in still_not-bound_in Ex(x,q)
by Th5,Th6;
then not x in still_not-bound_in All(x,p) => Ex(x,q) by Th7;
hence |- Ex(x,p => q) => (All(x,p) => Ex(x,q)) by A1,Th22;
|- All(x,p '&' 'not' q) => (All(x,p) '&' All(x,'not' q)) by Th40;
then |- 'not'(All(x,p) '&' All(x,'not' q)) => 'not' All(x,p '&' 'not' q) &
|- 'not' All(x,p '&' 'not' q) => Ex(x,'not'(p '&' 'not'
q)) by Th55,LUKASI_1:63;
then |- 'not'(All(x,p) '&' All(x,'not' q)) => Ex(x,'not'(p '&' 'not'
q)) by LUKASI_1:43;
then A2: |- 'not'(All(x,p) '&' All(x,'not'
q)) => Ex(x,p => q) by QC_LANG2:def 2;
A3: 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;
|- All(x,'not' q) => 'not' 'not' All(x,'not' q) by LUKASI_1:64;
then |- (All(x,p) '&' All(x,'not' q)) => (All(x,p) '&'
'not' 'not' All(x,'not' q)) by Lm9;
then |-
(All(x,p) => Ex(x,q)) => 'not'(All(x,p) '&' All(x,'not' q)) by A3,LUKASI_1:63;
hence |- (All(x,p) => Ex(x,q)) => Ex(x,p => q) by A2,LUKASI_1:43;
end;
theorem Th66:
|- Ex(x,p => q) <=> (All(x,p) => Ex(x,q))
proof
|- Ex(x,p => q) => (All(x,p) => Ex(x,q)) &
|- (All(x,p) => Ex(x,q)) => Ex(x,p => q) by Th65;
hence thesis by Lm14;
end;
theorem
|- Ex(x,p => q) iff |- All(x,p) => Ex(x,q)
proof
|- Ex(x,p => q) <=> (All(x,p) => Ex(x,q)) by Th66;
hence thesis by Lm15;
end;
theorem Th68:
|- All(x,p '&' q) => (p '&' All(x,q))
proof
|- All(x,p '&' q) => (p '&' q) & |- (p '&' q) => p & |- (p '&' q) => q
by Lm1,CQC_THE1:105;
then A1: |- All(x,p '&' q) => p & |- All(x,p '&' q) => q by LUKASI_1:43;
not x in still_not-bound_in All(x,p '&' q) by Th5;
then |- All(x,p '&' q) => p & |- All(x,p '&' q) => All(x,q)
by A1,CQC_THE1:106;
hence thesis by Lm3;
end;
theorem Th69:
|- All(x,p '&' q) => (All(x,p) '&' q)
proof
|- (p '&' q) => (q '&' p) by CQC_THE1:103;
then A1: |- All(x,(p '&' q) => (q '&' p)) by Th26;
|- All(x,(p '&' q) => (q '&' p)) => (All(x,p '&' q) => All(x,q '&' p))
by Th34;
then A2: |- All(x,p '&' q) => All(x,q '&' p) by A1,CQC_THE1:104;
|- All(x,q '&' p) => (q '&' All(x,p)) by Th68;
then A3: |- All(x,p '&' q) => (q '&' All(x,p)) by A2,LUKASI_1:43;
|- (q '&' All(x,p)) => (All(x,p) '&' q) by CQC_THE1:103;
hence thesis by A3,LUKASI_1:43;
end;
theorem Th70:
not x in still_not-bound_in p implies |- (p '&' All(x,q)) => All(x,p '&' q)
proof
assume A1: not x in still_not-bound_in p;
|- All(x,q) => q by CQC_THE1:105;
then A2: |- p '&' All(x,q) => p '&' q 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,Th9;
hence |- p '&' All(x,q) => All(x,p '&' q) by A2,CQC_THE1:106;
end;
theorem
not x in still_not-bound_in p & |- p '&' All(x,q) implies |- All(x,p '&' q)
proof
assume A1: not x in still_not-bound_in p & |- p '&' All(x,q);
then |- (p '&' All(x,q)) => All(x,p '&' q) by Th70;
hence thesis by A1,CQC_THE1:104;
end;
theorem Th72:
not x in
still_not-bound_in p implies |- (p 'or' All(x,q)) => All(x,p 'or' q) &
|- All(x,p 'or' q) => (p 'or' All(x,q))
proof
assume A1: not x in still_not-bound_in p;
|- p => p by LUKASI_1:44;
then |- p => All(x,p) by A1,CQC_THE1:106;
then |- (All(x,p) 'or' All(x,q)) => All(x,p 'or' q) &
|- (p 'or' All(x,q)) => (All(x,p) 'or' All(x,q)) by Lm10,Th43;
hence |- (p 'or' All(x,q)) => All(x,p 'or' q) by LUKASI_1:43;
|- All(x,p 'or' q) => (p 'or' q) & |- (p 'or' q) => ('not' p => q)
by Lm11,CQC_THE1:105;
then |- All(x,p 'or' q) => ('not' p => q) by LUKASI_1:43;
then A2: |- (All(x,p 'or' q) '&' 'not' p) => q by Th1;
not x in still_not-bound_in 'not'
p & not x in still_not-bound_in All(x,p 'or' q)
by A1,Th5,QC_LANG3:11;
then not x in still_not-bound_in All(x,p 'or' q) '&' 'not' p by Th9;
then |- (All(x,p 'or' q) '&' 'not' p) => All(x,q) by A2,CQC_THE1:106;
then |- All(x, p 'or' q) => ('not' p => All(x,q)) &
|- ('not' p => All(x,q)) => (p 'or' All(x,q)) by Lm12,Th3;
hence |- All(x,p 'or' q) => (p 'or' All(x,q)) by LUKASI_1:43;
end;
theorem Th73:
not x in still_not-bound_in p implies |- (p 'or' All(x,q)) <=> All(x,p 'or' q)
proof
assume not x in still_not-bound_in p;
then |- (p 'or' All(x,q)) => All(x,p 'or' q) &
|- All(x,p 'or' q) => (p 'or' All(x,q)) by Th72;
hence thesis by Lm14;
end;
theorem
not x in still_not-bound_in p implies
(|- p 'or' All(x,q) iff |- All(x,p 'or' q))
proof
assume not x in still_not-bound_in p;
then |- (p 'or' All(x,q)) <=> All(x,p 'or' q) by Th73;
hence thesis by Lm15;
end;
theorem Th75:
not x in still_not-bound_in p implies |- (p '&' Ex(x,q)) => Ex(x,p '&' q) &
|- Ex(x,p '&' q) => (p '&' Ex(x,q))
proof
assume A1: not x in still_not-bound_in p;
|- p '&' q => Ex(x,p '&' q) by Th18;
then A2: |- q => (p => Ex(x,p '&' q)) 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)) by A2,Th22;
hence |- (p '&' Ex(x,q)) => Ex(x,p '&' q) by Th2;
|- q => Ex(x,q) by Th18;
then A3: |- p '&' q => p '&' Ex(x,q) 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,Th9;
hence thesis by A3,Th22;
end;
theorem Th76:
not x in still_not-bound_in p implies |- (p '&' Ex(x,q)) <=> Ex(x,p '&' q)
proof
assume not x in still_not-bound_in p;
then |- (p '&' Ex(x,q)) => Ex(x,p '&' q) &
|- Ex(x,p '&' q) => (p '&' Ex(x,q)) by Th75;
hence thesis by Lm14;
end;
theorem
not x in still_not-bound_in p implies (|- p '&' Ex(x,q) iff |- Ex(x,p '&' q)
)
proof
assume not x in still_not-bound_in p;
then |- (p '&' Ex(x,q)) <=> Ex(x,p '&' q) by Th76;
hence thesis by Lm15;
end;
Lm17: not x in still_not-bound_in p implies |- All(x,p => q) => (p => All(x,q))
proof
|- All(x,p => q) => (All(x,p) => All(x,q)) by Th34;
then A1: |- All(x,p) => (All(x,p => q) => All(x,q)) by LUKASI_1:48;
assume not x in still_not-bound_in p;
then |- p => All(x,p) by Th27;
then |- p => (All(x,p => q) => All(x,q)) by A1,LUKASI_1:43;
hence thesis by LUKASI_1:48;
end;
theorem
Th78: not x in
still_not-bound_in p implies |- All(x,p => q) => (p => All(x,q))
& |- (p => All(x,q)) => All(x,p => q)
proof
assume A1: not x in still_not-bound_in p;
hence |- All(x,p => q) => (p => All(x,q)) by Lm17;
|- All(x,q) => q by CQC_THE1:105;
then A2: |- All(x,All(x,q) => q) by Th26;
|- (All(x,q) => q) => ((p => All(x,q)) => (p => q)) by LUKASI_1:59;
then A3: |- All(x,(All(x,q) => q) => ((p => All(x,q)) => (p => q))) by Th26;
|- 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))) by Th34;
then |- All(x,All(x,q) => q) => All(x,(p => All(x,q)) => (p => q))
by A3,CQC_THE1:104;
then A4: |- All(x,(p => All(x,q)) => (p => q)) by A2,CQC_THE1:104;
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 |- All(x,(p => All(x,q)) => (p => q)) =>
((p => All(x,q)) => All(x,p => q)) by Lm17;
hence thesis by A4,CQC_THE1:104;
end;
theorem Th79:
not x in still_not-bound_in p implies |- (p => All(x,q)) <=> All(x,p => q)
proof
assume not x in still_not-bound_in p;
then |- (p => All(x,q)) => All(x,p => q) &
|- All(x,p => q) => (p => All(x,q)) by Th78;
hence thesis by Lm14;
end;
theorem
not x in still_not-bound_in p implies (|- All(x,p => q) iff |- p => All(x,q)
)
proof
assume not x in still_not-bound_in p;
then |- (p => All(x,q)) <=> All(x,p => q) by Th79;
hence thesis by Lm15;
end;
theorem Th81:
not x in still_not-bound_in q implies |- Ex(x,p => q) => (All(x,p) => q)
proof
assume A1: not x in still_not-bound_in q;
|- All(x,p) => p by CQC_THE1:105;
then |- (p => q) => (All(x,p) => q) by LUKASI_1:42;
then |- All(x,(p => q) => (All(x,p) => q)) &
|- All(x,(p => q) => (All(x,p) => q)) =>
(Ex(x,p => q) => Ex(x,All(x,p) => q)) by Th26,Th38;
then A2: |- Ex(x,p => q) => Ex(x,All(x,p) => q) by CQC_THE1:104;
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 |- Ex(x,All(x,p) => q) => (All(x,p) => q) by Th23;
hence thesis by A2,LUKASI_1:43;
end;
theorem Th82:
|- (All(x,p) => q) => Ex(x,p => q)
proof
|- All(x,p '&' 'not' q) => All(x,p) '&' 'not' q by Th69;
then |- 'not'(All(x,p) '&' 'not' q) => 'not' All(x,p '&' 'not'
q) by LUKASI_1:63;
then A1: |- (All(x,p) => q) => 'not' All(x,p '&' 'not' q) by QC_LANG2:def 2;
|- 'not' 'not'(p '&' 'not' q) => (p '&' 'not' q) by LUKASI_1:65;
then A2: |- All(x,'not' 'not'(p '&' 'not' q) => (p '&' 'not' q)) by Th26;
|- All(x,'not' 'not'(p '&' 'not' q) => (p '&' 'not' q)) =>
(All(x,'not' 'not'(p '&' 'not' q)) => All(x,(p '&' 'not' q))) by Th34;
then |- All(x,'not' 'not'(p '&' 'not' q)) => All(x,(p '&' 'not'
q)) by A2,CQC_THE1:104;
then |- 'not' All(x,p '&' 'not' q) => 'not' All(x,'not' 'not'(p '&' 'not'
q)) by LUKASI_1:63;
then |- (All(x,p) => q) => 'not' All(x,'not' 'not'(p '&' 'not'
q)) by A1,LUKASI_1:43;
then |- (All(x,p) => q) => Ex(x,'not'(p '&' 'not' q)) by QC_LANG2:def 5;
hence |- (All(x,p) => q) => Ex(x,p => q) by QC_LANG2:def 2;
end;
theorem
not x in still_not-bound_in q implies (|- All(x,p) => q iff |- Ex(x,p => q))
proof
assume not x in still_not-bound_in q;
then |- (All(x,p) => q) => Ex(x,p => q) & |- Ex(x,p => q) => (All(x,p) => q
)
by Th81,Th82;
then |- (All(x,p) => q) <=> Ex(x,p => q) by Lm14;
hence thesis by Lm15;
end;
theorem Th84:
not x in still_not-bound_in q implies |- (Ex(x,p) => q) => All(x,p => q) &
|- All(x,p => q) => (Ex(x,p) => q)
proof
assume A1: not x in still_not-bound_in q;
then not x in still_not-bound_in Ex(x,p) & not x in still_not-bound_in q
by Th6;
then A2: not x in still_not-bound_in Ex(x,p) => q by Th7;
|- p => Ex(x,p) by Th18;
then |- (Ex(x,p) => q) => (p => q) by LUKASI_1:42;
hence |- (Ex(x,p) => q) => All(x,p => q) by A2,CQC_THE1:106;
|- All(x,p => q) => (Ex(x,p) => Ex(x,q)) by Th38;
then |- (All(x,p => q) '&' Ex(x,p)) => Ex(x,q) & |- Ex(x,q) => q
by A1,Th1,Th23;
then |- (All(x,p => q) '&' Ex(x,p)) => q by LUKASI_1:43;
hence thesis by Th3;
end;
theorem Th85:
not x in still_not-bound_in q implies |- (Ex(x,p) => q) <=> All(x,p => q)
proof
assume not x in still_not-bound_in q;
then |- (Ex(x,p) => q) => All(x,p => q) & |- All(x,p => q) => (Ex(x,p) => q
)
by Th84;
hence thesis by Lm14;
end;
theorem
not x in still_not-bound_in q implies (|- Ex(x,p) => q iff |- All(x,p => q))
proof
assume not x in still_not-bound_in q;
then |- (Ex(x,p) => q) <=> All(x,p => q) by Th85;
hence thesis by Lm15;
end;
theorem Th87:
not x in still_not-bound_in p implies |- Ex(x,p => q) => (p => Ex(x,q))
proof
assume A1: not x in still_not-bound_in p;
|- q => Ex(x,q) by Th18;
then |- (p => q) => (p => Ex(x,q)) by LUKASI_1:60;
then A2: |- All(x,(p => q) => (p => Ex(x,q))) by Th26;
|- All(x,(p => q) => (p => Ex(x,q))) =>
(Ex(x,p => q) => Ex(x,p => Ex(x,q))) by Th38;
then A3: |- (Ex(x,p => q) => Ex(x,p => Ex(x,q))) by A2,CQC_THE1:104;
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 |- Ex(x,p => Ex(x,q)) => (p => Ex(x,q)) by Th23;
hence |- Ex(x,p => q) => (p => Ex(x,q)) by A3,LUKASI_1:43;
end;
theorem Th88:
|- (p => Ex(x,q)) => Ex(x,p => q)
proof
|- All(x,p '&' 'not' q) => (p '&' All(x,'not' q)) by Th68;
then A1: |- 'not'(p '&' All(x,'not' q)) => 'not' All(x,p '&' 'not'
q) by LUKASI_1:63;
|- All(x,'not' q) <=> 'not' Ex(x,q) by Th58;
then |- All(x,'not' q) => 'not' Ex(x,q) by Lm14;
then |- (p '&' All(x,'not' q)) => (p '&' 'not' Ex(x,q)) by Lm9;
then |- 'not'(p '&' 'not' Ex(x,q)) => 'not'(p '&' All(x,'not'
q)) by LUKASI_1:63;
then |- 'not'(p '&' 'not' Ex(x,q)) => 'not' All(x,p '&' 'not'
q) by A1,LUKASI_1:43;
then A2: |- (p => Ex(x,q)) => 'not' All(x,p '&' 'not' q) by QC_LANG2:def 2;
|- 'not' 'not'(p '&' 'not' q) => (p '&' 'not' q) by LUKASI_1:65;
then |- All(x,'not' 'not'(p '&' 'not' q) => (p '&' 'not' q)) &
|- All(x,'not' 'not'(p '&' 'not' q) => (p '&' 'not' q)) =>
(All(x,'not' 'not'(p '&' 'not' q)) => All(x,p '&' 'not' q)) by Th26,Th34;
then |- All(x,'not' 'not'(p '&' 'not' q)) => All(x,p '&' 'not'
q) by CQC_THE1:104;
then |- 'not' All(x,p '&' 'not' q) => 'not' All(x,'not' 'not'(p '&' 'not'
q)) by LUKASI_1:63;
then |- (p => Ex(x,q)) => 'not' All(x,'not' 'not'(p '&' 'not'
q)) by A2,LUKASI_1:43;
then |- (p => Ex(x,q)) => 'not' All(x,'not'(p => q)) by QC_LANG2:def 2;
hence thesis by QC_LANG2:def 5;
end;
theorem Th89:
not x in still_not-bound_in p implies |- (p => Ex(x,q)) <=> Ex(x,p => q)
proof
assume not x in still_not-bound_in p;
then |- (p => Ex(x,q)) => Ex(x,p => q) &
|- Ex(x,p => q) => (p => Ex(x,q)) by Th87,Th88;
hence thesis by Lm14;
end;
theorem
not x in still_not-bound_in p implies (|- p => Ex(x,q) iff |- Ex(x,p => q))
proof
assume not x in still_not-bound_in p;
then |- (p => Ex(x,q)) <=> Ex(x,p => q) by Th89;
hence thesis by Lm15;
end;
theorem {p} |- p
proof
p in {p} & {p} c= Cn({p}) by CQC_THE1:38,TARSKI:def 1;
hence p in Cn({p});
end;
theorem Th92: Cn({p} \/ {q}) = Cn({p '&' q})
proof
for t holds t in Cn({p} \/ {q}) iff
for T st T is_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_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_a_theory and A3: {p '&' q} c= T;
A4: p '&' q in T by A3,ZFMISC_1:37;
p '&' q => p in TAUT & p '&' q => q in TAUT & TAUT c= T
by A2,CQC_THE1:74,PROCAL_1:19,21;
then p in T & q in T by A2,A4,CQC_THE1:def 1;
then {p} c= T & {q} c= T by ZFMISC_1:37;
then {p} \/ {q} c= T by XBOOLE_1:8;
hence thesis by A1,A2,CQC_THE1:def 2;
end;
thus (for T st T is_a_theory & {p '&' q} c= T holds t in T) implies
t in Cn({p} \/ {q})
proof
assume A5: for T st T is_a_theory & {p '&' q} c= T holds t in T;
for T st T is_a_theory & {p} \/ {q} c= T holds t in T
proof
let T; assume that A6: T is_a_theory and A7: {p} \/ {q} c= T;
{p} c= {p} \/ {q} & {q} c= {p} \/ {q} by XBOOLE_1:7;
then {p} c= T & {q} c= T by A7,XBOOLE_1:1;
then A8: p in T & q in T by ZFMISC_1:37;
p => (q => p '&' q) in TAUT & TAUT c= T by A6,CQC_THE1:74,PROCAL_1:28;
then (q => p '&' q) in T by A6,A8,CQC_THE1:def 1;
then p '&' q in T by A6,A8,CQC_THE1:def 1;
then {p '&' q} c= T by ZFMISC_1:37;
hence thesis by A5,A6;
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:41;
hence r in Cn({p '&' q}) by Th92;
end;
assume r in Cn({p '&' q});
then r in Cn({p} \/ {q}) by Th92;
hence r in Cn({p,q}) by ENUMSET1:41;
end;
theorem Th94: X|- p implies X|- All(x,p)
proof
assume A1: X|- p;
|- p => ((All(x,p) => All(x,p)) => p) by LUKASI_1:45;
then X|- p => ((All(x,p) => All(x,p)) => p) by CQC_THE1:98;
then A2: X|- (All(x,p) => All(x,p)) => p by A1,CQC_THE1:92;
not x in still_not-bound_in All(x,p) by Th5;
then not x in still_not-bound_in All(x,p) => All(x,p) by Th7;
then A3: X|- (All(x,p) => All(x,p)) => All(x,p) by A2,CQC_THE1:94;
|- All(x,p) => All(x,p) by LUKASI_1:44;
then X|- All(x,p) => All(x,p) by CQC_THE1:98;
hence thesis by A3,CQC_THE1:92;
end;
theorem
Th95: not x in still_not-bound_in p implies
X|- All(x,p => q) => (p => All(x,q))
proof
assume not x in still_not-bound_in p;
then |- All(x,p => q) => (p => All(x,q)) by Th78;
hence thesis by CQC_THE1:98;
end;
:: 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,CQC_THE1:def 9;
then consider f such that A3: f is_a_proof_wrt (X \/ {F}) and
A4: Effect f = G by CQC_THE1:70;
defpred P[Nat] means
1 <= $1 & $1 <= len f implies for H st H = (f.$1)`1 holds X|- F => H;
A5: for n st for k st k < n holds P[k] holds P[n]
proof
let n such that A6: for k st k < n holds
1 <= k & k <= len f implies for H st H = (f.k)`1 holds X|- F => H;
assume A7: 1 <= n & n <= len f;
let H such that A8: H = (f.n)`1;
A9: f,n is_a_correct_step_wrt (X \/ {F}) by A3,A7,CQC_THE1:def 5;
now per cases by A7,CQC_THE1:45;
suppose (f.n)`2 = 0;
then H in X \/ {F} by A8,A9,CQC_THE1:def 4;
then A10: H in X or H in {F} by XBOOLE_0:def 2;
now per cases by A10,TARSKI:def 1;
suppose A11: H in X;
X c= Cn(X) by CQC_THE1:38;
then H in Cn(X) & |- H => (F => H) by A11,LUKASI_1:45;
then X|- H & X|- H => (F => H) by CQC_THE1:98,def 9;
hence X|- F => H by CQC_THE1:92;
suppose H = F;
then |- F => H by LUKASI_1:44;
hence X|- F => H by CQC_THE1:98;
end;
hence thesis;
suppose (f.n)`2 = 1;
then H = VERUM by A8,A9,CQC_THE1:def 4;
then |- F => H by LUKASI_1:50;
hence X|- F => H by CQC_THE1:98;
suppose (f.n)`2 = 2;
then ex p st H = ('not' p => p) => p by A8,A9,CQC_THE1:def 4;
then |- H by CQC_THE1:100;
then X|- H by CQC_THE1:98;
hence X|- F => H by LUKASI_1:78;
suppose (f.n)`2 = 3;
then ex p,q st H = p => ('not' p => q) by A8,A9,CQC_THE1:def 4;
then |- H by CQC_THE1:101;
then X|- H by CQC_THE1:98;
hence X|- F => H by LUKASI_1:78;
suppose (f.n)`2 = 4;
then ex p,q,r st H = (p => q) => ('not'(q '&' r) => 'not'(p '&' r))
by A8,A9,CQC_THE1:def 4;
then |- H by CQC_THE1:102;
then X|- H by CQC_THE1:98;
hence X|- F => H by LUKASI_1:78;
suppose (f.n)`2 = 5;
then ex p,q st H = p '&' q => q '&' p by A8,A9,CQC_THE1:def 4;
then |- H by CQC_THE1:103;
then X|- H by CQC_THE1:98;
hence X|- F => H by LUKASI_1:78;
suppose (f.n)`2 = 6;
then ex p,x st H = All(x,p) => p by A8,A9,CQC_THE1:def 4;
then |- H by CQC_THE1:105;
then X|- H by CQC_THE1:98;
hence X|- F => H by LUKASI_1:78;
suppose (f.n)`2 = 7;
then consider i,j,p,q such that A12:1 <= i & i < n & 1 <=
j & j < i and
A13:p = (f.j)`1 & q = H & (f.i)`1 = p => q by A8,A9,CQC_THE1:def 4;
j < n & i <= n & j <= n by A12,AXIOMS:22;
then (i < n & 1 <= i & i <= len f) & (j < n & 1 <= j & j <= len f)
by A7,A12,AXIOMS:22;
then A14: X|- F => (p => q) & X|- F => p by A6,A13;
|- (F => (p => q)) => ((F => p) => (F => q)) by LUKASI_1:54;
then X|- (F => (p => q)) => ((F => p) => (F => q)) by CQC_THE1:98;
then X|- (F => p) => (F => q) by A14,CQC_THE1:92;
hence X|- F => H by A13,A14,CQC_THE1:92;
suppose (f.n)`2 = 8;
then consider i,p,q,x such that A15:1 <= i & i < n and
A16:(f.i)`1 = p => q and A17: not x in still_not-bound_in p &
H = p => All(x,q) by A8,A9,CQC_THE1:def 4;
A18: not x in still_not-bound_in F by A1,QC_LANG1:def 30;
i <= len f by A7,A15,AXIOMS:22;
then X|- F => (p => q) by A6,A15,A16;
then A19: X|- All(x,F => (p => q)) by Th94;
|- All(x,F => (p => q)) => (F => All(x,p => q)) by A18,Th78;
then X|- All(x,F => (p => q)) => (F => All(x,p => q))
by CQC_THE1:98;
then A20: X|- F => All(x,p => q) by A19,CQC_THE1:92;
X|- All(x,p => q) => (p => All(x,q)) by A17,Th95;
hence X|- F => H by A17,A20,LUKASI_1:76;
suppose (f.n)`2 = 9;
then consider i,x,y,s such that A21: 1 <= i & i < n and
A22: s.x in CQC-WFF & s.y in CQC-WFF and
A23: not x in still_not-bound_in s & s.x = (f.i)`1 & H = s.y
by A8,A9,CQC_THE1:def 4;
reconsider s1 = s.x, s2 = s.y as Element of CQC-WFF by A22;
i <= len f by A7,A21,AXIOMS:22;
then X|- F => s1 by A6,A21,A23;
then A24: X|- All(x,F => s1) by Th94;
not x in still_not-bound_in F by A1,QC_LANG1:def 30;
then X|- All(x,F => s1) => (F => All(x,s1)) by Th95;
then A25: X |- F => All(x,s1) by A24,CQC_THE1:92;
|- All(x,s1) => s2 by A23,Th28;
then X|- All(x,s1) => s2 by CQC_THE1:98;
hence X|- F => H by A23,A25,LUKASI_1:76;
end;
hence thesis;
end;
A26: P[n] from Comp_Ind(A5);
A27: 1 <= len f & len f <= len f by A3,CQC_THE1:58;
f <> {} by A3,CQC_THE1:def 5;
then G = (f.len f)`1 by A4,CQC_THE1:def 6;
hence thesis by A26,A27;
end;