<p>Here's an amusing approach by Brock-Nannestad and Schürmann:</p>

<p><a href="http://www.itu.dk/people/tbro/tma.pdf">Truthful Monadic Abstractions</a></p>

<p>The idea is to try to translate first-order sentences into <a href="http://en.wikipedia.org/wiki/Monadic_predicate_calculus"><strong>monadic first-order logic</strong></a>, by "forgetting" some of the arguments. Certainly the translation isn't <em>complete</em>: there are some consistent sentences which become inconsistent after translation.</p>

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

<p>$$ \overline F\not\vdash\bot$$</p>

<p>can be checked by a decision procedure, and implies</p>

<p>$$ F\not\vdash\bot$$</p>

<p>Which implies that $F$ has a model, by the completeness theorem.</p>

<p>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 <a href="http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories">SMT solvers</a> like <a href="http://z3.codeplex.com/">Z3</a> 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).</p>

<p>Forcing seems to be far out of reach of automated methods at the present.</p>

CC BY-SA 3.0
2014-10-07T23:46:59.760Z
This seems surprising to me. I'm trying to imagine translating NBG set theory into monadic logic, but I can't imagine that it's that easy. I imagine that it works well for real closed fields or presburger arithmetic as decidable first order theories with finite models already, but have a hard time imagining it works for something as expressive as set theory.
dezakin
CC BY-SA 3.0
2014-10-08T00:23:47.540Z
Everything is hard with NGB in automated reasoning. Note that the point of the article is not to use a *single* translation, but try many possible translations in search of a model.
cody
CC BY-SA 3.0
2014-10-07T22:44:04.943Z
2014-10-07T22:44:04.943Z
cody
<p>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. </p>

<p>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:</p>

<ol>
<li>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.</li>
<li>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.</li>
<li>We can use forcing, which assumes the existence of a model and also the consistency of the theory.</li>
</ol>

<p>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. </p>

<p>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?</p>

CC BY-SA 3.0
2017-10-13T13:26:29.487Z
The Infinox approach might be relevant to your question (without answering it). The idea is to use theorem provers to demonstrate the non-existence of finite models. See, for example, https://gupea.ub.gu.se/bitstream/2077/22058/1/gupea_2077_22058_1.pdf
selig
<reference-request><lo.logic><automated-theorem-proving>
First order satisfiability that doesn't have finite models
dezakin
# First order satisfiability that doesn't have finite models

(Asked by: username_0 on 2014-10-07)

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?

**Tags:** reference-request, lo.logic, automated-theorem-proving

> **Comments:**
> **username_1**: The Infinox approach might be relevant to your question (without answering it). The idea is to use theorem provers to demonstrate the non-existence of finite models. See, for example, https://gupea.ub.gu.se/bitstream/2077/22058/1/gupea_2077_22058_1.pdf  

---

## 1 answers

### Answer by username_2 on 2014-10-07. Score: 9 | Accepted answer

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

[Truthful Monadic Abstractions](http://www.itu.dk/people/tbro/tma.pdf)

The idea is to try to translate first-order sentences into [**monadic first-order logic**](http://en.wikipedia.org/wiki/Monadic_predicate_calculus), 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](http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories) like [Z3](http://z3.codeplex.com/) 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.

> **Comments:**
> **username_0**: This seems surprising to me. I'm trying to imagine translating NBG set theory into monadic logic, but I can't imagine that it's that easy. I imagine that it works well for real closed fields or presburger arithmetic as decidable first order theories with finite models already, but have a hard time imagining it works for something as expressive as set theory.  
> **username_2**: Everything is hard with NGB in automated reasoning. Note that the point of the article is not to use a *single* translation, but try many possible translations in search of a model.  

---

