begin
definition
let Al be
QC-alphabet ;
let A be non
empty set ;
let x be
bound_QC-variable of
Al;
let p be
Element of
Funcs (
(Valuations_in (Al,A)),
BOOLEAN);
existence
ex b1 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st
for v being Element of Valuations_in (Al,A) holds b1 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y }
uniqueness
for b1, b2 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st ( for v being Element of Valuations_in (Al,A) holds b1 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y } ) & ( for v being Element of Valuations_in (Al,A) holds b2 . v = ALL { (p . v9) where v9 is Element of Valuations_in (Al,A) : for y being bound_QC-variable of Al st x <> y holds
v9 . y = v . y } ) holds
b1 = b2
end;
definition
let Al be
QC-alphabet ;
let A be non
empty set ;
let J be
interpretation of
Al,
A;
let p be
Element of
CQC-WFF Al;
func Valid (
p,
J)
-> Element of
Funcs (
(Valuations_in (Al,A)),
BOOLEAN)
means :
Def6:
ex
F being
Function of
(CQC-WFF Al),
(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
(
it = F . p &
F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for
p,
q being
Element of
CQC-WFF Al for
x being
bound_QC-variable of
Al for
k being
Element of
NAT for
ll being
CQC-variable_list of
k,
Al for
P being
QC-pred_symbol of
k,
Al holds
(
F . (P ! ll) = ll 'in' (J . P) &
F . ('not' p) = 'not' (F . p) &
F . (p '&' q) = (F . p) '&' (F . q) &
F . (All (x,p)) = FOR_ALL (
x,
(F . p)) ) ) );
existence
ex b1 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( b1 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) )
uniqueness
for b1, b2 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( b1 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) & ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( b2 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) holds
b1 = b2
end;
::
deftheorem Def6 defines
Valid VALUAT_1:def 6 :
for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for p being Element of CQC-WFF Al
for b5 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( b5 = Valid (p,J) iff ex F being Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)) st
( b5 = F . p & F . (VERUM Al) = (Valuations_in (Al,A)) --> TRUE & ( for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Element of NAT
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( F . (P ! ll) = ll 'in' (J . P) & F . ('not' p) = 'not' (F . p) & F . (p '&' q) = (F . p) '&' (F . q) & F . (All (x,p)) = FOR_ALL (x,(F . p)) ) ) ) );
Lm1:
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for A being non empty set
for J being interpretation of Al,A holds
( Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE & ( for k being Element of NAT
for ll being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF Al holds Valid (('not' p),J) = 'not' (Valid (p,J)) ) & ( for q being Element of CQC-WFF Al holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) ) & ( for x being bound_QC-variable of Al holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) ) )
Lm2:
for u, w, z being Element of BOOLEAN holds 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE
Lm3:
now for Al being QC-alphabet
for A being non empty set
for Y, Z being bound_QC-variable of Al
for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z )
let Al be
QC-alphabet ;
for A being non empty set
for Y, Z being bound_QC-variable of Al
for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z )let A be non
empty set ;
for Y, Z being bound_QC-variable of Al
for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z )let Y,
Z be
bound_QC-variable of
Al;
for V1, V2 being Element of Valuations_in (Al,A) ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z )let V1,
V2 be
Element of
Valuations_in (
Al,
A);
ex v being Element of Valuations_in (Al,A) st
( ( for x being bound_QC-variable of Al st x <> Y holds
v . x = V1 . x ) & v . Y = V2 . Z )thus
ex
v being
Element of
Valuations_in (
Al,
A) st
( ( for
x being
bound_QC-variable of
Al st
x <> Y holds
v . x = V1 . x ) &
v . Y = V2 . Z )
verum
end;