:: HENMODEL semantic presentation

theorem Th1: :: HENMODEL:1

for b₁ being Nat
for b₂ being non empty finite Subset of NAT
for b₃ being Function of b₁,b₂ st ex b₄ being Nat st succ b₄ = b₁ & b₃ is one-to-one & rng b₃ = b₂ & ( for b₄, b₅ being Nat st b₅ in dom b₃ & b₄ in dom b₃ & b₄ < b₅ holds
b₃ . b₄ in b₃ . b₅ ) holds
b₃ . (union b₁) = union (rng b₃)

proof end;

theorem Th2: :: HENMODEL:2

for b₁ being non empty finite Subset of NAT holds
( union b₁ in b₁ & ( for b₂ being set holds
( not b₂ in b₁ or b₂ in union b₁ or b₂ = union b₁ ) ) )

proof end;

definition

let c₁ be set ;
func min* c₁ -> Nat means :Def1: :: HENMODEL:def 1
( a₂ in a₁ & ( for b₁ being Nat st b₁ in a₁ holds
a₂ <= b₁ ) ) if a₁ is non empty Subset of NAT
otherwise a₂ = 0;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def1 defines min* HENMODEL:def 1 :

theorem Th3: :: HENMODEL:3

for b₁ being non empty set
for b₂ being Function of NAT ,b₁
for b₃ being finite set st ( for b₄, b₅ being Nat st b₅ in dom b₂ & b₄ in dom b₂ & b₄ < b₅ holds
b₂ . b₄ c= b₂ . b₅ ) & b₃ c= union (rng b₂) holds
ex b₄ being Nat st b₃ c= b₂ . b₄

proof end;

definition

let c₁ be Subset of CQC-WFF ;
let c₂ be Element of CQC-WFF ;
pred c₁ |- c₂ means :Def2: :: HENMODEL:def 2
ex b₁ being FinSequence of CQC-WFF st
( rng b₁ c= a₁ & |- b₁ ^ <*a₂*> );

end;

:: deftheorem Def2 defines |- HENMODEL:def 2 :

definition

let c₁ be Subset of CQC-WFF ;
attr a₁ is Consistent means :Def3: :: HENMODEL:def 3
for b₁ being Element of CQC-WFF holds
( not a₁ |- b₁ or not a₁ |- 'not' b₁ );

end;

:: deftheorem Def3 defines Consistent HENMODEL:def 3 :

notation

let c₁ be Subset of CQC-WFF ;
antonym Inconsistent c₁ for Consistent c₁;

end;

definition

let c₁ be FinSequence of CQC-WFF ;
attr a₁ is Consistent means :Def4: :: HENMODEL:def 4
for b₁ being Element of CQC-WFF holds
( not |- a₁ ^ <*b₁*> or not |- a₁ ^ <*('not' b₁)*> );

end;

:: deftheorem Def4 defines Consistent HENMODEL:def 4 :

notation

let c₁ be FinSequence of CQC-WFF ;
antonym Inconsistent c₁ for Consistent c₁;

end;

theorem Th4: :: HENMODEL:4

for b₁ being Subset of CQC-WFF
for b₂ being FinSequence of CQC-WFF st b₁ is Consistent & rng b₂ c= b₁ holds
b₂ is Consistent

proof end;

theorem Th5: :: HENMODEL:5

for b₁ being Element of CQC-WFF
for b₂, b₃ being FinSequence of CQC-WFF st |- b₂ ^ <*b₁*> holds
|- (b₂ ^ b₃) ^ <*b₁*>

proof end;

theorem Th6: :: HENMODEL:6

for b₁ being Subset of CQC-WFF holds
( not b₁ is Consistent iff for b₂ being Element of CQC-WFF holds b₁ |- b₂ )

proof end;

theorem Th7: :: HENMODEL:7

for b₁ being Subset of CQC-WFF st not b₁ is Consistent holds
ex b₂ being Subset of CQC-WFF st
( b₂ c= b₁ & b₂ is finite & not b₂ is Consistent )

proof end;

Lemma12: for b₁, b₂ being FinSequence holds Seg (len (b₁ ^ b₂)) = (Seg (len b₁)) \/ (seq (len b₁),(len b₂))
by CALCUL_2:9;

Lemma13: for b₁, b₂ being Nat holds Seg b₁ misses seq b₁,b₂
by CALCUL_2:8;

theorem Th8: :: HENMODEL:8

for b₁ being Subset of CQC-WFF
for b₂, b₃ being Element of CQC-WFF st b₁ \/ {b₂} |- b₃ holds
ex b₄ being FinSequence of CQC-WFF st
( rng b₄ c= b₁ & |- (b₄ ^ <*b₂*>) ^ <*b₃*> )

proof end;

theorem Th9: :: HENMODEL:9

for b₁ being Subset of CQC-WFF
for b₂ being Element of CQC-WFF holds
( b₁ |- b₂ iff not b₁ \/ {('not' b₂)} is Consistent )

proof end;

theorem Th10: :: HENMODEL:10

for b₁ being Subset of CQC-WFF
for b₂ being Element of CQC-WFF holds
( b₁ |- 'not' b₂ iff not b₁ \/ {b₂} is Consistent )

proof end;

theorem Th11: :: HENMODEL:11

for b₁ being Function of NAT , bool CQC-WFF st ( for b₂, b₃ being Nat st b₃ in dom b₁ & b₂ in dom b₁ & b₂ < b₃ holds
( b₁ . b₂ is Consistent & b₁ . b₂ c= b₁ . b₃ ) ) holds
union (rng b₁) is Consistent

proof end;

theorem Th12: :: HENMODEL:12

for b₁ being Subset of CQC-WFF
for b₂ being non empty set st not b₁ is Consistent holds
for b₃ being interpretation of b₂
for b₄ being Element of Valuations_in b₂ holds not b₃,b₄ |= b₁

proof end;

theorem Th13: :: HENMODEL:13

{VERUM } is Consistent

proof end;

registration

cluster Consistent Element of bool CQC-WFF ;
existence by Th13;

end;

definition

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

end;

:: deftheorem Def5 defines HCar HENMODEL:def 5 :

definition

let c₁ be Element of QC-pred_symbols ;
let c₂ be CQC-variable_list of the_arity_of c₁;
redefine func ! as c₁ ! c₂ -> Element of CQC-WFF ;
coherence

proof end;

end;

definition

let c₁ be Consistent Subset of CQC-WFF ;
mode Henkin_interpretation of c₁ -> interpretation of HCar means :Def6: :: HENMODEL:def 6
for b₁ being Element of QC-pred_symbols
for b₂ being Element of relations_on HCar st a₂ . b₁ = b₂ holds
for b₃ being set holds
( b₃ in b₂ iff ex b₄ being CQC-variable_list of the_arity_of b₁ st
( b₃ = b₄ & a₁ |- b₁ ! b₄ ) );
existence

proof end;

end;

:: deftheorem Def6 defines Henkin_interpretation HENMODEL:def 6 :

definition

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

end;

:: deftheorem Def7 defines valH HENMODEL:def 7 :

theorem Th14: :: HENMODEL:14

for b₁ being Nat
for b₂ being CQC-variable_list of b₁ holds valH *' b₂ = b₂

proof end;

theorem Th15: :: HENMODEL:15

for b₁ being FinSequence of CQC-WFF holds |- b₁ ^ <*VERUM *>

proof end;

theorem Th16: :: HENMODEL:16

for b₁ being Consistent Subset of CQC-WFF
for b₂ being Henkin_interpretation of b₁ holds
( b₂, valH |= VERUM iff b₁ |- VERUM )

proof end;

theorem Th17: :: HENMODEL:17

for b₁ being Nat
for b₂ being QC-pred_symbol of b₁
for b₃ being CQC-variable_list of b₁
for b₄ being Consistent Subset of CQC-WFF
for b₅ being Henkin_interpretation of b₄ holds
( b₅, valH |= b₂ ! b₃ iff b₄ |- b₂ ! b₃ )

proof end;