begin
theorem Th1:
theorem Th2:
:: deftheorem SUBLEMMA:def 1 :
canceled;
:: deftheorem defines Val_S SUBLEMMA:def 2 :
theorem Th3:
:: deftheorem Def3 defines |= SUBLEMMA:def 3 :
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 :
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 :
:: deftheorem Def6 defines CQCSub_All SUBLEMMA:def 6 :
theorem Th28:
:: deftheorem Def7 defines CQCSub_the_scope_of SUBLEMMA:def 7 :
:: deftheorem Def8 defines CQCQuant SUBLEMMA:def 8 :
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 :
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 :
:: deftheorem Def11 defines RSub2 SUBLEMMA:def 11 :
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