I'm new to mathematical logic and I'm recently confused by some concepts about first-order logic validity and satisfiability, here are some of my problems:
I learned that validity and also unsatisfiability is semi-decidability, does that mean one can use method like resolution reasoning and eventually get a 'yes' once the statement is actually valid not matter how long it will take, but may get nothing (the mothod does not stop) if the statement is not valid?
I learned that satisfiability is undecidable and even not semi-decidable, because once it is it will lead to that the whole problem is decidable, I can understand it from this perspective but does that mean satisfiability is harder than validity? If it is so then it confuses me a lot, cause I think to prove satisfiability one just needs to find a model and an explanation but to prove validity one needs to check all models and explanations, which seems to me that satisfiability is easier than validity.
Is there something wrong about my understanding? Thanks!
Best Answer
Validity and satisfiability are either equally complicated or incomparably complicated, depending on how we compare complexities (i.e. many-one reductions or Turing reductions); basically, they're "dual" to each other, since $\varphi$ is valid iff $\neg\varphi$ is not satisfiable. Granted, in a sense semidecidability (or recursive enumerability, or computable enumerability) is more natural than "co-semidecidability" (or co-r.e.-ness, or co-c.e.-ness), but this doesn't really translate to a genuine "simpler than" comparison.
Now what about model checking? After all, a sentence is satisfiable iff it has a model, so shouldn't we be able to positively test for satisfiability by searching through all possible models? Well, this works for finite models. However, most models aren't finite: there are lots of sentences which are satisfiable but have no finite models. How are we supposed to search through all possible infinite models?
The fact that we're allowing infinite models as well as finite models makes both satisfiability and validity seem impossibly hard. This is where the highly nontrivial completeness theorem comes in, and I've written more about this here.
Incidentally, if we do restrict attention to finite models only, the situation reverses: satisfaction is semidecidable but not co-semidecidable, and validity is co-semidecidable but not semidecidable (see Trakhtenbrot's theorem). Finite model theory is a very different thing from infinite model theory!