:: deftheorem defines Correct FOMODEL4:def 67 :
for S being Language
for D being RuleSet of S holds
( D is Correct iff for phi being wff string of S
for X being set st phi is X,D -provable holds
for U being non empty set
for I being Element of U -InterpretersOf S st X is I -satisfied holds
I -TruthEval phi = 1 );