Let's say checking if a proof is valid is decidable. Then surely we can just enumerate the proofs then check if it's valid. This seems to be a semi-decidable procedure. But why Entscheidungsproblem is undecidable then?
Why is Entscheidungsproblem undecidable not semi-decidable
computabilitylogic
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 is a lot of terminology, and a lot of redundant terminology, in computability theory. Briefly, here's the situation:
Decidable, recursive, and computable are all equivalent.
Semidecidable, recognizable, recursively enumerable (r.e.), and computably enumerable (c.e.) are all equivalent.
In general, the "computation"- and "recursion"-centered terminologies are the standard ones - with the former more modern than the latter. So in the modern literature you'll see references to r.e. or c.e. sets, but rarely to semidecidable sets.
A set with c.e. (or etc.) complement is called co-r.e. or co-c.e.; I've not seen "co-semidecidable" before, but I wouldn't be surprised if it occurred.
There is no specific term for non-c.e. (or etc.). You just say "non-c.e."