What would be an example of decidable & undecidable in First Order Logic?
Edit: With first order formulas
[Math] Example of decidable & undecidable in First Order Logic
logic
Related Solutions
I'm not totally sure what you're asking, but let me take a stab at it:
Your sentence
One must see 'semi-decidable' as a property of the specific decision problem, i.e. keep apart "x is satisfiable" and "x is not satisfiable"
is absolutely correct. There are many senses in which two decision problems can be "equivalent," and the point is that semidecidability (or more commonly, computable or recursive enumerability) does not always respect these notions. For instance, every c.e. set is Turing equivalent to a co-c.e. set, but obviously no c.e. set is also co-c.e. unless it is computable. This is essentially the example you give of unsatisfiability for first-order formulas.
The passage about algebraically closed fields is correct but easy to be mislead by: the characteristic is not specified, so the theory ACL of algebraically closed fields does not decide, for example, the sentence "$\forall x(x+x=0)$." So ACL is indeed an example of an incomplete-but-decidable theory.
What is true is that ACL$_p$ - the theory of algebraically closed fields of characteristic $p$, for $p\in\{$primes$\}\cup\{0\}$ - is complete and decidable.
EDIT: The statement "$T$ does not decide $\varphi$" is potentially ambiguous, as it has two reasonable interpretations:
Neither $\varphi$ nor $\neg\varphi$ is $T$-provable (in symbols: $T\not\vdash\varphi$ and $T\not\vdash\neg\varphi$).
There are models of $T$ in which $\varphi$ holds, and there are models of $T$ in which $\varphi$ fails (in symbols: $T\not\models\neg\varphi$ and $T\not\models\varphi$).
Luckily, by the completeness theorem (see below) these two interpretations are equivalent. Note that this is a peculiarity of first-order logic; for this reason, it's good to avoid saying "$T$ decides $\varphi$" when discussing non-first-order logics unless one has already specified what this means.
I believe the above will resolve your question, but just for completeness (hehe) let me end by summarizing the situation:
Any recursively enumerably axiomatizable theory which is complete is also decidable (just search through proofs). However, a complete theory need not be decidable - e.g. $Th(\mathbb{N};+,\times)$ ("true arithmetic") is complete ($Th(\mathcal{M})$ is always complete, for any structure $\mathcal{M}$) but not decidable.
- Incidentally, by Craig's trick a theory is r.e.-axiomatizable iff it is recursively axiomatizable.
First-order logic is (sound and) complete, in the following sense: for any set of sentences $\Gamma$, a sentence $\varphi$ is true in every model of $\Gamma$ if and only if there is a proof of $\varphi$ from $\Gamma$. In symbols, $$\Gamma\models\varphi\iff\Gamma\vdash\varphi.$$ The right-to-left direction is basically trivial; the left-to-right direction takes work.
Best Answer
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$.