Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

What would be an example of decidable & undecidable in First Order Logic?

Edit: With first order formulas

share|cite|improve this question
The question is still nonsense. What is your definition of "decidable in first-order logic"? – boumol Dec 11 '12 at 9:04

There are two very different notions of undecidability.

1) Let $T$ be a theory (say thought of as a collection of axioms). Then a sentence $\varphi$ is undecidable in $T$ if $\varphi$ is not a theorem of $T$, and $\lnot\varphi$ is not a theorem of $T$. A more useful term to describe such a theory is to say that the theory is incomplete.

This kind of undecidability is very common, and often a deliberately built-in feature of a theory. Let $T$ for example be the usual axiomatization of group theory, and let $\varphi$ be the sentence $\forall x\forall y(x=y)$. Then $\varphi$ is not provable in $T$, for there are groups with more than $1$ element. And $\lnot\varphi$ is not provable in $T$, for there certainly is a $1$-element group.

Sometimes, undecidability of a theory in this sense is a surprise. Let $T$ for example be first-order Peano arithmetic. This theory is very strong. And yet it turns out to be incomplete.

Another example is the standard set theory ZFC. This is very strong indeed, enough for almost all of mathematics. Yet for general reasons it turns out to be incomplete. More specifically (if ZFC is consistent) then neither the continuum hypothesis nor its negation is a theorem of ZFC.

2) The probably more standard sense of undecidable is that there cannot be algorithm for accomplishing a certain task. A theory $T$ is undecidable in this sense if there is no possible computer program that will, on any input $\varphi$, determine whether of not $\varphi$ is a theorem of $T$.

It turns out that Peano Arithmetic, and ZFC, if consistent, are undecidable in this sense. There is a very large collection of theories known to be undecidable.

Much more is true. For example, there is no algorithm that, given any polynomial $P(x_1,\dots,x_n)$ with integer coefficients, will determine whether the equation $P(x_1,\dots,x_n)=0$ has integer solutions.

But there are interesting theories that are decidable. A nice example of such a theory is the theory of algebraically closed fields of characteristic $0$.

share|cite|improve this answer

It isn't at all clear what is being asked. First order what? A first order theory, or pure first order logic?

Which propositions $\varphi$ are decided by the first-order theory $T$ (i.e. which propositions $\varphi$ are such that either $T \vdash \varphi$ or $T \vdash \neg\varphi$) will depend on the theory: nothing usefully general can be said.

Which propositions $\varphi$ are decided by the first order logic (i.e. which propositions $\varphi$ are such that either $\vdash \varphi$ or $\vdash \neg\varphi$) is easier. By the completeness theorem they are the propositions such that $\vDash \varphi$ or $\vDash \neg\varphi$, the logical truths and the logical falsehoods.

But which propositions are they? In general we can't decide (now in the different sense of there being no algorithm for telling of a general $\varphi$ whether it is a first-order logical truth). But there are restricted cases where the problem is a decidable one: for example, there is an algorithm for deciding whether $\varphi$ is logically true if $\varphi$ has only one-place predicates.

And if none of those remarks help, then you are going to have to rephrase the question more carefully and explicitly.

share|cite|improve this answer
my bad, i have rephrased it hope that is clearer – Masterminder Dec 10 '12 at 16:34

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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