Ci si chiede se esistono un dominio e un'interpretazione dei predicati che rendono vera la formula. Per ∃xR(x) basta il dominio {a} con R(a) vera: c'è un modello, quindi la risposta è sì.
Una formula è soddisfacibile se è vera in almeno un modello, valida se è vera in ogni modello. Per esempio ∃xR(x) è soddisfacibile ma non valida: nel dominio {a} con R sempre falsa non vale.
Senza le restrizioni di Schönfinkel-Bernays non esiste un algoritmo che termini sempre e risponda correttamente per ogni formula. Alcune formule hanno soltanto modelli infiniti, quindi non basta cercare fra i domini finiti. φ è soddisfacibile se e solo se ¬φ non è valida: per questo il problema sta in coRE ed è indecidibile.
Complemento e collegamenti