Talk:Decidability (logic)

From Wikipedia, the free encyclopedia

THis is a comment or rather a question.

The article states:

If a system is undecidable, then there exist in it formulas which are not known to be either valid or invalid—perhaps such a formula can be categorized as neither valid nor invalid. Such formulas are said to be "undecided."

Isn't there some confusion with completeness? Decidability means availability of a procedure (algorithm) to figure out the deducibility of any formula without necessarily knowing its demonstration. If a theory is decidable, the algotithm in question can split any set of formulae in deducible (true, valid) and other. The idea of others being either invalid (false?) or indefinite (neither true nor false) comes from another concept.

Am I right?

81.195.25.24 19:51, 11 September 2005 (UTC)

You are completely right, the article was confused. I have fixed it now. -- EJ 19:00, 7 January 2006 (UTC)

[edit] Decidablility vs. Completeness

"Decidability means availability of a procedure (algorithm) to figure out the deducibility of any formula without necessarily knowing its demonstration. If a theory is decidable, the algotithm in question can split any set of formulae in deducible (true, valid) and other. The idea of others being either invalid (false?) or indefinite (neither true nor false) comes from another concept."

I can fathom from the above why a theory could be decidible but incomplete. You would then have a theory in which the halting problem is solvable (i.e. you could tell that a particular formula either evaluates as true or false, or else causes the checker to never halt, in which case it lands in the "other" pile along with the false formulas).

In a first-order theory, and especially in an incomplete one, it does not really make sense to say that a formula "evaluates as true or false". Anyway, to ensure decidability, there must be a checker which always halts, and outputs either "provable" or "not provable". Alternatively, if you insist on separating "true" and "false" sentences, it outputs "provable", "refutable", or "independent". -- EJ 19:12, 20 February 2006 (UTC)

But how can something be complete but undecidable? Doesn't incompleteness follow from undecidability? If there exists a finite proof of X or !X, that proof can be found by the so-called "British Museum Algorithm" (BMA) -- i.e. one just checks every finite, well-formed proof, until a proof of X or a proof of !X appears. Not a practical decision procedure, but, to my mind, that is a decision procedure. By that argument, any complete system must be decidable. The BMA only fails when a proof appears that cannot be checked, because the proof-checker never halts on it. And that only happens when there is an "indefinite" statement, a statement that is neither provable nor disprovable, or equivalently, a statement the proof of which is infinitely long, right? And _that_ only happens in an incomplete system...

...I think? I'm still working through a lot of this material but, well, let me put it this way -- if I'm wrong, I'd love for someone to explain to me why. I guess the definition of decidability above differs slightly from my understanding of it, in that the BMA relies on using proofs (i.e. it figures out the deducibility of a formula precisely by "knowing its demonstration"). Is "decidibility" really about being able to tell whether something is provable independently of its proof? Doesn't the decision algorithm then become just another method of proof? Solemnavalanche 19:16, 19 February 2006 (UTC)

There is an example in the article: the theory of true arithmetic is complete, but undecidable. More generally, any complete extension of, say, Robinson arithmetic, is complete and undecidable (Church-Rosser theorem, not to be confused with this one). What you call BMA is an algorithm only as long as you can decide whether something is or isn't a valid proof in the theory. In other words, it only works for recursively axiomatizable theories. -- EJ 19:12, 20 February 2006 (UTC)

I forgot to say: re: "Is "decidibility" really about being able to tell whether something is provable independently of its proof?" Yes, indeed, that's the whole point. A decision procedure may in some cases proceed by actually constructing a proof, but it is not a requirement. -- EJ 19:42, 20 February 2006 (UTC)

[edit] The theory of algebraically closed fields

Am I right in believing that Gödel's incompleteness theorem plus the decidability of the theory of algebraically closed fields (ACF) implies that there are propositions in arithmetic that cannot be translated into propositions in ACF? Naively, one would assume that propositions from arithmetic can be translated into statements about the obvious elements of any field of characteristic zero. In any case, it would be useful to have a link to some sort of introduction to ACF so readers can at least see what the axioms are, and perhaps see what the relationship to arithmetic is. Elroch 21:33, 15 March 2006 (UTC)

The axioms of ACF are just the usual axioms of a field plus a schema , where is a sentence which says "every polynomial of degree d has a root". In other words, models of ACF are exactly all algebraically closed fields, which is after all the intended meaning of "the theory of ...".

You cannot in general translate arithmetic sentences into fields of characteristic 0, simply because there is no way how to translate the quantifiers. For that you'd need a formula in the language of fields which defines the set of natural numbers in the field. No such formula exists for algebraically closed fields. However, such a formula may exist for other fields; for example, Julia Robinson proved that the integers are definable in the field of rational numbers, which implies that the theory of the rationals is undecidable. -- EJ 22:34, 15 March 2006 (UTC)