begin
:: deftheorem defines Valuations_in VALUAT_1:def 1 :
theorem
canceled;
theorem Th2:
:: deftheorem VALUAT_1:def 2 :
canceled;
:: deftheorem VALUAT_1:def 3 :
canceled;
:: deftheorem VALUAT_1:def 4 :
canceled;
:: deftheorem VALUAT_1:def 5 :
canceled;
:: deftheorem VALUAT_1:def 6 :
canceled;
:: deftheorem Def7 defines FOR_ALL VALUAT_1:def 7 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th7:
theorem Th8:
:: deftheorem Def8 defines *' VALUAT_1:def 8 :
:: deftheorem Def9 defines 'in' VALUAT_1:def 9 :
:: deftheorem defines interpretation VALUAT_1:def 10 :
definition
let A be non
empty set ;
let J be
interpretation of
A;
let p be
Element of
CQC-WFF ;
func Valid p,
J -> Element of
Funcs (Valuations_in A),
BOOLEAN means :
Def11:
ex
F being
Function of
CQC-WFF ,
Funcs (Valuations_in A),
BOOLEAN st
(
it = F . p &
F . VERUM = (Valuations_in A) --> TRUE & ( for
p,
q being
Element of
CQC-WFF for
x being
bound_QC-variable for
k being
Element of
NAT for
ll being
CQC-variable_list of
k for
P being
QC-pred_symbol of 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) ) ) );
correctness
existence
ex b1 being Element of Funcs (Valuations_in A),BOOLEAN ex F being Function of CQC-WFF , Funcs (Valuations_in A),BOOLEAN st
( b1 = F . p & F . VERUM = (Valuations_in A) --> TRUE & ( for p, q being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of 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 A),BOOLEAN st ex F being Function of CQC-WFF , Funcs (Valuations_in A),BOOLEAN st
( b1 = F . p & F . VERUM = (Valuations_in A) --> TRUE & ( for p, q being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of 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 , Funcs (Valuations_in A),BOOLEAN st
( b2 = F . p & F . VERUM = (Valuations_in A) --> TRUE & ( for p, q being Element of CQC-WFF
for x being bound_QC-variable
for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of 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 Def11 defines Valid VALUAT_1:def 11 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
Lm1:
for p being Element of CQC-WFF
for A being non empty set
for J being interpretation of A holds
( Valid VERUM ,J = (Valuations_in A) --> TRUE & ( for k being Element of NAT
for ll being CQC-variable_list of k
for P being QC-pred_symbol of holds Valid (P ! ll),J = ll 'in' (J . P) ) & ( for p being Element of CQC-WFF holds Valid ('not' p),J = 'not' (Valid p,J) ) & ( for q being Element of CQC-WFF holds Valid (p '&' q),J = (Valid p,J) '&' (Valid q,J) ) & ( for x being bound_QC-variable holds Valid (All x,p),J = FOR_ALL x,(Valid p,J) ) )
theorem
theorem Th14:
theorem
theorem Th16:
theorem Th17:
theorem
canceled;
theorem
theorem Th20:
theorem
theorem Th22:
theorem
theorem Th24:
theorem
:: deftheorem Def12 defines |= VALUAT_1:def 12 :
theorem
canceled;
theorem
theorem
theorem
theorem Th30:
theorem Th31:
theorem
theorem Th33:
theorem
canceled;
theorem Th35:
theorem Th36:
theorem Th37:
:: deftheorem Def13 defines |= VALUAT_1:def 13 :
Lm2:
for u, w, z being Element of BOOLEAN holds 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE
theorem
canceled;
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem
theorem Th50:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem