:: Calculus of Quantifiers. Deduction Theorem
:: by Agata Darmochwa\l
::
:: Received October 24, 1990
:: Copyright (c) 1990 Association of Mizar Users

begin

theorem Th1: :: CQC_THE2:1

for p, q, r being Element of CQC-WFF st p => (q => r) is valid holds
(p '&' q) => r is valid

proof end;

theorem Th2: :: CQC_THE2:2

for p, q, r being Element of CQC-WFF st p => (q => r) is valid holds
(q '&' p) => r is valid

proof end;

theorem Th3: :: CQC_THE2:3

for p, q, r being Element of CQC-WFF st (p '&' q) => r is valid holds
p => (q => r) is valid

proof end;

theorem Th4: :: CQC_THE2:4

for p, q, r being Element of CQC-WFF st (p '&' q) => r is valid holds
q => (p => r) is valid

proof end;

Lm1: for p, q being Element of CQC-WFF holds
( (p '&' q) => p is valid & (p '&' q) => q is valid )

proof end;

Lm2: for p, q being Element of CQC-WFF st p '&' q is valid holds
( p is valid & q is valid )

proof end;

Lm3: for p, q, r being Element of CQC-WFF st p => q is valid & p => r is valid holds
p => (q '&' r) is valid

proof end;

Lm4: for p, q, r, t being Element of CQC-WFF st p => q is valid & r => t is valid holds
(p 'or' r) => (q 'or' t) is valid

proof end;

Lm5: for p, q, r, t being Element of CQC-WFF st p => q is valid & r => t is valid holds
(p '&' r) => (q '&' t) is valid

proof end;

Lm6: for p, q being Element of CQC-WFF holds
( p => (p 'or' q) is valid & p => (q 'or' p) is valid )

proof end;

Lm7: for p, q, r being Element of CQC-WFF st p => q is valid & r => q is valid holds
(p 'or' r) => q is valid

proof end;

Lm8: for p, q being Element of CQC-WFF st p is valid & q is valid holds
p '&' q is valid

proof end;

Lm9: for p, q, r being Element of CQC-WFF st p => q is valid holds
(r '&' p) => (r '&' q) is valid

proof end;

Lm10: for p, q, r being Element of CQC-WFF st p => q is valid holds
(p 'or' r) => (q 'or' r) is valid

proof end;

Lm11: for p, q being Element of CQC-WFF holds (p 'or' q) => (('not' p) => q) is valid

proof end;

Lm12: for p, q being Element of CQC-WFF holds (('not' p) => q) => (p 'or' q) is valid

proof end;

Lm13: for p being Element of CQC-WFF holds p <=> p is valid

proof end;

Lm14: for p, q being Element of CQC-WFF holds
( ( p => q is valid & q => p is valid ) iff p <=> q is valid )

proof end;

Lm15: for p, q being Element of CQC-WFF st p <=> q is valid holds
( p is valid iff q is valid )

proof end;

Lm16: for p, q, r, t being Element of CQC-WFF st p => (q => r) is valid & r => t is valid holds
p => (q => t) is valid

proof end;

theorem Th5: :: CQC_THE2:5

for s being QC-formula
for y, x being bound_QC-variable holds
( y in still_not-bound_in (All x,s) iff ( y in still_not-bound_in s & y <> x ) )

proof end;

theorem Th6: :: CQC_THE2:6

for s being QC-formula
for y, x being bound_QC-variable holds
( y in still_not-bound_in (Ex x,s) iff ( y in still_not-bound_in s & y <> x ) )

proof end;

theorem Th7: :: CQC_THE2:7

for s, h being QC-formula
for y being bound_QC-variable holds
( 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 end;

theorem :: CQC_THE2:8

canceled;

theorem Th9: :: CQC_THE2:9

for s, h being QC-formula
for y being bound_QC-variable holds
( 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 end;

theorem Th10: :: CQC_THE2:10

for s, h being QC-formula
for y being bound_QC-variable holds
( 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 end;

theorem :: CQC_THE2:11

for s being QC-formula
for x, y being bound_QC-variable holds
( not x in still_not-bound_in (All x,y,s) & not y in still_not-bound_in (All x,y,s) )

proof end;

theorem :: CQC_THE2:12

for s being QC-formula
for x, y being bound_QC-variable holds
( not x in still_not-bound_in (Ex x,y,s) & not y in still_not-bound_in (Ex x,y,s) )

proof end;

theorem :: CQC_THE2:13

canceled;

theorem Th14: :: CQC_THE2:14

for s, h being QC-formula
for x being bound_QC-variable holds (s => h) . x = (s . x) => (h . x)

proof end;

theorem :: CQC_THE2:15

for s, h being QC-formula
for x being bound_QC-variable holds (s 'or' h) . x = (s . x) 'or' (h . x)

proof end;

theorem :: CQC_THE2:16

canceled;

theorem :: CQC_THE2:17

for p being Element of CQC-WFF
for x, y being bound_QC-variable st x <> y holds
(Ex x,p) . y = Ex x,(p . y)

proof end;

theorem Th18: :: CQC_THE2:18

for p being Element of CQC-WFF
for x being bound_QC-variable holds p => (Ex x,p) is valid

proof end;

theorem Th19: :: CQC_THE2:19

for p being Element of CQC-WFF
for x being bound_QC-variable st p is valid holds
Ex x,p is valid

proof end;

theorem :: CQC_THE2:20

for p being Element of CQC-WFF
for x being bound_QC-variable holds (All x,p) => (Ex x,p) is valid

proof end;

theorem :: CQC_THE2:21

for p being Element of CQC-WFF
for x, y being bound_QC-variable holds (All x,p) => (Ex y,p) is valid

proof end;

theorem Th22: :: CQC_THE2:22

for p, q being Element of CQC-WFF
for x being bound_QC-variable st p => q is valid & not x in still_not-bound_in q holds
(Ex x,p) => q is valid

proof end;

theorem Th23: :: CQC_THE2:23

for p being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
(Ex x,p) => p is valid

proof end;

theorem :: CQC_THE2:24

for p being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p & Ex x,p is valid holds
p is valid

proof end;

theorem Th25: :: CQC_THE2:25

for p, q being Element of CQC-WFF
for h being QC-formula
for x, y being bound_QC-variable st p = h . x & q = h . y & not y in still_not-bound_in h holds
p => (Ex y,q) is valid

proof end;

theorem Th26: :: CQC_THE2:26

for p being Element of CQC-WFF
for x being bound_QC-variable st p is valid holds
All x,p is valid

proof end;

theorem Th27: :: CQC_THE2:27

for p being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
p => (All x,p) is valid

proof end;

theorem Th28: :: CQC_THE2:28

for p, q being Element of CQC-WFF
for h being QC-formula
for x, y being bound_QC-variable st p = h . x & q = h . y & not x in still_not-bound_in h holds
(All x,p) => q is valid

proof end;

theorem :: CQC_THE2:29

for p being Element of CQC-WFF
for y, x being bound_QC-variable st not y in still_not-bound_in p holds
(All x,p) => (All y,p) is valid

proof end;

theorem :: CQC_THE2:30

for p, q being Element of CQC-WFF
for h being QC-formula
for x, y being bound_QC-variable st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in p holds
(All x,p) => (All y,q) is valid

proof end;

theorem :: CQC_THE2:31

for p being Element of CQC-WFF
for x, y being bound_QC-variable st not x in still_not-bound_in p holds
(Ex x,p) => (Ex y,p) is valid

proof end;

theorem :: CQC_THE2:32

for p, q being Element of CQC-WFF
for h being QC-formula
for x, y being bound_QC-variable st p = h . x & q = h . y & not x in still_not-bound_in q & not y in still_not-bound_in h holds
(Ex x,p) => (Ex y,q) is valid

proof end;

theorem :: CQC_THE2:33

canceled;

theorem Th34: :: CQC_THE2:34

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds (All x,(p => q)) => ((All x,p) => (All x,q)) is valid

proof end;

theorem Th35: :: CQC_THE2:35

for p, q being Element of CQC-WFF
for x being bound_QC-variable st All x,(p => q) is valid holds
(All x,p) => (All x,q) is valid

proof end;

theorem Th36: :: CQC_THE2:36

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds (All x,(p <=> q)) => ((All x,p) <=> (All x,q)) is valid

proof end;

theorem :: CQC_THE2:37

for p, q being Element of CQC-WFF
for x being bound_QC-variable st All x,(p <=> q) is valid holds
(All x,p) <=> (All x,q) is valid

proof end;

theorem Th38: :: CQC_THE2:38

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds (All x,(p => q)) => ((Ex x,p) => (Ex x,q)) is valid

proof end;

theorem Th39: :: CQC_THE2:39

for p, q being Element of CQC-WFF
for x being bound_QC-variable st All x,(p => q) is valid holds
(Ex x,p) => (Ex x,q) is valid

proof end;

theorem Th40: :: CQC_THE2:40

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds
( (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 end;

theorem Th41: :: CQC_THE2:41

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds (All x,(p '&' q)) <=> ((All x,p) '&' (All x,q)) is valid

proof end;

theorem :: CQC_THE2:42

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds
( All x,(p '&' q) is valid iff (All x,p) '&' (All x,q) is valid )

proof end;

theorem Th43: :: CQC_THE2:43

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds ((All x,p) 'or' (All x,q)) => (All x,(p 'or' q)) is valid

proof end;

theorem Th44: :: CQC_THE2:44

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds
( (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 end;

theorem Th45: :: CQC_THE2:45

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds (Ex x,(p 'or' q)) <=> ((Ex x,p) 'or' (Ex x,q)) is valid

proof end;

theorem :: CQC_THE2:46

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds
( Ex x,(p 'or' q) is valid iff (Ex x,p) 'or' (Ex x,q) is valid )

proof end;

theorem Th47: :: CQC_THE2:47

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds (Ex x,(p '&' q)) => ((Ex x,p) '&' (Ex x,q)) is valid

proof end;

theorem :: CQC_THE2:48

for p, q being Element of CQC-WFF
for x being bound_QC-variable st Ex x,(p '&' q) is valid holds
(Ex x,p) '&' (Ex x,q) is valid

proof end;

theorem Th49: :: CQC_THE2:49

for p being Element of CQC-WFF
for x being bound_QC-variable holds
( (All x,('not' ('not' p))) => (All x,p) is valid & (All x,p) => (All x,('not' ('not' p))) is valid )

proof end;

theorem :: CQC_THE2:50

for p being Element of CQC-WFF
for x being bound_QC-variable holds (All x,('not' ('not' p))) <=> (All x,p) is valid

proof end;

theorem Th51: :: CQC_THE2:51

for p being Element of CQC-WFF
for x being bound_QC-variable holds
( (Ex x,('not' ('not' p))) => (Ex x,p) is valid & (Ex x,p) => (Ex x,('not' ('not' p))) is valid )

proof end;

theorem :: CQC_THE2:52

for p being Element of CQC-WFF
for x being bound_QC-variable holds (Ex x,('not' ('not' p))) <=> (Ex x,p) is valid

proof end;

theorem Th53: :: CQC_THE2:53

for p being Element of CQC-WFF
for x being bound_QC-variable holds
( ('not' (Ex x,('not' p))) => (All x,p) is valid & (All x,p) => ('not' (Ex x,('not' p))) is valid )

proof end;

theorem :: CQC_THE2:54

for p being Element of CQC-WFF
for x being bound_QC-variable holds ('not' (Ex x,('not' p))) <=> (All x,p) is valid

proof end;

theorem Th55: :: CQC_THE2:55

for p being Element of CQC-WFF
for x being bound_QC-variable holds
( ('not' (All x,p)) => (Ex x,('not' p)) is valid & (Ex x,('not' p)) => ('not' (All x,p)) is valid )

proof end;

theorem :: CQC_THE2:56

for p being Element of CQC-WFF
for x being bound_QC-variable holds ('not' (All x,p)) <=> (Ex x,('not' p)) is valid

proof end;

theorem :: CQC_THE2:57

for p being Element of CQC-WFF
for x being bound_QC-variable holds
( ('not' (Ex x,p)) => (All x,('not' p)) is valid & (All x,('not' p)) => ('not' (Ex x,p)) is valid )

proof end;

theorem Th58: :: CQC_THE2:58

for p being Element of CQC-WFF
for x being bound_QC-variable holds (All x,('not' p)) <=> ('not' (Ex x,p)) is valid

proof end;

theorem :: CQC_THE2:59

for p being Element of CQC-WFF
for x, y being bound_QC-variable holds
( (All x,(All y,p)) => (All y,(All x,p)) is valid & (All x,y,p) => (All y,x,p) is valid )

proof end;

theorem :: CQC_THE2:60

for p, q being Element of CQC-WFF
for h being QC-formula
for x, y being bound_QC-variable st p = h . x & q = h . y & not y in still_not-bound_in h holds
(All x,(All y,q)) => (All x,p) is valid

proof end;

theorem :: CQC_THE2:61

for p being Element of CQC-WFF
for x, y being bound_QC-variable holds
( (Ex x,(Ex y,p)) => (Ex y,(Ex x,p)) is valid & (Ex x,y,p) => (Ex y,x,p) is valid )

proof end;

theorem :: CQC_THE2:62

for p, q being Element of CQC-WFF
for h being QC-formula
for x, y being bound_QC-variable st p = h . x & q = h . y & not y in still_not-bound_in h holds
(Ex x,p) => (Ex x,y,q) is valid

proof end;

theorem :: CQC_THE2:63

for p being Element of CQC-WFF
for x, y being bound_QC-variable holds (Ex x,(All y,p)) => (All y,(Ex x,p)) is valid

proof end;

theorem :: CQC_THE2:64

for p being Element of CQC-WFF
for x being bound_QC-variable holds Ex x,(p <=> p) is valid by Lm13, Th19;

theorem Th65: :: CQC_THE2:65

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds
( (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 end;

theorem Th66: :: CQC_THE2:66

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds (Ex x,(p => q)) <=> ((All x,p) => (Ex x,q)) is valid

proof end;

theorem :: CQC_THE2:67

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds
( Ex x,(p => q) is valid iff (All x,p) => (Ex x,q) is valid )

proof end;

theorem Th68: :: CQC_THE2:68

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds (All x,(p '&' q)) => (p '&' (All x,q)) is valid

proof end;

theorem Th69: :: CQC_THE2:69

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds (All x,(p '&' q)) => ((All x,p) '&' q) is valid

proof end;

theorem Th70: :: CQC_THE2:70

for p, q being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
(p '&' (All x,q)) => (All x,(p '&' q)) is valid

proof end;

theorem :: CQC_THE2:71

for p, q being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p & p '&' (All x,q) is valid holds
All x,(p '&' q) is valid

proof end;

theorem Th72: :: CQC_THE2:72

for p, q being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
( (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 end;

theorem Th73: :: CQC_THE2:73

for p, q being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
(p 'or' (All x,q)) <=> (All x,(p 'or' q)) is valid

proof end;

theorem :: CQC_THE2:74

for p, q being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
( p 'or' (All x,q) is valid iff All x,(p 'or' q) is valid )

proof end;

theorem Th75: :: CQC_THE2:75

for p, q being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
( (p '&' (Ex x,q)) => (Ex x,(p '&' q)) is valid & (Ex x,(p '&' q)) => (p '&' (Ex x,q)) is valid )

proof end;

theorem Th76: :: CQC_THE2:76

for p, q being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
(p '&' (Ex x,q)) <=> (Ex x,(p '&' q)) is valid

proof end;

theorem :: CQC_THE2:77

for p, q being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
( p '&' (Ex x,q) is valid iff Ex x,(p '&' q) is valid )

proof end;

Lm17: for p, q being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
(All x,(p => q)) => (p => (All x,q)) is valid

proof end;

theorem Th78: :: CQC_THE2:78

for p, q being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
( (All x,(p => q)) => (p => (All x,q)) is valid & (p => (All x,q)) => (All x,(p => q)) is valid )

proof end;

theorem Th79: :: CQC_THE2:79

for p, q being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
(p => (All x,q)) <=> (All x,(p => q)) is valid

proof end;

theorem :: CQC_THE2:80

for p, q being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
( All x,(p => q) is valid iff p => (All x,q) is valid )

proof end;

theorem Th81: :: CQC_THE2:81

for q, p being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in q holds
(Ex x,(p => q)) => ((All x,p) => q) is valid

proof end;

theorem Th82: :: CQC_THE2:82

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds ((All x,p) => q) => (Ex x,(p => q)) is valid

proof end;

theorem :: CQC_THE2:83

for q, p being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in q holds
( (All x,p) => q is valid iff Ex x,(p => q) is valid )

proof end;

theorem Th84: :: CQC_THE2:84

for q, p being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in q holds
( ((Ex x,p) => q) => (All x,(p => q)) is valid & (All x,(p => q)) => ((Ex x,p) => q) is valid )

proof end;

theorem Th85: :: CQC_THE2:85

for q, p being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in q holds
((Ex x,p) => q) <=> (All x,(p => q)) is valid

proof end;

theorem :: CQC_THE2:86

for q, p being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in q holds
( (Ex x,p) => q is valid iff All x,(p => q) is valid )

proof end;

theorem Th87: :: CQC_THE2:87

for p, q being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
(Ex x,(p => q)) => (p => (Ex x,q)) is valid

proof end;

theorem Th88: :: CQC_THE2:88

for p, q being Element of CQC-WFF
for x being bound_QC-variable holds (p => (Ex x,q)) => (Ex x,(p => q)) is valid

proof end;

theorem Th89: :: CQC_THE2:89

for p, q being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
(p => (Ex x,q)) <=> (Ex x,(p => q)) is valid

proof end;

theorem :: CQC_THE2:90

for p, q being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
( p => (Ex x,q) is valid iff Ex x,(p => q) is valid )

proof end;

theorem :: CQC_THE2:91

for p being Element of CQC-WFF holds {p} |- p

proof end;

theorem Th92: :: CQC_THE2:92

for p, q being Element of CQC-WFF holds Cn ({p} \/ {q}) = Cn {(p '&' q)}

proof end;

theorem :: CQC_THE2:93

for p, q, r being Element of CQC-WFF holds
( {p,q} |- r iff {(p '&' q)} |- r )

proof end;

theorem Th94: :: CQC_THE2:94

for X being Subset of
for p being Element of CQC-WFF
for x being bound_QC-variable st X |- p holds
X |- All x,p

proof end;

theorem :: CQC_THE2:95

for X being Subset of
for p, q being Element of CQC-WFF
for x being bound_QC-variable st not x in still_not-bound_in p holds
X |- (All x,(p => q)) => (p => (All x,q)) by Th78, CQC_THE1:98;

theorem :: CQC_THE2:96

for X being Subset of
for F, G being Element of CQC-WFF st F is closed & X \/ {F} |- G holds
X |- F => G

proof end;