:: HENMODEL semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: HENMODEL:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for A being non empty finite Subset of NAT
for f being Function of n,A st ex m being Nat st succ m = n & f is one-to-one & rng f = A & ( for n, m being 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 end;

theorem Th2: :: HENMODEL:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

definition
let A be set ;
func min* A -> Nat means :Def1: :: HENMODEL:def 1
( it in A & ( for k being Nat st k in A holds
it <= k ) ) if A is non empty Subset of NAT
otherwise it = 0;
existence
( ( A is non empty Subset of NAT implies ex b1 being Nat st
( b1 in A & ( for k being Nat st k in A holds
b1 <= k ) ) ) & ( A is not non empty Subset of NAT implies ex b1 being Nat st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Nat holds
( ( A is non empty Subset of NAT & b1 in A & ( for k being Nat st k in A holds
b1 <= k ) & b2 in A & ( for k being Nat st k in A holds
b2 <= k ) implies b1 = b2 ) & ( A is not non empty Subset of NAT & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
consistency
for b1 being Nat holds verum
;
end;

:: deftheorem Def1 defines min* HENMODEL:def 1 :
for A being set
for b2 being Nat holds
( ( A is non empty Subset of NAT implies ( b2 = min* A iff ( b2 in A & ( for k being Nat st k in A holds
b2 <= k ) ) ) ) & ( A is not non empty Subset of NAT implies ( b2 = min* A iff b2 = 0 ) ) );

theorem Th3: :: HENMODEL:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty set
for f being Function of NAT ,C
for X being finite set st ( for n, m being 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 Nat st X c= f . k
proof end;

definition
let X be Subset of CQC-WFF ;
let p be Element of CQC-WFF ;
pred X |- p means :Def2: :: HENMODEL:def 2
ex f being FinSequence of CQC-WFF st
( rng f c= X & |- f ^ <*p*> );
end;

:: deftheorem Def2 defines |- HENMODEL:def 2 :
for X being Subset of CQC-WFF
for p being Element of CQC-WFF holds
( X |- p iff ex f being FinSequence of CQC-WFF st
( rng f c= X & |- f ^ <*p*> ) );

definition
let X be Subset of CQC-WFF ;
attr X is Consistent means :Def3: :: HENMODEL:def 3
for p being Element of CQC-WFF holds
( not X |- p or not X |- 'not' p );
end;

:: deftheorem Def3 defines Consistent HENMODEL:def 3 :
for X being Subset of CQC-WFF holds
( X is Consistent iff for p being Element of CQC-WFF holds
( not X |- p or not X |- 'not' p ) );

notation
let X be Subset of CQC-WFF ;
antonym Inconsistent X for Consistent X;
end;

definition
let f be FinSequence of CQC-WFF ;
attr f is Consistent means :Def4: :: HENMODEL:def 4
for p being Element of CQC-WFF holds
( not |- f ^ <*p*> or not |- f ^ <*('not' p)*> );
end;

:: deftheorem Def4 defines Consistent HENMODEL:def 4 :
for f being FinSequence of CQC-WFF holds
( f is Consistent iff for p being Element of CQC-WFF holds
( not |- f ^ <*p*> or not |- f ^ <*('not' p)*> ) );

notation
let f be FinSequence of CQC-WFF ;
antonym Inconsistent f for Consistent f;
end;

theorem Th4: :: HENMODEL:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for g being FinSequence of CQC-WFF st X is Consistent & rng g c= X holds
g is Consistent
proof end;

theorem Th5: :: HENMODEL:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of CQC-WFF
for f, g being FinSequence of CQC-WFF st |- f ^ <*p*> holds
|- (f ^ g) ^ <*p*>
proof end;

theorem Th6: :: HENMODEL:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF holds
( not X is Consistent iff for p being Element of CQC-WFF holds X |- p )
proof end;

theorem Th7: :: HENMODEL:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF st not X is Consistent holds
ex Y being Subset of CQC-WFF st
( Y c= X & Y is finite & not Y is Consistent )
proof end;

Lm1: for f, g being FinSequence holds Seg (len (f ^ g)) = (Seg (len f)) \/ (seq (len f),(len g))
by CALCUL_2:9;

Lm2: for n, m being Nat holds Seg n misses seq n,m
by CALCUL_2:8;

theorem :: HENMODEL:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p, q being Element of CQC-WFF st X \/ {p} |- q holds
ex g being FinSequence of CQC-WFF st
( rng g c= X & |- (g ^ <*p*>) ^ <*q*> )
proof end;

theorem :: HENMODEL:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p being Element of CQC-WFF holds
( X |- p iff not X \/ {('not' p)} is Consistent )
proof end;

theorem :: HENMODEL:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for p being Element of CQC-WFF holds
( X |- 'not' p iff not X \/ {p} is Consistent )
proof end;

theorem :: HENMODEL:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function of NAT , bool CQC-WFF st ( for n, m being 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 end;

theorem Th12: :: HENMODEL:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of CQC-WFF
for A being non empty set st not X is Consistent holds
for J being interpretation of A
for v being Element of Valuations_in A holds not J,v |= X
proof end;

theorem Th13: :: HENMODEL:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
{VERUM } is Consistent
proof end;

registration
cluster Consistent Element of bool CQC-WFF ;
existence
ex b1 being Subset of CQC-WFF st b1 is Consistent
by Th13;
end;

definition
func HCar -> non empty set equals :: HENMODEL:def 5
bound_QC-variables ;
coherence
bound_QC-variables is non empty set
;
end;

:: deftheorem defines HCar HENMODEL:def 5 :
HCar = bound_QC-variables ;

definition
let P be Element of QC-pred_symbols ;
let ll be CQC-variable_list of the_arity_of P;
:: original: !
redefine func P ! ll -> Element of CQC-WFF ;
coherence
P ! ll is Element of CQC-WFF
proof end;
end;

definition
let CX be Consistent Subset of CQC-WFF ;
mode Henkin_interpretation of CX -> interpretation of HCar means :Def6: :: HENMODEL:def 6
for P being Element of QC-pred_symbols
for r being Element of relations_on HCar 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 st
( a = ll & CX |- P ! ll ) );
existence
ex b1 being interpretation of HCar st
for P being Element of QC-pred_symbols
for r being Element of relations_on HCar 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 st
( a = ll & CX |- P ! ll ) )
proof end;
end;

:: deftheorem Def6 defines Henkin_interpretation HENMODEL:def 6 :
for CX being Consistent Subset of CQC-WFF
for b2 being interpretation of HCar holds
( b2 is Henkin_interpretation of CX iff for P being Element of QC-pred_symbols
for r being Element of relations_on HCar st b2 . P = r holds
for a being set holds
( a in r iff ex ll being CQC-variable_list of the_arity_of P st
( a = ll & CX |- P ! ll ) ) );

definition
func valH -> Element of Valuations_in HCar equals :: HENMODEL:def 7
id bound_QC-variables ;
coherence
id bound_QC-variables is Element of Valuations_in HCar
by VALUAT_1:def 1;
end;

:: deftheorem defines valH HENMODEL:def 7 :
valH = id bound_QC-variables ;

theorem Th14: :: HENMODEL:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for ll being CQC-variable_list of k holds valH *' ll = ll
proof end;

theorem Th15: :: HENMODEL:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of CQC-WFF holds |- f ^ <*VERUM *>
proof end;

theorem :: HENMODEL:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for CX being Consistent Subset of CQC-WFF
for JH being Henkin_interpretation of CX holds
( JH, valH |= VERUM iff CX |- VERUM )
proof end;

theorem :: HENMODEL:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for CX being Consistent Subset of CQC-WFF
for JH being Henkin_interpretation of CX holds
( JH, valH |= P ! ll iff CX |- P ! ll )
proof end;