1
$\begingroup$

Suppose we have a first order sentences $\phi$, $\psi$, and $\chi$ such that:

$\phi$ $\longleftrightarrow$ ($\psi$ $\land$ $\chi$)

And $\phi$ and $\chi$ are known or fixed. How can we search for a formula $\psi$ such that the statement is valid?

I understand the proof calculus to search for consequences of first order sentences, using deduction and rules of inference, or to test if a particular statement is valid. With the resolution rule it becomes simple and straightforward to turn everything into clauses, assume the negation, and search for the empty clause (contradiction.)

It's not obvious to me how we can search for a sentence $\psi$ without doing brute force enumeration of well formed formulas and using resolution to test for validity of the equivalence statement. Are there any more efficient techniques?

$\endgroup$
1
  • $\begingroup$ If you have access to an oracle, then this is doable in constant time. Unfortunately, we don't really have access to oracles in this physical reality. :-( $\endgroup$ – Asaf Karagila♦ Jul 2 '14 at 2:41
2
$\begingroup$

Edit:

Assuming your first order theory $T$, (where $T$ may possibly be the empty theory) does not have quantifier elimination, the following holds (furthermore, we can possibly argue that in most cases that do not have effective quantifier elimination, the following holds).

As you probably know, given a sentence in FOL, there is no algorithm which will tell you where or not a sentence is a validity. However, both the set of valid sentences and the set of contradictions are computably (recursively) enumerable. This can be done by taking two Turing machines, and as you say, 'brute forcing' the matter.

Now, your question above is actually "harder" than determining whether a sentence is valid or not (by harder, I mean that your question encodes the question above). Suppose we fix $\varphi$ and $\chi$ such that $\varphi \equiv \chi \equiv \tau$ (By $\equiv$, I mean logically equivalent), where $\tau$ is some logical validity. Then, finding $\psi$ is the exactly the same as finding the set of valid sentences. Again, while this set is recursively enumerable, it is not recursive, and so there is no way of actually finding all the sentences which satisfy this sentence.

$\endgroup$
3
  • 1
    $\begingroup$ This answer is almost correct. Note that the question didn't specify the language of the formulas. If the language include only equality, and possibly unary predicate symbols, then the valid sentences do make a decidable set. (I do assume, however, that the OP is interested in the case where there are at least some binary predicates, and probably function symbols too.) $\endgroup$ – Asaf Karagila♦ Jul 2 '14 at 2:14
  • $\begingroup$ @AsafKaragila; Thanks Asaf, I think I caught it. $\endgroup$ – Kyle Gannon Jul 2 '14 at 2:37
  • $\begingroup$ Confused what you mean "doesn't have quantifier elimination." Does this mean somehow we can't use Skolem normal form? Or just that quantifier rank is 1 or less? Because as long as we can skolemize our statement, there is a semi-algorithm to tell you if a first order statement is a validity, and that's first order resolution. It doesn't work on undecidable sentences, but it does admit a proof calculus for any sentence that is decidable. $\endgroup$ – dezakin Jul 2 '14 at 18:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.