:: deftheorem Def5 defines Henkin_interpretation HENMODEL:def 5 :
for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al)
for b₃ being interpretation of Al, HCar Al holds
( b₃ 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₃ . 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 ) ) );