begin
theorem Th1:
theorem Th2:
:: deftheorem SUBLEMMA:def 1 :
canceled;
:: deftheorem defines Val_S SUBLEMMA:def 2 :
for S being Element of CQC-Sub-WFF
for A being non empty set
for v being Element of Valuations_in A holds Val_S (v,S) = (@ (S `2)) * v;
theorem Th3:
:: deftheorem Def3 defines |= SUBLEMMA:def 3 :
for S being Element of CQC-Sub-WFF
for A being non empty set
for v being Element of Valuations_in A
for J being interpretation of A holds
( J,v |= S iff J,v |= S `1 );
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem
canceled;
theorem Th9:
theorem
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
:: deftheorem Def4 defines CQCSub_& SUBLEMMA:def 4 :
for S1, S2 being Element of CQC-Sub-WFF st S1 `2 = S2 `2 holds
CQCSub_& (S1,S2) = Sub_& (S1,S2);
theorem Th21:
theorem Th22:
theorem
theorem Th24:
theorem Th25:
theorem Th26:
for
A being non
empty set for
J being
interpretation of
A for
S1,
S2 being
Element of
CQC-Sub-WFF st
S1 `2 = S2 `2 & ( for
v being
Element of
Valuations_in A holds
(
J,
v |= CQC_Sub S1 iff
J,
v . (Val_S (v,S1)) |= S1 ) ) & ( for
v being
Element of
Valuations_in A holds
(
J,
v |= CQC_Sub S2 iff
J,
v . (Val_S (v,S2)) |= S2 ) ) holds
for
v being
Element of
Valuations_in A holds
(
J,
v |= CQC_Sub (CQCSub_& (S1,S2)) iff
J,
v . (Val_S (v,(CQCSub_& (S1,S2)))) |= CQCSub_& (
S1,
S2) )
theorem Th27:
:: deftheorem Def5 defines CQC-WFF-like SUBLEMMA:def 5 :
for B being Element of [:QC-Sub-WFF,bound_QC-variables:] holds
( B is CQC-WFF-like iff B `1 in CQC-Sub-WFF );
:: deftheorem Def6 defines CQCSub_All SUBLEMMA:def 6 :
for B being CQC-WFF-like Element of [:QC-Sub-WFF,bound_QC-variables:]
for SQ being second_Q_comp of B st B is quantifiable holds
CQCSub_All (B,SQ) = Sub_All (B,SQ);
theorem Th28:
:: deftheorem Def7 defines CQCSub_the_scope_of SUBLEMMA:def 7 :
for S being Element of CQC-Sub-WFF st S is Sub_universal holds
CQCSub_the_scope_of S = Sub_the_scope_of S;
:: deftheorem Def8 defines CQCQuant SUBLEMMA:def 8 :
for S1 being Element of CQC-Sub-WFF
for p being Element of CQC-WFF st S1 is Sub_universal & p = CQC_Sub (CQCSub_the_scope_of S1) holds
CQCQuant (S1,p) = Quant (S1,p);
theorem Th29:
theorem Th30:
begin
theorem Th31:
for
x being
bound_QC-variable for
S being
Element of
CQC-Sub-WFF for
xSQ being
second_Q_comp of
[S,x] st
[S,x] is
quantifiable holds
(
CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ)) = S &
CQCQuant (
(CQCSub_All ([S,x],xSQ)),
(CQC_Sub (CQCSub_the_scope_of (CQCSub_All ([S,x],xSQ)))))
= CQCQuant (
(CQCSub_All ([S,x],xSQ)),
(CQC_Sub S)) )
theorem Th32:
theorem
theorem
theorem Th35:
theorem Th36:
theorem Th37:
theorem
theorem Th39:
for
x being
bound_QC-variable for
S being
Element of
CQC-Sub-WFF for
xSQ being
second_Q_comp of
[S,x] st
[S,x] is
quantifiable &
x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) holds
( not
S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) & not
S_Bound (@ (CQCSub_All ([S,x],xSQ))) in Bound_Vars (S `1) )
theorem Th40:
for
x being
bound_QC-variable for
S being
Element of
CQC-Sub-WFF for
xSQ being
second_Q_comp of
[S,x] st
[S,x] is
quantifiable & not
x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) holds
not
S_Bound (@ (CQCSub_All ([S,x],xSQ))) in rng (RestrictSub (x,(All (x,(S `1))),xSQ))
theorem Th41:
theorem Th42:
theorem
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
definition
let S be
Element of
CQC-Sub-WFF ;
let x be
bound_QC-variable;
let xSQ be
second_Q_comp of
[S,x];
let A be non
empty set ;
let v be
Element of
Valuations_in A;
func NEx_Val (
v,
S,
x,
xSQ)
-> Val_Sub of
A equals
(@ (RestrictSub (x,(All (x,(S `1))),xSQ))) * v;
coherence
(@ (RestrictSub (x,(All (x,(S `1))),xSQ))) * v is Val_Sub of A
;
end;
:: deftheorem defines NEx_Val SUBLEMMA:def 9 :
for S being Element of CQC-Sub-WFF
for x being bound_QC-variable
for xSQ being second_Q_comp of [S,x]
for A being non empty set
for v being Element of Valuations_in A holds NEx_Val (v,S,x,xSQ) = (@ (RestrictSub (x,(All (x,(S `1))),xSQ))) * v;
theorem Th52:
for
x being
bound_QC-variable for
S being
Element of
CQC-Sub-WFF for
xSQ being
second_Q_comp of
[S,x] st
[S,x] is
quantifiable &
x in rng (RestrictSub (x,(All (x,(S `1))),xSQ)) holds
S_Bound (@ (CQCSub_All ([S,x],xSQ))) = x. (upVar ((RestrictSub (x,(All (x,(S `1))),xSQ)),(S `1)))
theorem Th53:
theorem Th54:
for
x being
bound_QC-variable for
A being non
empty set for
v being
Element of
Valuations_in A for
S being
Element of
CQC-Sub-WFF for
xSQ being
second_Q_comp of
[S,x] st
[S,x] is
quantifiable holds
for
a being
Element of
A holds
(
Val_S (
(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),
S)
= (NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) +* (x | a) &
dom (RestrictSub (x,(All (x,(S `1))),xSQ)) misses {x} )
theorem Th55:
for
x being
bound_QC-variable for
A being non
empty set for
J being
interpretation of
A for
v being
Element of
Valuations_in A for
S being
Element of
CQC-Sub-WFF for
xSQ being
second_Q_comp of
[S,x] st
[S,x] is
quantifiable holds
( ( for
a being
Element of
A holds
J,
(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . (Val_S ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S)) |= S ) iff for
a being
Element of
A holds
J,
(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) +* (x | a)) |= S )
theorem Th56:
for
x being
bound_QC-variable for
A being non
empty set for
v being
Element of
Valuations_in A for
S being
Element of
CQC-Sub-WFF for
xSQ being
second_Q_comp of
[S,x] st
[S,x] is
quantifiable holds
for
a being
Element of
A holds
NEx_Val (
(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),
S,
x,
xSQ)
= NEx_Val (
v,
S,
x,
xSQ)
theorem Th57:
for
x being
bound_QC-variable for
A being non
empty set for
J being
interpretation of
A for
v being
Element of
Valuations_in A for
S being
Element of
CQC-Sub-WFF for
xSQ being
second_Q_comp of
[S,x] st
[S,x] is
quantifiable holds
( ( for
a being
Element of
A holds
J,
(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val ((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)),S,x,xSQ)) +* (x | a)) |= S ) iff for
a being
Element of
A holds
J,
(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a)) |= S )
begin
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
for
p,
q being
Element of
CQC-WFF for
A being non
empty set for
J being
interpretation of
A st ( for
v,
w being
Element of
Valuations_in A st
v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
(
J,
v |= p iff
J,
w |= p ) ) & ( for
v,
w being
Element of
Valuations_in A st
v | (still_not-bound_in q) = w | (still_not-bound_in q) holds
(
J,
v |= q iff
J,
w |= q ) ) holds
for
v,
w being
Element of
Valuations_in A st
v | (still_not-bound_in (p '&' q)) = w | (still_not-bound_in (p '&' q)) holds
(
J,
v |= p '&' q iff
J,
w |= p '&' q )
theorem Th64:
theorem
theorem
theorem Th67:
theorem Th68:
for
p being
Element of
CQC-WFF for
x being
bound_QC-variable for
A being non
empty set for
J being
interpretation of
A st ( for
v,
w being
Element of
Valuations_in A st
v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
(
J,
v |= p iff
J,
w |= p ) ) holds
for
v,
w being
Element of
Valuations_in A st
v | (still_not-bound_in (All (x,p))) = w | (still_not-bound_in (All (x,p))) holds
(
J,
v |= All (
x,
p) iff
J,
w |= All (
x,
p) )
theorem
canceled;
theorem Th70:
theorem Th71:
for
x being
bound_QC-variable for
A being non
empty set for
v being
Element of
Valuations_in A for
S being
Element of
CQC-Sub-WFF for
xSQ being
second_Q_comp of
[S,x] for
a being
Element of
A st
[S,x] is
quantifiable holds
((v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1)) = (v . ((NEx_Val (v,S,x,xSQ)) +* (x | a))) | (still_not-bound_in (S `1))
theorem Th72:
for
x being
bound_QC-variable for
A being non
empty set for
J being
interpretation of
A for
v being
Element of
Valuations_in A for
S being
Element of
CQC-Sub-WFF for
xSQ being
second_Q_comp of
[S,x] st
[S,x] is
quantifiable holds
( ( for
a being
Element of
A holds
J,
(v . ((S_Bound (@ (CQCSub_All ([S,x],xSQ)))) | a)) . ((NEx_Val (v,S,x,xSQ)) +* (x | a)) |= S ) iff for
a being
Element of
A holds
J,
v . ((NEx_Val (v,S,x,xSQ)) +* (x | a)) |= S )
theorem Th73:
theorem
canceled;
theorem Th75:
theorem Th76:
theorem
canceled;
theorem Th78:
theorem Th79:
theorem Th80:
theorem Th81:
for
p,
q being
Element of
CQC-WFF for
A being non
empty set for
J being
interpretation of
A st ( for
v being
Element of
Valuations_in A for
vS,
vS1,
vS2 being
Val_Sub of
A st ( for
y being
bound_QC-variable st
y in dom vS1 holds
not
y in still_not-bound_in p ) & ( for
y being
bound_QC-variable st
y in dom vS2 holds
vS2 . y = v . y ) &
dom vS misses dom vS2 holds
(
J,
v . vS |= p iff
J,
v . ((vS +* vS1) +* vS2) |= p ) ) & ( for
v being
Element of
Valuations_in A for
vS,
vS1,
vS2 being
Val_Sub of
A st ( for
y being
bound_QC-variable st
y in dom vS1 holds
not
y in still_not-bound_in q ) & ( for
y being
bound_QC-variable st
y in dom vS2 holds
vS2 . y = v . y ) &
dom vS misses dom vS2 holds
(
J,
v . vS |= q iff
J,
v . ((vS +* vS1) +* vS2) |= q ) ) holds
for
v being
Element of
Valuations_in A for
vS,
vS1,
vS2 being
Val_Sub of
A st ( for
y being
bound_QC-variable st
y in dom vS1 holds
not
y in still_not-bound_in (p '&' q) ) & ( for
y being
bound_QC-variable st
y in dom vS2 holds
vS2 . y = v . y ) &
dom vS misses dom vS2 holds
(
J,
v . vS |= p '&' q iff
J,
v . ((vS +* vS1) +* vS2) |= p '&' q )
theorem Th82:
theorem Th83:
theorem Th84:
for
p being
Element of
CQC-WFF for
x being
bound_QC-variable for
A being non
empty set for
J being
interpretation of
A st ( for
v being
Element of
Valuations_in A for
vS,
vS1,
vS2 being
Val_Sub of
A st ( for
y being
bound_QC-variable st
y in dom vS1 holds
not
y in still_not-bound_in p ) & ( for
y being
bound_QC-variable st
y in dom vS2 holds
vS2 . y = v . y ) &
dom vS misses dom vS2 holds
(
J,
v . vS |= p iff
J,
v . ((vS +* vS1) +* vS2) |= p ) ) holds
for
v being
Element of
Valuations_in A for
vS,
vS1,
vS2 being
Val_Sub of
A st ( for
y being
bound_QC-variable st
y in dom vS1 holds
not
y in still_not-bound_in (All (x,p)) ) & ( for
y being
bound_QC-variable st
y in dom vS2 holds
vS2 . y = v . y ) &
dom vS misses dom vS2 holds
(
J,
v . vS |= All (
x,
p) iff
J,
v . ((vS +* vS1) +* vS2) |= All (
x,
p) )
theorem Th85:
:: deftheorem Def10 defines RSub1 SUBLEMMA:def 10 :
for p being Element of CQC-WFF
for b2 being set holds
( b2 = RSub1 p iff for b being set holds
( b in b2 iff ex x being bound_QC-variable st
( x = b & not x in still_not-bound_in p ) ) );
:: deftheorem Def11 defines RSub2 SUBLEMMA:def 11 :
for p being Element of CQC-WFF
for Sub being CQC_Substitution
for b3 being set holds
( b3 = RSub2 (p,Sub) iff for b being set holds
( b in b3 iff ex x being bound_QC-variable st
( x = b & x in still_not-bound_in p & x = (@ Sub) . x ) ) );
theorem Th86:
theorem Th87:
theorem Th88:
theorem Th89:
for
x being
bound_QC-variable for
S being
Element of
CQC-Sub-WFF for
xSQ being
second_Q_comp of
[S,x] st
[S,x] is
quantifiable holds
@ ((CQCSub_All ([S,x],xSQ)) `2) = ((@ (RestrictSub (x,(All (x,(S `1))),xSQ))) +* ((@ xSQ) | (RSub1 (All (x,(S `1)))))) +* ((@ xSQ) | (RSub2 ((All (x,(S `1))),xSQ)))
theorem Th90:
for
x being
bound_QC-variable for
A being non
empty set for
v being
Element of
Valuations_in A for
S being
Element of
CQC-Sub-WFF for
xSQ being
second_Q_comp of
[S,x] st
[S,x] is
quantifiable holds
ex
vS1,
vS2 being
Val_Sub of
A st
( ( for
y being
bound_QC-variable st
y in dom vS1 holds
not
y in still_not-bound_in (All (x,(S `1))) ) & ( for
y being
bound_QC-variable st
y in dom vS2 holds
vS2 . y = v . y ) &
dom (NEx_Val (v,S,x,xSQ)) misses dom vS2 &
v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) = v . (((NEx_Val (v,S,x,xSQ)) +* vS1) +* vS2) )
theorem Th91:
for
x being
bound_QC-variable for
A being non
empty set for
J being
interpretation of
A for
S being
Element of
CQC-Sub-WFF for
xSQ being
second_Q_comp of
[S,x] st
[S,x] is
quantifiable holds
for
v being
Element of
Valuations_in A holds
(
J,
v . (NEx_Val (v,S,x,xSQ)) |= All (
x,
(S `1)) iff
J,
v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All (
[S,x],
xSQ) )
theorem Th92:
for
x being
bound_QC-variable for
A being non
empty set for
J being
interpretation of
A for
S being
Element of
CQC-Sub-WFF for
xSQ being
second_Q_comp of
[S,x] st
[S,x] is
quantifiable & ( for
v being
Element of
Valuations_in A holds
(
J,
v |= CQC_Sub S iff
J,
v . (Val_S (v,S)) |= S ) ) holds
for
v being
Element of
Valuations_in A holds
(
J,
v |= CQC_Sub (CQCSub_All ([S,x],xSQ)) iff
J,
v . (Val_S (v,(CQCSub_All ([S,x],xSQ)))) |= CQCSub_All (
[S,x],
xSQ) )
theorem