:: Calculus of Quantifiers. Deduction Theorem :: by Agata Darmochwa\l :: :: Received October 24, 1990 :: Copyright (c) 1990-2017 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; 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 :: CQC_THE2:1 p => (q => r) is valid implies (p '&' q) => r is valid; theorem :: CQC_THE2:2 p => (q => r) is valid implies (q '&' p) => r is valid; theorem :: CQC_THE2:3 (p '&' q) => r is valid implies p => (q => r) is valid; theorem :: CQC_THE2:4 (p '&' q) => r is valid implies q => (p => r) is valid; ::------------------------------------------------ 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; theorem :: CQC_THE2:8 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:9 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:10 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:11 not x in still_not-bound_in Ex(x,y,s) & not y in still_not-bound_in Ex (x,y,s); theorem :: CQC_THE2:12 (s => h).x = (s.x) => (h.x); theorem :: CQC_THE2:13 (s 'or' h).x = (s.x) 'or' (h.x); theorem :: CQC_THE2:14 x<>y implies (Ex(x,p)).y = Ex(x,p.y); ::--------------------------------------------------------- theorem :: CQC_THE2:15 p => Ex(x,p) is valid; theorem :: CQC_THE2:16 p is valid implies Ex(x,p) is valid; theorem :: CQC_THE2:17 All(x,p) => Ex(x,p) is valid; theorem :: CQC_THE2:18 All(x,p) => Ex(y,p) is valid; theorem :: CQC_THE2:19 p => q is valid & not x in still_not-bound_in q implies Ex(x,p) => q is valid ; theorem :: CQC_THE2:20 not x in still_not-bound_in p implies Ex(x,p) => p is valid; theorem :: CQC_THE2:21 not x in still_not-bound_in p & Ex(x,p) is valid implies p is valid; theorem :: CQC_THE2:22 p=h.x & q=h.y & not y in still_not-bound_in h implies p => Ex(y, q) is valid; theorem :: CQC_THE2:23 p is valid implies All(x,p) is valid; theorem :: CQC_THE2:24 not x in still_not-bound_in p implies p => All(x,p) is valid; theorem :: CQC_THE2:25 p=h.x & q=h.y & not x in still_not-bound_in h implies All(x,p) => q is valid; theorem :: CQC_THE2:26 not y in still_not-bound_in p implies All(x,p) => All(y,p) is valid; theorem :: CQC_THE2:27 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; theorem :: CQC_THE2:28 not x in still_not-bound_in p implies Ex(x,p) => Ex(y,p) is valid; theorem :: CQC_THE2:29 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; theorem :: CQC_THE2:30 All(x,p => q) => (All(x,p) => All(x,q)) is valid; theorem :: CQC_THE2:31 All(x,p => q) is valid implies All(x,p) => All(x,q) is valid; theorem :: CQC_THE2:32 All(x,p <=> q) => (All(x,p) <=> All(x,q)) is valid; theorem :: CQC_THE2:33 All(x,p <=> q) is valid implies All(x,p) <=> All(x,q) is valid; theorem :: CQC_THE2:34 All(x,p => q) => (Ex(x,p) => Ex(x,q)) is valid; theorem :: CQC_THE2:35 All(x,p => q) is valid implies Ex(x,p) => Ex(x,q) is valid; theorem :: CQC_THE2:36 All(x,p '&' q) => (All(x,p) '&' All(x,q)) is valid & (All(x,p) '&' All(x,q)) => All(x,p '&' q) is valid; theorem :: CQC_THE2:37 All(x,p '&' q) <=> (All(x,p) '&' All(x,q)) is valid; theorem :: CQC_THE2:38 All(x,p '&' q) is valid iff All(x,p) '&' All(x,q) is valid; theorem :: CQC_THE2:39 (All(x,p) 'or' All(x,q)) => All(x,p 'or' q) is valid; theorem :: CQC_THE2:40 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; theorem :: CQC_THE2:41 Ex(x,p 'or' q) <=> (Ex(x,p) 'or' Ex(x,q)) is valid; theorem :: CQC_THE2:42 Ex(x,p 'or' q) is valid iff Ex(x,p) 'or' Ex(x,q) is valid; theorem :: CQC_THE2:43 Ex(x,p '&' q) => (Ex(x,p) '&' Ex(x,q)) is valid; theorem :: CQC_THE2:44 Ex(x,p '&' q) is valid implies Ex(x,p) '&' Ex(x,q) is valid; theorem :: CQC_THE2:45 All(x,'not' 'not' p) => All(x,p) is valid & All(x,p) => All(x, 'not' 'not' p) is valid; theorem :: CQC_THE2:46 All(x,'not' 'not' p) <=> All(x,p) is valid; theorem :: CQC_THE2:47 Ex(x,'not' 'not' p) => Ex(x,p) is valid & Ex(x,p) => Ex(x,'not' 'not' p) is valid; theorem :: CQC_THE2:48 Ex(x,'not' 'not' p) <=> Ex(x,p) is valid; theorem :: CQC_THE2:49 'not' Ex(x,'not' p) => All(x,p) is valid & All(x,p) => 'not' Ex( x,'not' p) is valid; theorem :: CQC_THE2:50 'not' Ex(x,'not' p) <=> All(x,p) is valid; theorem :: CQC_THE2:51 'not' All(x,p) => Ex(x,'not' p) is valid & Ex(x,'not' p) => 'not' All(x,p) is valid; theorem :: CQC_THE2:52 'not' All(x,p) <=> Ex(x,'not' p) is valid; theorem :: CQC_THE2:53 'not' Ex(x,p) => All(x,'not' p) is valid & All(x,'not' p) => 'not' Ex( x, p ) is valid; theorem :: CQC_THE2:54 All(x,'not' p) <=> 'not' Ex(x,p) is valid; theorem :: CQC_THE2:55 All(x,All(y,p)) => All(y,All(x,p)) is valid & All(x,y,p) => All(y,x,p) is valid; theorem :: CQC_THE2:56 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; theorem :: CQC_THE2:57 Ex(x,Ex(y,p)) => Ex(y,Ex(x,p)) is valid & Ex(x,y,p) => Ex(y,x,p) is valid; theorem :: CQC_THE2:58 p=h.x & q=h.y & not y in still_not-bound_in h implies Ex(x,p) => Ex(x, y,q) is valid; theorem :: CQC_THE2:59 Ex(x,All(y,p)) => All(y,Ex(x,p)) is valid; theorem :: CQC_THE2:60 Ex(x,p <=> p) is valid; theorem :: CQC_THE2:61 Ex(x,p => q) => (All(x,p) => Ex(x,q)) is valid & (All(x,p) => Ex (x,q)) => Ex(x,p => q) is valid; theorem :: CQC_THE2:62 Ex(x,p => q) <=> (All(x,p) => Ex(x,q)) is valid; theorem :: CQC_THE2:63 Ex(x,p => q) is valid iff All(x,p) => Ex(x,q) is valid; theorem :: CQC_THE2:64 All(x,p '&' q) => (p '&' All(x,q)) is valid; theorem :: CQC_THE2:65 All(x,p '&' q) => (All(x,p) '&' q) is valid; theorem :: CQC_THE2:66 not x in still_not-bound_in p implies (p '&' All(x,q)) => All(x, p '&' q) is valid; theorem :: CQC_THE2:67 not x in still_not-bound_in p & p '&' All(x,q) is valid implies All(x, p '&' q ) is valid; theorem :: CQC_THE2:68 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; theorem :: CQC_THE2:69 not x in still_not-bound_in p implies (p 'or' All(x,q)) <=> All( x,p 'or' q) is valid; theorem :: CQC_THE2:70 not x in still_not-bound_in p implies ( p 'or' All(x,q) is valid iff All(x,p 'or' q) is valid); theorem :: CQC_THE2:71 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; theorem :: CQC_THE2:72 not x in still_not-bound_in p implies (p '&' Ex(x,q)) <=> Ex(x,p '&' q) is valid; theorem :: CQC_THE2:73 not x in still_not-bound_in p implies ( p '&' Ex(x,q) is valid iff Ex( x,p '&' q ) is valid ); theorem :: CQC_THE2:74 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; theorem :: CQC_THE2:75 not x in still_not-bound_in p implies (p => All(x,q)) <=> All(x, p => q) is valid; theorem :: CQC_THE2:76 not x in still_not-bound_in p implies ( All(x,p => q) is valid iff p => All(x, q ) is valid ); theorem :: CQC_THE2:77 not x in still_not-bound_in q implies Ex(x,p => q) => (All(x,p) => q) is valid; theorem :: CQC_THE2:78 (All(x,p) => q) => Ex(x,p => q) is valid; theorem :: CQC_THE2:79 not x in still_not-bound_in q implies ( All(x,p) => q is valid iff Ex( x,p => q ) is valid ); theorem :: CQC_THE2:80 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; theorem :: CQC_THE2:81 not x in still_not-bound_in q implies (Ex(x,p) => q) <=> All(x,p => q) is valid; theorem :: CQC_THE2:82 not x in still_not-bound_in q implies ( Ex(x,p) => q is valid iff All( x,p => q) is valid ); theorem :: CQC_THE2:83 not x in still_not-bound_in p implies Ex(x,p => q) => (p => Ex(x ,q)) is valid; theorem :: CQC_THE2:84 (p => Ex(x,q)) => Ex(x,p => q) is valid; theorem :: CQC_THE2:85 not x in still_not-bound_in p implies (p => Ex(x,q)) <=> Ex(x,p => q) is valid; theorem :: CQC_THE2:86 not x in still_not-bound_in p implies ( p => Ex(x,q) is valid iff Ex(x ,p => q ) is valid ); theorem :: CQC_THE2:87 {p} |- p; theorem :: CQC_THE2:88 Cn({p} \/ {q}) = Cn({p '&' q}); theorem :: CQC_THE2:89 {p,q} |- r iff {p '&' q} |- r; theorem :: CQC_THE2:90 X|- p implies X|- All(x,p); theorem :: CQC_THE2:91 not x in still_not-bound_in p implies X|- All(x,p => q) => (p => All(x ,q)); ::\$N Deduction Theorem theorem :: CQC_THE2:92 F is closed & (X \/ {F})|- G implies X |- F => G;