The abstract of the Mizar article:

Calculus of Quantifiers. Deduction Theorem

by

Agata Darmochwal

Received October 24, 1990

MML identifier: CQC_THE2

[ Mizar article, MML identifier index ]

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;


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 :: CQC_THE2:1
 |- p => (q => r) implies |- (p '&' q) => r;

theorem :: CQC_THE2:2
|- p => (q => r) implies |- (q '&' p) => r;

theorem :: CQC_THE2:3
|- (p '&' q) => r implies |- p => (q => r);

theorem :: CQC_THE2:4
|- (p '&' q) => r implies |- q => (p => r);

::------------------------------------------------

theorem :: CQC_THE2:5
y in still_not-bound_in All(x,s) iff
 y in still_not-bound_in s & y <> x;

theorem :: CQC_THE2:6
y in still_not-bound_in Ex(x,s) iff
 y in still_not-bound_in s & y <> x;

theorem :: CQC_THE2:7
y in still_not-bound_in s => h iff
 y in still_not-bound_in s or y in still_not-bound_in h;

canceled;

theorem :: CQC_THE2:9
y in still_not-bound_in s '&' h iff
 y in still_not-bound_in s or y in still_not-bound_in h;

theorem :: CQC_THE2:10
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;

theorem :: CQC_THE2:11
not x in still_not-bound_in All(x,y,s) &
  not y in still_not-bound_in All(x,y,s);

theorem :: CQC_THE2:12
not x in still_not-bound_in Ex(x,y,s) &
  not y in still_not-bound_in Ex(x,y,s);

canceled;

theorem :: CQC_THE2:14
(s => h).x = (s.x) => (h.x);

theorem :: CQC_THE2:15
(s 'or' h).x = (s.x) 'or' (h.x);

canceled;

theorem :: CQC_THE2:17
x<>y implies (Ex(x,p)).y = Ex(x,p.y);

::---------------------------------------------------------

theorem :: CQC_THE2:18
|- p => Ex(x,p);

theorem :: CQC_THE2:19
|- p implies |- Ex(x,p);

theorem :: CQC_THE2:20
|- All(x,p) => Ex(x,p);

theorem :: CQC_THE2:21
|- All(x,p) => Ex(y,p);

theorem :: CQC_THE2:22
|- p => q & not x in still_not-bound_in q implies
 |- Ex(x,p) => q;

theorem :: CQC_THE2:23
not x in still_not-bound_in p implies |- Ex(x,p) => p;

theorem :: CQC_THE2:24
not x in still_not-bound_in p & |- Ex(x,p) implies |- p;

theorem :: CQC_THE2:25
p=h.x & q=h.y & not y in still_not-bound_in h
 implies |- p => Ex(y,q);

theorem :: CQC_THE2:26
|- p implies |- All(x,p);

theorem :: CQC_THE2:27
not x in still_not-bound_in p implies |- p => All(x,p);

theorem :: CQC_THE2:28
p=h.x & q=h.y & not x in still_not-bound_in h
 implies |- All(x,p) => q;

theorem :: CQC_THE2:29
    not y in still_not-bound_in p implies |- All(x,p) => All(y,p);

theorem :: CQC_THE2:30
   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);

theorem :: CQC_THE2:31
    not x in still_not-bound_in p implies |- Ex(x,p) => Ex(y,p);

theorem :: CQC_THE2:32
   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);

canceled;

theorem :: CQC_THE2:34
  |- All(x,p => q) => (All(x,p) => All(x,q));

theorem :: CQC_THE2:35
  |- All(x,p => q) implies |- All(x,p) => All(x,q);

theorem :: CQC_THE2:36
 |- All(x,p <=> q) => (All(x,p) <=> All(x,q));

theorem :: CQC_THE2:37
   |- All(x,p <=> q) implies |- All(x,p) <=> All(x,q);

theorem :: CQC_THE2:38
  |- All(x,p => q) => (Ex(x,p) => Ex(x,q));

theorem :: CQC_THE2:39
|- All(x,p => q) implies |- Ex(x,p) => Ex(x,q);

theorem :: CQC_THE2:40
  |- All(x,p '&' q) => (All(x,p) '&' All(x,q)) &
 |- (All(x,p) '&' All(x,q)) => All(x,p '&' q);

theorem :: CQC_THE2:41
  |- All(x,p '&' q) <=> (All(x,p) '&' All(x,q));

theorem :: CQC_THE2:42
|- All(x,p '&' q) iff |- All(x,p) '&' All(x,q);

theorem :: CQC_THE2:43
  |- (All(x,p) 'or' All(x,q)) => All(x,p 'or' q);

theorem :: CQC_THE2:44
  |- Ex(x,p 'or' q) => (Ex(x,p) 'or' Ex(x,q)) &
  |- (Ex(x,p) 'or' Ex(x,q)) => Ex(x,p 'or' q);

theorem :: CQC_THE2:45
  |- Ex(x,p 'or' q) <=> (Ex(x,p) 'or' Ex(x,q));

theorem :: CQC_THE2:46
   |- Ex(x,p 'or' q) iff |- Ex(x,p) 'or' Ex(x,q);

theorem :: CQC_THE2:47
 |- Ex(x,p '&' q) => (Ex(x,p) '&' Ex(x,q));

theorem :: CQC_THE2:48
   |- Ex(x,p '&' q) implies |- Ex(x,p) '&' Ex(x,q);

theorem :: CQC_THE2:49
|- All(x,'not' 'not' p) => All(x,p) & |- All(x,p) => All(x,'not'
'not' p);

theorem :: CQC_THE2:50
|- All(x,'not' 'not' p) <=> All(x,p);

theorem :: CQC_THE2:51
|- Ex(x,'not' 'not' p) => Ex(x,p) &
 |- Ex(x,p) => Ex(x,'not' 'not' p);

theorem :: CQC_THE2:52
|- Ex(x,'not' 'not' p) <=> Ex(x,p);

theorem :: CQC_THE2:53
 |- 'not' Ex(x,'not' p) => All(x,p) & |- All(x,p) => 'not' Ex(x,'not' p);

theorem :: CQC_THE2:54
|- 'not' Ex(x,'not' p) <=> All(x,p);

theorem :: CQC_THE2:55
|- 'not' All(x,p) => Ex(x,'not' p) & |- Ex(x,'not' p) => 'not'
All(x,p);

theorem :: CQC_THE2:56
|- 'not' All(x,p) <=> Ex(x,'not' p);

theorem :: CQC_THE2:57
|- 'not' Ex(x,p) => All(x,'not' p) & |- All(x,'not' p) => 'not' Ex(x,
p
);

theorem :: CQC_THE2:58
|- All(x,'not' p) <=> 'not' Ex(x,p);

theorem :: CQC_THE2:59
   |- All(x,All(y,p)) => All(y,All(x,p)) & |- All(x,y,p) => All(y,x,p);

theorem :: CQC_THE2:60
   p=h.x & q=h.y & not y in still_not-bound_in h
 implies |- All(x,All(y,q)) => All(x,p);

theorem :: CQC_THE2:61
   |- Ex(x,Ex(y,p)) => Ex(y,Ex(x,p)) & |- Ex(x,y,p) => Ex(y,x,p);

theorem :: CQC_THE2:62
   p=h.x & q=h.y & not y in still_not-bound_in h implies
  |- Ex(x,p) => Ex(x,y,q);

theorem :: CQC_THE2:63
   |- Ex(x,All(y,p)) => All(y,Ex(x,p));

theorem :: CQC_THE2:64
|- Ex(x,p <=> p);

theorem :: CQC_THE2:65
 |- Ex(x,p => q) => (All(x,p) => Ex(x,q)) &
  |- (All(x,p) => Ex(x,q)) => Ex(x,p => q);

theorem :: CQC_THE2:66
 |- Ex(x,p => q) <=> (All(x,p) => Ex(x,q));

theorem :: CQC_THE2:67
   |- Ex(x,p => q) iff |- All(x,p) => Ex(x,q);

theorem :: CQC_THE2:68
 |- All(x,p '&' q) => (p '&' All(x,q));

theorem :: CQC_THE2:69
 |- All(x,p '&' q) => (All(x,p) '&' q);

theorem :: CQC_THE2:70
 not x in still_not-bound_in p implies |- (p '&' All(x,q)) => All(x,p '&' q);

theorem :: CQC_THE2:71
   not x in still_not-bound_in p & |- p '&' All(x,q) implies |- All(x,p '&' q);

theorem :: CQC_THE2:72
 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));


theorem :: CQC_THE2:73
 not x in still_not-bound_in p implies |- (p 'or' All(x,q)) <=> All(x,p 'or' q)
;

theorem :: CQC_THE2:74
   not x in still_not-bound_in p implies
  (|- p 'or' All(x,q) iff |- All(x,p 'or' q));

theorem :: CQC_THE2:75
 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));

theorem :: CQC_THE2:76
 not x in still_not-bound_in p implies |- (p '&' Ex(x,q)) <=> Ex(x,p '&' q);

theorem :: CQC_THE2:77
   not x in still_not-bound_in p implies (|- p '&' Ex(x,q) iff |- Ex(x,p '&' q)
);

theorem :: CQC_THE2:78
  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);

theorem :: CQC_THE2:79
 not x in still_not-bound_in p implies |- (p => All(x,q)) <=> All(x,p => q);

theorem :: CQC_THE2:80
   not x in still_not-bound_in p implies (|- All(x,p => q) iff |- p => All(x,q)
);

theorem :: CQC_THE2:81
 not x in still_not-bound_in q implies |- Ex(x,p => q) => (All(x,p) => q);

theorem :: CQC_THE2:82
 |- (All(x,p) => q) => Ex(x,p => q);

theorem :: CQC_THE2:83
   not x in still_not-bound_in q implies (|- All(x,p) => q iff |- Ex(x,p => q))
;

theorem :: CQC_THE2:84
 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);

theorem :: CQC_THE2:85
 not x in still_not-bound_in q implies |- (Ex(x,p) => q) <=> All(x,p => q);

theorem :: CQC_THE2:86
   not x in still_not-bound_in q implies (|- Ex(x,p) => q iff |- All(x,p => q))
;

theorem :: CQC_THE2:87
 not x in still_not-bound_in p implies |- Ex(x,p => q) => (p => Ex(x,q));

theorem :: CQC_THE2:88
 |- (p => Ex(x,q)) => Ex(x,p => q);

theorem :: CQC_THE2:89
 not x in still_not-bound_in p implies |- (p => Ex(x,q)) <=> Ex(x,p => q);

theorem :: CQC_THE2:90
   not x in still_not-bound_in p implies (|- p => Ex(x,q) iff |- Ex(x,p => q));

theorem :: CQC_THE2:91
{p} |- p;

theorem :: CQC_THE2:92
Cn({p} \/ {q}) = Cn({p '&' q});

theorem :: CQC_THE2:93
{p,q} |- r iff {p '&' q} |- r;

theorem :: CQC_THE2:94
X|- p implies X|- All(x,p);

theorem :: CQC_THE2:95
  not x in still_not-bound_in p implies
  X|- All(x,p => q) => (p => All(x,q));

:: Deduction Theorem

theorem :: CQC_THE2:96
   F is closed & (X \/ {F})|- G implies X |- F => G;