:: by Patrick Braselmann and Peter Koepke

::

:: Received September 25, 2004

:: Copyright (c) 2004-2016 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)

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 ) ) )

( 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

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
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*> ) );

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

end;
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 );

for p being Element of CQC-WFF Al holds

( not X |- p or not X |- 'not' p );

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

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
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)*> ) );

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

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*>

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 )

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 )

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*> )

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 )

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 )

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

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

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;

registration

let Al be QC-alphabet ;

existence

ex b_{1} being Subset of (CQC-WFF Al) st b_{1} is Consistent

end;
existence

ex b

proof end;

:: deftheorem defines HCar HENMODEL:def 4 :

for Al being QC-alphabet holds HCar Al = bound_QC-variables Al;

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

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

definition

let Al be QC-alphabet ;

let CX be Consistent Subset of (CQC-WFF Al);

ex b_{1} 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 b_{1} . 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 ) )

end;
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 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 ) );

ex b

for P being Element of QC-pred_symbols Al

for r being Element of relations_on (HCar Al) st b

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;

:: deftheorem Def5 defines Henkin_interpretation HENMODEL:def 5 :

for Al being QC-alphabet

for CX being Consistent Subset of (CQC-WFF Al)

for b_{3} being interpretation of Al, HCar Al holds

( b_{3} 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 b_{3} . 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 ) ) );

for Al being QC-alphabet

for CX being Consistent Subset of (CQC-WFF Al)

for b

( b

for r being Element of relations_on (HCar Al) st b

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 ;

id (bound_QC-variables Al) is Element of Valuations_in (Al,(HCar Al)) by VALUAT_1:def 1;

end;
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);

id (bound_QC-variables Al) is Element of Valuations_in (Al,(HCar Al)) by VALUAT_1:def 1;

:: deftheorem defines valH HENMODEL:def 6 :

for Al being QC-alphabet holds valH Al = id (bound_QC-variables Al);

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

for k being Nat

for ll being CQC-variable_list of k,Al holds (valH Al) *' ll = ll

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 )

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 )

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;