let Al be QC-alphabet ; :: thesis: 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 )
let k be Nat; :: thesis: 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 )
let P be QC-pred_symbol of k,Al; :: thesis: 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 )
let ll be CQC-variable_list of k,Al; :: thesis: 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 )
let CX be Consistent Subset of (CQC-WFF Al); :: thesis: for JH being Henkin_interpretation of CX holds
( JH, valH Al |= P ! ll iff CX |- P ! ll )
let JH be Henkin_interpretation of CX; :: thesis: ( JH, valH Al |= P ! ll iff CX |- P ! ll )
thus ( JH, valH Al |= P ! ll implies CX |- P ! ll ) :: thesis: ( CX |- P ! ll implies JH, valH Al |= P ! ll )
proof
set rel = JH . P;
reconsider rel = JH . P as Element of relations_on (HCar Al) ;
assume JH, valH Al |= P ! ll ; :: thesis: CX |- P ! ll
then (Valid ((P ! ll),JH)) . (valH Al) = TRUE by VALUAT_1:def 7;
then (valH Al) *' ll in rel by VALUAT_1:7;
then ll in rel by Th14;
then ex ll9 being CQC-variable_list of the_arity_of P,Al st
( ll9 = ll & CX |- P ! ll9 ) by Def5;
hence CX |- P ! ll ; :: thesis: verum
end;
thus ( CX |- P ! ll implies JH, valH Al |= P ! ll ) :: thesis: verum
proof
P is QC-pred_symbol of (the_arity_of P),Al by QC_LANG3:1;
then A1: the_arity_of P = k by SUBSTUT2:3;
assume CX |- P ! ll ; :: thesis: JH, valH Al |= P ! ll
then ll in JH . P by A1, Def5;
then (valH Al) *' ll in JH . P by Th14;
then (Valid ((P ! ll),JH)) . (valH Al) = TRUE by VALUAT_1:7;
hence JH, valH Al |= P ! ll by VALUAT_1:def 7; :: thesis: verum
end;