:: Calculus of Quantifiers. Deduction Theorem
:: by Agata Darmochwa\l
::
:: Received October 24, 1990
:: Copyright (c) 1990-2016 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;