:: Interpretation and Satisfiability in the First Order Logic
:: by Edmund Woronowicz
::
:: Received June 1, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem defines Valuations_in VALUAT_1:def 1 :
theorem :: VALUAT_1:1
canceled;
theorem Th2: :: VALUAT_1:2
:: 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 :: VALUAT_1:3
canceled;
theorem :: VALUAT_1:4
canceled;
theorem :: VALUAT_1:5
canceled;
theorem :: VALUAT_1:6
canceled;
theorem Th7: :: VALUAT_1:7
theorem Th8: :: VALUAT_1:8
:: 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:
:: VALUAT_1:def 11
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
for
P being
QC-pred_symbol of
k 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
for P being QC-pred_symbol of k 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
for P being QC-pred_symbol of k 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
for P being QC-pred_symbol of k 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 :: VALUAT_1:9
canceled;
theorem :: VALUAT_1:10
canceled;
theorem :: VALUAT_1:11
canceled;
theorem :: VALUAT_1:12
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
for P being QC-pred_symbol of k 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 :: VALUAT_1:13
theorem Th14: :: VALUAT_1:14
theorem :: VALUAT_1:15
theorem Th16: :: VALUAT_1:16
theorem Th17: :: VALUAT_1:17
theorem :: VALUAT_1:18
canceled;
theorem :: VALUAT_1:19
theorem Th20: :: VALUAT_1:20
theorem :: VALUAT_1:21
theorem Th22: :: VALUAT_1:22
theorem :: VALUAT_1:23
theorem Th24: :: VALUAT_1:24
theorem :: VALUAT_1:25
:: deftheorem Def12 defines |= VALUAT_1:def 12 :
theorem :: VALUAT_1:26
canceled;
theorem :: VALUAT_1:27
theorem :: VALUAT_1:28
theorem :: VALUAT_1:29
theorem Th30: :: VALUAT_1:30
theorem Th31: :: VALUAT_1:31
theorem :: VALUAT_1:32
theorem Th33: :: VALUAT_1:33
theorem :: VALUAT_1:34
canceled;
theorem Th35: :: VALUAT_1:35
theorem Th36: :: VALUAT_1:36
theorem Th37: :: VALUAT_1:37
:: 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 :: VALUAT_1:38
canceled;
theorem Th39: :: VALUAT_1:39
theorem Th40: :: VALUAT_1:40
theorem Th41: :: VALUAT_1:41
theorem Th42: :: VALUAT_1:42
theorem Th43: :: VALUAT_1:43
theorem Th44: :: VALUAT_1:44
theorem Th45: :: VALUAT_1:45
theorem Th46: :: VALUAT_1:46
theorem Th47: :: VALUAT_1:47
theorem Th48: :: VALUAT_1:48
theorem :: VALUAT_1:49
theorem Th50: :: VALUAT_1:50
theorem :: VALUAT_1:51
theorem :: VALUAT_1:52
theorem :: VALUAT_1:53
theorem :: VALUAT_1:54
theorem :: VALUAT_1:55
theorem :: VALUAT_1:56
theorem :: VALUAT_1:57
theorem :: VALUAT_1:58
theorem :: VALUAT_1:59