:: Equivalences of Inconsistency and {H}enkin Models
:: by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users


theorem Th1: :: HENMODEL:1
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 & 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
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;

theorem Th3: :: HENMODEL:3
for C being non empty set
for f being sequence of 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 Al be QC-alphabet ;
let X be Subset of (CQC-WFF Al);
let p be Element of CQC-WFF Al;
pred X |- p means :: HENMODEL:def 1
 ex f being FinSequence of CQC-WFF Al st
( rng f c= X & |- f ^ <*p*> );
end;

:: deftheorem 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);
attr X is Consistent means :: HENMODEL:def 2
 for p being Element of CQC-WFF Al holds
( not X |- p or not X |- 'not' p );
end;

:: deftheorem 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;
attr f is Consistent means :: HENMODEL:def 3
 for p being Element of CQC-WFF Al holds
( not |- f ^ <*p*> or not |- f ^ <*('not' p)*> );
end;

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

Lm1: for f, g being FinSequence holds Seg (len (f ^ g)) = (Seg (len f)) \/ (seq ((len f),(len g)))
proof 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 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 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 end;

theorem :: HENMODEL:11
for Al being QC-alphabet
for f being sequence of (bool (CQC-WFF Al)) 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
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 end;

theorem Th13: :: HENMODEL:13
for Al being QC-alphabet holds {(VERUM Al)} is Consistent
proof 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 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 func P ! ll -> Element of CQC-WFF Al;
coherence
P ! ll is Element of CQC-WFF Al
proof 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 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);

theorem Th14: :: HENMODEL:14
for Al being QC-alphabet
for k being Nat
for ll being CQC-variable_list of k,Al holds (valH Al) *' ll = ll
proof end;

theorem Th15: :: HENMODEL:15
for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al holds |- f ^ <*(VERUM Al)*>
proof 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 end;

theorem :: HENMODEL:17
for Al being QC-alphabet
for k being 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 end;