Let $\Phi$ be a finite set of first order formulas over a signature $S$. Assume that (we can prove that) $\Phi$ is complete, i.e. for each first order formula $\phi$ over $S$, we have $\Phi \vdash \phi$ or $\Phi \vdash \neg\phi$ or both.

Is the question of the consistency of $\Phi$ decidable in this case, i.e. can it be decided whether the case that both $\Phi \vdash \phi$ and $\Phi \vdash \neg\phi$ occurs?

It was remarked that I need to specify in more details how the problem is presented to an algorithm which should decide about the consistency. Because $\Phi$ is a finite set of formulas, it is equivalent to a single formula $\varphi$. Hence $\Phi$ can be presented (to the algorithm which should decide its consistency) by the sequence of symbols which make up the first order formula $\varphi$. The "(we can prove that)" part can be interpreted as the existence of a proof in $\operatorname{RCA}_0$ that $\Phi$ is complete. That proof could also be appended to the input, but if such a proof is known to exist, then the algorithm can also find it himself, hence there is no need to append it to the input. However, if we don't fix $\operatorname{RCA}_0$, then the information in which formal system the completeness of $\Phi$ can be proved should be part of the input.

  • 1
    $\begingroup$ Let me rephrase the question clarifying what I understand is the input and the output of the problem you are interested. INPUT: a first-order formula $\varphi$ such that it has at most (up to elementary equivalence) one model. OUTPUT: Yes/No depending whether the input formula has one or zero models. Thomas, is this reformalization the adequate one you are interested in? $\endgroup$ – boumol Jun 14 '13 at 8:30
  • $\begingroup$ Let me say that the problem in my remark is non computable (i.e., undecidable). This can be shown translating Hilbert's tenth problem (about the existential theory of natural numbers with addition and product) into your setting, because there is a mechanical way to translate a diophantine equation into a first-order formula (in the language with order,addition and product) expressing "it is a finite initial segment of the standard natural numbers of a fixed size and where there is a solution of the initial diophantine equation". Now I cannot can develop this into a full answer (maybe later). $\endgroup$ – boumol Jun 14 '13 at 9:16
  • $\begingroup$ @boumol The reformulation is nearly adequate, except for the "(we can prove that)" part, where the initial question is a bit open anyway. $\endgroup$ – Thomas Klimpel Jun 14 '13 at 20:10
  • $\begingroup$ Let me note that by completeness theorem of first-order logic it is equivalent for every sentence (using conjunction this allows to consider finite sets of sentences) the statements: 1) the sentence generates a complete theory in the sense of your question (i.e., you can prove ...), 2) the sentence has at most (up to elementary equivalence) one model. $\endgroup$ – boumol Jun 15 '13 at 11:55

As noted previously, a finite set $\Phi$ of formulas is equivalent to a single formula $\varphi$. The inconsistent first order formulas are sufficiently well understood (computably enumerable, but not decidable). Hence the answer depends only on the properties of the consistent complete finitely axiomatized theories. There are complete finitely axiomatized theories with countable models, take the dense linear orders without endpoints as example. Probably enough is known about finitely axiomatized theories to provide a negative answer to the question without the "(we can prove that)" part, but I probably won't take the pain to dig through that material. Below is a proof that decidability follows if the "(we can prove that)" part would give rise to a computably enumerable set of "candidate" consistent complete theories (for example if the proof would be a consistent and complete theory whose axioms could be derived from $\Phi$).

  1. The inconsistent first order formulas over a signature $S$ are computably enumerable, because being inconsistent means that $\bot$ can be derived in a finite number of steps.

  2. Iff the consistent (provably) complete finitely axiomatized theories $\mathcal T$ are computably enumerable, then the consistency of $\Phi$ from the question is decidable.

The algorithm is as follows: Check whether $\Phi$ is inconsistent. Simultaneously also check whether $\Phi$ corresponds to a theory $T \in \mathcal T$. Because each $T\in \mathcal T$ is complete, it is decidable whether $\Phi$ corresponds to $T$. So this algorithm will terminate by either finding a consistent theory $T$ which corresponds to $\Phi$, or otherwise finding a proof that $\Phi$ is inconsistent.

For the "only if" part, consider that the finite sets $\Phi$ of first order formulas over a signature $S$ which can be proved to be complete in a given formal system like $\operatorname{RCA}_0$ are computably enumerable, because any proof in a formal system has a finite number of steps. Hence decidability of consistency would make the set of the consistent (provably) complete theories computably enumerable.

| cite | improve this answer | |

A minimal answer to the question as originally posed. Consider the signature $S$ with no names, no predicates (not even identity), no function symbols, and just a single propositional variable $P$. So all wffs in this signature are (equivalent to) truth-functions of $P$, equivalent to either $P$ or $\neg P$ or $P \lor P$ or $P \land \neg P$.

Let $\Phi$ be a finite set of wffs including at least one wff that is equivalent to either $P$ or $\neg P$. Then trivially it entails $\varphi$ or $\neg \varphi$ for every available $\varphi$. So we have proved that $\Phi$ is complete.

But I haven't told you exactly what's in $\Phi$ so you can't decide whether it is consistent.

| cite | improve this answer | |
  • $\begingroup$ Of course the question assumes that $\Phi$ is given explicitly. I'm not sure whether this answer is just nitpicking on the formulation of the question, or whether it is a "real" answer that I should try to understand (on a deeper level). $\endgroup$ – Thomas Klimpel Jun 14 '13 at 7:15
  • $\begingroup$ The point I was making was, exactly, that you need some (explicit!) constraints on how $\Phi$ is presented to get an interesting question here. And requiring $\Phi$ to be "given explicitly" isn't quite the best way of putting the constraint either (consider "$\Phi$ if $\{P\}$ if Goldbach's conjecture is true, and $\{P, \neg P\}$ otherwise": that's explicit in one good sense, but to decide $\Phi$'s consistency requires settling Goldbach's conjecture, which isn't the sort of thing you had in mind, I guess!). $\endgroup$ – Peter Smith Jun 14 '13 at 10:26
  • $\begingroup$ I am afraid that the question has the common ambiguity of the word "decidable": in some contexts it refers to "computable", and in some others it refers to "provable in some particular logical system". Peter refers here to second meaning, but it is not clear to me what is the meaning in the original question (I bet for the computability one). $\endgroup$ – boumol Jun 14 '13 at 11:09
  • $\begingroup$ @PeterSmith OK, then I understand your point. So I will have to edit the question to make it clear that $\Phi$ is presented (to the algorithm which should decide its consistency) as the sequence of symbols which make up the first order formula $\varphi$ (which represents $\Phi$). But before I do this, I have to think about how the proof that $\phi$ is complete should be presented (to the algorithm). Maybe I will just omit the "(we can prove that)" part, even if this might open the door for simple counter examples. $\endgroup$ – Thomas Klimpel Jun 14 '13 at 20:02

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.