:: HENMODEL semantic presentation begin theorem Th1: :: HENMODEL:1 for n being Element of NAT for A being non empty finite Subset of NAT for f being Function of n,A st ex m being Element of NAT st succ m = n & rng f = A & ( for n, m being Element of NAT st m in dom f & n in dom f & n < m holds f . n in f . m ) holds f . (union n) = union (rng f) proof let n be Element of NAT ; ::_thesis: for A being non empty finite Subset of NAT for f being Function of n,A st ex m being Element of NAT st succ m = n & rng f = A & ( for n, m being Element of NAT st m in dom f & n in dom f & n < m holds f . n in f . m ) holds f . (union n) = union (rng f) let A be non empty finite Subset of NAT; ::_thesis: for f being Function of n,A st ex m being Element of NAT st succ m = n & rng f = A & ( for n, m being Element of NAT st m in dom f & n in dom f & n < m holds f . n in f . m ) holds f . (union n) = union (rng f) let f be Function of n,A; ::_thesis: ( ex m being Element of NAT st succ m = n & rng f = A & ( for n, m being Element of NAT st m in dom f & n in dom f & n < m holds f . n in f . m ) implies f . (union n) = union (rng f) ) assume that A1: ex m being Element of NAT st succ m = n and A2: rng f = A and A3: for n, m being Element of NAT st m in dom f & n in dom f & n < m holds f . n in f . m ; ::_thesis: f . (union n) = union (rng f) thus f . (union n) c= union (rng f) :: according to XBOOLE_0:def_10 ::_thesis: union (rng f) c= f . (union n) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f . (union n) or a in union (rng f) ) consider m being Element of NAT such that A4: n = succ m by A1; dom f = n by FUNCT_2:def_1; then A5: f . m in rng f by A4, FUNCT_1:3, ORDINAL1:6; assume a in f . (union n) ; ::_thesis: a in union (rng f) then a in f . m by A4, ORDINAL2:2; hence a in union (rng f) by A5, TARSKI:def_4; ::_thesis: verum end; thus union (rng f) c= f . (union n) ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union (rng f) or a in f . (union n) ) assume a in union (rng f) ; ::_thesis: a in f . (union n) then consider b being set such that A6: a in b and A7: b in rng f by TARSKI:def_4; consider c being set such that A8: c in dom f and A9: f . c = b by A7, FUNCT_1:def_3; reconsider i = c as Ordinal by A8; reconsider i = i as Element of NAT by A8, ORDINAL1:10; consider m being Element of NAT such that A10: n = succ m by A1; i c= m by A8, A10, ORDINAL1:22; then ( i c< m or i = m ) by XBOOLE_0:def_8; then A11: ( i in m or i = m ) by ORDINAL1:11; A12: dom f = n by FUNCT_2:def_1; then A13: m in dom f by A10, ORDINAL1:6; A14: now__::_thesis:_(_f_._i_in_f_._m_implies_a_in_f_._(union_n)_) i in dom f by A11, A12, A13, ORDINAL1:10; then f . i in rng f by FUNCT_1:3; then reconsider i1 = f . i as Element of NAT by A2; f . m in rng f by A10, A12, FUNCT_1:3, ORDINAL1:6; then reconsider i2 = f . m as Element of NAT by A2; assume f . i in f . m ; ::_thesis: a in f . (union n) then i1 c= i2 by ORDINAL1:def_2; then a in i2 by A6, A9; hence a in f . (union n) by A10, ORDINAL2:2; ::_thesis: verum end; ( i in { k where k is Element of NAT : k < m } or i = m ) by A11, AXIOMS:4; then ( ex k being Element of NAT st ( k = i & k < m ) or i = m ) ; hence a in f . (union n) by A3, A6, A8, A9, A10, A13, A14, ORDINAL2:2; ::_thesis: verum end; end; theorem Th2: :: HENMODEL:2 for A being non empty finite Subset of NAT holds ( union A in A & ( for a being set holds ( not a in A or a in union A or a = union A ) ) ) proof let A be non empty finite Subset of NAT; ::_thesis: ( union A in A & ( for a being set holds ( not a in A or a in union A or a = union A ) ) ) consider a being Ordinal such that A1: RelIncl A, RelIncl a are_isomorphic by WELLORD2:8, WELLORD2:13; consider F1 being Function such that A2: F1 is_isomorphism_of RelIncl A, RelIncl a by A1, WELLORD1:def_8; A3: dom F1 = field (RelIncl A) by A2, WELLORD1:def_7; then dom F1 = A by WELLORD2:def_1; then consider b being set such that A4: b in dom F1 by XBOOLE_0:def_1; rng F1 is finite by A3, FINSET_1:8; then field (RelIncl a) is finite by A2, WELLORD1:def_7; then A5: a is finite by WELLORD2:def_1; F1 . b in rng F1 by A4, FUNCT_1:3; then not field (RelIncl a) is empty by A2, WELLORD1:def_7; then not a is empty by WELLORD2:def_1; then A6: {} in a by ORDINAL1:16, XBOOLE_1:3; A7: now__::_thesis:_not_a_is_limit_ordinal assume a is limit_ordinal ; ::_thesis: contradiction then omega c= a by A6, ORDINAL1:def_11; hence contradiction by A5; ::_thesis: verum end; RelIncl a, RelIncl A are_isomorphic by A1, WELLORD1:40; then consider F being Function such that A8: F is_isomorphism_of RelIncl a, RelIncl A by WELLORD1:def_8; A9: for m, n being Element of NAT st m in dom F & n in dom F & n < m holds F . n in F . m proof let m, n be Element of NAT ; ::_thesis: ( m in dom F & n in dom F & n < m implies F . n in F . m ) assume that A10: m in dom F and A11: n in dom F and A12: n < m ; ::_thesis: F . n in F . m F . n in rng F by A11, FUNCT_1:3; then F . n in field (RelIncl A) by A8, WELLORD1:def_7; then A13: F . n in A by WELLORD2:def_1; then reconsider b = F . n as Element of NAT ; n in field (RelIncl a) by A8, A11, WELLORD1:def_7; then A14: n in a by WELLORD2:def_1; F . m in rng F by A10, FUNCT_1:3; then F . m in field (RelIncl A) by A8, WELLORD1:def_7; then A15: F . m in A by WELLORD2:def_1; then reconsider c = F . m as Element of NAT ; n in { i where i is Element of NAT : i < m } by A12; then n in m by AXIOMS:4; then A16: n c= m by ORDINAL1:def_2; m in field (RelIncl a) by A8, A10, WELLORD1:def_7; then m in a by WELLORD2:def_1; then [n,m] in RelIncl a by A14, A16, WELLORD2:def_1; then [(F . n),(F . m)] in RelIncl A by A8, WELLORD1:def_7; then A17: F . n c= F . m by A13, A15, WELLORD2:def_1; F is one-to-one by A8, WELLORD1:def_7; then F . n <> F . m by A10, A11, A12, FUNCT_1:def_4; then F . n c< F . m by A17, XBOOLE_0:def_8; then b in c by ORDINAL1:11; hence F . n in F . m ; ::_thesis: verum end; reconsider a = a as Element of NAT by A5, FINSET_1:1, ORDINAL1:16; dom F = field (RelIncl a) by A8, WELLORD1:def_7; then A18: dom F = a by WELLORD2:def_1; A19: now__::_thesis:_for_b_being_Ordinal_st_succ_b_=_a_holds_ b_is_Element_of_NAT let b be Ordinal; ::_thesis: ( succ b = a implies b is Element of NAT ) assume succ b = a ; ::_thesis: b is Element of NAT then b in a by ORDINAL1:6; hence b is Element of NAT by ORDINAL1:10; ::_thesis: verum end; A20: ex m being Element of NAT st succ m = a proof consider b being Ordinal such that A21: succ b = a by A7, ORDINAL1:29; reconsider b = b as Element of NAT by A19, A21; take b ; ::_thesis: succ b = a thus succ b = a by A21; ::_thesis: verum end; then consider m being Element of NAT such that A22: succ m = a ; A23: rng F = field (RelIncl A) by A8, WELLORD1:def_7; then A24: rng F = A by WELLORD2:def_1; then reconsider F = F as Function of a,A by A18, FUNCT_2:1; A25: for n, m being Element of NAT st m in dom F & n in dom F & n < m holds F . n in F . m by A9; rng F = A by A23, WELLORD2:def_1; then A26: F . (union a) = union (rng F) by A20, A25, Th1; A27: union a = m by A22, ORDINAL2:2; hence union A in A by A24, A18, A22, A26, FUNCT_1:3, ORDINAL1:6; ::_thesis: for a being set holds ( not a in A or a in union A or a = union A ) thus for b being set holds ( not b in A or b in union A or b = union A ) ::_thesis: verum proof let b be set ; ::_thesis: ( not b in A or b in union A or b = union A ) assume A28: b in A ; ::_thesis: ( b in union A or b = union A ) now__::_thesis:_(_not_b_<>_union_A_or_b_in_union_A_or_b_=_union_A_) A29: m in dom F by A18, A22, ORDINAL1:6; assume A30: b <> union A ; ::_thesis: ( b in union A or b = union A ) consider c being set such that A31: c in dom F and A32: F . c = b by A24, A28, FUNCT_1:def_3; reconsider c = c as Element of NAT by A31, ORDINAL1:10; ( c in m or c = m ) by A22, A31, ORDINAL1:8; then c in { k where k is Element of NAT : k < m } by A24, A22, A26, A30, A32, AXIOMS:4, ORDINAL2:2; then ex k being Element of NAT st ( k = c & k < m ) ; hence ( b in union A or b = union A ) by A9, A24, A26, A27, A31, A32, A29; ::_thesis: verum end; hence ( b in union A or b = union A ) ; ::_thesis: verum end; end; theorem Th3: :: HENMODEL:3 for C being non empty set for f being Function of NAT,C for X being finite set st ( for n, m being Element of NAT st m in dom f & n in dom f & n < m holds f . n c= f . m ) & X c= union (rng f) holds ex k being Element of NAT st X c= f . k proof let C be non empty set ; ::_thesis: for f being Function of NAT,C for X being finite set st ( for n, m being Element of NAT st m in dom f & n in dom f & n < m holds f . n c= f . m ) & X c= union (rng f) holds ex k being Element of NAT st X c= f . k let f be Function of NAT,C; ::_thesis: for X being finite set st ( for n, m being Element of NAT st m in dom f & n in dom f & n < m holds f . n c= f . m ) & X c= union (rng f) holds ex k being Element of NAT st X c= f . k let X be finite set ; ::_thesis: ( ( for n, m being Element of NAT st m in dom f & n in dom f & n < m holds f . n c= f . m ) & X c= union (rng f) implies ex k being Element of NAT st X c= f . k ) assume that A1: for n, m being Element of NAT st m in dom f & n in dom f & n < m holds f . n c= f . m and A2: X c= union (rng f) ; ::_thesis: ex k being Element of NAT st X c= f . k A3: now__::_thesis:_(_not_X_is_empty_implies_ex_a_being_Element_of_NAT_st_X_c=_f_._a_) deffunc H1( set ) -> Element of NAT = min* { i where i is Element of NAT : $1 in f . i } ; consider g being Function such that A4: ( dom g = X & ( for a being set st a in X holds g . a = H1(a) ) ) from FUNCT_1:sch_3(); reconsider A = rng g as finite set by A4, FINSET_1:8; A5: now__::_thesis:_for_b_being_set_st_b_in_A_holds_ b_in_NAT let b be set ; ::_thesis: ( b in A implies b in NAT ) assume b in A ; ::_thesis: b in NAT then consider a being set such that A6: ( a in dom g & g . a = b ) by FUNCT_1:def_3; b = min* { i where i is Element of NAT : a in f . i } by A4, A6; hence b in NAT ; ::_thesis: verum end; assume not X is empty ; ::_thesis: ex a being Element of NAT st X c= f . a then ex c being set st c in dom g by A4, XBOOLE_0:def_1; then reconsider A = A as non empty finite Subset of NAT by A5, FUNCT_1:3, TARSKI:def_3; union A in A by Th2; then reconsider a = union A as Element of NAT ; take a = a; ::_thesis: X c= f . a thus X c= f . a ::_thesis: verum proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in X or b in f . a ) assume A7: b in X ; ::_thesis: b in f . a then consider c being set such that A8: b in c and A9: c in rng f by A2, TARSKI:def_4; consider d being set such that A10: d in dom f and A11: f . d = c by A9, FUNCT_1:def_3; reconsider d = d as Element of NAT by A10; d in { i where i is Element of NAT : b in f . i } by A8, A11; then reconsider Y = { i where i is Element of NAT : b in f . i } as non empty set ; now__::_thesis:_for_a_being_set_st_a_in_Y_holds_ a_in_NAT let a be set ; ::_thesis: ( a in Y implies a in NAT ) assume a in Y ; ::_thesis: a in NAT then ex i being Element of NAT st ( i = a & b in f . i ) ; hence a in NAT ; ::_thesis: verum end; then reconsider Y = Y as non empty Subset of NAT by TARSKI:def_3; A12: g . b = min* Y by A4, A7; then reconsider Y9 = g . b as Element of NAT ; Y9 in Y by A12, NAT_1:def_1; then A13: ex i being Element of NAT st ( i = g . b & b in f . i ) ; A14: dom f = NAT by FUNCT_2:def_1; A15: now__::_thesis:_(_Y9_in_a_implies_b_in_f_._a_) assume Y9 in a ; ::_thesis: b in f . a then Y9 in { k where k is Element of NAT : k < a } by AXIOMS:4; then ex k being Element of NAT st ( k = Y9 & k < a ) ; then f . Y9 c= f . a by A1, A14; hence b in f . a by A13; ::_thesis: verum end; Y9 in A by A4, A7, FUNCT_1:3; hence b in f . a by A13, A15, Th2; ::_thesis: verum end; end; now__::_thesis:_(_X_is_empty_implies_ex_k_being_Element_of_NAT_ex_k_being_Element_of_NAT_st_X_c=_f_._k_) assume A16: X is empty ; ::_thesis: ex k being Element of NAT ex k being Element of NAT st X c= f . k take k = 0 ; ::_thesis: ex k being Element of NAT st X c= f . k {} c= f . k by XBOOLE_1:2; hence ex k being Element of NAT st X c= f . k by A16; ::_thesis: verum end; hence ex k being Element of NAT st X c= f . k by A3; ::_thesis: verum end; definition let Al be QC-alphabet ; let X be Subset of (CQC-WFF Al); let p be Element of CQC-WFF Al; predX |- p means :Def1: :: HENMODEL:def 1 ex f being FinSequence of CQC-WFF Al st ( rng f c= X & |- f ^ <*p*> ); end; :: deftheorem Def1 defines |- HENMODEL:def_1_:_ for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p being Element of CQC-WFF Al holds ( X |- p iff ex f being FinSequence of CQC-WFF Al st ( rng f c= X & |- f ^ <*p*> ) ); definition let Al be QC-alphabet ; let X be Subset of (CQC-WFF Al); attrX is Consistent means :Def2: :: HENMODEL:def 2 for p being Element of CQC-WFF Al holds ( not X |- p or not X |- 'not' p ); end; :: deftheorem Def2 defines Consistent HENMODEL:def_2_:_ for Al being QC-alphabet for X being Subset of (CQC-WFF Al) holds ( X is Consistent iff for p being Element of CQC-WFF Al holds ( not X |- p or not X |- 'not' p ) ); notation let Al be QC-alphabet ; let X be Subset of (CQC-WFF Al); antonym Inconsistent X for Consistent ; end; definition let Al be QC-alphabet ; let f be FinSequence of CQC-WFF Al; attrf is Consistent means :Def3: :: HENMODEL:def 3 for p being Element of CQC-WFF Al holds ( not |- f ^ <*p*> or not |- f ^ <*('not' p)*> ); end; :: deftheorem Def3 defines Consistent HENMODEL:def_3_:_ for Al being QC-alphabet for f being FinSequence of CQC-WFF Al holds ( f is Consistent iff for p being Element of CQC-WFF Al holds ( not |- f ^ <*p*> or not |- f ^ <*('not' p)*> ) ); notation let Al be QC-alphabet ; let f be FinSequence of CQC-WFF Al; antonym Inconsistent f for Consistent ; end; theorem Th4: :: HENMODEL:4 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for g being FinSequence of CQC-WFF Al st X is Consistent & rng g c= X holds g is Consistent proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) for g being FinSequence of CQC-WFF Al st X is Consistent & rng g c= X holds g is Consistent let X be Subset of (CQC-WFF Al); ::_thesis: for g being FinSequence of CQC-WFF Al st X is Consistent & rng g c= X holds g is Consistent let g be FinSequence of CQC-WFF Al; ::_thesis: ( X is Consistent & rng g c= X implies g is Consistent ) assume that A1: X is Consistent and A2: rng g c= X ; ::_thesis: g is Consistent now__::_thesis:_not_g_is_Inconsistent assume g is Inconsistent ; ::_thesis: contradiction then consider p being Element of CQC-WFF Al such that A3: ( |- g ^ <*p*> & |- g ^ <*('not' p)*> ) by Def3; ( X |- p & X |- 'not' p ) by A2, A3, Def1; hence contradiction by A1, Def2; ::_thesis: verum end; hence g is Consistent ; ::_thesis: verum end; theorem Th5: :: HENMODEL:5 for Al being QC-alphabet for p being Element of CQC-WFF Al for f, g being FinSequence of CQC-WFF Al st |- f ^ <*p*> holds |- (f ^ g) ^ <*p*> proof let Al be QC-alphabet ; ::_thesis: for p being Element of CQC-WFF Al for f, g being FinSequence of CQC-WFF Al st |- f ^ <*p*> holds |- (f ^ g) ^ <*p*> let p be Element of CQC-WFF Al; ::_thesis: for f, g being FinSequence of CQC-WFF Al st |- f ^ <*p*> holds |- (f ^ g) ^ <*p*> let f, g be FinSequence of CQC-WFF Al; ::_thesis: ( |- f ^ <*p*> implies |- (f ^ g) ^ <*p*> ) A1: ( Ant (f ^ <*p*>) = f & Ant ((f ^ g) ^ <*p*>) = f ^ g ) by CALCUL_1:5; Suc ((f ^ g) ^ <*p*>) = p by CALCUL_1:5; then A2: Suc (f ^ <*p*>) = Suc ((f ^ g) ^ <*p*>) by CALCUL_1:5; assume |- f ^ <*p*> ; ::_thesis: |- (f ^ g) ^ <*p*> hence |- (f ^ g) ^ <*p*> by A1, A2, CALCUL_1:8, CALCUL_1:36; ::_thesis: verum end; theorem Th6: :: HENMODEL:6 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) holds ( X is Inconsistent iff for p being Element of CQC-WFF Al holds X |- p ) proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) holds ( X is Inconsistent iff for p being Element of CQC-WFF Al holds X |- p ) let X be Subset of (CQC-WFF Al); ::_thesis: ( X is Inconsistent iff for p being Element of CQC-WFF Al holds X |- p ) thus ( X is Inconsistent implies for p being Element of CQC-WFF Al holds X |- p ) ::_thesis: ( ( for p being Element of CQC-WFF Al holds X |- p ) implies X is Inconsistent ) proof assume X is Inconsistent ; ::_thesis: for p being Element of CQC-WFF Al holds X |- p then consider q being Element of CQC-WFF Al such that A1: X |- q and A2: X |- 'not' q by Def2; consider f2 being FinSequence of CQC-WFF Al such that A3: rng f2 c= X and A4: |- f2 ^ <*('not' q)*> by A2, Def1; let p be Element of CQC-WFF Al; ::_thesis: X |- p consider f1 being FinSequence of CQC-WFF Al such that A5: rng f1 c= X and A6: |- f1 ^ <*q*> by A1, Def1; take f3 = f1 ^ f2; :: according to HENMODEL:def_1 ::_thesis: ( rng f3 c= X & |- f3 ^ <*p*> ) A7: rng f3 = (rng f1) \/ (rng f2) by FINSEQ_1:31; A8: |- (f1 ^ f2) ^ <*('not' q)*> by A4, CALCUL_2:20; |- (f1 ^ f2) ^ <*q*> by A6, Th5; hence ( rng f3 c= X & |- f3 ^ <*p*> ) by A5, A3, A8, A7, CALCUL_2:25, XBOOLE_1:8; ::_thesis: verum end; assume for p being Element of CQC-WFF Al holds X |- p ; ::_thesis: X is Inconsistent then ( X |- VERUM Al & X |- 'not' (VERUM Al) ) ; hence X is Inconsistent by Def2; ::_thesis: verum end; theorem Th7: :: HENMODEL:7 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) st X is Inconsistent holds ex Y being Subset of (CQC-WFF Al) st ( Y c= X & Y is finite & Y is Inconsistent ) proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) st X is Inconsistent holds ex Y being Subset of (CQC-WFF Al) st ( Y c= X & Y is finite & Y is Inconsistent ) let X be Subset of (CQC-WFF Al); ::_thesis: ( X is Inconsistent implies ex Y being Subset of (CQC-WFF Al) st ( Y c= X & Y is finite & Y is Inconsistent ) ) assume X is Inconsistent ; ::_thesis: ex Y being Subset of (CQC-WFF Al) st ( Y c= X & Y is finite & Y is Inconsistent ) then consider p being Element of CQC-WFF Al such that A1: X |- p and A2: X |- 'not' p by Def2; consider f1 being FinSequence of CQC-WFF Al such that A3: rng f1 c= X and A4: |- f1 ^ <*p*> by A1, Def1; consider f2 being FinSequence of CQC-WFF Al such that A5: rng f2 c= X and A6: |- f2 ^ <*('not' p)*> by A2, Def1; reconsider Y = rng (f1 ^ f2) as Subset of (CQC-WFF Al) ; take Y ; ::_thesis: ( Y c= X & Y is finite & Y is Inconsistent ) Y = (rng f1) \/ (rng f2) by FINSEQ_1:31; hence Y c= X by A3, A5, XBOOLE_1:8; ::_thesis: ( Y is finite & Y is Inconsistent ) |- (f1 ^ f2) ^ <*('not' p)*> by A6, CALCUL_2:20; then A7: Y |- 'not' p by Def1; |- (f1 ^ f2) ^ <*p*> by A4, Th5; then Y |- p by Def1; hence ( Y is finite & Y is Inconsistent ) by A7, Def2; ::_thesis: verum end; Lm1: for f, g being FinSequence holds Seg (len (f ^ g)) = (Seg (len f)) \/ (seq ((len f),(len g))) proof let f, g be FinSequence; ::_thesis: Seg (len (f ^ g)) = (Seg (len f)) \/ (seq ((len f),(len g))) thus Seg (len (f ^ g)) = dom (f ^ g) by FINSEQ_1:def_3 .= (dom f) \/ (seq ((len f),(len g))) by CALCUL_2:9 .= (Seg (len f)) \/ (seq ((len f),(len g))) by FINSEQ_1:def_3 ; ::_thesis: verum end; theorem :: HENMODEL:8 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p, q being Element of CQC-WFF Al st X \/ {p} |- q holds ex g being FinSequence of CQC-WFF Al st ( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) for p, q being Element of CQC-WFF Al st X \/ {p} |- q holds ex g being FinSequence of CQC-WFF Al st ( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) let X be Subset of (CQC-WFF Al); ::_thesis: for p, q being Element of CQC-WFF Al st X \/ {p} |- q holds ex g being FinSequence of CQC-WFF Al st ( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) let p, q be Element of CQC-WFF Al; ::_thesis: ( X \/ {p} |- q implies ex g being FinSequence of CQC-WFF Al st ( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) ) assume X \/ {p} |- q ; ::_thesis: ex g being FinSequence of CQC-WFF Al st ( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) then consider f being FinSequence of CQC-WFF Al such that A1: rng f c= X \/ {p} and A2: |- f ^ <*q*> by Def1; A3: now__::_thesis:_(_not_rng_f_c=_X_implies_ex_g,_g_being_FinSequence_of_CQC-WFF_Al_st_ (_rng_g_c=_X_&_|-_(g_^_<*p*>)_^_<*q*>_)_) set g = f - {p}; reconsider A = f " {p} as finite set ; reconsider B = dom f as finite set ; set n = card A; set h = (f - {p}) ^ (IdFinS (p,(card A))); A4: len (IdFinS (p,(card A))) = card A by CARD_1:def_7; A c= B by RELAT_1:132; then A5: A c= Seg (len f) by FINSEQ_1:def_3; A6: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_seq_((len_(f_-_{p})),(card_A))_holds_ i_-_(len_(f_-_{p}))_in_dom_(Sgm_A) let i be Element of NAT ; ::_thesis: ( i in seq ((len (f - {p})),(card A)) implies i - (len (f - {p})) in dom (Sgm A) ) reconsider j = i - (len (f - {p})) as Integer ; assume A7: i in seq ((len (f - {p})),(card A)) ; ::_thesis: i - (len (f - {p})) in dom (Sgm A) then A8: 1 + (len (f - {p})) <= i by CALCUL_2:1; then A9: 1 <= j by XREAL_1:19; i <= (card A) + (len (f - {p})) by A7, CALCUL_2:1; then A10: j <= card A by XREAL_1:20; 0 <= j by A8, XREAL_1:19; then reconsider j = j as Element of NAT by INT_1:3; j in Seg (card A) by A9, A10, FINSEQ_1:1; hence i - (len (f - {p})) in dom (Sgm A) by A5, FINSEQ_3:40; ::_thesis: verum end; assume not rng f c= X ; ::_thesis: ex g, g being FinSequence of CQC-WFF Al st ( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) then consider a being set such that A11: a in rng f and A12: not a in X by TARSKI:def_3; ( a in X or a in {p} ) by A1, A11, XBOOLE_0:def_3; then a = p by A12, TARSKI:def_1; then consider i being Nat such that A13: i in B and A14: f . i = p by A11, FINSEQ_2:10; reconsider C = B \ A as finite set ; defpred S1[ Nat, set ] means ( ( $1 in Seg (len (f - {p})) implies $2 = (Sgm (B \ A)) . $1 ) & ( $1 in seq ((len (f - {p})),(card A)) implies $2 = (Sgm A) . ($1 - (len (f - {p}))) ) ); A15: card C = (card B) - (card A) by CARD_2:44, RELAT_1:132 .= (card (Seg (len f))) - (card A) by FINSEQ_1:def_3 .= (len f) - (card A) by FINSEQ_1:57 .= len (f - {p}) by FINSEQ_3:59 ; A16: for k being Nat st k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) holds ex a being set st S1[k,a] proof let k be Nat; ::_thesis: ( k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) implies ex a being set st S1[k,a] ) assume k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) ; ::_thesis: ex a being set st S1[k,a] now__::_thesis:_(_k_in_Seg_(len_(f_-_{p}))_implies_ex_a_being_set_st_S1[k,a]_) assume A17: k in Seg (len (f - {p})) ; ::_thesis: ex a being set st S1[k,a] take a = (Sgm (B \ A)) . k; ::_thesis: S1[k,a] Seg (len (f - {p})) misses seq ((len (f - {p})),(card A)) by CALCUL_2:8; hence S1[k,a] by A17, XBOOLE_0:3; ::_thesis: verum end; hence ex a being set st S1[k,a] ; ::_thesis: verum end; consider F being FinSequence such that A18: ( dom F = Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) & ( for k being Nat st k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) holds S1[k,F . k] ) ) from FINSEQ_1:sch_1(A16); now__::_thesis:_for_b_being_set_st_b_in_C_holds_ b_in_Seg_(len_f) let b be set ; ::_thesis: ( b in C implies b in Seg (len f) ) assume b in C ; ::_thesis: b in Seg (len f) then b in dom f ; hence b in Seg (len f) by FINSEQ_1:def_3; ::_thesis: verum end; then A19: C c= Seg (len f) by TARSKI:def_3; then A20: dom (Sgm C) = Seg (card C) by FINSEQ_3:40; A21: rng F = B proof now__::_thesis:_for_a_being_set_st_a_in_rng_F_holds_ a_in_B let a be set ; ::_thesis: ( a in rng F implies a in B ) assume a in rng F ; ::_thesis: a in B then consider i being Nat such that A22: i in dom F and A23: F . i = a by FINSEQ_2:10; A24: now__::_thesis:_(_i_in_Seg_(len_(f_-_{p}))_implies_a_in_B_) assume i in Seg (len (f - {p})) ; ::_thesis: a in B then ( a = (Sgm C) . i & i in dom (Sgm C) ) by A18, A19, A15, A22, A23, FINSEQ_3:40; then a in rng (Sgm C) by FUNCT_1:3; then a in C by A19, FINSEQ_1:def_13; hence a in B ; ::_thesis: verum end; A25: now__::_thesis:_(_i_in_seq_((len_(f_-_{p})),(card_A))_implies_a_in_B_) A26: rng (Sgm A) = A by A5, FINSEQ_1:def_13; A27: A c= B by RELAT_1:132; assume A28: i in seq ((len (f - {p})),(card A)) ; ::_thesis: a in B then a = (Sgm A) . (i - (len (f - {p}))) by A18, A22, A23; then a in A by A6, A28, A26, FUNCT_1:3; hence a in B by A27; ::_thesis: verum end; i in (Seg (len (f - {p}))) \/ (seq ((len (f - {p})),(card A))) by A4, A18, A22, Lm1; hence a in B by A24, A25, XBOOLE_0:def_3; ::_thesis: verum end; hence rng F c= B by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: B c= rng F let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B or a in rng F ) assume A29: a in B ; ::_thesis: a in rng F A30: now__::_thesis:_(_not_a_in_A_implies_a_in_rng_F_) now__::_thesis:_for_b_being_set_st_b_in_C_holds_ b_in_Seg_(len_f) let b be set ; ::_thesis: ( b in C implies b in Seg (len f) ) assume b in C ; ::_thesis: b in Seg (len f) then b in dom f ; hence b in Seg (len f) by FINSEQ_1:def_3; ::_thesis: verum end; then A31: C c= Seg (len f) by TARSKI:def_3; assume not a in A ; ::_thesis: a in rng F then a in C by A29, XBOOLE_0:def_5; then a in rng (Sgm C) by A31, FINSEQ_1:def_13; then consider i being Nat such that A32: i in dom (Sgm C) and A33: (Sgm C) . i = a by FINSEQ_2:10; A34: 1 <= i by A32, FINSEQ_3:25; len (Sgm C) = len (f - {p}) by A20, A15, FINSEQ_1:def_3; then A35: i <= len (f - {p}) by A32, FINSEQ_3:25; len (f - {p}) <= len ((f - {p}) ^ (IdFinS (p,(card A)))) by CALCUL_1:6; then i <= len ((f - {p}) ^ (IdFinS (p,(card A)))) by A35, XXREAL_0:2; then A36: i in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) by A34, FINSEQ_1:1; i in Seg (len (f - {p})) by A34, A35, FINSEQ_1:1; then a = F . i by A18, A33, A36; hence a in rng F by A18, A36, FUNCT_1:3; ::_thesis: verum end; now__::_thesis:_(_a_in_A_implies_a_in_rng_F_) assume A37: a in A ; ::_thesis: a in rng F rng (Sgm A) = A by A5, FINSEQ_1:def_13; then consider i being Nat such that A38: i in dom (Sgm A) and A39: (Sgm A) . i = a by A37, FINSEQ_2:10; reconsider i = i as Element of NAT by ORDINAL1:def_12; set m = i + (len (f - {p})); len (Sgm A) = card A by A5, FINSEQ_3:39; then i <= card A by A38, FINSEQ_3:25; then A40: i + (len (f - {p})) <= (card A) + (len (f - {p})) by XREAL_1:6; then i + (len (f - {p})) <= (len (f - {p})) + (len (IdFinS (p,(card A)))) by CARD_1:def_7; then A41: i + (len (f - {p})) <= len ((f - {p}) ^ (IdFinS (p,(card A)))) by FINSEQ_1:22; A42: 1 <= i by A38, FINSEQ_3:25; then 1 + (len (f - {p})) <= i + (len (f - {p})) by XREAL_1:6; then A43: i + (len (f - {p})) in seq ((len (f - {p})),(card A)) by A40, CALCUL_2:1; i <= i + (len (f - {p})) by NAT_1:11; then 1 <= i + (len (f - {p})) by A42, XXREAL_0:2; then i + (len (f - {p})) in dom ((f - {p}) ^ (IdFinS (p,(card A)))) by A41, FINSEQ_3:25; then A44: i + (len (f - {p})) in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) by FINSEQ_1:def_3; a = (Sgm A) . ((i + (len (f - {p}))) - (len (f - {p}))) by A39; then a = F . (i + (len (f - {p}))) by A18, A43, A44; hence a in rng F by A18, A44, FUNCT_1:3; ::_thesis: verum end; hence a in rng F by A30; ::_thesis: verum end; A45: len ((f - {p}) ^ (IdFinS (p,(card A)))) = (len (f - {p})) + (len (IdFinS (p,(card A)))) by FINSEQ_1:22 .= ((len f) - (card A)) + (len (IdFinS (p,(card A)))) by FINSEQ_3:59 .= ((len f) - (card A)) + (card A) by CARD_1:def_7 .= len f ; then A46: dom F = B by A18, FINSEQ_1:def_3; then reconsider F = F as Relation of B,B by A21, RELSET_1:4; rng F c= B ; then reconsider F = F as Function of B,B by A46, FUNCT_2:2; F is one-to-one proof let a1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not a1 in dom F or not b1 in dom F or not F . a1 = F . b1 or a1 = b1 ) let a2 be set ; ::_thesis: ( not a1 in dom F or not a2 in dom F or not F . a1 = F . a2 or a1 = a2 ) assume that A47: a1 in dom F and A48: a2 in dom F and A49: F . a1 = F . a2 ; ::_thesis: a1 = a2 A50: a2 in (Seg (len (f - {p}))) \/ (seq ((len (f - {p})),(card A))) by A4, A18, A48, Lm1; A51: now__::_thesis:_(_a1_in_Seg_(len_(f_-_{p}))_implies_a1_=_a2_) assume A52: a1 in Seg (len (f - {p})) ; ::_thesis: a1 = a2 then A53: a1 in dom (Sgm C) by A19, A15, FINSEQ_3:40; F . a1 = (Sgm C) . a1 by A18, A47, A52; then F . a1 in rng (Sgm C) by A53, FUNCT_1:3; then A54: F . a1 in C by A19, FINSEQ_1:def_13; A55: now__::_thesis:_not_a2_in_seq_((len_(f_-_{p})),(card_A)) assume A56: a2 in seq ((len (f - {p})),(card A)) ; ::_thesis: contradiction then reconsider i = a2 as Element of NAT ; (Sgm A) . (i - (len (f - {p}))) in rng (Sgm A) by A6, A56, FUNCT_1:3; then F . a2 in rng (Sgm A) by A18, A48, A56; then F . a2 in A by A5, FINSEQ_1:def_13; hence contradiction by A49, A54, XBOOLE_0:def_5; ::_thesis: verum end; now__::_thesis:_(_a2_in_Seg_(len_(f_-_{p}))_implies_a1_=_a2_) assume A57: a2 in Seg (len (f - {p})) ; ::_thesis: a1 = a2 then F . a2 = (Sgm C) . a2 by A18, A48; then A58: (Sgm C) . a1 = (Sgm C) . a2 by A18, A47, A49, A52; A59: Sgm C is one-to-one by A19, FINSEQ_3:92; a2 in dom (Sgm C) by A19, A15, A57, FINSEQ_3:40; hence a1 = a2 by A53, A58, A59, FUNCT_1:def_4; ::_thesis: verum end; hence a1 = a2 by A50, A55, XBOOLE_0:def_3; ::_thesis: verum end; A60: now__::_thesis:_(_a1_in_seq_((len_(f_-_{p})),(card_A))_implies_a1_=_a2_) assume A61: a1 in seq ((len (f - {p})),(card A)) ; ::_thesis: a1 = a2 then reconsider i = a1 as Element of NAT ; A62: i - (len (f - {p})) in dom (Sgm A) by A6, A61; A63: now__::_thesis:_(_a2_in_seq_((len_(f_-_{p})),(card_A))_implies_a1_=_a2_) assume A64: a2 in seq ((len (f - {p})),(card A)) ; ::_thesis: a1 = a2 then reconsider i1 = a2 as Element of NAT ; F . a2 = (Sgm A) . (i1 - (len (f - {p}))) by A18, A48, A64; then A65: (Sgm A) . (i1 - (len (f - {p}))) = (Sgm A) . (i - (len (f - {p}))) by A18, A47, A49, A61; A66: Sgm A is one-to-one by A5, FINSEQ_3:92; i1 - (len (f - {p})) in dom (Sgm A) by A6, A64; then (i1 - (len (f - {p}))) + (len (f - {p})) = (i - (len (f - {p}))) + (len (f - {p})) by A62, A65, A66, FUNCT_1:def_4; hence a1 = a2 ; ::_thesis: verum end; (Sgm A) . (i - (len (f - {p}))) in rng (Sgm A) by A6, A61, FUNCT_1:3; then F . a1 in rng (Sgm A) by A18, A47, A61; then A67: F . a1 in A by A5, FINSEQ_1:def_13; now__::_thesis:_not_a2_in_Seg_(len_(f_-_{p})) assume a2 in Seg (len (f - {p})) ; ::_thesis: contradiction then ( F . a2 = (Sgm C) . a2 & a2 in dom (Sgm C) ) by A18, A19, A15, A48, FINSEQ_3:40; then F . a2 in rng (Sgm C) by FUNCT_1:3; then F . a2 in C by A19, FINSEQ_1:def_13; hence contradiction by A49, A67, XBOOLE_0:def_5; ::_thesis: verum end; hence a1 = a2 by A50, A63, XBOOLE_0:def_3; ::_thesis: verum end; a1 in (Seg (len (f - {p}))) \/ (seq ((len (f - {p})),(card A))) by A4, A18, A47, Lm1; hence a1 = a2 by A51, A60, XBOOLE_0:def_3; ::_thesis: verum end; then reconsider F = F as Permutation of (dom f) by A21, FUNCT_2:57; consider j being Nat such that A68: j in dom F and A69: F . j = i by A21, A13, FINSEQ_2:10; A70: dom (Per (f,F)) = B by CALCUL_2:19 .= dom F by A18, A45, FINSEQ_1:def_3 .= dom ((f - {p}) ^ (IdFinS (p,(card A)))) by A18, FINSEQ_1:def_3 ; A71: now__::_thesis:_for_k_being_Nat_st_k_in_dom_((f_-_{p})_^_(IdFinS_(p,(card_A))))_holds_ (Per_(f,F))_._k_=_((f_-_{p})_^_(IdFinS_(p,(card_A))))_._k let k be Nat; ::_thesis: ( k in dom ((f - {p}) ^ (IdFinS (p,(card A)))) implies (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k ) assume A72: k in dom ((f - {p}) ^ (IdFinS (p,(card A)))) ; ::_thesis: (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k A73: k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) by A72, FINSEQ_1:def_3; A74: now__::_thesis:_(_ex_i_being_Nat_st_ (_i_in_dom_(IdFinS_(p,(card_A)))_&_k_=_(len_(f_-_{p}))_+_i_)_implies_(Per_(f,F))_._k_=_((f_-_{p})_^_(IdFinS_(p,(card_A))))_._k_) A75: k in dom (F * f) by A70, A72, CALCUL_2:def_2; given i being Nat such that A76: i in dom (IdFinS (p,(card A))) and A77: k = (len (f - {p})) + i ; ::_thesis: (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k len (IdFinS (p,(card A))) = card A by CARD_1:def_7; then A78: i <= card A by A76, FINSEQ_3:25; then A79: k <= (card A) + (len (f - {p})) by A77, XREAL_1:6; A80: 1 <= i by A76, FINSEQ_3:25; then 1 + (len (f - {p})) <= k by A77, XREAL_1:6; then A81: k in seq ((len (f - {p})),(card A)) by A79, CALCUL_2:1; then F . k = (Sgm A) . (k - (len (f - {p}))) by A18, A73; then F . k in rng (Sgm A) by A6, A81, FUNCT_1:3; then F . k in A by A5, FINSEQ_1:def_13; then f . (F . k) in {p} by FUNCT_1:def_7; then f . (F . k) = p by TARSKI:def_1; then (F * f) . k = p by A75, FUNCT_1:12; then A82: (Per (f,F)) . k = p by CALCUL_2:def_2; i in Seg (card A) by A80, A78, FINSEQ_1:1; hence (Per (f,F)) . k = (IdFinS (p,(card A))) . i by A82, FUNCOP_1:7 .= ((f - {p}) ^ (IdFinS (p,(card A)))) . k by A76, A77, FINSEQ_1:def_7 ; ::_thesis: verum end; now__::_thesis:_(_k_in_dom_(f_-_{p})_implies_(Per_(f,F))_._k_=_((f_-_{p})_^_(IdFinS_(p,(card_A))))_._k_) assume A83: k in dom (f - {p}) ; ::_thesis: (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k then A84: k in dom (Sgm C) by A20, A15, FINSEQ_1:def_3; k in Seg (len (f - {p})) by A83, FINSEQ_1:def_3; then A85: F . k = (Sgm C) . k by A18, A73; k in dom (F * f) by A70, A72, CALCUL_2:def_2; then (F * f) . k = f . ((Sgm C) . k) by A85, FUNCT_1:12; hence (Per (f,F)) . k = f . ((Sgm C) . k) by CALCUL_2:def_2 .= ((Sgm C) * f) . k by A84, FUNCT_1:13 .= (f - {p}) . k by FINSEQ_3:def_1 .= ((f - {p}) ^ (IdFinS (p,(card A)))) . k by A83, FINSEQ_1:def_7 ; ::_thesis: verum end; hence (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k by A72, A74, FINSEQ_1:25; ::_thesis: verum end; then A86: Per (f,F) = (f - {p}) ^ (IdFinS (p,(card A))) by A70, FINSEQ_1:13; reconsider h = (f - {p}) ^ (IdFinS (p,(card A))) as FinSequence of CQC-WFF Al by A70, A71, FINSEQ_1:13; (F * f) . j = p by A14, A68, A69, FUNCT_1:13; then A87: h . j = p by A86, CALCUL_2:def_2; A88: now__::_thesis:_not_j_in_dom_(f_-_{p}) assume A89: j in dom (f - {p}) ; ::_thesis: contradiction then (f - {p}) . j = p by A87, FINSEQ_1:def_7; then A90: (f - {p}) . j in {p} by TARSKI:def_1; A91: rng (f - {p}) = (rng f) \ {p} by FINSEQ_3:65; (f - {p}) . j in rng (f - {p}) by A89, FUNCT_1:3; hence contradiction by A90, A91, XBOOLE_0:def_5; ::_thesis: verum end; j in dom f by A68; then j in dom h by A70, CALCUL_2:19; then consider k being Nat such that A92: k in dom (IdFinS (p,(card A))) and j = (len (f - {p})) + k by A88, FINSEQ_1:25; reconsider g = f - {p} as FinSequence of CQC-WFF Al by FINSEQ_3:86; ( 1 <= k & k <= len (IdFinS (p,(card A))) ) by A92, FINSEQ_3:25; then 1 <= len (IdFinS (p,(card A))) by XXREAL_0:2; then A93: 1 <= card A by CARD_1:def_7; |- h ^ <*q*> by A2, A86, CALCUL_2:30; then A94: |- (g ^ <*p*>) ^ <*q*> by A93, CALCUL_2:32; take g = g; ::_thesis: ex g being FinSequence of CQC-WFF Al st ( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) ( rng g = (rng f) \ {p} & (rng f) \ {p} c= (X \/ {p}) \ {p} ) by A1, FINSEQ_3:65, XBOOLE_1:33; then A95: rng g c= X \ {p} by XBOOLE_1:40; X \ {p} c= X by XBOOLE_1:36; hence ex g being FinSequence of CQC-WFF Al st ( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) by A94, A95, XBOOLE_1:1; ::_thesis: verum end; now__::_thesis:_(_rng_f_c=_X_implies_ex_f,_g_being_FinSequence_of_CQC-WFF_Al_st_ (_rng_g_c=_X_&_|-_(g_^_<*p*>)_^_<*q*>_)_) assume A96: rng f c= X ; ::_thesis: ex f, g being FinSequence of CQC-WFF Al st ( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) take f = f; ::_thesis: ex g being FinSequence of CQC-WFF Al st ( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) |- (f ^ <*p*>) ^ <*q*> by A2, Th5; hence ex g being FinSequence of CQC-WFF Al st ( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) by A96; ::_thesis: verum end; hence ex g being FinSequence of CQC-WFF Al st ( rng g c= X & |- (g ^ <*p*>) ^ <*q*> ) by A3; ::_thesis: verum end; theorem :: HENMODEL:9 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p being Element of CQC-WFF Al holds ( X |- p iff X \/ {('not' p)} is Inconsistent ) proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) for p being Element of CQC-WFF Al holds ( X |- p iff X \/ {('not' p)} is Inconsistent ) let X be Subset of (CQC-WFF Al); ::_thesis: for p being Element of CQC-WFF Al holds ( X |- p iff X \/ {('not' p)} is Inconsistent ) let p be Element of CQC-WFF Al; ::_thesis: ( X |- p iff X \/ {('not' p)} is Inconsistent ) thus ( X |- p implies X \/ {('not' p)} is Inconsistent ) ::_thesis: ( X \/ {('not' p)} is Inconsistent implies X |- p ) proof assume X |- p ; ::_thesis: X \/ {('not' p)} is Inconsistent then consider f being FinSequence of CQC-WFF Al such that A1: rng f c= X and A2: |- f ^ <*p*> by Def1; set f2 = f ^ <*('not' p)*>; set f1 = (f ^ <*('not' p)*>) ^ <*('not' p)*>; A3: Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>) = f ^ <*('not' p)*> by CALCUL_1:5; 1 in Seg 1 by FINSEQ_1:1; then 1 in dom <*('not' p)*> by FINSEQ_1:38; then A4: (len f) + 1 in dom (Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>)) by A3, FINSEQ_1:28; Suc ((f ^ <*('not' p)*>) ^ <*('not' p)*>) = 'not' p by CALCUL_1:5; then (Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>)) . ((len f) + 1) = Suc ((f ^ <*('not' p)*>) ^ <*('not' p)*>) by A3, FINSEQ_1:42; then Suc ((f ^ <*('not' p)*>) ^ <*('not' p)*>) is_tail_of Ant ((f ^ <*('not' p)*>) ^ <*('not' p)*>) by A4, CALCUL_1:def_16; then A5: |- (f ^ <*('not' p)*>) ^ <*('not' p)*> by CALCUL_1:33; A6: 0 + 1 <= len (f ^ <*('not' p)*>) by CALCUL_1:10; ( Ant (f ^ <*('not' p)*>) = f & Suc (f ^ <*('not' p)*>) = 'not' p ) by CALCUL_1:5; then A7: rng (f ^ <*('not' p)*>) = (rng f) \/ {('not' p)} by A6, CALCUL_1:3; |- (f ^ <*('not' p)*>) ^ <*p*> by A2, Th5; then not f ^ <*('not' p)*> is Consistent by A5, Def3; hence X \/ {('not' p)} is Inconsistent by A1, A7, Th4, XBOOLE_1:9; ::_thesis: verum end; thus ( X \/ {('not' p)} is Inconsistent implies X |- p ) ::_thesis: verum proof assume X \/ {('not' p)} is Inconsistent ; ::_thesis: X |- p then X \/ {('not' p)} |- p by Th6; then consider f being FinSequence of CQC-WFF Al such that A8: rng f c= X \/ {('not' p)} and A9: |- f ^ <*p*> by Def1; now__::_thesis:_(_not_rng_f_c=_X_implies_X_|-_p_) set g = f - {('not' p)}; reconsider A = f " {('not' p)} as finite set ; reconsider B = dom f as finite set ; set n = card A; set h = (f - {('not' p)}) ^ (IdFinS (('not' p),(card A))); A10: len (IdFinS (('not' p),(card A))) = card A by CARD_1:def_7; A c= B by RELAT_1:132; then A11: A c= Seg (len f) by FINSEQ_1:def_3; A12: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_seq_((len_(f_-_{('not'_p)})),(card_A))_holds_ i_-_(len_(f_-_{('not'_p)}))_in_dom_(Sgm_A) let i be Element of NAT ; ::_thesis: ( i in seq ((len (f - {('not' p)})),(card A)) implies i - (len (f - {('not' p)})) in dom (Sgm A) ) reconsider j = i - (len (f - {('not' p)})) as Integer ; assume A13: i in seq ((len (f - {('not' p)})),(card A)) ; ::_thesis: i - (len (f - {('not' p)})) in dom (Sgm A) then A14: 1 + (len (f - {('not' p)})) <= i by CALCUL_2:1; then A15: 1 <= j by XREAL_1:19; i <= (card A) + (len (f - {('not' p)})) by A13, CALCUL_2:1; then A16: j <= card A by XREAL_1:20; 0 <= j by A14, XREAL_1:19; then reconsider j = j as Element of NAT by INT_1:3; j in Seg (card A) by A15, A16, FINSEQ_1:1; hence i - (len (f - {('not' p)})) in dom (Sgm A) by A11, FINSEQ_3:40; ::_thesis: verum end; assume not rng f c= X ; ::_thesis: X |- p then consider a being set such that A17: a in rng f and A18: not a in X by TARSKI:def_3; ( a in X or a in {('not' p)} ) by A8, A17, XBOOLE_0:def_3; then a = 'not' p by A18, TARSKI:def_1; then consider i being Nat such that A19: i in B and A20: f . i = 'not' p by A17, FINSEQ_2:10; reconsider C = B \ A as finite set ; defpred S1[ Nat, set ] means ( ( $1 in Seg (len (f - {('not' p)})) implies $2 = (Sgm (B \ A)) . $1 ) & ( $1 in seq ((len (f - {('not' p)})),(card A)) implies $2 = (Sgm A) . ($1 - (len (f - {('not' p)}))) ) ); A21: card C = (card B) - (card A) by CARD_2:44, RELAT_1:132 .= (card (Seg (len f))) - (card A) by FINSEQ_1:def_3 .= (len f) - (card A) by FINSEQ_1:57 .= len (f - {('not' p)}) by FINSEQ_3:59 ; A22: for k being Nat st k in Seg (len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A))))) holds ex a being set st S1[k,a] proof let k be Nat; ::_thesis: ( k in Seg (len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A))))) implies ex a being set st S1[k,a] ) assume k in Seg (len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A))))) ; ::_thesis: ex a being set st S1[k,a] now__::_thesis:_(_k_in_Seg_(len_(f_-_{('not'_p)}))_implies_ex_a_being_set_st_S1[k,a]_) assume A23: k in Seg (len (f - {('not' p)})) ; ::_thesis: ex a being set st S1[k,a] take a = (Sgm (B \ A)) . k; ::_thesis: S1[k,a] Seg (len (f - {('not' p)})) misses seq ((len (f - {('not' p)})),(card A)) by CALCUL_2:8; hence S1[k,a] by A23, XBOOLE_0:3; ::_thesis: verum end; hence ex a being set st S1[k,a] ; ::_thesis: verum end; consider F being FinSequence such that A24: ( dom F = Seg (len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A))))) & ( for k being Nat st k in Seg (len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A))))) holds S1[k,F . k] ) ) from FINSEQ_1:sch_1(A22); now__::_thesis:_for_b_being_set_st_b_in_C_holds_ b_in_Seg_(len_f) let b be set ; ::_thesis: ( b in C implies b in Seg (len f) ) assume b in C ; ::_thesis: b in Seg (len f) then b in dom f ; hence b in Seg (len f) by FINSEQ_1:def_3; ::_thesis: verum end; then A25: C c= Seg (len f) by TARSKI:def_3; then A26: dom (Sgm C) = Seg (card C) by FINSEQ_3:40; A27: rng F = B proof now__::_thesis:_for_a_being_set_st_a_in_rng_F_holds_ a_in_B let a be set ; ::_thesis: ( a in rng F implies a in B ) assume a in rng F ; ::_thesis: a in B then consider i being Nat such that A28: i in dom F and A29: F . i = a by FINSEQ_2:10; A30: now__::_thesis:_(_i_in_Seg_(len_(f_-_{('not'_p)}))_implies_a_in_B_) assume i in Seg (len (f - {('not' p)})) ; ::_thesis: a in B then ( a = (Sgm C) . i & i in dom (Sgm C) ) by A24, A25, A21, A28, A29, FINSEQ_3:40; then a in rng (Sgm C) by FUNCT_1:3; then a in C by A25, FINSEQ_1:def_13; hence a in B ; ::_thesis: verum end; A31: now__::_thesis:_(_i_in_seq_((len_(f_-_{('not'_p)})),(card_A))_implies_a_in_B_) A32: rng (Sgm A) = A by A11, FINSEQ_1:def_13; A33: A c= B by RELAT_1:132; assume A34: i in seq ((len (f - {('not' p)})),(card A)) ; ::_thesis: a in B then a = (Sgm A) . (i - (len (f - {('not' p)}))) by A24, A28, A29; then a in A by A12, A34, A32, FUNCT_1:3; hence a in B by A33; ::_thesis: verum end; i in (Seg (len (f - {('not' p)}))) \/ (seq ((len (f - {('not' p)})),(card A))) by A10, A24, A28, Lm1; hence a in B by A30, A31, XBOOLE_0:def_3; ::_thesis: verum end; hence rng F c= B by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: B c= rng F let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B or a in rng F ) assume A35: a in B ; ::_thesis: a in rng F A36: now__::_thesis:_(_not_a_in_A_implies_a_in_rng_F_) now__::_thesis:_for_b_being_set_st_b_in_C_holds_ b_in_Seg_(len_f) let b be set ; ::_thesis: ( b in C implies b in Seg (len f) ) assume b in C ; ::_thesis: b in Seg (len f) then b in dom f ; hence b in Seg (len f) by FINSEQ_1:def_3; ::_thesis: verum end; then A37: C c= Seg (len f) by TARSKI:def_3; assume not a in A ; ::_thesis: a in rng F then a in C by A35, XBOOLE_0:def_5; then a in rng (Sgm C) by A37, FINSEQ_1:def_13; then consider i being Nat such that A38: i in dom (Sgm C) and A39: (Sgm C) . i = a by FINSEQ_2:10; A40: 1 <= i by A38, FINSEQ_3:25; len (Sgm C) = len (f - {('not' p)}) by A26, A21, FINSEQ_1:def_3; then A41: i <= len (f - {('not' p)}) by A38, FINSEQ_3:25; len (f - {('not' p)}) <= len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) by CALCUL_1:6; then i <= len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) by A41, XXREAL_0:2; then A42: i in Seg (len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A))))) by A40, FINSEQ_1:1; i in Seg (len (f - {('not' p)})) by A40, A41, FINSEQ_1:1; then a = F . i by A24, A39, A42; hence a in rng F by A24, A42, FUNCT_1:3; ::_thesis: verum end; now__::_thesis:_(_a_in_A_implies_a_in_rng_F_) assume A43: a in A ; ::_thesis: a in rng F rng (Sgm A) = A by A11, FINSEQ_1:def_13; then consider i being Nat such that A44: i in dom (Sgm A) and A45: (Sgm A) . i = a by A43, FINSEQ_2:10; reconsider i = i as Element of NAT by ORDINAL1:def_12; set m = i + (len (f - {('not' p)})); len (Sgm A) = card A by A11, FINSEQ_3:39; then i <= card A by A44, FINSEQ_3:25; then A46: i + (len (f - {('not' p)})) <= (card A) + (len (f - {('not' p)})) by XREAL_1:6; then i + (len (f - {('not' p)})) <= (len (f - {('not' p)})) + (len (IdFinS (('not' p),(card A)))) by CARD_1:def_7; then A47: i + (len (f - {('not' p)})) <= len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) by FINSEQ_1:22; A48: 1 <= i by A44, FINSEQ_3:25; then 1 + (len (f - {('not' p)})) <= i + (len (f - {('not' p)})) by XREAL_1:6; then A49: i + (len (f - {('not' p)})) in seq ((len (f - {('not' p)})),(card A)) by A46, CALCUL_2:1; i <= i + (len (f - {('not' p)})) by NAT_1:11; then 1 <= i + (len (f - {('not' p)})) by A48, XXREAL_0:2; then i + (len (f - {('not' p)})) in dom ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) by A47, FINSEQ_3:25; then A50: i + (len (f - {('not' p)})) in Seg (len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A))))) by FINSEQ_1:def_3; a = (Sgm A) . ((i + (len (f - {('not' p)}))) - (len (f - {('not' p)}))) by A45; then a = F . (i + (len (f - {('not' p)}))) by A24, A49, A50; hence a in rng F by A24, A50, FUNCT_1:3; ::_thesis: verum end; hence a in rng F by A36; ::_thesis: verum end; A51: len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) = (len (f - {('not' p)})) + (len (IdFinS (('not' p),(card A)))) by FINSEQ_1:22 .= ((len f) - (card A)) + (len (IdFinS (('not' p),(card A)))) by FINSEQ_3:59 .= ((len f) - (card A)) + (card A) by CARD_1:def_7 .= len f ; then A52: dom F = B by A24, FINSEQ_1:def_3; then reconsider F = F as Relation of B,B by A27, RELSET_1:4; rng F c= B ; then reconsider F = F as Function of B,B by A52, FUNCT_2:2; F is one-to-one proof let a1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not a1 in dom F or not b1 in dom F or not F . a1 = F . b1 or a1 = b1 ) let a2 be set ; ::_thesis: ( not a1 in dom F or not a2 in dom F or not F . a1 = F . a2 or a1 = a2 ) assume that A53: a1 in dom F and A54: a2 in dom F and A55: F . a1 = F . a2 ; ::_thesis: a1 = a2 A56: a2 in (Seg (len (f - {('not' p)}))) \/ (seq ((len (f - {('not' p)})),(card A))) by A10, A24, A54, Lm1; A57: now__::_thesis:_(_a1_in_Seg_(len_(f_-_{('not'_p)}))_implies_a1_=_a2_) assume A58: a1 in Seg (len (f - {('not' p)})) ; ::_thesis: a1 = a2 then A59: a1 in dom (Sgm C) by A25, A21, FINSEQ_3:40; F . a1 = (Sgm C) . a1 by A24, A53, A58; then F . a1 in rng (Sgm C) by A59, FUNCT_1:3; then A60: F . a1 in C by A25, FINSEQ_1:def_13; A61: now__::_thesis:_not_a2_in_seq_((len_(f_-_{('not'_p)})),(card_A)) assume A62: a2 in seq ((len (f - {('not' p)})),(card A)) ; ::_thesis: contradiction then reconsider i = a2 as Element of NAT ; (Sgm A) . (i - (len (f - {('not' p)}))) in rng (Sgm A) by A12, A62, FUNCT_1:3; then F . a2 in rng (Sgm A) by A24, A54, A62; then F . a2 in A by A11, FINSEQ_1:def_13; hence contradiction by A55, A60, XBOOLE_0:def_5; ::_thesis: verum end; now__::_thesis:_(_a2_in_Seg_(len_(f_-_{('not'_p)}))_implies_a1_=_a2_) assume A63: a2 in Seg (len (f - {('not' p)})) ; ::_thesis: a1 = a2 then F . a2 = (Sgm C) . a2 by A24, A54; then A64: (Sgm C) . a1 = (Sgm C) . a2 by A24, A53, A55, A58; A65: Sgm C is one-to-one by A25, FINSEQ_3:92; a2 in dom (Sgm C) by A25, A21, A63, FINSEQ_3:40; hence a1 = a2 by A59, A64, A65, FUNCT_1:def_4; ::_thesis: verum end; hence a1 = a2 by A56, A61, XBOOLE_0:def_3; ::_thesis: verum end; A66: now__::_thesis:_(_a1_in_seq_((len_(f_-_{('not'_p)})),(card_A))_implies_a1_=_a2_) assume A67: a1 in seq ((len (f - {('not' p)})),(card A)) ; ::_thesis: a1 = a2 then reconsider i = a1 as Element of NAT ; A68: i - (len (f - {('not' p)})) in dom (Sgm A) by A12, A67; A69: now__::_thesis:_(_a2_in_seq_((len_(f_-_{('not'_p)})),(card_A))_implies_a1_=_a2_) assume A70: a2 in seq ((len (f - {('not' p)})),(card A)) ; ::_thesis: a1 = a2 then reconsider i1 = a2 as Element of NAT ; F . a2 = (Sgm A) . (i1 - (len (f - {('not' p)}))) by A24, A54, A70; then A71: (Sgm A) . (i1 - (len (f - {('not' p)}))) = (Sgm A) . (i - (len (f - {('not' p)}))) by A24, A53, A55, A67; A72: Sgm A is one-to-one by A11, FINSEQ_3:92; i1 - (len (f - {('not' p)})) in dom (Sgm A) by A12, A70; then i1 - (len (f - {('not' p)})) = i - (len (f - {('not' p)})) by A68, A71, A72, FUNCT_1:def_4; hence a1 = a2 ; ::_thesis: verum end; (Sgm A) . (i - (len (f - {('not' p)}))) in rng (Sgm A) by A12, A67, FUNCT_1:3; then F . a1 in rng (Sgm A) by A24, A53, A67; then A73: F . a1 in A by A11, FINSEQ_1:def_13; now__::_thesis:_not_a2_in_Seg_(len_(f_-_{('not'_p)})) assume a2 in Seg (len (f - {('not' p)})) ; ::_thesis: contradiction then ( F . a2 = (Sgm C) . a2 & a2 in dom (Sgm C) ) by A24, A25, A21, A54, FINSEQ_3:40; then F . a2 in rng (Sgm C) by FUNCT_1:3; then F . a2 in C by A25, FINSEQ_1:def_13; hence contradiction by A55, A73, XBOOLE_0:def_5; ::_thesis: verum end; hence a1 = a2 by A56, A69, XBOOLE_0:def_3; ::_thesis: verum end; a1 in (Seg (len (f - {('not' p)}))) \/ (seq ((len (f - {('not' p)})),(card A))) by A10, A24, A53, Lm1; hence a1 = a2 by A57, A66, XBOOLE_0:def_3; ::_thesis: verum end; then reconsider F = F as Permutation of (dom f) by A27, FUNCT_2:57; consider j being Nat such that A74: j in dom F and A75: F . j = i by A27, A19, FINSEQ_2:10; A76: dom (Per (f,F)) = B by CALCUL_2:19 .= dom F by A24, A51, FINSEQ_1:def_3 .= dom ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) by A24, FINSEQ_1:def_3 ; A77: now__::_thesis:_for_k_being_Nat_st_k_in_dom_((f_-_{('not'_p)})_^_(IdFinS_(('not'_p),(card_A))))_holds_ (Per_(f,F))_._k_=_((f_-_{('not'_p)})_^_(IdFinS_(('not'_p),(card_A))))_._k let k be Nat; ::_thesis: ( k in dom ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) implies (Per (f,F)) . k = ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) . k ) assume A78: k in dom ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) ; ::_thesis: (Per (f,F)) . k = ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) . k A79: k in Seg (len ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A))))) by A78, FINSEQ_1:def_3; A80: now__::_thesis:_(_ex_i_being_Nat_st_ (_i_in_dom_(IdFinS_(('not'_p),(card_A)))_&_k_=_(len_(f_-_{('not'_p)}))_+_i_)_implies_(Per_(f,F))_._k_=_((f_-_{('not'_p)})_^_(IdFinS_(('not'_p),(card_A))))_._k_) A81: k in dom (F * f) by A76, A78, CALCUL_2:def_2; given i being Nat such that A82: i in dom (IdFinS (('not' p),(card A))) and A83: k = (len (f - {('not' p)})) + i ; ::_thesis: (Per (f,F)) . k = ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) . k len (IdFinS (('not' p),(card A))) = card A by CARD_1:def_7; then A84: i <= card A by A82, FINSEQ_3:25; then A85: k <= (card A) + (len (f - {('not' p)})) by A83, XREAL_1:6; A86: 1 <= i by A82, FINSEQ_3:25; then 1 + (len (f - {('not' p)})) <= k by A83, XREAL_1:6; then A87: k in seq ((len (f - {('not' p)})),(card A)) by A85, CALCUL_2:1; then F . k = (Sgm A) . (k - (len (f - {('not' p)}))) by A24, A79; then F . k in rng (Sgm A) by A12, A87, FUNCT_1:3; then F . k in A by A11, FINSEQ_1:def_13; then f . (F . k) in {('not' p)} by FUNCT_1:def_7; then f . (F . k) = 'not' p by TARSKI:def_1; then (F * f) . k = 'not' p by A81, FUNCT_1:12; then A88: (Per (f,F)) . k = 'not' p by CALCUL_2:def_2; i in Seg (card A) by A86, A84, FINSEQ_1:1; hence (Per (f,F)) . k = (IdFinS (('not' p),(card A))) . i by A88, FUNCOP_1:7 .= ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) . k by A82, A83, FINSEQ_1:def_7 ; ::_thesis: verum end; now__::_thesis:_(_k_in_dom_(f_-_{('not'_p)})_implies_(Per_(f,F))_._k_=_((f_-_{('not'_p)})_^_(IdFinS_(('not'_p),(card_A))))_._k_) assume A89: k in dom (f - {('not' p)}) ; ::_thesis: (Per (f,F)) . k = ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) . k then A90: k in dom (Sgm C) by A26, A21, FINSEQ_1:def_3; k in Seg (len (f - {('not' p)})) by A89, FINSEQ_1:def_3; then A91: F . k = (Sgm C) . k by A24, A79; k in dom (F * f) by A76, A78, CALCUL_2:def_2; then (F * f) . k = f . ((Sgm C) . k) by A91, FUNCT_1:12; hence (Per (f,F)) . k = f . ((Sgm C) . k) by CALCUL_2:def_2 .= ((Sgm C) * f) . k by A90, FUNCT_1:13 .= (f - {('not' p)}) . k by FINSEQ_3:def_1 .= ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) . k by A89, FINSEQ_1:def_7 ; ::_thesis: verum end; hence (Per (f,F)) . k = ((f - {('not' p)}) ^ (IdFinS (('not' p),(card A)))) . k by A78, A80, FINSEQ_1:25; ::_thesis: verum end; then A92: Per (f,F) = (f - {('not' p)}) ^ (IdFinS (('not' p),(card A))) by A76, FINSEQ_1:13; reconsider h = (f - {('not' p)}) ^ (IdFinS (('not' p),(card A))) as FinSequence of CQC-WFF Al by A76, A77, FINSEQ_1:13; (F * f) . j = 'not' p by A20, A74, A75, FUNCT_1:13; then A93: h . j = 'not' p by A92, CALCUL_2:def_2; A94: now__::_thesis:_not_j_in_dom_(f_-_{('not'_p)}) assume A95: j in dom (f - {('not' p)}) ; ::_thesis: contradiction then (f - {('not' p)}) . j = 'not' p by A93, FINSEQ_1:def_7; then A96: (f - {('not' p)}) . j in {('not' p)} by TARSKI:def_1; A97: rng (f - {('not' p)}) = (rng f) \ {('not' p)} by FINSEQ_3:65; (f - {('not' p)}) . j in rng (f - {('not' p)}) by A95, FUNCT_1:3; hence contradiction by A96, A97, XBOOLE_0:def_5; ::_thesis: verum end; j in dom f by A74; then j in dom h by A76, CALCUL_2:19; then consider k being Nat such that A98: k in dom (IdFinS (('not' p),(card A))) and j = (len (f - {('not' p)})) + k by A94, FINSEQ_1:25; reconsider g = f - {('not' p)} as FinSequence of CQC-WFF Al by FINSEQ_3:86; ( 1 <= k & k <= len (IdFinS (('not' p),(card A))) ) by A98, FINSEQ_3:25; then 1 <= len (IdFinS (('not' p),(card A))) by XXREAL_0:2; then A99: 1 <= card A by CARD_1:def_7; |- h ^ <*p*> by A9, A92, CALCUL_2:30; then A100: |- (g ^ <*('not' p)*>) ^ <*p*> by A99, CALCUL_2:32; ( rng g = (rng f) \ {('not' p)} & (rng f) \ {('not' p)} c= (X \/ {('not' p)}) \ {('not' p)} ) by A8, FINSEQ_3:65, XBOOLE_1:33; then A101: rng g c= X \ {('not' p)} by XBOOLE_1:40; X \ {('not' p)} c= X by XBOOLE_1:36; then A102: rng g c= X by A101, XBOOLE_1:1; |- (g ^ <*p*>) ^ <*p*> by CALCUL_2:21; then |- g ^ <*p*> by A100, CALCUL_2:26; hence X |- p by A102, Def1; ::_thesis: verum end; hence X |- p by A9, Def1; ::_thesis: verum end; end; theorem :: HENMODEL:10 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for p being Element of CQC-WFF Al holds ( X |- 'not' p iff X \/ {p} is Inconsistent ) proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) for p being Element of CQC-WFF Al holds ( X |- 'not' p iff X \/ {p} is Inconsistent ) let X be Subset of (CQC-WFF Al); ::_thesis: for p being Element of CQC-WFF Al holds ( X |- 'not' p iff X \/ {p} is Inconsistent ) let p be Element of CQC-WFF Al; ::_thesis: ( X |- 'not' p iff X \/ {p} is Inconsistent ) thus ( X |- 'not' p implies X \/ {p} is Inconsistent ) ::_thesis: ( X \/ {p} is Inconsistent implies X |- 'not' p ) proof assume X |- 'not' p ; ::_thesis: X \/ {p} is Inconsistent then consider f being FinSequence of CQC-WFF Al such that A1: rng f c= X and A2: |- f ^ <*('not' p)*> by Def1; set f2 = f ^ <*p*>; set f1 = (f ^ <*p*>) ^ <*p*>; A3: Ant ((f ^ <*p*>) ^ <*p*>) = f ^ <*p*> by CALCUL_1:5; 1 in Seg 1 by FINSEQ_1:1; then 1 in dom <*p*> by FINSEQ_1:38; then A4: (len f) + 1 in dom (Ant ((f ^ <*p*>) ^ <*p*>)) by A3, FINSEQ_1:28; Suc ((f ^ <*p*>) ^ <*p*>) = p by CALCUL_1:5; then (Ant ((f ^ <*p*>) ^ <*p*>)) . ((len f) + 1) = Suc ((f ^ <*p*>) ^ <*p*>) by A3, FINSEQ_1:42; then Suc ((f ^ <*p*>) ^ <*p*>) is_tail_of Ant ((f ^ <*p*>) ^ <*p*>) by A4, CALCUL_1:def_16; then A5: |- (f ^ <*p*>) ^ <*p*> by CALCUL_1:33; A6: 0 + 1 <= len (f ^ <*p*>) by CALCUL_1:10; ( Ant (f ^ <*p*>) = f & Suc (f ^ <*p*>) = p ) by CALCUL_1:5; then A7: rng (f ^ <*p*>) = (rng f) \/ {p} by A6, CALCUL_1:3; |- (f ^ <*p*>) ^ <*('not' p)*> by A2, Th5; then not f ^ <*p*> is Consistent by A5, Def3; hence X \/ {p} is Inconsistent by A1, A7, Th4, XBOOLE_1:9; ::_thesis: verum end; thus ( X \/ {p} is Inconsistent implies X |- 'not' p ) ::_thesis: verum proof assume X \/ {p} is Inconsistent ; ::_thesis: X |- 'not' p then X \/ {p} |- 'not' p by Th6; then consider f being FinSequence of CQC-WFF Al such that A8: rng f c= X \/ {p} and A9: |- f ^ <*('not' p)*> by Def1; now__::_thesis:_(_not_rng_f_c=_X_implies_X_|-_'not'_p_) set g = f - {p}; reconsider A = f " {p} as finite set ; reconsider B = dom f as finite set ; set n = card A; set h = (f - {p}) ^ (IdFinS (p,(card A))); A10: len (IdFinS (p,(card A))) = card A by CARD_1:def_7; A c= B by RELAT_1:132; then A11: A c= Seg (len f) by FINSEQ_1:def_3; A12: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_seq_((len_(f_-_{p})),(card_A))_holds_ i_-_(len_(f_-_{p}))_in_dom_(Sgm_A) let i be Element of NAT ; ::_thesis: ( i in seq ((len (f - {p})),(card A)) implies i - (len (f - {p})) in dom (Sgm A) ) reconsider j = i - (len (f - {p})) as Integer ; assume A13: i in seq ((len (f - {p})),(card A)) ; ::_thesis: i - (len (f - {p})) in dom (Sgm A) then A14: 1 + (len (f - {p})) <= i by CALCUL_2:1; then A15: 1 <= j by XREAL_1:19; i <= (card A) + (len (f - {p})) by A13, CALCUL_2:1; then A16: j <= card A by XREAL_1:20; 0 <= j by A14, XREAL_1:19; then reconsider j = j as Element of NAT by INT_1:3; j in Seg (card A) by A15, A16, FINSEQ_1:1; hence i - (len (f - {p})) in dom (Sgm A) by A11, FINSEQ_3:40; ::_thesis: verum end; assume not rng f c= X ; ::_thesis: X |- 'not' p then consider a being set such that A17: a in rng f and A18: not a in X by TARSKI:def_3; ( a in X or a in {p} ) by A8, A17, XBOOLE_0:def_3; then a = p by A18, TARSKI:def_1; then consider i being Nat such that A19: i in B and A20: f . i = p by A17, FINSEQ_2:10; reconsider C = B \ A as finite set ; defpred S1[ Nat, set ] means ( ( $1 in Seg (len (f - {p})) implies $2 = (Sgm (B \ A)) . $1 ) & ( $1 in seq ((len (f - {p})),(card A)) implies $2 = (Sgm A) . ($1 - (len (f - {p}))) ) ); A21: card C = (card B) - (card A) by CARD_2:44, RELAT_1:132 .= (card (Seg (len f))) - (card A) by FINSEQ_1:def_3 .= (len f) - (card A) by FINSEQ_1:57 .= len (f - {p}) by FINSEQ_3:59 ; A22: for k being Nat st k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) holds ex a being set st S1[k,a] proof let k be Nat; ::_thesis: ( k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) implies ex a being set st S1[k,a] ) assume k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) ; ::_thesis: ex a being set st S1[k,a] now__::_thesis:_(_k_in_Seg_(len_(f_-_{p}))_implies_ex_a_being_set_st_S1[k,a]_) assume A23: k in Seg (len (f - {p})) ; ::_thesis: ex a being set st S1[k,a] take a = (Sgm (B \ A)) . k; ::_thesis: S1[k,a] Seg (len (f - {p})) misses seq ((len (f - {p})),(card A)) by CALCUL_2:8; hence S1[k,a] by A23, XBOOLE_0:3; ::_thesis: verum end; hence ex a being set st S1[k,a] ; ::_thesis: verum end; consider F being FinSequence such that A24: ( dom F = Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) & ( for k being Nat st k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) holds S1[k,F . k] ) ) from FINSEQ_1:sch_1(A22); now__::_thesis:_for_b_being_set_st_b_in_C_holds_ b_in_Seg_(len_f) let b be set ; ::_thesis: ( b in C implies b in Seg (len f) ) assume b in C ; ::_thesis: b in Seg (len f) then b in dom f ; hence b in Seg (len f) by FINSEQ_1:def_3; ::_thesis: verum end; then A25: C c= Seg (len f) by TARSKI:def_3; then A26: dom (Sgm C) = Seg (card C) by FINSEQ_3:40; A27: rng F = B proof now__::_thesis:_for_a_being_set_st_a_in_rng_F_holds_ a_in_B let a be set ; ::_thesis: ( a in rng F implies a in B ) assume a in rng F ; ::_thesis: a in B then consider i being Nat such that A28: i in dom F and A29: F . i = a by FINSEQ_2:10; A30: now__::_thesis:_(_i_in_Seg_(len_(f_-_{p}))_implies_a_in_B_) assume i in Seg (len (f - {p})) ; ::_thesis: a in B then ( a = (Sgm C) . i & i in dom (Sgm C) ) by A24, A25, A21, A28, A29, FINSEQ_3:40; then a in rng (Sgm C) by FUNCT_1:3; then a in C by A25, FINSEQ_1:def_13; hence a in B ; ::_thesis: verum end; A31: now__::_thesis:_(_i_in_seq_((len_(f_-_{p})),(card_A))_implies_a_in_B_) A32: rng (Sgm A) = A by A11, FINSEQ_1:def_13; A33: A c= B by RELAT_1:132; assume A34: i in seq ((len (f - {p})),(card A)) ; ::_thesis: a in B then a = (Sgm A) . (i - (len (f - {p}))) by A24, A28, A29; then a in A by A12, A34, A32, FUNCT_1:3; hence a in B by A33; ::_thesis: verum end; i in (Seg (len (f - {p}))) \/ (seq ((len (f - {p})),(card A))) by A10, A24, A28, Lm1; hence a in B by A30, A31, XBOOLE_0:def_3; ::_thesis: verum end; hence rng F c= B by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: B c= rng F let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in B or a in rng F ) assume A35: a in B ; ::_thesis: a in rng F A36: now__::_thesis:_(_not_a_in_A_implies_a_in_rng_F_) now__::_thesis:_for_b_being_set_st_b_in_C_holds_ b_in_Seg_(len_f) let b be set ; ::_thesis: ( b in C implies b in Seg (len f) ) assume b in C ; ::_thesis: b in Seg (len f) then b in dom f ; hence b in Seg (len f) by FINSEQ_1:def_3; ::_thesis: verum end; then A37: C c= Seg (len f) by TARSKI:def_3; assume not a in A ; ::_thesis: a in rng F then a in C by A35, XBOOLE_0:def_5; then a in rng (Sgm C) by A37, FINSEQ_1:def_13; then consider i being Nat such that A38: i in dom (Sgm C) and A39: (Sgm C) . i = a by FINSEQ_2:10; A40: 1 <= i by A38, FINSEQ_3:25; len (Sgm C) = len (f - {p}) by A26, A21, FINSEQ_1:def_3; then A41: i <= len (f - {p}) by A38, FINSEQ_3:25; len (f - {p}) <= len ((f - {p}) ^ (IdFinS (p,(card A)))) by CALCUL_1:6; then i <= len ((f - {p}) ^ (IdFinS (p,(card A)))) by A41, XXREAL_0:2; then A42: i in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) by A40, FINSEQ_1:1; i in Seg (len (f - {p})) by A40, A41, FINSEQ_1:1; then a = F . i by A24, A39, A42; hence a in rng F by A24, A42, FUNCT_1:3; ::_thesis: verum end; now__::_thesis:_(_a_in_A_implies_a_in_rng_F_) assume A43: a in A ; ::_thesis: a in rng F rng (Sgm A) = A by A11, FINSEQ_1:def_13; then consider i being Nat such that A44: i in dom (Sgm A) and A45: (Sgm A) . i = a by A43, FINSEQ_2:10; reconsider i = i as Element of NAT by ORDINAL1:def_12; set m = i + (len (f - {p})); len (Sgm A) = card A by A11, FINSEQ_3:39; then i <= card A by A44, FINSEQ_3:25; then A46: i + (len (f - {p})) <= (card A) + (len (f - {p})) by XREAL_1:6; then i + (len (f - {p})) <= (len (f - {p})) + (len (IdFinS (p,(card A)))) by CARD_1:def_7; then A47: i + (len (f - {p})) <= len ((f - {p}) ^ (IdFinS (p,(card A)))) by FINSEQ_1:22; A48: 1 <= i by A44, FINSEQ_3:25; then 1 + (len (f - {p})) <= i + (len (f - {p})) by XREAL_1:6; then A49: i + (len (f - {p})) in seq ((len (f - {p})),(card A)) by A46, CALCUL_2:1; i <= i + (len (f - {p})) by NAT_1:11; then 1 <= i + (len (f - {p})) by A48, XXREAL_0:2; then i + (len (f - {p})) in dom ((f - {p}) ^ (IdFinS (p,(card A)))) by A47, FINSEQ_3:25; then A50: i + (len (f - {p})) in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) by FINSEQ_1:def_3; a = (Sgm A) . ((i + (len (f - {p}))) - (len (f - {p}))) by A45; then a = F . (i + (len (f - {p}))) by A24, A49, A50; hence a in rng F by A24, A50, FUNCT_1:3; ::_thesis: verum end; hence a in rng F by A36; ::_thesis: verum end; A51: len ((f - {p}) ^ (IdFinS (p,(card A)))) = (len (f - {p})) + (len (IdFinS (p,(card A)))) by FINSEQ_1:22 .= ((len f) - (card A)) + (len (IdFinS (p,(card A)))) by FINSEQ_3:59 .= ((len f) - (card A)) + (card A) by CARD_1:def_7 .= len f ; then A52: dom F = B by A24, FINSEQ_1:def_3; then reconsider F = F as Relation of B,B by A27, RELSET_1:4; rng F c= B ; then reconsider F = F as Function of B,B by A52, FUNCT_2:2; F is one-to-one proof let a1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not a1 in dom F or not b1 in dom F or not F . a1 = F . b1 or a1 = b1 ) let a2 be set ; ::_thesis: ( not a1 in dom F or not a2 in dom F or not F . a1 = F . a2 or a1 = a2 ) assume that A53: a1 in dom F and A54: a2 in dom F and A55: F . a1 = F . a2 ; ::_thesis: a1 = a2 A56: a2 in (Seg (len (f - {p}))) \/ (seq ((len (f - {p})),(card A))) by A10, A24, A54, Lm1; A57: now__::_thesis:_(_a1_in_Seg_(len_(f_-_{p}))_implies_a1_=_a2_) assume A58: a1 in Seg (len (f - {p})) ; ::_thesis: a1 = a2 then A59: a1 in dom (Sgm C) by A25, A21, FINSEQ_3:40; F . a1 = (Sgm C) . a1 by A24, A53, A58; then F . a1 in rng (Sgm C) by A59, FUNCT_1:3; then A60: F . a1 in C by A25, FINSEQ_1:def_13; A61: now__::_thesis:_not_a2_in_seq_((len_(f_-_{p})),(card_A)) assume A62: a2 in seq ((len (f - {p})),(card A)) ; ::_thesis: contradiction then reconsider i = a2 as Element of NAT ; (Sgm A) . (i - (len (f - {p}))) in rng (Sgm A) by A12, A62, FUNCT_1:3; then F . a2 in rng (Sgm A) by A24, A54, A62; then F . a2 in A by A11, FINSEQ_1:def_13; hence contradiction by A55, A60, XBOOLE_0:def_5; ::_thesis: verum end; now__::_thesis:_(_a2_in_Seg_(len_(f_-_{p}))_implies_a1_=_a2_) assume A63: a2 in Seg (len (f - {p})) ; ::_thesis: a1 = a2 then F . a2 = (Sgm C) . a2 by A24, A54; then A64: (Sgm C) . a1 = (Sgm C) . a2 by A24, A53, A55, A58; A65: Sgm C is one-to-one by A25, FINSEQ_3:92; a2 in dom (Sgm C) by A25, A21, A63, FINSEQ_3:40; hence a1 = a2 by A59, A64, A65, FUNCT_1:def_4; ::_thesis: verum end; hence a1 = a2 by A56, A61, XBOOLE_0:def_3; ::_thesis: verum end; A66: now__::_thesis:_(_a1_in_seq_((len_(f_-_{p})),(card_A))_implies_a1_=_a2_) assume A67: a1 in seq ((len (f - {p})),(card A)) ; ::_thesis: a1 = a2 then reconsider i = a1 as Element of NAT ; A68: i - (len (f - {p})) in dom (Sgm A) by A12, A67; A69: now__::_thesis:_(_a2_in_seq_((len_(f_-_{p})),(card_A))_implies_a1_=_a2_) assume A70: a2 in seq ((len (f - {p})),(card A)) ; ::_thesis: a1 = a2 then reconsider i1 = a2 as Element of NAT ; F . a2 = (Sgm A) . (i1 - (len (f - {p}))) by A24, A54, A70; then A71: (Sgm A) . (i1 - (len (f - {p}))) = (Sgm A) . (i - (len (f - {p}))) by A24, A53, A55, A67; A72: Sgm A is one-to-one by A11, FINSEQ_3:92; i1 - (len (f - {p})) in dom (Sgm A) by A12, A70; then (i1 - (len (f - {p}))) + (len (f - {p})) = (i - (len (f - {p}))) + (len (f - {p})) by A68, A71, A72, FUNCT_1:def_4; hence a1 = a2 ; ::_thesis: verum end; (Sgm A) . (i - (len (f - {p}))) in rng (Sgm A) by A12, A67, FUNCT_1:3; then F . a1 in rng (Sgm A) by A24, A53, A67; then A73: F . a1 in A by A11, FINSEQ_1:def_13; now__::_thesis:_not_a2_in_Seg_(len_(f_-_{p})) assume a2 in Seg (len (f - {p})) ; ::_thesis: contradiction then ( F . a2 = (Sgm C) . a2 & a2 in dom (Sgm C) ) by A24, A25, A21, A54, FINSEQ_3:40; then F . a2 in rng (Sgm C) by FUNCT_1:3; then F . a2 in C by A25, FINSEQ_1:def_13; hence contradiction by A55, A73, XBOOLE_0:def_5; ::_thesis: verum end; hence a1 = a2 by A56, A69, XBOOLE_0:def_3; ::_thesis: verum end; a1 in (Seg (len (f - {p}))) \/ (seq ((len (f - {p})),(card A))) by A10, A24, A53, Lm1; hence a1 = a2 by A57, A66, XBOOLE_0:def_3; ::_thesis: verum end; then reconsider F = F as Permutation of (dom f) by A27, FUNCT_2:57; consider j being Nat such that A74: j in dom F and A75: F . j = i by A27, A19, FINSEQ_2:10; A76: dom (Per (f,F)) = B by CALCUL_2:19 .= dom F by A24, A51, FINSEQ_1:def_3 .= dom ((f - {p}) ^ (IdFinS (p,(card A)))) by A24, FINSEQ_1:def_3 ; A77: now__::_thesis:_for_k_being_Nat_st_k_in_dom_((f_-_{p})_^_(IdFinS_(p,(card_A))))_holds_ (Per_(f,F))_._k_=_((f_-_{p})_^_(IdFinS_(p,(card_A))))_._k let k be Nat; ::_thesis: ( k in dom ((f - {p}) ^ (IdFinS (p,(card A)))) implies (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k ) assume A78: k in dom ((f - {p}) ^ (IdFinS (p,(card A)))) ; ::_thesis: (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k A79: k in Seg (len ((f - {p}) ^ (IdFinS (p,(card A))))) by A78, FINSEQ_1:def_3; A80: now__::_thesis:_(_ex_i_being_Nat_st_ (_i_in_dom_(IdFinS_(p,(card_A)))_&_k_=_(len_(f_-_{p}))_+_i_)_implies_(Per_(f,F))_._k_=_((f_-_{p})_^_(IdFinS_(p,(card_A))))_._k_) A81: k in dom (F * f) by A76, A78, CALCUL_2:def_2; given i being Nat such that A82: i in dom (IdFinS (p,(card A))) and A83: k = (len (f - {p})) + i ; ::_thesis: (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k len (IdFinS (p,(card A))) = card A by CARD_1:def_7; then A84: i <= card A by A82, FINSEQ_3:25; then A85: k <= (card A) + (len (f - {p})) by A83, XREAL_1:6; A86: 1 <= i by A82, FINSEQ_3:25; then 1 + (len (f - {p})) <= k by A83, XREAL_1:6; then A87: k in seq ((len (f - {p})),(card A)) by A85, CALCUL_2:1; then F . k = (Sgm A) . (k - (len (f - {p}))) by A24, A79; then F . k in rng (Sgm A) by A12, A87, FUNCT_1:3; then F . k in A by A11, FINSEQ_1:def_13; then f . (F . k) in {p} by FUNCT_1:def_7; then f . (F . k) = p by TARSKI:def_1; then (F * f) . k = p by A81, FUNCT_1:12; then A88: (Per (f,F)) . k = p by CALCUL_2:def_2; i in Seg (card A) by A86, A84, FINSEQ_1:1; hence (Per (f,F)) . k = (IdFinS (p,(card A))) . i by A88, FUNCOP_1:7 .= ((f - {p}) ^ (IdFinS (p,(card A)))) . k by A82, A83, FINSEQ_1:def_7 ; ::_thesis: verum end; now__::_thesis:_(_k_in_dom_(f_-_{p})_implies_(Per_(f,F))_._k_=_((f_-_{p})_^_(IdFinS_(p,(card_A))))_._k_) assume A89: k in dom (f - {p}) ; ::_thesis: (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k then A90: k in dom (Sgm C) by A26, A21, FINSEQ_1:def_3; k in Seg (len (f - {p})) by A89, FINSEQ_1:def_3; then A91: F . k = (Sgm C) . k by A24, A79; k in dom (F * f) by A76, A78, CALCUL_2:def_2; then (F * f) . k = f . ((Sgm C) . k) by A91, FUNCT_1:12; hence (Per (f,F)) . k = f . ((Sgm C) . k) by CALCUL_2:def_2 .= ((Sgm C) * f) . k by A90, FUNCT_1:13 .= (f - {p}) . k by FINSEQ_3:def_1 .= ((f - {p}) ^ (IdFinS (p,(card A)))) . k by A89, FINSEQ_1:def_7 ; ::_thesis: verum end; hence (Per (f,F)) . k = ((f - {p}) ^ (IdFinS (p,(card A)))) . k by A78, A80, FINSEQ_1:25; ::_thesis: verum end; then A92: Per (f,F) = (f - {p}) ^ (IdFinS (p,(card A))) by A76, FINSEQ_1:13; reconsider h = (f - {p}) ^ (IdFinS (p,(card A))) as FinSequence of CQC-WFF Al by A76, A77, FINSEQ_1:13; (F * f) . j = p by A20, A74, A75, FUNCT_1:13; then A93: h . j = p by A92, CALCUL_2:def_2; A94: now__::_thesis:_not_j_in_dom_(f_-_{p}) assume A95: j in dom (f - {p}) ; ::_thesis: contradiction then (f - {p}) . j = p by A93, FINSEQ_1:def_7; then A96: (f - {p}) . j in {p} by TARSKI:def_1; A97: rng (f - {p}) = (rng f) \ {p} by FINSEQ_3:65; (f - {p}) . j in rng (f - {p}) by A95, FUNCT_1:3; hence contradiction by A96, A97, XBOOLE_0:def_5; ::_thesis: verum end; j in dom f by A74; then j in dom h by A76, CALCUL_2:19; then consider k being Nat such that A98: k in dom (IdFinS (p,(card A))) and j = (len (f - {p})) + k by A94, FINSEQ_1:25; reconsider g = f - {p} as FinSequence of CQC-WFF Al by FINSEQ_3:86; ( 1 <= k & k <= len (IdFinS (p,(card A))) ) by A98, FINSEQ_3:25; then 1 <= len (IdFinS (p,(card A))) by XXREAL_0:2; then A99: 1 <= card A by CARD_1:def_7; |- h ^ <*('not' p)*> by A9, A92, CALCUL_2:30; then A100: |- (g ^ <*p*>) ^ <*('not' p)*> by A99, CALCUL_2:32; ( rng g = (rng f) \ {p} & (rng f) \ {p} c= (X \/ {p}) \ {p} ) by A8, FINSEQ_3:65, XBOOLE_1:33; then A101: rng g c= X \ {p} by XBOOLE_1:40; X \ {p} c= X by XBOOLE_1:36; then A102: rng g c= X by A101, XBOOLE_1:1; |- (g ^ <*('not' p)*>) ^ <*('not' p)*> by CALCUL_2:21; then |- g ^ <*('not' p)*> by A100, CALCUL_2:26; hence X |- 'not' p by A102, Def1; ::_thesis: verum end; hence X |- 'not' p by A9, Def1; ::_thesis: verum end; end; begin theorem :: HENMODEL:11 for Al being QC-alphabet for f being Function of NAT,(bool (CQC-WFF Al)) st ( for n, m being Element of NAT st m in dom f & n in dom f & n < m holds ( f . n is Consistent & f . n c= f . m ) ) holds union (rng f) is Consistent proof let Al be QC-alphabet ; ::_thesis: for f being Function of NAT,(bool (CQC-WFF Al)) st ( for n, m being Element of NAT st m in dom f & n in dom f & n < m holds ( f . n is Consistent & f . n c= f . m ) ) holds union (rng f) is Consistent let f be Function of NAT,(bool (CQC-WFF Al)); ::_thesis: ( ( for n, m being Element of NAT st m in dom f & n in dom f & n < m holds ( f . n is Consistent & f . n c= f . m ) ) implies union (rng f) is Consistent ) assume A1: for n, m being Element of NAT st m in dom f & n in dom f & n < m holds ( f . n is Consistent & f . n c= f . m ) ; ::_thesis: union (rng f) is Consistent now__::_thesis:_union_(rng_f)_is_Consistent A2: for n being Element of NAT st n in dom f holds f . n is Consistent proof let n be Element of NAT ; ::_thesis: ( n in dom f implies f . n is Consistent ) assume A3: n in dom f ; ::_thesis: f . n is Consistent n + 1 in NAT ; then ( n < n + 1 & n + 1 in dom f ) by FUNCT_2:def_1, NAT_1:13; hence f . n is Consistent by A1, A3; ::_thesis: verum end; assume not union (rng f) is Consistent ; ::_thesis: contradiction then consider Z being Subset of (CQC-WFF Al) such that A4: ( Z c= union (rng f) & Z is finite ) and A5: Z is Inconsistent by Th7; for n, m being Element of NAT st m in dom f & n in dom f & n < m holds f . n c= f . m by A1; then consider k being Element of NAT such that A6: Z c= f . k by A4, Th3; reconsider Y = f . k as Subset of (CQC-WFF Al) ; consider p being Element of CQC-WFF Al such that A7: Z |- p and A8: Z |- 'not' p by A5, Def2; consider f1 being FinSequence of CQC-WFF Al such that A9: rng f1 c= Z and A10: |- f1 ^ <*p*> by A7, Def1; consider f2 being FinSequence of CQC-WFF Al such that A11: rng f2 c= Z and A12: |- f2 ^ <*('not' p)*> by A8, Def1; rng (f1 ^ f2) = (rng f1) \/ (rng f2) by FINSEQ_1:31; then rng (f1 ^ f2) c= Z by A9, A11, XBOOLE_1:8; then A13: rng (f1 ^ f2) c= Y by A6, XBOOLE_1:1; |- (f1 ^ f2) ^ <*('not' p)*> by A12, CALCUL_2:20; then A14: Y |- 'not' p by A13, Def1; |- (f1 ^ f2) ^ <*p*> by A10, Th5; then Y |- p by A13, Def1; then A15: not Y is Consistent by A14, Def2; k in NAT ; then k in dom f by FUNCT_2:def_1; hence contradiction by A15, A2; ::_thesis: verum end; hence union (rng f) is Consistent ; ::_thesis: verum end; begin theorem Th12: :: HENMODEL:12 for Al being QC-alphabet for X being Subset of (CQC-WFF Al) for A being non empty set st X is Inconsistent holds for J being interpretation of Al,A for v being Element of Valuations_in (Al,A) holds not J,v |= X proof let Al be QC-alphabet ; ::_thesis: for X being Subset of (CQC-WFF Al) for A being non empty set st X is Inconsistent holds for J being interpretation of Al,A for v being Element of Valuations_in (Al,A) holds not J,v |= X let X be Subset of (CQC-WFF Al); ::_thesis: for A being non empty set st X is Inconsistent holds for J being interpretation of Al,A for v being Element of Valuations_in (Al,A) holds not J,v |= X let A be non empty set ; ::_thesis: ( X is Inconsistent implies for J being interpretation of Al,A for v being Element of Valuations_in (Al,A) holds not J,v |= X ) reconsider p = 'not' (VERUM Al) as Element of CQC-WFF Al ; assume not X is Consistent ; ::_thesis: for J being interpretation of Al,A for v being Element of Valuations_in (Al,A) holds not J,v |= X then X |- 'not' (VERUM Al) by Th6; then consider f being FinSequence of CQC-WFF Al such that A1: rng f c= X and A2: |- f ^ <*('not' (VERUM Al))*> by Def1; let J be interpretation of Al,A; ::_thesis: for v being Element of Valuations_in (Al,A) holds not J,v |= X let v be Element of Valuations_in (Al,A); ::_thesis: not J,v |= X A3: Suc (f ^ <*p*>) = p by CALCUL_1:5; rng (Ant (f ^ <*p*>)) c= X by A1, CALCUL_1:5; then p is_formal_provable_from X by A2, A3, CALCUL_1:def_10; then A4: X |= p by CALCUL_1:32; now__::_thesis:_not_J,v_|=_X assume J,v |= X ; ::_thesis: contradiction then J,v |= 'not' (VERUM Al) by A4, CALCUL_1:def_12; then not J,v |= VERUM Al by VALUAT_1:17; hence contradiction by VALUAT_1:32; ::_thesis: verum end; hence not J,v |= X ; ::_thesis: verum end; theorem Th13: :: HENMODEL:13 for Al being QC-alphabet holds {(VERUM Al)} is Consistent proof let Al be QC-alphabet ; ::_thesis: {(VERUM Al)} is Consistent set A = the non empty set ; set J = the interpretation of Al, the non empty set ; set v = the Element of Valuations_in (Al, the non empty set ); the interpretation of Al, the non empty set , the Element of Valuations_in (Al, the non empty set ) |= VERUM Al by VALUAT_1:32; then for p being Element of CQC-WFF Al st p in {(VERUM Al)} holds the interpretation of Al, the non empty set , the Element of Valuations_in (Al, the non empty set ) |= p by TARSKI:def_1; then the interpretation of Al, the non empty set , the Element of Valuations_in (Al, the non empty set ) |= {(VERUM Al)} by CALCUL_1:def_11; hence {(VERUM Al)} is Consistent by Th12; ::_thesis: verum end; registration let Al be QC-alphabet ; cluster Consistent for Element of bool (CQC-WFF Al); existence ex b1 being Subset of (CQC-WFF Al) st b1 is Consistent proof {(VERUM Al)} is Consistent by Th13; hence ex b1 being Subset of (CQC-WFF Al) st b1 is Consistent ; ::_thesis: verum end; end; definition let Al be QC-alphabet ; func HCar Al -> non empty set equals :: HENMODEL:def 4 bound_QC-variables Al; coherence bound_QC-variables Al is non empty set ; end; :: deftheorem defines HCar HENMODEL:def_4_:_ for Al being QC-alphabet holds HCar Al = bound_QC-variables Al; definition let Al be QC-alphabet ; let P be Element of QC-pred_symbols Al; let ll be CQC-variable_list of the_arity_of P,Al; :: original: ! redefine funcP ! ll -> Element of CQC-WFF Al; coherence P ! ll is Element of CQC-WFF Al proof set k = the_arity_of P; reconsider P9 = P as QC-pred_symbol of (the_arity_of P),Al by QC_LANG3:1; P9 ! ll is Element of CQC-WFF Al ; hence P ! ll is Element of CQC-WFF Al ; ::_thesis: verum end; end; definition let Al be QC-alphabet ; let CX be Consistent Subset of (CQC-WFF Al); mode Henkin_interpretation of CX -> interpretation of Al, HCar Al means :Def5: :: HENMODEL:def 5 for P being Element of QC-pred_symbols Al for r being Element of relations_on (HCar Al) st it . P = r holds for a being set holds ( a in r iff ex ll being CQC-variable_list of the_arity_of P,Al st ( a = ll & CX |- P ! ll ) ); existence ex b1 being interpretation of Al, HCar Al st for P being Element of QC-pred_symbols Al for r being Element of relations_on (HCar Al) st b1 . P = r holds for a being set holds ( a in r iff ex ll being CQC-variable_list of the_arity_of P,Al st ( a = ll & CX |- P ! ll ) ) proof defpred S1[ set , set ] means ex P9 being Element of QC-pred_symbols Al st ( P9 = $1 & $2 = { ll where ll is CQC-variable_list of the_arity_of P9,Al : CX |- P9 ! ll } ); set A = QC-pred_symbols Al; A1: for a being set st a in QC-pred_symbols Al holds ex b being set st S1[a,b] proof let a be set ; ::_thesis: ( a in QC-pred_symbols Al implies ex b being set st S1[a,b] ) assume a in QC-pred_symbols Al ; ::_thesis: ex b being set st S1[a,b] then reconsider a = a as Element of QC-pred_symbols Al ; consider b being set such that A2: b = { ll where ll is CQC-variable_list of the_arity_of a,Al : CX |- a ! ll } ; take b ; ::_thesis: S1[a,b] take a ; ::_thesis: ( a = a & b = { ll where ll is CQC-variable_list of the_arity_of a,Al : CX |- a ! ll } ) thus ( a = a & b = { ll where ll is CQC-variable_list of the_arity_of a,Al : CX |- a ! ll } ) by A2; ::_thesis: verum end; consider f being Function such that A3: ( dom f = QC-pred_symbols Al & ( for a being set st a in QC-pred_symbols Al holds S1[a,f . a] ) ) from CLASSES1:sch_1(A1); A4: for P being Element of QC-pred_symbols Al for r being Element of relations_on (HCar Al) st f . P = r holds for a being set holds ( a in r iff ex ll being CQC-variable_list of the_arity_of P,Al st ( a = ll & CX |- P ! ll ) ) proof let P be Element of QC-pred_symbols Al; ::_thesis: for r being Element of relations_on (HCar Al) st f . P = r holds for a being set holds ( a in r iff ex ll being CQC-variable_list of the_arity_of P,Al st ( a = ll & CX |- P ! ll ) ) let r be Element of relations_on (HCar Al); ::_thesis: ( f . P = r implies for a being set holds ( a in r iff ex ll being CQC-variable_list of the_arity_of P,Al st ( a = ll & CX |- P ! ll ) ) ) assume A5: f . P = r ; ::_thesis: for a being set holds ( a in r iff ex ll being CQC-variable_list of the_arity_of P,Al st ( a = ll & CX |- P ! ll ) ) let a be set ; ::_thesis: ( a in r iff ex ll being CQC-variable_list of the_arity_of P,Al st ( a = ll & CX |- P ! ll ) ) thus ( a in r implies ex ll being CQC-variable_list of the_arity_of P,Al st ( a = ll & CX |- P ! ll ) ) ::_thesis: ( ex ll being CQC-variable_list of the_arity_of P,Al st ( a = ll & CX |- P ! ll ) implies a in r ) proof assume A6: a in r ; ::_thesis: ex ll being CQC-variable_list of the_arity_of P,Al st ( a = ll & CX |- P ! ll ) ex P9 being Element of QC-pred_symbols Al st ( P9 = P & f . P = { ll where ll is CQC-variable_list of the_arity_of P9,Al : CX |- P9 ! ll } ) by A3; hence ex ll being CQC-variable_list of the_arity_of P,Al st ( a = ll & CX |- P ! ll ) by A5, A6; ::_thesis: verum end; thus ( ex ll being CQC-variable_list of the_arity_of P,Al st ( a = ll & CX |- P ! ll ) implies a in r ) ::_thesis: verum proof given ll being CQC-variable_list of the_arity_of P,Al such that A7: ( a = ll & CX |- P ! ll ) ; ::_thesis: a in r ex P9 being Element of QC-pred_symbols Al st ( P9 = P & f . P = { l where l is CQC-variable_list of the_arity_of P9,Al : CX |- P9 ! l } ) by A3; hence a in r by A5, A7; ::_thesis: verum end; end; A8: for P being Element of QC-pred_symbols Al for r being Element of relations_on (HCar Al) holds ( not f . P = r or r = empty_rel (HCar Al) or the_arity_of P = the_arity_of r ) proof let P be Element of QC-pred_symbols Al; ::_thesis: for r being Element of relations_on (HCar Al) holds ( not f . P = r or r = empty_rel (HCar Al) or the_arity_of P = the_arity_of r ) let r be Element of relations_on (HCar Al); ::_thesis: ( not f . P = r or r = empty_rel (HCar Al) or the_arity_of P = the_arity_of r ) assume A9: f . P = r ; ::_thesis: ( r = empty_rel (HCar Al) or the_arity_of P = the_arity_of r ) consider P9 being Element of QC-pred_symbols Al such that A10: ( P9 = P & f . P = { ll where ll is CQC-variable_list of the_arity_of P9,Al : CX |- P9 ! ll } ) by A3; assume A11: not r = empty_rel (HCar Al) ; ::_thesis: the_arity_of P = the_arity_of r then r <> {} by MARGREL1:9; then consider a being set such that A12: a in r by XBOOLE_0:def_1; consider ll9 being CQC-variable_list of the_arity_of P9,Al such that A13: a = ll9 and CX |- P9 ! ll9 by A9, A12, A10; rng ll9 c= bound_QC-variables Al by RELAT_1:def_19; then reconsider a = a as FinSequence of HCar Al by A13, FINSEQ_1:def_4; the_arity_of r = len a by A11, A12, MARGREL1:def_10; hence the_arity_of P = the_arity_of r by A10, A13, CARD_1:def_7; ::_thesis: verum end; for b being set st b in rng f holds b in relations_on (HCar Al) proof let b be set ; ::_thesis: ( b in rng f implies b in relations_on (HCar Al) ) assume b in rng f ; ::_thesis: b in relations_on (HCar Al) then consider a being set such that A14: a in dom f and A15: b = f . a by FUNCT_1:def_3; consider P9 being Element of QC-pred_symbols Al such that A16: ( P9 = a & f . a = { ll where ll is CQC-variable_list of the_arity_of P9,Al : CX |- P9 ! ll } ) by A3, A14; for c being set st c in b holds c in (HCar Al) * proof let c be set ; ::_thesis: ( c in b implies c in (HCar Al) * ) assume c in b ; ::_thesis: c in (HCar Al) * then consider ll being CQC-variable_list of the_arity_of P9,Al such that A17: c = ll and CX |- P9 ! ll by A15, A16; rng ll c= bound_QC-variables Al by RELAT_1:def_19; then ll is FinSequence of HCar Al by FINSEQ_1:def_4; hence c in (HCar Al) * by A17, FINSEQ_1:def_11; ::_thesis: verum end; then A18: b c= (HCar Al) * by TARSKI:def_3; for fin, fin9 being FinSequence of HCar Al st fin in b & fin9 in b holds len fin = len fin9 proof let fin, fin9 be FinSequence of HCar Al; ::_thesis: ( fin in b & fin9 in b implies len fin = len fin9 ) assume that A19: fin in b and A20: fin9 in b ; ::_thesis: len fin = len fin9 ex ll being CQC-variable_list of the_arity_of P9,Al st ( fin = ll & CX |- P9 ! ll ) by A15, A16, A19; then A21: len fin = the_arity_of P9 by CARD_1:def_7; ex ll9 being CQC-variable_list of the_arity_of P9,Al st ( fin9 = ll9 & CX |- P9 ! ll9 ) by A15, A16, A20; hence len fin = len fin9 by A21, CARD_1:def_7; ::_thesis: verum end; hence b in relations_on (HCar Al) by A18, MARGREL1:def_7; ::_thesis: verum end; then rng f c= relations_on (HCar Al) by TARSKI:def_3; then reconsider f = f as Function of (QC-pred_symbols Al),(relations_on (HCar Al)) by A3, FUNCT_2:2; reconsider f = f as interpretation of Al, HCar Al by A8, VALUAT_1:def_5; take f ; ::_thesis: for P being Element of QC-pred_symbols Al for r being Element of relations_on (HCar Al) st f . P = r holds for a being set holds ( a in r iff ex ll being CQC-variable_list of the_arity_of P,Al st ( a = ll & CX |- P ! ll ) ) thus for P being Element of QC-pred_symbols Al for r being Element of relations_on (HCar Al) st f . P = r holds for a being set holds ( a in r iff ex ll being CQC-variable_list of the_arity_of P,Al st ( a = ll & CX |- P ! ll ) ) by A4; ::_thesis: verum end; end; :: deftheorem Def5 defines Henkin_interpretation HENMODEL:def_5_:_ for Al being QC-alphabet for CX being Consistent Subset of (CQC-WFF Al) for b3 being interpretation of Al, HCar Al holds ( b3 is Henkin_interpretation of CX iff for P being Element of QC-pred_symbols Al for r being Element of relations_on (HCar Al) st b3 . P = r holds for a being set holds ( a in r iff ex ll being CQC-variable_list of the_arity_of P,Al st ( a = ll & CX |- P ! ll ) ) ); definition let Al be QC-alphabet ; func valH Al -> Element of Valuations_in (Al,(HCar Al)) equals :: HENMODEL:def 6 id (bound_QC-variables Al); coherence id (bound_QC-variables Al) is Element of Valuations_in (Al,(HCar Al)) by VALUAT_1:def_1; end; :: deftheorem defines valH HENMODEL:def_6_:_ for Al being QC-alphabet holds valH Al = id (bound_QC-variables Al); begin theorem Th14: :: HENMODEL:14 for Al being QC-alphabet for k being Element of NAT for ll being CQC-variable_list of k,Al holds (valH Al) *' ll = ll proof let Al be QC-alphabet ; ::_thesis: for k being Element of NAT for ll being CQC-variable_list of k,Al holds (valH Al) *' ll = ll let k be Element of NAT ; ::_thesis: for ll being CQC-variable_list of k,Al holds (valH Al) *' ll = ll let ll be CQC-variable_list of k,Al; ::_thesis: (valH Al) *' ll = ll A1: for i being Element of NAT st i in dom ((valH Al) *' ll) holds (valH Al) . (ll . i) = ll . i proof A2: dom ((valH Al) *' ll) c= dom ll by RELAT_1:25; let i be Element of NAT ; ::_thesis: ( i in dom ((valH Al) *' ll) implies (valH Al) . (ll . i) = ll . i ) assume i in dom ((valH Al) *' ll) ; ::_thesis: (valH Al) . (ll . i) = ll . i then A3: ll . i in rng ll by A2, FUNCT_1:3; rng ll c= bound_QC-variables Al by RELAT_1:def_19; hence (valH Al) . (ll . i) = ll . i by A3, FUNCT_1:18; ::_thesis: verum end; A4: for i being Element of NAT st 1 <= i & i <= k holds (valH Al) . (ll . i) = ll . i proof let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= k implies (valH Al) . (ll . i) = ll . i ) assume that A5: 1 <= i and A6: i <= k ; ::_thesis: (valH Al) . (ll . i) = ll . i i <= len ((valH Al) *' ll) by A6, VALUAT_1:def_3; then i in dom ((valH Al) *' ll) by A5, FINSEQ_3:25; hence (valH Al) . (ll . i) = ll . i by A1; ::_thesis: verum end; A7: len ll = k by CARD_1:def_7; then A8: dom ll = Seg k by FINSEQ_1:def_3; A9: for i being Nat st i in dom ll holds ((valH Al) *' ll) . i = ll . i proof let i be Nat; ::_thesis: ( i in dom ll implies ((valH Al) *' ll) . i = ll . i ) assume A10: i in dom ll ; ::_thesis: ((valH Al) *' ll) . i = ll . i reconsider i = i as Element of NAT by ORDINAL1:def_12; A11: ( 1 <= i & i <= k ) by A8, A10, FINSEQ_1:1; then ((valH Al) *' ll) . i = (valH Al) . (ll . i) by VALUAT_1:def_3; hence ((valH Al) *' ll) . i = ll . i by A4, A11; ::_thesis: verum end; len ((valH Al) *' ll) = k by VALUAT_1:def_3; hence (valH Al) *' ll = ll by A7, A9, FINSEQ_2:9; ::_thesis: verum end; theorem Th15: :: HENMODEL:15 for Al being QC-alphabet for f being FinSequence of CQC-WFF Al holds |- f ^ <*(VERUM Al)*> proof let Al be QC-alphabet ; ::_thesis: for f being FinSequence of CQC-WFF Al holds |- f ^ <*(VERUM Al)*> let f be FinSequence of CQC-WFF Al; ::_thesis: |- f ^ <*(VERUM Al)*> set PR = <*[(f ^ <*(VERUM Al)*>),1]*>; A1: rng <*[(f ^ <*(VERUM Al)*>),1]*> = {[(f ^ <*(VERUM Al)*>),1]} by FINSEQ_1:38; now__::_thesis:_for_a_being_set_st_a_in_rng_<*[(f_^_<*(VERUM_Al)*>),1]*>_holds_ a_in_[:(set_of_CQC-WFF-seq_Al),Proof_Step_Kinds:] let a be set ; ::_thesis: ( a in rng <*[(f ^ <*(VERUM Al)*>),1]*> implies a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] ) assume a in rng <*[(f ^ <*(VERUM Al)*>),1]*> ; ::_thesis: a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] then A2: a = [(f ^ <*(VERUM Al)*>),1] by A1, TARSKI:def_1; f ^ <*(VERUM Al)*> in set_of_CQC-WFF-seq Al by CALCUL_1:def_6; hence a in [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] by A2, CQC_THE1:21, ZFMISC_1:87; ::_thesis: verum end; then rng <*[(f ^ <*(VERUM Al)*>),1]*> c= [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] by TARSKI:def_3; then reconsider PR = <*[(f ^ <*(VERUM Al)*>),1]*> as FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] by FINSEQ_1:def_4; now__::_thesis:_for_n_being_Nat_st_1_<=_n_&_n_<=_len_PR_holds_ PR,n_is_a_correct_step let n be Nat; ::_thesis: ( 1 <= n & n <= len PR implies PR,n is_a_correct_step ) assume that A3: 1 <= n and A4: n <= len PR ; ::_thesis: PR,n is_a_correct_step n <= 1 by A4, FINSEQ_1:39; then n = 1 by A3, XXREAL_0:1; then PR . n = [(f ^ <*(VERUM Al)*>),1] by FINSEQ_1:40; then ( (PR . n) `1 = f ^ <*(VERUM Al)*> & (PR . n) `2 = 1 ) by MCART_1:7; hence PR,n is_a_correct_step by CALCUL_1:def_7; ::_thesis: verum end; then A5: PR is a_proof by CALCUL_1:def_8; PR . 1 = [(f ^ <*(VERUM Al)*>),1] by FINSEQ_1:40; then PR . (len PR) = [(f ^ <*(VERUM Al)*>),1] by FINSEQ_1:40; then (PR . (len PR)) `1 = f ^ <*(VERUM Al)*> by MCART_1:7; hence |- f ^ <*(VERUM Al)*> by A5, CALCUL_1:def_9; ::_thesis: verum end; theorem :: HENMODEL:16 for Al being QC-alphabet for CX being Consistent Subset of (CQC-WFF Al) for JH being Henkin_interpretation of CX holds ( JH, valH Al |= VERUM Al iff CX |- VERUM Al ) proof let Al be QC-alphabet ; ::_thesis: for CX being Consistent Subset of (CQC-WFF Al) for JH being Henkin_interpretation of CX holds ( JH, valH Al |= VERUM Al iff CX |- VERUM Al ) let CX be Consistent Subset of (CQC-WFF Al); ::_thesis: for JH being Henkin_interpretation of CX holds ( JH, valH Al |= VERUM Al iff CX |- VERUM Al ) let JH be Henkin_interpretation of CX; ::_thesis: ( JH, valH Al |= VERUM Al iff CX |- VERUM Al ) set f = <*> (CQC-WFF Al); ( rng (<*> (CQC-WFF Al)) c= CX & |- (<*> (CQC-WFF Al)) ^ <*(VERUM Al)*> ) by Th15, XBOOLE_1:2; hence ( JH, valH Al |= VERUM Al iff CX |- VERUM Al ) by Def1, VALUAT_1:32; ::_thesis: verum end; theorem :: HENMODEL:17 for Al being QC-alphabet for k being Element of NAT for P being QC-pred_symbol of k,Al for ll being CQC-variable_list of k,Al for CX being Consistent Subset of (CQC-WFF Al) for JH being Henkin_interpretation of CX holds ( JH, valH Al |= P ! ll iff CX |- P ! ll ) proof let Al be QC-alphabet ; ::_thesis: for k being Element of NAT for P being QC-pred_symbol of k,Al for ll being CQC-variable_list of k,Al for CX being Consistent Subset of (CQC-WFF Al) for JH being Henkin_interpretation of CX holds ( JH, valH Al |= P ! ll iff CX |- P ! ll ) let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,Al for ll being CQC-variable_list of k,Al for CX being Consistent Subset of (CQC-WFF Al) for JH being Henkin_interpretation of CX holds ( JH, valH Al |= P ! ll iff CX |- P ! ll ) let P be QC-pred_symbol of k,Al; ::_thesis: for ll being CQC-variable_list of k,Al for CX being Consistent Subset of (CQC-WFF Al) for JH being Henkin_interpretation of CX holds ( JH, valH Al |= P ! ll iff CX |- P ! ll ) let ll be CQC-variable_list of k,Al; ::_thesis: for CX being Consistent Subset of (CQC-WFF Al) for JH being Henkin_interpretation of CX holds ( JH, valH Al |= P ! ll iff CX |- P ! ll ) let CX be Consistent Subset of (CQC-WFF Al); ::_thesis: for JH being Henkin_interpretation of CX holds ( JH, valH Al |= P ! ll iff CX |- P ! ll ) let JH be Henkin_interpretation of CX; ::_thesis: ( JH, valH Al |= P ! ll iff CX |- P ! ll ) thus ( JH, valH Al |= P ! ll implies CX |- P ! ll ) ::_thesis: ( CX |- P ! ll implies JH, valH Al |= P ! ll ) proof set rel = JH . P; reconsider rel = JH . P as Element of relations_on (HCar Al) ; assume JH, valH Al |= P ! ll ; ::_thesis: CX |- P ! ll then (Valid ((P ! ll),JH)) . (valH Al) = TRUE by VALUAT_1:def_7; then (valH Al) *' ll in rel by VALUAT_1:7; then ll in rel by Th14; then ex ll9 being CQC-variable_list of the_arity_of P,Al st ( ll9 = ll & CX |- P ! ll9 ) by Def5; hence CX |- P ! ll ; ::_thesis: verum end; thus ( CX |- P ! ll implies JH, valH Al |= P ! ll ) ::_thesis: verum proof P is QC-pred_symbol of (the_arity_of P),Al by QC_LANG3:1; then A1: the_arity_of P = k by SUBSTUT2:3; assume CX |- P ! ll ; ::_thesis: JH, valH Al |= P ! ll then ll in JH . P by A1, Def5; then (valH Al) *' ll in JH . P by Th14; then (Valid ((P ! ll),JH)) . (valH Al) = TRUE by VALUAT_1:7; hence JH, valH Al |= P ! ll by VALUAT_1:def_7; ::_thesis: verum end; end;