:: Substitution in First-Order Formulas -- Part II. {T}he Construction of
:: First-Order Formulas
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-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 NUMBERS, SUBSET_1, CQC_LANG, QC_LANG1, SUBSTUT1, MCART_1,
MARGREL1, REALSET1, FINSEQ_1, ORDINAL4, XBOOLEAN, CARD_1, ZFMISC_1,
RELAT_1, BVFUNC_2, XBOOLE_0, FUNCT_1, TARSKI, ZF_LANG, FUNCT_4, FUNCOP_1,
CLASSES2, SUBLEMMA, PARTFUN1, CQC_SIM1, ARYTM_3, XXREAL_0, ARYTM_1,
SUBSTUT2, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, ORDINAL1, SUBSET_1, FINSEQ_1,
FUNCT_1, QC_LANG1, QC_LANG2, QC_LANG3, PARTFUN1, NUMBERS, XCMPLX_0,
XXREAL_0, NAT_1, CQC_LANG, FUNCOP_1, RELAT_1, FUNCT_4, FUNCT_2, CQC_SIM1,
DOMAIN_1, MCART_1, SUBSTUT1, SUBLEMMA;
constructors PARTFUN1, DOMAIN_1, XXREAL_0, NAT_1, INT_1, QC_LANG3, CQC_SIM1,
SUBLEMMA, RELSET_1, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
XREAL_0, NAT_1, INT_1, QC_LANG1, CQC_LANG, SUBSTUT1, SUBLEMMA, XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
equalities FUNCOP_1;
expansions TARSKI;
theorems TARSKI, FUNCT_1, XBOOLE_0, XBOOLE_1, CQC_LANG, QC_LANG1, ZFMISC_1,
RELAT_1, QC_LANG3, PARTFUN1, RELSET_1, QC_LANG2, SUBSTUT1, FUNCT_4,
SUBLEMMA, CQC_SIM1, FUNCT_2, NAT_1, INT_1, XREAL_1, XXREAL_0, FUNCOP_1,
CARD_1, XTUPLE_0;
schemes CQC_LANG, NAT_1;
begin :: Further Properties of Substitution
reserve Al for QC-alphabet;
reserve a,b,b1 for object,
i,j,k,n for Nat,
p,q,r,s for Element of CQC-WFF(Al),
x,y,y1 for bound_QC-variable of Al,
P for QC-pred_symbol of k,Al,
l,ll for CQC-variable_list of k,Al,
Sub,Sub1 for CQC_Substitution of Al,
S,S1,S2 for Element of CQC-Sub-WFF(Al),
P1,P2 for Element of QC-pred_symbols(Al);
theorem Th1:
for Sub holds ex S st S`1 = VERUM(Al) & S`2 = Sub
proof
let Sub;
VERUM(Al) = <*[0,0]*> by QC_LANG1:def 14;
then reconsider S = [VERUM(Al),Sub] as Element of QC-Sub-WFF(Al)
by SUBSTUT1:def 16;
take S;
set X = { G where G is Element of QC-Sub-WFF(Al) :
G`1 is Element of CQC-WFF(Al) };
X = CQC-Sub-WFF(Al) by SUBSTUT1:def 39;
then A1: for G being Element of QC-Sub-WFF(Al) holds
G`1 is Element of CQC-WFF(Al) implies G in CQC-Sub-WFF(Al);
S`1 = VERUM(Al);
then reconsider S as Element of CQC-Sub-WFF(Al) by A1;
S`2 = Sub;
hence thesis;
end;
Lm1: for k,l being Nat st P is (QC-pred_symbol of k,Al) & P is (
QC-pred_symbol of l,Al) holds k = l
proof
let k,l be Nat;
assume
A1: P is (QC-pred_symbol of k,Al) & P is (QC-pred_symbol of l,Al);
then P in l-ary_QC-pred_symbols(Al);
then P in {P2 : the_arity_of P2 = l} by QC_LANG1:def 9;
then
A2: ex P2 st P2 = P & the_arity_of P2 = l;
P in k-ary_QC-pred_symbols(Al) by A1;
then P in {P1 : the_arity_of P1 = k} by QC_LANG1:def 9;
then ex P1 st P1 = P & the_arity_of P1 = k;
hence thesis by A2;
end;
theorem Th2:
for Sub holds ex S st S`1 = P!ll & S`2 = Sub
proof
let Sub;
P is QC-pred_symbol of the_arity_of P,Al by QC_LANG3:1;
then k = the_arity_of P by Lm1;
then [<*P*>^ll,Sub] in QC-Sub-WFF(Al) & len ll = the_arity_of P
by CARD_1:def 7,SUBSTUT1:def 16;
then reconsider S = [P!ll,Sub] as Element of QC-Sub-WFF(Al)
by QC_LANG1:def 12;
set X = { G where G is Element of QC-Sub-WFF(Al) :
G`1 is Element of CQC-WFF(Al) };
X = CQC-Sub-WFF(Al) by SUBSTUT1:def 39;
then A1: for G being Element of QC-Sub-WFF(Al) holds
G`1 is Element of CQC-WFF(Al) implies G in CQC-Sub-WFF(Al);
take S;
S`1 = P!ll;
then reconsider S as Element of CQC-Sub-WFF(Al) by A1;
S`2 = Sub;
hence thesis;
end;
theorem
for k,l being Nat st P is (QC-pred_symbol of k,Al) & P is (
QC-pred_symbol of l,Al) holds k = l by Lm1;
theorem Th4:
(for Sub holds ex S st S`1 = p & S`2 = Sub) implies for Sub holds
ex S st S`1 = 'not' p & S`2 = Sub
proof
assume
A1: for Sub holds ex S st S`1 = p & S`2 = Sub;
let Sub;
consider S such that
A2: S`1 = p & S`2 = Sub by A1;
S = [p,Sub] by A2,SUBSTUT1:10;
then [p,Sub] in QC-Sub-WFF(Al);
then [@p,Sub] in QC-Sub-WFF(Al) by QC_LANG1:def 13;
then [<*[1, 0]*>^@p,Sub] in QC-Sub-WFF(Al) by SUBSTUT1:def 16;
then reconsider S = ['not' p,Sub] as Element of QC-Sub-WFF(Al)
by QC_LANG1:def 15;
set X = { G where G is Element of QC-Sub-WFF(Al) :
G`1 is Element of CQC-WFF(Al) };
X = CQC-Sub-WFF(Al) by SUBSTUT1:def 39;
then A3: for G being Element of QC-Sub-WFF(Al) holds
G`1 is Element of CQC-WFF(Al) implies G in CQC-Sub-WFF(Al);
take S;
S`1 = 'not' p;
then reconsider S as Element of CQC-Sub-WFF(Al) by A3;
S`2 = Sub;
hence thesis;
end;
theorem Th5:
(for Sub holds ex S st S`1 = p & S`2 = Sub) & (for Sub holds ex S
st S`1 = q & S`2 = Sub) implies for Sub holds ex S st S`1 = p '&' q & S`2 = Sub
proof
assume that
A1: for Sub holds ex S st S`1 = p & S`2 = Sub and
A2: for Sub holds ex S st S`1 = q & S`2 = Sub;
let Sub;
consider S1 such that
A3: S1`1 = p & S1`2 = Sub by A1;
consider S2 such that
A4: S2`1 = q & S2`2 = Sub by A2;
S2 = [q,Sub] by A4,SUBSTUT1:10;
then [q,Sub] in QC-Sub-WFF(Al);
then
A5: [@q,Sub] in QC-Sub-WFF(Al) by QC_LANG1:def 13;
S1 = [p,Sub] by A3,SUBSTUT1:10;
then [p,Sub] in QC-Sub-WFF(Al);
then [@p,Sub] in QC-Sub-WFF(Al) by QC_LANG1:def 13;
then [<*[2, 0]*>^@p^@q,Sub] in QC-Sub-WFF(Al) by A5,SUBSTUT1:def 16;
then reconsider S = [p '&' q,Sub] as Element of QC-Sub-WFF(Al)
by QC_LANG1:def 16;
set X = { G where G is Element of QC-Sub-WFF(Al) :
G`1 is Element of CQC-WFF(Al) };
X = CQC-Sub-WFF(Al) by SUBSTUT1:def 39;
then A6: for G being Element of QC-Sub-WFF(Al) holds
G`1 is Element of CQC-WFF(Al) implies G in CQC-Sub-WFF(Al);
take S;
S`1 = p '&' q;
then reconsider S as Element of CQC-Sub-WFF(Al) by A6;
S`2 = Sub;
hence thesis;
end;
definition
let Al, p, Sub;
redefine func [p,Sub] -> Element of [:QC-WFF(Al),vSUB(Al):];
coherence by ZFMISC_1:def 2;
end;
theorem Th6:
dom RestrictSub(x,All(x,p),Sub) misses {x}
proof
set finSub = RestrictSub(x,All(x,p),Sub);
now
set q = All(x,p);
set X = {y1 : y1 in still_not-bound_in q & y1 is Element of dom Sub & y1
<> x & y1 <> Sub.y1};
assume dom finSub meets {x};
then consider b being object such that
A1: b in dom finSub and
A2: b in {x} by XBOOLE_0:3;
finSub = Sub|X by SUBSTUT1:def 6;
then finSub = (@Sub)|X by SUBSTUT1:def 2;
then @finSub = (@Sub)|X by SUBSTUT1:def 2;
then dom @finSub = dom @Sub /\ X by RELAT_1:61;
then
A3: dom @finSub c= X by XBOOLE_1:17;
b in dom @finSub by A1,SUBSTUT1:def 2;
then b in X by A3;
then ex y st y = b & y in still_not-bound_in q & y is Element of dom Sub &
y <> x & y <> Sub.y;
hence contradiction by A2,TARSKI:def 1;
end;
hence thesis;
end;
theorem Th7:
x in rng RestrictSub(x,All(x,p),Sub) implies S_Bound([All(x,p),
Sub]) = x.upVar(RestrictSub(x,All(x,p),Sub),p)
proof
set finSub = RestrictSub(x,All(x,p),Sub);
set S = [All(x,p),Sub];
assume
A1: x in rng finSub;
reconsider q = S`1 as Element of CQC-WFF(Al);
A2: S`2 = Sub;
bound_in q = x & the_scope_of q = p by QC_LANG2:7;
hence thesis by A1,A2,SUBSTUT1:def 36;
end;
theorem Th8:
not x in rng RestrictSub(x,All(x,p),Sub) implies S_Bound([All(x,p ),Sub]) = x
proof
set finSub = RestrictSub(x,All(x,p),Sub);
set S = [All(x,p),Sub];
assume
A1: not x in rng finSub;
reconsider q = S`1 as Element of CQC-WFF(Al);
S`2 = Sub & bound_in q = x by QC_LANG2:7;
hence thesis by A1,SUBSTUT1:def 36;
end;
theorem Th9:
ExpandSub(x,p,RestrictSub(x,All(x,p),Sub)) = @RestrictSub(x,All(x
,p),Sub) +* (x|S_Bound([All(x,p),Sub]))
proof
set finSub = RestrictSub(x,All(x,p),Sub);
A1: now
reconsider F = {[x,x.upVar(finSub,p)]} as Function;
dom F = {x} by RELAT_1:9;
then dom finSub misses dom F by Th6;
then dom @finSub misses dom F by SUBSTUT1:def 2;
then
A2: @finSub \/ F = @finSub +* F by FUNCT_4:31;
assume
A3: x in rng finSub;
then ExpandSub(x,p,finSub) = finSub \/ F by SUBSTUT1:def 13;
then {[x,x.upVar(finSub,p)]} = x .--> x.upVar(finSub,p) &
ExpandSub(x,p,finSub) = @finSub +* F by A2,FUNCT_4:82,SUBSTUT1:def 2;
hence thesis by A3,Th7;
end;
now
reconsider F = {[x,x]} as Function;
dom F = {x} by RELAT_1:9;
then dom finSub misses dom F by Th6;
then dom @finSub misses dom F by SUBSTUT1:def 2;
then
A4: @finSub \/ F = @finSub +* F by FUNCT_4:31;
assume
A5: not x in rng finSub;
then ExpandSub(x,p,finSub) = finSub \/ F by SUBSTUT1:def 13;
then {[x,x]} = x .--> x & ExpandSub(x,p,finSub) = @finSub +* F by A4,
FUNCT_4:82,SUBSTUT1:def 2;
hence thesis by A5,Th8;
end;
hence thesis by A1;
end;
theorem Th10:
S`2 = @RestrictSub(x,All(x,p),Sub) +* (x|S_Bound([All(x,p),Sub])
) & S`1 = p implies [S,x] is quantifiable & ex S1 st S1 = [All(x,p),Sub]
proof
set Sub1 = @RestrictSub(x,All(x,p),Sub) +* (x|S_Bound([All(x,p),Sub]));
reconsider Sub as CQC_Substitution of Al;
assume that
A1: S`2 = Sub1 and
A2: S`1 = p;
A3: [S,x]`2 = x & ([S,x]`1)`1 = p by A2;
A4: the_scope_of All(x,p) = p & All(x,p) is universal by QC_LANG1:def 21
,QC_LANG2:7;
Sub1 = ExpandSub(x,p,RestrictSub(x,All(x,p),Sub)) & bound_in All(x,p) =
x by Th9,QC_LANG2:7;
then All(x,p),Sub PQSub Sub1 by A4,SUBSTUT1:def 14;
then consider a such that
A5: a = [[All(x,p),Sub],Sub1] and
A6: All(x,p),Sub PQSub Sub1;
a in QSub(Al) by A5,A6,SUBSTUT1:def 15;
then
A7: (QSub(Al)).[All(x,p),Sub] = Sub1 by A5,FUNCT_1:1;
A8: ([S,x]`1)`2 = Sub1 by A1;
hence [S,x] is quantifiable by A7,A3,SUBSTUT1:def 22;
A9: [S,x] is quantifiable by A7,A8,A3,SUBSTUT1:def 22;
then reconsider Sub as second_Q_comp of [S,x] by A7,A8,A3,SUBSTUT1:def 23;
take S1 = CQCSub_All([S,x],Sub);
S1 = Sub_All([S,x],Sub) by A9,SUBLEMMA:def 5;
hence thesis by A3,A9,SUBSTUT1:def 24;
end;
theorem Th11:
(for Sub holds ex S st S`1 = p & S`2 = Sub) implies for Sub
holds ex S st S`1 = All(x,p) & S`2 = Sub
proof
assume
A1: for Sub holds ex S st S`1 = p & S`2 = Sub;
let Sub;
set Sub1 = @RestrictSub(x,All(x,p),Sub) +* (x|S_Bound([All(x,p),Sub]));
Sub1 is CQC_Substitution of Al iff Sub1 is Element of
PFuncs(bound_QC-variables(Al),bound_QC-variables(Al)) by SUBSTUT1:def 1;
then reconsider Sub1 as CQC_Substitution of Al
by PARTFUN1:45;
ex S st S`1 = p & S`2 = Sub1 by A1;
then consider S1 such that
A2: S1 = [All(x,p),Sub] by Th10;
take S1;
thus thesis by A2;
end;
theorem Th12:
for p, Sub holds ex S st S`1 = p & S`2 = Sub
proof
defpred P[Element of CQC-WFF(Al)] means
for Sub holds ex S st S`1 = $1 & S`2 = Sub;
A1: for p,q,x,k for ll being CQC-variable_list of k,Al for P being
QC-pred_symbol of k,Al holds P[VERUM(Al)] & P[P!ll] &
(P[p] implies P['not' p]) & (P[p] & P[q] implies P[p '&' q]) &
(P[p] implies P[All(x,p)]) by Th1,Th2,Th4,Th5,Th11;
thus for p holds P[p] from CQC_LANG:sch 1(A1);
end;
definition
let Al,p,Sub;
redefine func [p,Sub] -> Element of CQC-Sub-WFF(Al);
coherence
proof
ex S st S`1 = p & S`2 = Sub by Th12;
hence thesis by SUBSTUT1:10;
end;
end;
notation
let Al,x,y;
synonym Sbst(x,y) for x .--> y;
end;
definition
let Al,x,y;
redefine func Sbst(x,y) -> CQC_Substitution of Al;
coherence
proof
A1: x .--> y is CQC_Substitution of Al iff x .--> y is Element of
PFuncs(bound_QC-variables(Al),bound_QC-variables(Al)) by SUBSTUT1:def 1;
dom(x .--> y) = {x} & rng(x .--> y) = {y} by FUNCOP_1:8,13;
then x .--> y is PartFunc of bound_QC-variables(Al),bound_QC-variables(Al)
by RELSET_1:4;
hence thesis by A1,PARTFUN1:45;
end;
end;
begin :: Facts about Substitution and Quantifiers of a Formula
definition
let Al,p,x,y;
func p.(x,y) -> Element of CQC-WFF(Al) equals
CQC_Sub([p,Sbst(x,y)]);
coherence;
end;
scheme
CQCInd1 { Al() -> QC-alphabet, P[set]} :
for p being Element of CQC-WFF(Al()) holds P[p]
provided
A1: for p being Element of CQC-WFF(Al()) st QuantNbr(p) = 0 holds P[p] and
A2: for k st for p being Element of CQC-WFF(Al()) st QuantNbr(p) = k
holds P[p] holds for p being Element of CQC-WFF(Al()) st QuantNbr(p) = k+1
holds P[p]
proof
let p be Element of CQC-WFF(Al());
defpred Q[Nat] means for p being Element of CQC-WFF(Al())
st QuantNbr(p) = $1 holds P[p];
A3: for k being Nat st Q[k] holds Q[k + 1] by A2;
A4: Q[0] by A1;
for k holds Q[k] from NAT_1:sch 2(A4,A3);
then Q[QuantNbr(p)];
hence thesis;
end;
scheme
CQCInd2 {Al() -> QC-alphabet, P[set]}:
for p being Element of CQC-WFF(Al()) holds P[p]
provided
A1: for p being Element of CQC-WFF(Al()) st QuantNbr(p) <= 0 holds P[p] and
A2: for k st for p being Element of CQC-WFF(Al()) st QuantNbr(p) <= k
holds P[p] holds for p being Element of CQC-WFF(Al())
st QuantNbr(p) <= k+1 holds P[p]
proof
let p being Element of CQC-WFF(Al());
defpred Q[Nat] means
for p being Element of CQC-WFF(Al()) st QuantNbr(p) <= $1 holds P[p];
A3: for k st Q[k] holds Q[k + 1] by A2;
A4: Q[0] by A1;
for k holds Q[k] from NAT_1:sch 2(A4,A3);
then Q[QuantNbr(p)];
hence thesis;
end;
theorem
VERUM(Al).(x,y) = VERUM(Al)
proof
set S = [VERUM(Al),Sbst(x,y)];
S is Al-Sub_VERUM by SUBSTUT1:def 19;
hence thesis by SUBLEMMA:3;
end;
theorem
(P!l).(x,y) = P!CQC_Subst(l,Sbst(x,y)) & QuantNbr(P!l) = QuantNbr((P!l
).(x,y))
proof
set S = [P!l,Sbst(x,y)];
S = Sub_P(P,l,Sbst(x,y)) by SUBSTUT1:9;
then
A1: (P!l).(x,y) = P!CQC_Subst(l,Sbst(x,y)) by SUBLEMMA:8;
QuantNbr(P!CQC_Subst(l,Sbst(x,y))) = 0 by CQC_SIM1:15;
hence thesis by A1,CQC_SIM1:15;
end;
theorem Th15:
QuantNbr(P!l) = QuantNbr(CQC_Sub([P!l,Sub]))
proof
set S = [P!l,Sub];
S = Sub_P(P,l,Sub) by SUBSTUT1:9;
then
A1: CQC_Sub([(P!l),Sub]) = P!CQC_Subst(l,Sub) by SUBLEMMA:8;
QuantNbr(P!CQC_Subst(l,Sub)) = 0 by CQC_SIM1:15;
hence thesis by A1,CQC_SIM1:15;
end;
definition
let Al;
let S be Element of QC-Sub-WFF(Al);
redefine func S`2 -> CQC_Substitution of Al;
coherence
proof
ex p being Element of QC-WFF(Al),Sub st S = [p,Sub] by SUBSTUT1:8;
hence thesis;
end;
end;
theorem Th16:
['not' p,Sub] = Sub_not [p,Sub]
proof
set S = [p,Sub];
Sub_not S = ['not' S`1,S`2] by SUBSTUT1:def 20;
hence thesis;
end;
theorem
'not' p.(x,y) = 'not' (p.(x,y)) & (QuantNbr(p) = QuantNbr(p.(x,y))
implies QuantNbr('not' p) = QuantNbr('not' p.(x,y)))
proof
set S = ['not' p,Sbst(x,y)];
A1: S = Sub_not [p,Sbst(x,y)] by Th16;
then
A2: ('not' p).(x,y) = 'not' CQC_Sub([p,Sbst(x,y)]) by SUBSTUT1:29;
QuantNbr(p) = QuantNbr(p.(x,y)) implies QuantNbr('not' p) = QuantNbr((
'not' p).(x,y))
proof
assume
A3: QuantNbr(p) = QuantNbr(p.(x,y));
QuantNbr(('not' p).(x,y)) = QuantNbr(p.(x,y)) by A2,CQC_SIM1:16;
hence thesis by A3,CQC_SIM1:16;
end;
hence thesis by A1,SUBSTUT1:29;
end;
theorem Th18:
(for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]))) implies
for Sub holds QuantNbr('not' p) = QuantNbr(CQC_Sub(['not' p,Sub]))
proof
assume
A1: for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]));
let Sub;
set S = ['not' p,Sub];
S = Sub_not [p,Sub] by Th16;
then QuantNbr(CQC_Sub(S)) = QuantNbr('not' CQC_Sub([p,Sub])) by SUBSTUT1:29
.= QuantNbr(CQC_Sub([p,Sub])) by CQC_SIM1:16
.= QuantNbr(p) by A1;
hence thesis by CQC_SIM1:16;
end;
theorem Th19:
[p '&' q,Sub] = CQCSub_&([p,Sub],[q,Sub])
proof
set S1 = [p,Sub];
set S2 = [q,Sub];
A1: S1`1 = p & S2`1 = q;
A2: S1`2 = Sub & S2`2 = Sub;
then CQCSub_&(S1,S2) = Sub_&(S1,S2) by SUBLEMMA:def 3;
hence thesis by A2,A1,SUBSTUT1:def 21;
end;
theorem
(p '&' q).(x,y) = (p.(x,y)) '&' (q.(x,y)) & ( QuantNbr(p) = QuantNbr(p
.(x,y)) & QuantNbr(q) = QuantNbr(q.(x,y)) implies QuantNbr(p '&'q) = QuantNbr((
p '&' q).(x,y)))
proof
set S = [p '&' q,Sbst(x,y)];
set S1 = [p,Sbst(x,y)];
set S2 = [q,Sbst(x,y)];
A1: S1`2 = Sbst(x,y) & S2`2 = Sbst(x,y);
S = CQCSub_&(S1,S2) by Th19;
then
A2: S = Sub_&(S1,S2) by A1,SUBLEMMA:def 3;
then
A3: (p '&' q).(x,y) = (CQC_Sub(S1)) '&' (CQC_Sub(S2)) by A1,SUBSTUT1:31;
QuantNbr(p) = QuantNbr(p.(x,y)) & QuantNbr(q) = QuantNbr(q.(x,y))
implies QuantNbr(p '&' q) = QuantNbr((p '&' q).(x,y))
proof
assume
A4: QuantNbr(p) = QuantNbr(p.(x,y)) & QuantNbr(q) = QuantNbr(q.(x,y));
QuantNbr((p '&' q).(x,y)) = QuantNbr(p.(x,y)) + QuantNbr(q.(x,y)) by A3,
CQC_SIM1:17;
hence thesis by A4,CQC_SIM1:17;
end;
hence thesis by A1,A2,SUBSTUT1:31;
end;
theorem Th21:
(for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]))) & (for
Sub holds QuantNbr(q) = QuantNbr(CQC_Sub([q,Sub]))) implies for Sub holds
QuantNbr(p '&' q) = QuantNbr(CQC_Sub[p '&' q,Sub])
proof
assume that
A1: for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub])) and
A2: for Sub holds QuantNbr(q) = QuantNbr(CQC_Sub([q,Sub]));
let Sub;
set S = [p '&' q,Sub];
set S1 = [p,Sub];
set S2 = [q,Sub];
A3: S1`2 = Sub & S2`2 = Sub;
S = CQCSub_&(S1,S2) by Th19;
then S = Sub_&(S1,S2) by A3,SUBLEMMA:def 3;
then CQC_Sub(S) = (CQC_Sub(S1)) '&' (CQC_Sub(S2)) by A3,SUBSTUT1:31;
then
QuantNbr(CQC_Sub(S)) = QuantNbr(CQC_Sub(S1)) + QuantNbr(CQC_Sub(S2)) by
CQC_SIM1:17
.= QuantNbr(p) + QuantNbr(CQC_Sub(S2)) by A1
.= QuantNbr(p) + QuantNbr(q) by A2;
hence thesis by CQC_SIM1:17;
end;
definition
let Al;
func CFQ(Al) -> Function of CQC-Sub-WFF(Al),vSUB(Al) equals
(QSub(Al))|CQC-Sub-WFF(Al);
coherence
proof
now
let a be object;
assume a in CQC-Sub-WFF(Al);
then consider p being Element of QC-WFF(Al),Sub such that
A1: a = [p,Sub] by SUBSTUT1:8;
A2: now
set b = {};
assume not p is universal;
then p,Sub PQSub b by SUBSTUT1:def 14;
then [[p,Sub],b] in QSub(Al) by SUBSTUT1:def 15;
hence a in dom QSub(Al) by A1,FUNCT_1:1;
end;
now
set b = ExpandSub(bound_in p,the_scope_of p, RestrictSub(bound_in p,p,
Sub));
assume p is universal;
then p,Sub PQSub b by SUBSTUT1:def 14;
then [[p,Sub],b] in QSub(Al) by SUBSTUT1:def 15;
hence a in dom QSub(Al) by A1,FUNCT_1:1;
end;
hence a in dom QSub(Al) by A2;
end;
then CQC-Sub-WFF(Al) c= dom QSub(Al);
then
A3: dom((QSub(Al))|CQC-Sub-WFF(Al)) = CQC-Sub-WFF(Al) by RELAT_1:62;
rng((QSub(Al))|CQC-Sub-WFF(Al)) c= vSUB(Al)
proof
let b be object;
assume b in rng((QSub(Al))|CQC-Sub-WFF(Al));
then consider a being object such that
A4: a in dom((QSub(Al))|CQC-Sub-WFF(Al)) & ((QSub(Al))|CQC-Sub-WFF(Al)).a = b
by FUNCT_1:def 3;
A5: (QSub(Al))|CQC-Sub-WFF(Al) c= QSub(Al) by RELAT_1:59;
[a,b] in (QSub(Al))|CQC-Sub-WFF(Al) by A4,FUNCT_1:1;
then consider p being Element of QC-WFF(Al),Sub,b1 such that
A6: [a,b] = [[p,Sub],b1] and
A7: p,Sub PQSub b1 by A5,SUBSTUT1:def 15;
A8: now
A9: b1 is CQC_Substitution of Al iff b1 is Element of
PFuncs(bound_QC-variables(Al),bound_QC-variables(Al)) by SUBSTUT1:def 1;
assume not p is universal;
then b1 = {} by A7,SUBSTUT1:def 14;
then b1 is PartFunc of bound_QC-variables(Al),bound_QC-variables(Al) by
RELSET_1:12;
hence b is CQC_Substitution of Al by A9,A6,PARTFUN1:45,XTUPLE_0:1;
end;
now
assume p is universal;
then
b1 = ExpandSub(bound_in p,the_scope_of p, RestrictSub(bound_in p,
p,Sub)) by A7,SUBSTUT1:def 14;
hence b is CQC_Substitution of Al by A6,XTUPLE_0:1;
end;
hence thesis by A8;
end;
hence thesis by A3,FUNCT_2:2;
end;
end;
definition
let Al,p,x,Sub;
func QScope(p,x,Sub) -> CQC-WFF-like Element of [:QC-Sub-WFF(Al),
bound_QC-variables(Al):] equals
[[p,(CFQ(Al)).[All(x,p),Sub]],x];
coherence;
end;
definition
let Al,p,x,Sub;
func Qsc(p,x,Sub) -> second_Q_comp of QScope(p,x,Sub) equals
Sub;
coherence
proof
A1: (QScope(p,x,Sub)`1)`2 = (QSub(Al)).[All(x,p),Sub] by FUNCT_1:49;
A2: QScope(p,x,Sub)`2 = x & (QScope(p,x,Sub)`1)`1 = p;
then QScope(p,x,Sub) is quantifiable by A1,SUBSTUT1:def 22;
hence thesis by A2,A1,SUBSTUT1:def 23;
end;
end;
theorem Th22:
[All(x,p),Sub] = CQCSub_All(QScope(p,x,Sub),Qsc(p,x,Sub)) &
QScope(p,x,Sub) is quantifiable
proof
set S = [p,(CFQ(Al)).[All(x,p),Sub]];
set B = [[p,(CFQ(Al)).[All(x,p),Sub]],x];
A1: B`2 = x & (B`1)`1 = p;
[All(x,p),Sub] in CQC-Sub-WFF(Al);
then
A2: [All(x,p),Sub] in dom CFQ(Al) by FUNCT_2:def 1;
(B`1)`2 = (QSub(Al)).[All(B`2,(B`1)`1),Sub] by A2,FUNCT_1:47;
then
A3: B is quantifiable by SUBSTUT1:def 22;
then
CQCSub_All(QScope(p,x,Sub),Qsc(p,x,Sub)) = Sub_All(QScope(p,x,Sub),Qsc(p
,x,Sub)) by SUBLEMMA:def 5;
hence thesis by A1,A3,SUBSTUT1:def 24;
end;
theorem Th23:
(for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]))) implies
for Sub holds QuantNbr(All(x,p)) = QuantNbr(CQC_Sub([All(x,p),Sub]))
proof
assume
A1: for Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]));
let Sub;
set S1 = [All(x,p),Sub];
set S = [p,(CFQ(Al)).[All(x,p),Sub]];
set y = S_Bound(@CQCSub_All(QScope(p,x,Sub),Qsc(p,x,Sub)));
A2: QScope(p,x,Sub) is quantifiable by Th22;
A3: Sub_All(QScope(p,x,Sub),Qsc(p,x,Sub)) = CQCSub_All(QScope(p,x,Sub),Qsc(p
,x,Sub)) by Th22,SUBLEMMA:def 5
.= S1 by Th22;
then
A4: S1 is Sub_universal by A2,SUBSTUT1:def 28;
then
A5: CQC_Sub(S1) = CQCQuant(S1,CQC_Sub(CQCSub_the_scope_of S1)) by SUBLEMMA:28;
CQCSub_the_scope_of S1 = Sub_the_scope_of Sub_All(QScope(p,x,Sub),Qsc(p,
x,Sub)) by A3,A4,SUBLEMMA:def 6
.= [S,x]`1 by A2,SUBSTUT1:21
.= S;
then
CQC_Sub(S1) = CQCQuant(CQCSub_All(QScope(p,x,Sub), Qsc(p,x,Sub)),CQC_Sub
(S)) by A5,Th22;
then QuantNbr(CQC_Sub(S1)) = QuantNbr(All(y,CQC_Sub(S))) by Th22,SUBLEMMA:31
.= QuantNbr(CQC_Sub(S))+1 by CQC_SIM1:18
.= QuantNbr(p)+1 by A1;
hence thesis by CQC_SIM1:18;
end;
theorem Th24:
QuantNbr(VERUM(Al)) = QuantNbr(CQC_Sub([VERUM(Al),Sub]))
proof
[VERUM(Al),Sub] is Al-Sub_VERUM by SUBSTUT1:def 19;
hence thesis by SUBLEMMA:3;
end;
theorem
for p, Sub holds QuantNbr(p) = QuantNbr(CQC_Sub([p,Sub]))
proof
defpred P[Element of CQC-WFF(Al)] means for Sub holds
QuantNbr($1) = QuantNbr(CQC_Sub([$1,Sub]));
A1: for r,s,x,k for l being CQC-variable_list of k,Al for P being
QC-pred_symbol of k,Al holds P[VERUM(Al)] & P[P!l] & (P[r]
implies P['not' r]) & (P[r] & P[s] implies P[r '&' s]) & (P[r]
implies P[All(x, r)]) by Th15,Th18,Th21,Th23,Th24;
thus for r holds P[r] from CQC_LANG:sch 1(A1);
end;
theorem
p is atomic implies ex k,P,ll st p = P!ll
proof
assume p is atomic;
then consider k being Nat, P being (QC-pred_symbol of k,Al),
l being QC-variable_list of k,Al such that
A1: p = P!l by QC_LANG1:def 18;
A2: { l.j : 1 <= j & j <= len l & l.j in fixed_QC-variables(Al) } = {} by A1,
CQC_LANG:7;
{ l.i : 1 <= i & i <= len l & l.i in free_QC-variables(Al) } = {} by A1,
CQC_LANG:7;
then reconsider l as CQC-variable_list of k,Al by A2,CQC_LANG:5;
take k,P,l;
thus thesis by A1;
end;
scheme
CQCInd3 {Al() -> QC-alphabet, P[set]} :
for p being Element of CQC-WFF(Al()) st QuantNbr(p) = 0 holds P[p]
provided
A1: for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k,Al()
for P being QC-pred_symbol of k,Al()
holds P[VERUM(Al())] & P[P!l] &
(P[r] implies P['not' r]) & (P[r] & P[s] implies P[r '&' s])
proof
defpred Prop[Element of CQC-WFF(Al())] means QuantNbr($1) = 0 implies P[$1];
A2: for x being bound_QC-variable of Al(), p being Element of CQC-WFF(Al())
st Prop[p] holds Prop[All(x, p)]
proof
let x be bound_QC-variable of Al(), p be Element of CQC-WFF(Al()) such that
Prop[p];
assume QuantNbr(All(x,p)) = 0;
then QuantNbr(p)+1 = 0 by CQC_SIM1:18;
hence thesis;
end;
for p,q being Element of CQC-WFF(Al())
st Prop[p] & Prop[q] holds Prop[p '&' q]
proof
let p,q be Element of CQC-WFF(Al()) such that
A3: Prop[p] & Prop[q];
assume QuantNbr(p '&' q) = 0;
then QuantNbr(p) + QuantNbr(q) = 0 by CQC_SIM1:17;
hence thesis by A1,A3;
end;
then
A4: for r,s being Element of CQC-WFF(Al())
for x being bound_QC-variable of Al()
for k
for l being CQC-variable_list of k,Al()
for P being QC-pred_symbol of k,Al()
holds Prop[VERUM(Al())] & Prop[P!l] &
(Prop[r] implies Prop['not' r]) & (Prop[r] & Prop[s] implies Prop[r '&' s])&
(Prop[r] implies Prop[All(x,r)]) by A1,A2,CQC_SIM1:16;
for p being Element of CQC-WFF(Al()) holds Prop[p] from CQC_LANG:sch 1(A4);
hence thesis;
end;
begin :: Results about the Construction of Formulas
reserve F1,F2,F3 for QC-formula of Al,
L for FinSequence;
definition
let Al;
let G,H be QC-formula of Al;
assume
A1: G is_subformula_of H;
mode PATH of G,H -> FinSequence means
:Def5:
1 <= len it & it.1 = G & it.(
len it) = H & for k st 1 <= k & k < len it ex G1,H1
being Element of QC-WFF(Al) st it.k = G1 & it.(k+1) = H1 &
G1 is_immediate_constituent_of H1;
existence
proof
ex n,L st 1 <= n & len L = n & L.1 = G & L.n = H & for k st 1 <= k & k
< n ex G1,H1 being Element of QC-WFF(Al) st L.k = G1 & L.(k+1) = H1 & G1
is_immediate_constituent_of H1 by A1,QC_LANG2:def 20;
then consider L such that
A2: ex n st 1 <= n & len L = n & L.1 = G & L.n = H & for k st 1 <= k &
k < n ex G1,H1 being Element of QC-WFF(Al) st L.k = G1 & L.(k+1) = H1 & G1
is_immediate_constituent_of H1;
take L;
thus thesis by A2;
end;
end;
theorem
for L being PATH of F1,F2 st F1 is_subformula_of F2 & 1 <= i & i <=
len L holds ex F3 st F3 = L.i & F3 is_subformula_of F2
proof
let L be PATH of F1,F2;
set n = len L;
assume that
A1: F1 is_subformula_of F2 and
A2: 1 <= i and
A3: i <= n;
n+1 <= n+i by A2,XREAL_1:6;
then n+1+(-1) <= n+i+(-1) by XREAL_1:6;
then
A4: n+(-i) <= n-1+i+(-i) by XREAL_1:6;
i+(-i) <= n+(-i) by A3,XREAL_1:6;
then reconsider l = n-i as Element of NAT by INT_1:3;
defpred P[Nat] means $1 <= n-1 implies ex F3 st F3 = L.(n-$1) &
F3 is_subformula_of F2;
A5: for k st P[k] holds P[k+1]
proof
let k such that
A6: P[k];
assume
A7: k+1 <= n-1;
then k+1+1 <= n-1+1 by XREAL_1:6;
then
A8: 2+k+(-k) <= n+(-k) by XREAL_1:6;
then reconsider j = n-k as Element of NAT by INT_1:3;
n <= n+k by NAT_1:11;
then n+(-k) <= n+k+(-k) by XREAL_1:6;
then
A9: j-1 < n by XREAL_1:146,XXREAL_0:2;
A10: 1+1+(-1) <= j+(-1) by A8,XREAL_1:6;
then reconsider j1 = j-1 as Element of NAT by INT_1:3;
j1+1 = j;
then
A11: ex G1,H1 being Element of QC-WFF(Al) st L.j1 = G1 & L.j = H1 & G1
is_immediate_constituent_of H1 by A1,A10,A9,Def5;
then reconsider F3 = L.j1 as QC-formula of Al;
take F3;
k < k+1 by NAT_1:13;
then F3 is_proper_subformula_of F2 by A6,A7,A11,QC_LANG2:63,XXREAL_0:2;
hence thesis by QC_LANG2:def 21;
end;
L.n = F2 by A1,Def5;
then
A12: P[0];
for k holds P[k] from NAT_1:sch 2(A12,A5);
then ex F3 st F3 = L.(n-l) & F3 is_subformula_of F2 by A4;
hence thesis;
end;
theorem Th28:
for L being PATH of F1,p st F1 is_subformula_of p & 1 <= i & i
<= len L holds L.i is Element of CQC-WFF(Al)
proof
let L be PATH of F1,p;
set n = len L;
assume that
A1: F1 is_subformula_of p and
A2: 1 <= i and
A3: i <= n;
n+1 <= n+i by A2,XREAL_1:6;
then n+1+(-1) <= n+i+(-1) by XREAL_1:6;
then
A4: n+(-i) <= n-1+i+(-i) by XREAL_1:6;
i+(-i) <= n+(-i) by A3,XREAL_1:6;
then reconsider l = n-i as Element of NAT by INT_1:3;
defpred P[Nat] means $1 <= n-1 implies L.(n-$1) is Element of
CQC-WFF(Al);
A5: for k st P[k] holds P[k+1]
proof
let k such that
A6: P[k];
assume
A7: k+1 <= n-1;
then k+1+1 <= n-1+1 by XREAL_1:6;
then
A8: 2+k+(-k) <= n+(-k) by XREAL_1:6;
then reconsider j = n-k as Element of NAT by INT_1:3;
k < k+1 by NAT_1:13;
then reconsider q = L.j as Element of CQC-WFF(Al) by A6,A7,XXREAL_0:2;
n <= n+k by NAT_1:11;
then n+(-k) <= n+k+(-k) by XREAL_1:6;
then
A9: j-1 < n by XREAL_1:146,XXREAL_0:2;
A10: 1+1+(-1) <= j+(-1) by A8,XREAL_1:6;
then reconsider j1 = j-1 as Element of NAT by INT_1:3;
j1+1 = j;
then consider G1,H1 being Element of QC-WFF(Al) such that
A11: L.j1 = G1 and
A12: q = H1 & G1 is_immediate_constituent_of H1 by A1,A10,A9,Def5;
A13: (ex F being Element of QC-WFF(Al) st q = G1 '&' F) implies thesis by A11,
CQC_LANG:9;
A14: (ex x st q = All(x,G1)) implies thesis by A11,CQC_LANG:13;
A15: (ex F being Element of QC-WFF(Al) st q = F '&' G1) implies thesis by A11,
CQC_LANG:9;
q = 'not' G1 implies thesis by A11,CQC_LANG:8;
hence thesis by A12,A13,A15,A14,QC_LANG2:def 19;
end;
A16: P[0] by A1,Def5;
for k holds P[k] from NAT_1:sch 2(A16,A5);
then L.(n-l) is Element of CQC-WFF(Al) by A4;
hence thesis;
end;
theorem Th29:
for L being PATH of q,p st QuantNbr(p) <= n & q is_subformula_of
p & 1 <= i & i <= len L holds ex r st r = L.i & QuantNbr(r) <= n
proof
let L be PATH of q,p;
set m = len L;
assume that
A1: QuantNbr(p) <= n and
A2: q is_subformula_of p and
A3: 1 <= i and
A4: i <= m;
i+(-i) <= m+(-i) by A4,XREAL_1:6;
then reconsider l = m-i as Element of NAT by INT_1:3;
m+1 <= m+i by A3,XREAL_1:6;
then m+1+(-1) <= m+i+(-1) by XREAL_1:6;
then
A5: m+(-i) <= m-1+i+(-i) by XREAL_1:6;
defpred P[Nat] means $1 <= m-1 implies ex r st r = L.(m-$1) &
QuantNbr(r) <= n;
A6: for k st P[k] holds P[k+1]
proof
let k such that
A7: P[k];
assume
A8: k+1 <= m-1;
then k+1+1 <= m-1+1 by XREAL_1:6;
then
A9: 2+k+(-k) <= m+(-k) by XREAL_1:6;
then reconsider j = m-k as Element of NAT by INT_1:3;
A10: 1+1+(-1) <= j+(-1) by A9,XREAL_1:6;
then reconsider j1 = j-1 as Element of NAT by INT_1:3;
m <= m+k by NAT_1:11;
then m+(-k) <= m+k+(-k) by XREAL_1:6;
then
A11: j-1 < m by XREAL_1:146,XXREAL_0:2;
j1+1 = j;
then consider G1,H1 being Element of QC-WFF(Al) such that
A12: L.j1 = G1 and
A13: L.j = H1 & G1 is_immediate_constituent_of H1 by A2,A10,A11,Def5;
reconsider r = G1 as Element of CQC-WFF(Al) by A2,A10,A11,A12,Th28;
k < k+1 by NAT_1:13;
then consider q such that
A14: q = L.j and
A15: QuantNbr(q) <= n by A7,A8,XXREAL_0:2;
A16: now
given x such that
A17: q = All(x,G1);
take r;
QuantNbr(r)+1 <= n by A15,A17,CQC_SIM1:18;
then QuantNbr(r) <= n by NAT_1:13;
hence thesis by A12;
end;
A18: now
given F being Element of QC-WFF(Al) such that
A19: q = F '&' G1;
reconsider F as Element of CQC-WFF(Al) by A19,CQC_LANG:9;
take r;
n <= n+QuantNbr(F) by NAT_1:11;
then
A20: n+(-QuantNbr(F)) <= n+QuantNbr(F)+(-QuantNbr(F)) by XREAL_1:6;
QuantNbr(r) + QuantNbr(F) <= n by A15,A19,CQC_SIM1:17;
then QuantNbr(r) + QuantNbr(F)+(-QuantNbr(F)) <= n +(-QuantNbr(F)) by
XREAL_1:6;
hence thesis by A12,A20,XXREAL_0:2;
end;
A21: now
given F being Element of QC-WFF(Al) such that
A22: q = G1 '&' F;
reconsider F as Element of CQC-WFF(Al) by A22,CQC_LANG:9;
take r;
n <= n+QuantNbr(F) by NAT_1:11;
then
A23: n+(-QuantNbr(F)) <= n+QuantNbr(F)+(-QuantNbr(F)) by XREAL_1:6;
QuantNbr(r) + QuantNbr(F) <= n by A15,A22,CQC_SIM1:17;
then QuantNbr(r) + QuantNbr(F)+(-QuantNbr(F)) <= n +(-QuantNbr(F)) by
XREAL_1:6;
hence thesis by A12,A23,XXREAL_0:2;
end;
now
assume
A24: q = 'not' G1;
take r;
QuantNbr(r) <= n by A15,A24,CQC_SIM1:16;
hence thesis by A12;
end;
hence thesis by A14,A13,A21,A18,A16,QC_LANG2:def 19;
end;
L.m = p by A2,Def5;
then
A25: P[0] by A1;
for k holds P[k] from NAT_1:sch 2(A25,A6);
then ex r st r = L.(m-l) & QuantNbr(r) <= n by A5;
hence thesis;
end;
theorem
QuantNbr(p) = n & q is_subformula_of p implies QuantNbr(q) <= n
proof
set L =the PATH of q,p;
set m = len L;
assume that
A1: QuantNbr(p) = n and
A2: q is_subformula_of p;
1 <= m by A2,Def5;
then ex r st r = L.1 & QuantNbr(r) <= n by A1,A2,Th29;
hence thesis by A2,Def5;
end;
theorem
for n,p st (for q st q is_subformula_of p holds QuantNbr(q) = n) holds n = 0
proof
let n,p such that
A1: for q st q is_subformula_of p holds QuantNbr(q) = n;
defpred P[Element of CQC-WFF(Al)] means
$1 is_subformula_of p implies QuantNbr($1) = 0;
A2: for x, r st P[r] holds P[All(x, r)]
proof
let x,r such that
P[r];
now
assume
A3: All(x, r) is_subformula_of p;
r is_immediate_constituent_of All(x,r) by QC_LANG2:46;
then r is_proper_subformula_of p by A3,QC_LANG2:63;
then r is_subformula_of p by QC_LANG2:def 21;
then
A4: QuantNbr(r) = n by A1;
QuantNbr(All(x,r)) = n by A1,A3;
then n+(-n) = 1+n+(-n) by A4,CQC_SIM1:18;
hence contradiction;
end;
hence thesis;
end;
A5: for r,s st P[r] & P[s] holds P[r '&' s]
proof
let r,s such that
A6: ( P[r])& P[s];
assume
A7: r '&' s is_subformula_of p;
s is_immediate_constituent_of r '&' s by QC_LANG2:45;
then
A8: s is_proper_subformula_of p by A7,QC_LANG2:63;
r is_immediate_constituent_of r '&' s by QC_LANG2:45;
then r is_proper_subformula_of p by A7,QC_LANG2:63;
then QuantNbr(r '&' s) = 0+0 by A6,A8,CQC_SIM1:17,QC_LANG2:def 21;
hence thesis;
end;
for r st P[r] holds P['not' r]
proof
let r such that
A9: P[r];
A10: r is_immediate_constituent_of 'not' r by QC_LANG2:43;
assume 'not' r is_subformula_of p;
then r is_proper_subformula_of p by A10,QC_LANG2:63;
hence thesis by A9,CQC_SIM1:16,QC_LANG2:def 21;
end;
then
A11: for r,s,x,k for l being CQC-variable_list of k,Al for P being
QC-pred_symbol of k,Al holds P[VERUM(Al)] & P[P!l] &
(P[r] implies P['not' r]) & (P[r] & P[s] implies P[r '&' s]) &
(P[r] implies P[All(x, r)]) by A5,A2,CQC_SIM1:14,15;
A12: for r holds P[r] from CQC_LANG:sch 1(A11);
QuantNbr(p) = n by A1;
hence thesis by A12;
end;
theorem
for p st (for q st q is_subformula_of p holds for x,r holds q <> All(x
,r)) holds QuantNbr(p) = 0
proof
let p such that
A1: for q st q is_subformula_of p holds for x,r holds q <> All(x,r);
defpred P[Element of CQC-WFF(Al)] means $1 is_subformula_of p
implies QuantNbr($1) = 0;
A2: for r,s st P[r] & P[s] holds P[r '&' s]
proof
let r,s such that
A3: ( P[r])& P[s];
assume
A4: r '&' s is_subformula_of p;
s is_immediate_constituent_of r '&' s by QC_LANG2:45;
then
A5: s is_proper_subformula_of p by A4,QC_LANG2:63;
r is_immediate_constituent_of r '&' s by QC_LANG2:45;
then r is_proper_subformula_of p by A4,QC_LANG2:63;
then QuantNbr(r '&' s) = 0+0 by A3,A5,CQC_SIM1:17,QC_LANG2:def 21;
hence thesis;
end;
for r st P[r] holds P['not' r]
proof
let r such that
A6: P[r];
A7: r is_immediate_constituent_of 'not' r by QC_LANG2:43;
assume 'not' r is_subformula_of p;
then r is_proper_subformula_of p by A7,QC_LANG2:63;
hence thesis by A6,CQC_SIM1:16,QC_LANG2:def 21;
end;
then
A8: for r,s,x,k for l being CQC-variable_list of k,Al for P being
QC-pred_symbol of k,Al holds P[VERUM(Al)] & P[P!l] &
(P[r] implies P['not' r]) & (P[r] & P[s] implies P[r '&' s]) &
(P[r] implies P[All(x, r)]) by A1,A2,CQC_SIM1:14,15;
for r holds P[r] from CQC_LANG:sch 1(A8);
hence thesis;
end;
theorem Th33:
for p st for q st q is_subformula_of p holds QuantNbr(q) <> 1
holds QuantNbr(p) = 0
proof
let p such that
A1: for q st q is_subformula_of p holds QuantNbr(q) <> 1;
defpred P[Element of CQC-WFF(Al)] means $1 is_subformula_of p
implies QuantNbr($1) = 0;
A2: for x, r st P[r] holds P[All(x, r)]
proof
let x,r such that
A3: P[r];
now
assume
A4: All(x, r) is_subformula_of p;
r is_immediate_constituent_of All(x,r) by QC_LANG2:46;
then r is_proper_subformula_of p by A4,QC_LANG2:63;
then QuantNbr(All(x,r)) = 0+1 by A3,CQC_SIM1:18,QC_LANG2:def 21;
hence contradiction by A1,A4;
end;
hence thesis;
end;
A5: for r,s st P[r] & P[s] holds P[r '&' s]
proof
let r,s such that
A6: ( P[r])& P[s];
assume
A7: r '&' s is_subformula_of p;
s is_immediate_constituent_of r '&' s by QC_LANG2:45;
then
A8: s is_proper_subformula_of p by A7,QC_LANG2:63;
r is_immediate_constituent_of r '&' s by QC_LANG2:45;
then r is_proper_subformula_of p by A7,QC_LANG2:63;
then QuantNbr(r '&' s) = 0+0 by A6,A8,CQC_SIM1:17,QC_LANG2:def 21;
hence thesis;
end;
for r st P[r] holds P['not' r]
proof
let r such that
A9: P[r];
A10: r is_immediate_constituent_of 'not' r by QC_LANG2:43;
assume 'not' r is_subformula_of p;
then r is_proper_subformula_of p by A10,QC_LANG2:63;
hence thesis by A9,CQC_SIM1:16,QC_LANG2:def 21;
end;
then
A11: for r,s,x,k for l being CQC-variable_list of k,Al for P being
QC-pred_symbol of k,Al holds P[VERUM(Al)] & P[P!l] &
(P[r] implies P['not' r]) & (P[r] & P[s] implies P[r '&' s]) &
(P[r] implies P[All(x, r)]) by A5,A2,CQC_SIM1:14,15;
for r holds P[r] from CQC_LANG:sch 1(A11);
hence thesis;
end;
theorem
1 <= QuantNbr(p) implies ex q st q is_subformula_of p & QuantNbr(q)=1
by Th33;