Chiediamo 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: abbiamo un modello e quindi una risposta sì.
Soddisfacibilità significa «vera in almeno un modello»; validità significa «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 cercare solo domini finiti non basta. φ è soddisfacibile se e solo se ¬φ non è valida: per questo il problema appartiene a coRE ed è indecidibile.
Complemento e collegamenti