We know from Church's theorem that determining first order satisfiability is undecidable in general, but there are several techniques we can use to determine first order satisfiability. The most obvious is to search for a finite model. However, there are a number of statements in first order logic that we can demonstrate have no finite models. For instance, any domain in which an injective and non-surjective function operates is infinite.
How do we demonstrate satisfiability for first order statements where there aren't finite models or the existence of finite models is unknown? In automated theorem proving we can determine satisfiability several ways:
- We can negate the sentence, and search for a contradiction. If one is found, we prove first order validity of the statement and thus satisfiability.
- We use saturation with resolution and run out of inferences. More often than not, we will have an infinite amount of inferences to make, so this isn't dependable.
- We can use forcing, which assumes the existence of a model and also the consistency of the theory.
I don't know of anyone implementing forcing as a mechanized technique for automated theorem proving, and it doesn't look easy, but I'm interested if it's been done or attempted, as it's been used to prove independence for a number of statements in set theory, which itself has no finite models.
Are there other techniques known for searching for first order satisfiability that are applicable for automated reasoning or has anyone worked on an automated forcing algorithm?