Why is predicate logic semidecidable? Could someone explain clearly why predicate logic is said to be "semidecidable"? I know that the set of invalid formulas of a predicate language is not effectively numerable, which implies that predicate logic is not decidable (a set of expressions is decidable iff both it and its relative complement - in this case the set of invalid formulas - are effectively numerable). Instead, the set of valid formulas of a predicate language is effectively numerable. Does "semidecidable" simply means that the set of valid formulas of predicate logic is effectively numerable?
A further question: which are the main "reasons" for the undecidability of predicate logic?
Thanks a lot for your help.
Fish


Does "semidecidable" simply means that the set of valid formulas of predicate logic is effectively numerable?

Yes, "semidecidable," "effectively numerable," "recursively enumerable," and "computably enumerable" are all synonyms.
Now, as to the phrase "predicate logic is semidecidable": usually when we refer to a logic as being semidecidable, what we mean is that the inference problem - "does $p\vdash q$?" - is semidecidable (the set of pairs $(p, q)$ such that $p\vdash q$ is semidecidable). For strong enough logics, though, $p\vdash q$ iff $\vdash p\implies q$, so the logic is semidecidable iff the set of validities is. (For an example where this is not true, take e.g. a logic that doesn't even have a symbol for implication - like equational logic, which might sound artificially weak but is actually in certain ways the "right" logic for universal algebra.)
