:: Interpretation and Satisfiability in the First Order Logic :: by Edmund Woronowicz :: :: Received June 1, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin definition let Al be QC-alphabet ; let A be set ; func Valuations_in (Al,A) -> set equals :: VALUAT_1:def 1 Funcs ((bound_QC-variables Al),A); coherence Funcs ((bound_QC-variables Al),A) is set ; end; :: deftheorem defines Valuations_in VALUAT_1:def_1_:_ for Al being QC-alphabet for A being set holds Valuations_in (Al,A) = Funcs ((bound_QC-variables Al),A); registration let Al be QC-alphabet ; let A be non empty set ; cluster Valuations_in (Al,A) -> functional non empty ; coherence ( not Valuations_in (Al,A) is empty & Valuations_in (Al,A) is functional ) ; end; theorem Th1: :: VALUAT_1:1 for Al being QC-alphabet for A being non empty set for x being set st x is Element of Valuations_in (Al,A) holds x is Function of (bound_QC-variables Al),A proofend; definition let Al be QC-alphabet ; let A be non empty set ; :: original:Valuations_in redefine func Valuations_in (Al,A) -> FUNCTION_DOMAIN of bound_QC-variables Al,A; coherence Valuations_in (Al,A) is FUNCTION_DOMAIN of bound_QC-variables Al,A proofend; end; 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); func FOR_ALL (x,p) -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) means :Def2: :: VALUAT_1:def 2 for v being Element of Valuations_in (Al,A) holds it . 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 } ; 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 } proofend; 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 proofend; end; :: deftheorem Def2 defines FOR_ALL VALUAT_1:def_2_:_ for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for p, b5 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( b5 = FOR_ALL (x,p) iff for v being Element of Valuations_in (Al,A) holds b5 . 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 } ); theorem Th2: :: VALUAT_1:2 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in (Al,A) st ( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) ) ) proofend; theorem Th3: :: VALUAT_1:3 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( (FOR_ALL (x,p)) . v = TRUE iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds p . v1 = TRUE ) proofend; notation let Al be QC-alphabet ; let A be non empty set ; let k be Element of NAT ; let ll be CQC-variable_list of k,Al; let v be Element of Valuations_in (Al,A); synonym v *' ll for A * Al; end; definition let Al be QC-alphabet ; let A be non empty set ; let k be Element of NAT ; let ll be CQC-variable_list of k,Al; let v be Element of Valuations_in (Al,A); :: original:*' redefine funcv *' ll -> FinSequence of A means :Def3: :: VALUAT_1:def 3 ( len it = k & ( for i being natural number st 1 <= i & i <= k holds it . i = v . (ll . i) ) ); coherence *' is FinSequence of A proofend; compatibility for b1 being FinSequence of A holds ( b1 = *' iff ( len b1 = k & ( for i being natural number st 1 <= i & i <= k holds b1 . i = v . (ll . i) ) ) ) proofend; end; :: deftheorem Def3 defines *' VALUAT_1:def_3_:_ for Al being QC-alphabet for A being non empty set for k being Element of NAT for ll being CQC-variable_list of k,Al for v being Element of Valuations_in (Al,A) for b6 being FinSequence of A holds ( b6 = v *' ll iff ( len b6 = k & ( for i being natural number st 1 <= i & i <= k holds b6 . i = v . (ll . i) ) ) ); definition let Al be QC-alphabet ; let A be non empty set ; let k be Element of NAT ; let ll be CQC-variable_list of k,Al; let r be Element of relations_on A; funcll 'in' r -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) means :Def4: :: VALUAT_1:def 4 for v being Element of Valuations_in (Al,A) holds ( ( v *' ll in r implies it . v = TRUE ) & ( it . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies it . v = FALSE ) & ( it . v = FALSE implies not v *' ll in r ) ); existence ex b1 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st for v being Element of Valuations_in (Al,A) holds ( ( v *' ll in r implies b1 . v = TRUE ) & ( b1 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b1 . v = FALSE ) & ( b1 . v = FALSE implies not v *' ll in r ) ) proofend; uniqueness for b1, b2 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st ( for v being Element of Valuations_in (Al,A) holds ( ( v *' ll in r implies b1 . v = TRUE ) & ( b1 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b1 . v = FALSE ) & ( b1 . v = FALSE implies not v *' ll in r ) ) ) & ( for v being Element of Valuations_in (Al,A) holds ( ( v *' ll in r implies b2 . v = TRUE ) & ( b2 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b2 . v = FALSE ) & ( b2 . v = FALSE implies not v *' ll in r ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines 'in' VALUAT_1:def_4_:_ for Al being QC-alphabet for A being non empty set for k being Element of NAT for ll being CQC-variable_list of k,Al for r being Element of relations_on A for b6 being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds ( b6 = ll 'in' r iff for v being Element of Valuations_in (Al,A) holds ( ( v *' ll in r implies b6 . v = TRUE ) & ( b6 . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b6 . v = FALSE ) & ( b6 . v = FALSE implies not v *' ll in r ) ) ); definition let Al be QC-alphabet ; let A be non empty set ; let F be Function of (CQC-WFF Al),(Funcs ((Valuations_in (Al,A)),BOOLEAN)); let p be Element of CQC-WFF Al; :: original:. redefine funcF . p -> Element of Funcs ((Valuations_in (Al,A)),BOOLEAN); coherence F . p is Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) proofend; end; definition let Al be QC-alphabet ; let D be non empty set ; mode interpretation of Al,D -> Function of (QC-pred_symbols Al),(relations_on D) means :: VALUAT_1:def 5 for P being Element of QC-pred_symbols Al for r being Element of relations_on D holds ( not it . P = r or r = empty_rel D or the_arity_of P = the_arity_of r ); existence ex b1 being Function of (QC-pred_symbols Al),(relations_on D) st for P being Element of QC-pred_symbols Al for r being Element of relations_on D holds ( not b1 . P = r or r = empty_rel D or the_arity_of P = the_arity_of r ) proofend; end; :: deftheorem defines interpretation VALUAT_1:def_5_:_ for Al being QC-alphabet for D being non empty set for b3 being Function of (QC-pred_symbols Al),(relations_on D) holds ( b3 is interpretation of Al,D iff for P being Element of QC-pred_symbols Al for r being Element of relations_on D holds ( not b3 . P = r or r = empty_rel D or the_arity_of P = the_arity_of r ) ); definition let Al be QC-alphabet ; let A be non empty set ; let k be Element of NAT ; let J be interpretation of Al,A; let P be QC-pred_symbol of k,Al; :: original:. redefine funcJ . P -> Element of relations_on A; coherence J . P is Element of relations_on A by FUNCT_2:5; 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: :: VALUAT_1:def 6 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)) ) ) ) proofend; 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 proofend; 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))) ) ) proofend; theorem :: VALUAT_1:4 for Al being QC-alphabet for A being non empty set for J being interpretation of Al,A holds Valid ((VERUM Al),J) = (Valuations_in (Al,A)) --> TRUE by Lm1; theorem Th5: :: VALUAT_1:5 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for J being interpretation of Al,A holds (Valid ((VERUM Al),J)) . v = TRUE proofend; theorem :: VALUAT_1:6 for Al being QC-alphabet for k being Element of NAT for A being non empty set for ll being CQC-variable_list of k,Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al holds Valid ((P ! ll),J) = ll 'in' (J . P) by Lm1; theorem Th7: :: VALUAT_1:7 for Al being QC-alphabet for k being Element of NAT for A being non empty set for v being Element of Valuations_in (Al,A) for ll being CQC-variable_list of k,Al for p being Element of CQC-WFF Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( v *' ll in r iff (Valid (p,J)) . v = TRUE ) proofend; theorem Th8: :: VALUAT_1:8 for Al being QC-alphabet for k being Element of NAT for A being non empty set for v being Element of Valuations_in (Al,A) for ll being CQC-variable_list of k,Al for p being Element of CQC-WFF Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al for r being Element of relations_on A st p = P ! ll & r = J . P holds ( not v *' ll in r iff (Valid (p,J)) . v = FALSE ) proofend; theorem :: VALUAT_1:9 for Al being QC-alphabet for A being non empty set for p being Element of CQC-WFF Al for J being interpretation of Al,A holds Valid (('not' p),J) = 'not' (Valid (p,J)) by Lm1; theorem Th10: :: VALUAT_1:10 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid (('not' p),J)) . v = 'not' ((Valid (p,J)) . v) proofend; theorem :: VALUAT_1:11 for Al being QC-alphabet for A being non empty set for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds Valid ((p '&' q),J) = (Valid (p,J)) '&' (Valid (q,J)) by Lm1; theorem Th12: :: VALUAT_1:12 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid ((p '&' q),J)) . v = ((Valid (p,J)) . v) '&' ((Valid (q,J)) . v) proofend; theorem :: VALUAT_1:13 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for p being Element of CQC-WFF Al for J being interpretation of Al,A holds Valid ((All (x,p)),J) = FOR_ALL (x,(Valid (p,J))) by Lm1; theorem Th14: :: VALUAT_1:14 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid ((p '&' ('not' p)),J)) . v = FALSE proofend; theorem :: VALUAT_1:15 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds (Valid (('not' (p '&' ('not' p))),J)) . v = TRUE proofend; definition let Al be QC-alphabet ; let A be non empty set ; let p be Element of CQC-WFF Al; let J be interpretation of Al,A; let v be Element of Valuations_in (Al,A); predJ,v |= p means :Def7: :: VALUAT_1:def 7 (Valid (p,J)) . v = TRUE ; end; :: deftheorem Def7 defines |= VALUAT_1:def_7_:_ for Al being QC-alphabet for A being non empty set for p being Element of CQC-WFF Al for J being interpretation of Al,A for v being Element of Valuations_in (Al,A) holds ( J,v |= p iff (Valid (p,J)) . v = TRUE ); theorem :: VALUAT_1:16 for Al being QC-alphabet for k being Element of NAT for A being non empty set for v being Element of Valuations_in (Al,A) for ll being CQC-variable_list of k,Al for J being interpretation of Al,A for P being QC-pred_symbol of k,Al holds ( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE ) proofend; theorem :: VALUAT_1:17 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= 'not' p iff not J,v |= p ) proofend; theorem :: VALUAT_1:18 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= p '&' q iff ( J,v |= p & J,v |= q ) ) proofend; theorem Th19: :: VALUAT_1:19 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff (FOR_ALL (x,(Valid (p,J)))) . v = TRUE ) proofend; theorem Th20: :: VALUAT_1:20 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff for v1 being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds v1 . y = v . y ) holds (Valid (p,J)) . v1 = TRUE ) proofend; theorem :: VALUAT_1:21 for Al being QC-alphabet for A being non empty set for p being Element of CQC-WFF Al for J being interpretation of Al,A holds Valid (('not' ('not' p)),J) = Valid (p,J) proofend; theorem Th22: :: VALUAT_1:22 for Al being QC-alphabet for A being non empty set for p being Element of CQC-WFF Al for J being interpretation of Al,A holds Valid ((p '&' p),J) = Valid (p,J) proofend; theorem Th23: :: VALUAT_1:23 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= p => q iff ( (Valid (p,J)) . v = FALSE or (Valid (q,J)) . v = TRUE ) ) proofend; theorem Th24: :: VALUAT_1:24 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= p => q iff ( J,v |= p implies J,v |= q ) ) proofend; theorem Th25: :: VALUAT_1:25 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) st (FOR_ALL (x,p)) . v = TRUE holds p . v = TRUE proofend; 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; predJ |= p means :Def8: :: VALUAT_1:def 8 for v being Element of Valuations_in (Al,A) holds J,v |= p; end; :: deftheorem Def8 defines |= VALUAT_1:def_8_:_ 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 holds ( J |= p iff for v being Element of Valuations_in (Al,A) holds J,v |= p ); Lm2: for u, w, z being Element of BOOLEAN holds 'not' (('not' (u '&' ('not' w))) '&' (('not' (w '&' z)) '&' (u '&' z))) = TRUE proofend; Lm3: now__::_thesis:_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 ; ::_thesis: 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 ; ::_thesis: 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; ::_thesis: 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); ::_thesis: 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 ) ::_thesis: verum proof deffunc H1( set ) -> Element of A = V2 . Z; deffunc H2( set ) -> set = V1 . $1; defpred S1[ set ] means for x1 being bound_QC-variable of Al st x1 = $1 holds x1 <> Y; A1: for x being set st x in bound_QC-variables Al holds ( ( S1[x] implies H2(x) in A ) & ( not S1[x] implies H1(x) in A ) ) by FUNCT_2:5; consider f being Function of (bound_QC-variables Al),A such that A2: for x being set st x in bound_QC-variables Al holds ( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) from FUNCT_2:sch_5(A1); ( dom f = bound_QC-variables Al & rng f c= A ) by FUNCT_2:def_1, RELAT_1:def_19; then reconsider f = f as Element of Valuations_in (Al,A) by FUNCT_2:def_2; take f ; ::_thesis: ( ( for x being bound_QC-variable of Al st x <> Y holds f . x = V1 . x ) & f . Y = V2 . Z ) now__::_thesis:_for_x_being_bound_QC-variable_of_Al_holds_ (_(_x_<>_Y_implies_f_._x_=_V1_._x_)_&_(_x_=_Y_implies_f_._Y_=_V2_._Z_)_) let x be bound_QC-variable of Al; ::_thesis: ( ( x <> Y implies f . x = V1 . x ) & ( x = Y implies f . Y = V2 . Z ) ) now__::_thesis:_(_x_<>_Y_implies_f_._x_=_V1_._x_) assume A3: x <> Y ; ::_thesis: f . x = V1 . x ( ( for x1 being bound_QC-variable of Al st x1 = x holds x1 <> Y ) implies f . x = V1 . x ) by A2; hence f . x = V1 . x by A3; ::_thesis: verum end; hence ( x <> Y implies f . x = V1 . x ) ; ::_thesis: ( x = Y implies f . Y = V2 . Z ) thus ( x = Y implies f . Y = V2 . Z ) by A2; ::_thesis: verum end; hence ( ( for x being bound_QC-variable of Al st x <> Y holds f . x = V1 . x ) & f . Y = V2 . Z ) ; ::_thesis: verum end; end; theorem :: VALUAT_1:26 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 ) by Lm3; theorem Th27: :: VALUAT_1:27 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for p being Element of CQC-WFF Al for J being interpretation of Al,A st not x in still_not-bound_in p holds for v, w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds (Valid (p,J)) . v = (Valid (p,J)) . w proofend; theorem Th28: :: VALUAT_1:28 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A st J,v |= p & not x in still_not-bound_in p holds for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p proofend; theorem Th29: :: VALUAT_1:29 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds ( J,v |= All (x,p) iff for w being Element of Valuations_in (Al,A) st ( for y being bound_QC-variable of Al st x <> y holds w . y = v . y ) holds J,w |= p ) proofend; theorem Th30: :: VALUAT_1:30 for Al being QC-alphabet for A being non empty set for x, y being bound_QC-variable of Al for p, q being Element of CQC-WFF Al for J being interpretation of Al,A for s9 being QC-formula of Al st x <> y & p = s9 . x & q = s9 . y holds for v being Element of Valuations_in (Al,A) st v . x = v . y holds (Valid (p,J)) . v = (Valid (q,J)) . v proofend; theorem Th31: :: VALUAT_1:31 for Al being QC-alphabet for x, y being bound_QC-variable of Al for s9 being QC-formula of Al st x <> y & not x in still_not-bound_in s9 holds not x in still_not-bound_in (s9 . y) proofend; theorem Th32: :: VALUAT_1:32 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for J being interpretation of Al,A holds J,v |= VERUM Al proofend; theorem Th33: :: VALUAT_1:33 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (p '&' q) => (q '&' p) proofend; theorem Th34: :: VALUAT_1:34 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (('not' p) => p) => p proofend; theorem Th35: :: VALUAT_1:35 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= p => (('not' p) => q) proofend; theorem Th36: :: VALUAT_1:36 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p, q, t being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) proofend; theorem :: VALUAT_1:37 for Al being QC-alphabet for A being non empty set for v being Element of Valuations_in (Al,A) for p, q being Element of CQC-WFF Al for J being interpretation of Al,A st J,v |= p & J,v |= p => q holds J,v |= q by Th24; theorem Th38: :: VALUAT_1:38 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for v being Element of Valuations_in (Al,A) for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J,v |= (All (x,p)) => p proofend; theorem :: VALUAT_1:39 for Al being QC-alphabet for A being non empty set for J being interpretation of Al,A holds J |= VERUM Al proofend; theorem :: VALUAT_1:40 for Al being QC-alphabet for A being non empty set for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= (p '&' q) => (q '&' p) proofend; theorem :: VALUAT_1:41 for Al being QC-alphabet for A being non empty set for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= (('not' p) => p) => p proofend; theorem :: VALUAT_1:42 for Al being QC-alphabet for A being non empty set for p, q being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= p => (('not' p) => q) proofend; theorem :: VALUAT_1:43 for Al being QC-alphabet for A being non empty set for p, q, t being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= (p => q) => (('not' (q '&' t)) => ('not' (p '&' t))) proofend; theorem :: VALUAT_1:44 for Al being QC-alphabet for A being non empty set for p, q being Element of CQC-WFF Al for J being interpretation of Al,A st J |= p & J |= p => q holds J |= q proofend; theorem :: VALUAT_1:45 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for p being Element of CQC-WFF Al for J being interpretation of Al,A holds J |= (All (x,p)) => p proofend; theorem :: VALUAT_1:46 for Al being QC-alphabet for A being non empty set for x being bound_QC-variable of Al for p, q being Element of CQC-WFF Al for J being interpretation of Al,A st J |= p => q & not x in still_not-bound_in p holds J |= p => (All (x,q)) proofend; theorem :: VALUAT_1:47 for Al being QC-alphabet for A being non empty set for x, y being bound_QC-variable of Al for p, q being Element of CQC-WFF Al for J being interpretation of Al,A for s being QC-formula of Al st p = s . x & q = s . y & not x in still_not-bound_in s & J |= p holds J |= q proofend;