:: 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;