Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Calculus of Quantifiers. Deduction Theorem

by
Agata Darmochwal

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;
```