First order satisfiability that doesn't have finite models

Question

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:

1. 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.
2. 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.
3. 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?

Answer 1

Here's an amusing approach by Brock-Nannestad and Schürmann:

Truthful Monadic Abstractions

The idea is to try to translate first-order sentences into monadic first-order logic, by "forgetting" some of the arguments. Certainly the translation isn't complete: there are some consistent sentences which become inconsistent after translation.

However, monadic first order logic is decidable. One can therefore verify if the translation $\overline F$ of a formula $F$ is consistent:

$$ \overline F\not\vdash\bot$$

can be checked by a decision procedure, and implies

$$ F\not\vdash\bot$$

Which implies that $F$ has a model, by the completeness theorem.

This theme can apply somewhat more generally: identify a decidable sub-logic of your problem, then translate your problem into it, in a way that preserves truth. In particular modern SMT solvers like Z3 have gotten astonishingly good at proving satisfiability of formulas with quantifiers (by default $\Sigma^0_1$, but can perform well on $\Pi^0_2$ formulas).

Forcing seems to be far out of reach of automated methods at the present.