Talk:Decidability (logic)

Inconsistency?

The article says that group theory is undecidable. However this wikipedia article List of first-order theories says that Abelian group theory is decidable. It seems to me that if Abelian group theory is decidable, then certainly ordinary group theory should be. Can someone please clarify? — Preceding unsigned comment added by 72.48.98.27 (talk) 18:25, 4 January 2013 (UTC)

CS

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)

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)

Hey, wait a second, the theory of true arithmetic is not complete, courtesy of Gödel. I would also like a good explanation of how any theory could be complete but undecidable! – Kiewbra (talk) 12:33, 9 January 2013 (UTC)

You seem to be confused about the notions involved. A theory is complete, by definition, if for every sentence, it proves the sentence or its negation. The true arithmetic is, by definition, the set of all sentences valid in the standard model of arithmetic $\mathbb {N}$. Since the definition of satisfaction in a model guarantees that every sentence or its negation holds in the model, true arithmetic (or the theory of any other model for that matter) is complete. Gödel’s theorem is not applicable, since the theory is not recursively axiomatizable. There are of course much simpler complete undecidable theories: for instance, let L be the language with one unary predicate P and countably many constants c_n, n ∈ N, let X be any undecidable subset of N, and let T be the theory axiomatized by the sentences c_n ≠ c_m for every n ≠ m, P(c_n) for every n ∈ N, and ¬P(c_n) for every n ∈ N \ X. Then T is complete and undecidable.—Emil J. 13:31, 9 January 2013 (UTC)

Why the theory of ACL is decidable but incomplete? I think when we talk about the completeness of a theory, we talk about syntactical completeness. Syntactical completeness means for each sentence φ, either φ or ¬φ is a theorem, while decidability means there is an effective procedure to decides φ or ¬φ is a theorem. It seems that the syntactical completeness is a consequence of the decidability. Am I wrong? - Namasikanam (talk) 08:07, 5 April 2022 (UTC)

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 $\{\varphi _{d};\,d>0\}$, where $\varphi _{d}$ 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)

The article claims that the Theory of Real Closed Fields is incomplete, contradicting also this page (provided that the characteristic is fixed). Martin Ziegler (talk) 09:44, 12 October 2017 (UTC)

Precise and imprecise definitions

There is some confusion in the definition of Decidability (logic) that needs resolution. It is related to the concepts of effective method, algorithm, and recursive computability. The essence of Church's thesis is that the latter precise notion adequately captures the imprecise informal notion of effectiveness.

In computability theory, the usual approach is to formalize the notion of algorithm in terms of computable function, where the latter notion is defined by reference to the set of (in this respect) equivalent approaches that include (general) recursion, Turing machines, and the lambda calculus.

In giving definitions based on these notions, we must not assume the truth of Church's thesis as being given, but be clear whether they are based on the informal notion or the precise notion. For the purpose of discussion, I call a concept precise when its definition uses the precise notion as used in computability theory, and imprecise when its definition is based on the imprecise notion of effectiveness.

• Decidable language redirects to Recursive language, which is precise.
• Decidable set redirects to Recursive set, which is precise.
• Decidable problem redirects to Decision problem, which gives a precise definition.
• Decidability redirects to Decidable, a disambiguation page.
• Decidability (logic) is imprecise.

Decidability (logic) used to be unequivocally precise, but as of this revision it became equivocal. The definition came to be based on the wff's forming a decidable set (precise), which however was declared to be equivalent to the existence of an effective method (imprecise).

Then, as of this revision, the concept was made unequivocally imprecise.

I find the current revision (as of this moment) hardly comprehensible where it goes off into "We may put this another way", but it is in any case still definitely imprecise.

The present definition actually follows the definition given in Hunter (1973), Metalogic: An Introduction to the Metatheory of Standard First Order Logic (p. 118):

A system S is decidable iff there is an effective method for telling, ...

In this book, "effective method" is explicitly imprecise; after giving a definition of effective method, the text states: "This is not a very precise definition, but the concept is not a precise one" (p. 14).

I am insufficiently familiar with the use of the notion of decidability in logic to figure out which among the following possibilities best describes the situation:

1. The notions of decidability in logic and in computability theory are fundamentally different: the former is imprecise and the latter is precise. This means that the Wikipedia version before the revisions referred to above (which was precise) was wrong. In this case we must make it explicit to the reader that the notions are fundamentally different.
2. In the field of logic several definitions are current, precise and imprecise. In that case we must make it explicit to the reader that there are several definitions. How do other texts than Metalogic define the notion?
3. Metalogic uses an oddball definition (like it does, in fact, for decidable set; see p. 16), and also in the field of logic the notion is usually precise. In that case we should use the precise definition and perhaps point out in a footnote that there is a text defining this imprecisely.

 --Lambiam 16:24, 8 February 2008 (UTC)

I have trouble following what you're getting at. Are you saying that you do not consider the words "effective", "decidable", "computable" to be synonymous? That would, I think, be a rather non-standard usage. –Henning Makholm 21:37, 8 February 2008 (UTC)

FWIW, I am not happy with the recent changes either, but for a different reason. The new wording seems to tacitly identify a theory with the set of wffs that are theorems in it, and expects the unprepared reader to understand casual references to a formula being "in" the theory. That level of technical arrogance is not worthy of a general encyclopedia. –Henning Makholm 21:37, 8 February 2008 (UTC)

First, if you wish to make it precise, change the article to say that a decidable logic is one whose set of theorems and its complement are both semirecursive (in the usual sense of semirecursive as it applies to sets). Or you may wish to substitute for 'effective method' 'recursive function' which in the present situation is a characteristic function that, when given a formula as argument, returns a 1 if the formula is a theorem, and returns a 0 otherwise.

Second, not every article is to be entirely self-contained. I think this sort of article, relatively narrow in scope, is allowed to assume a certain amount of basic metatheory from the reader, regardless of the fact that it is encyclopedic.

Last, it is nowhere claimed that a logic and its theory are the same thing, though this is frequently done in the literature(e.g. see Blackburn et al Modal Logic). The present definition of a decidable logic given in terms of the set of theorems of a logic is general. I see nothing wrong with this. If you wish, you may edit the article to account for every kind of logic (e.g. natural deduction systems, sequent calculi, etc.) so that for an axiom system, for example, the article will say that each axiom is finite and each rule is recursive (taking schemata to be rules). This sort of definition lacks generality. Or you may wish to give these sorts of definitions as further examples.

Notice that the article also assumes that the set of wffs is recursive. Maybe you want to say something about this as well.Nortexoid (talk) 22:51, 8 February 2008 (UTC)

Responses. (1) It is not so much a question of what I want, as of what we want – which is what is best for the project. But what is best? (2) Unlike Henning Makholm, I do not think the automatic equation of "effectiveness" with "recursive computability" is standard. Our articles do not assume it, and neither does the book Metalogic.  --Lambiam 02:54, 9 February 2008 (UTC)

It is not like there needs to be a "compromise". The article may include a definition in terms of effective methods and another in terms of recursive sets or functions. The one in terms of effective methods is accessible to a wider audience (e.g. those who know little or nothing about recursion/computability theory). And you're right, effective calculability is not synonymous with recursive computability (or any other extensionally equivalent notion), nor is it wrongly assumed in the article. Nortexoid (talk) 13:17, 9 February 2008 (UTC)

There are many things that "may", but what "should"? Is the definition of Metalogic an oddball definition or is this normal, perhaps even standard, in logic? The answer to this question (which I don't know) makes a difference in how we should cover this in Wikipedia.  --Lambiam 18:47, 9 February 2008 (UTC)

Some texts aim to be more rigorous than others. It depends on the intended audience. I cannot recall a logic text that defines decidability in terms effective procedures, though now that I think of it, perhaps Cutland's does, since throughout he is continuously invoking Church's thesis. Unfortunately my text is not at home. In any case, what do you think is the intended audience of a Wikipedia article? I think it would be nice to include both definitions with an appropriate remark regarding the differences between them. Nortexoid (talk) 21:22, 9 February 2008 (UTC)

Cutland defines effectively decidable as: the characteristic predicate is computable (p. 22), where the latter notion is short for URM-computable, or computable by an unlimited register machine, a universal model for computation equal in power to Turing machines. Additionally, the book embraces Church's Thesis explicitly (pp. 67–68). In this respect the text is no different from any other text on recursive function theory that I have seen; all use this or an equivalent approach. What I do not know is the situation in logic.  --Lambiam 06:56, 10 February 2008 (UTC)

The premise of your objection is false. Your definition and use of "precise" is obviously unacceptable as it presuppposes your view. It is more precise to say effective method, than it is to say algorithm. An algorithm is a type of effective method, not the other way around. To define it in terms of algorithm is to leave out a denumerably infinite number of other valid interpretations of this term "decidability". I think you are confused on precision in appropriateness for your needs, with precision in a description corresponding to the reality. The encyclopedia seeks the latter.

What exactly justifies your belief that effective method is informal? The requirement of rigor is a part of it's definition, so you are off on that. This is another conflict arising from the issue of accounting for the meta-logical/mathematical foundations of mathematical activity.

The relationship of both terms should be made explicit in all of the articles you mention. Where both terms are related to the topic, they should both be included in the article. Be well. Pontiff Greg Bard (talk) 23:09, 9 February 2008 (UTC)

I don't know what the premise is you are referring to. If I, for the purpose of some discussion, choose to define the word "deep" as meaning "derived using methods of complex analysis in an essential way", then that is what it means in the context of that discussion, and it is pointless to say that this definition is "unacceptable" and that it "presupposes" some view. It just encapsulates, for the purpose of discussion, a ten-word phrase in a single word. Above I could also have written "purple concept" and "indigo concept" instead of "precise concept" and "imprecise concept", without any change in meaning. I did not do that because it would be difficult to remember which of the two again was purple and which indigo. Please reread what I wrote. There are two definitions of "decidable", call them indigo-decidable and purple-decidable, or hotly-decidable and coldly-decidable, or whatever. They are not known to be equivalent. Some articles use one notion, others use the other notion. Nowhere is there a warning of this to the unsuspecting reader. Recently, the present article switched from using a cold definition to an indigo definition. All I did was point out that situation. The following questions are now (in my opinion) eminently reasonable and do not presuppose any particular view. (1) Is this hot approach standard, or do other authors use purple? (2) How common is one, how common the other? (3) Should we give both definitions? These questions are not independent. Many terms in mathematics and logic have different definitions depending on the author, and usually we will give both if they are common enough. If not, we would nevertheless try to issue some kind of warning, as is done for example in our article Local ring concerning the assumption of being a Noetherian ring. After all, a statement that is true for one version may well be false for the other one. What we typically would avoid is using one definition in one article and another definition in other articles without a warning, as is the case here now.  --Lambiam 06:23, 10 February 2008 (UTC)

I am actually quite familiar with the distinction between "effective" vs. "computable" functions. The terms "effectively calculable" and "algorithm" are each undefined, slightly vague terms of natural language, while "computable" is a precisely defined term. Church's thesis claims that the terms are extensionally the same, and in some contexts it's convenient to idenitfy them (see the lede to Decidable_set).

My impression is that the majority of logic texts would identify the decidable theories as the ones with a computable characteristic function. Perhaps we can make a list of texts and the definitions they employ, to check. I'll add some here later this morning. — Carl (CBM · talk) 13:08, 11 February 2008 (UTC)

I tried to resolve this a different way when I edited the article this morning. I hope that the section on relationships with computability is enough to clarify what's going on. Please feel free to improve it. — Carl (CBM · talk) 16:07, 11 February 2008 (UTC)

Introduction

Could Nortexoid please explain this revert?

What is incorrect about my explanation of "semi-decidable"? Why does the introduction have to be obscurified by introducing symbolic such as T and A when ordinary nouns will clearly suffice? What do you find "obscure" about the words generate and eventually? What do you have against telling the reader plainly that the difference between semi-decicability and full decidability is that in a system that is only semi-decidable it may be impossible to know for sure that a formula is not provable?

And why do you insist on supposing that a reader will know without explanation that you use "accept" to stand for recursive enumerability rather than decidability? I would not have guessed this if I had not already known what must be meant. –Henning Makholm 03:54, 11 February 2008 (UTC)

Your edit stated "A semi-decidable system is one for which there is an effective method for generating theorems (and only threorems) such that every theorem will eventually be generated" where I have emphasized the incorrect parenthetical part. It would follow that no decidable system is semi-decidable. However later you confusingly though correctly add "Every decidable theory is also semi-decidable". And from talking about "systems" you have now gone back to talking about theories. In fact I thought that whole paragraph was unclear. So was the epistemic remark about knowing which has nothing to do with decidability.

The initial addition of 'accept' is not my doing. I reverted to the wrong one. JRSpriggs reverted to the "right" one. You reverted back again to the 'accept' one. As for the introduction, you may rewrite it to avoid naming theories, languages, or arbitrary formulas, as long as it retains its clarity. Nortexoid (talk) 09:02, 11 February 2008 (UTC)

The addition of "accept" was my doing, and it was meant to be just a quick fix to the previous flawed wording which defined, in effect, semidecidable systems as those which are decidable. I do not claim that it is particularly nice or clear style.

I think that Henning Makholm's version is pretty good, and certainly much more clear than the current one. I fail to understand how do you want the "and only theorems" part to preclude decidable systems from being semidecidable. In fact, if you omit the parenthesis, then every set becomes semidecidable by the definition, as witnessed by the algorithm which enumerates all finite strings in the given language. -- EJ (talk) 12:21, 11 February 2008 (UTC)

Hmmm, that's right about the parenthetical remark. I had something else in mind. Nonetheless, the bit about 'we may never know...' is unhelpful, as was the entire paragraph from which it was taken.

I don't see how your quick fix has fixed anything. What exactly was the problem? What does it mean to say that decidability is symmetric? Nortexoid (talk) 13:22, 11 February 2008 (UTC)

Decidability is symmetric in the sense that the existence of a decision procedure for a set X is equivalent to the existence of a decision procedure for its complement. The problem was that the version of the article said

"If there is an effective method for deciding for any A in the language L of T whether A is in T then T is semi-decidable"

which is completely wrong, if there is an effective method for deciding for any A whether A is in T, then T is already decidable, not just semidecidable. Semidecidability needs an algorithm which merely accepts T, i.e., terminates with a "YES" answer for any A in T, and either terminates with a "NO" answer or does not terminate at all for any A not in T. -- EJ (talk) 13:50, 11 February 2008 (UTC)

No, it says whether A is in T, not "whether or not A is in T". These mean different things. Nortexoid (talk) 14:39, 11 February 2008 (UTC)

N., a piece of advice style manuals often give is that "whether or not" means the same as "whether", and the former should be avoided as redundant. So at the least, you can't assume the reader will think they mean different things. In particular, I will usually remove the "or not" when I copyedit an article. — Carl (CBM · talk) 15:41, 11 February 2008 (UTC)

Second meaning

The article is currently conflating two different meanings of the term decidable:

• A set of sentences is called decidable if its characteristic function is computable.
• A logical systems (propositional or first-order logic, for example) is called decidable if the set of logical validities is computable.

I don't have time to fix this right now, but I marked the two places where the second definition is intended, while the lede gives only the first definition. — Carl (CBM · talk) 13:12, 11 February 2008 (UTC)

It depends what you mean by "a logical system". Sometimes that is taken to include a semantics (e.g. classical model theory) and sometimes it is purely syntactic, meaning a deduction system or a presentation of one. What is usually meant by the decidability of a logical system is that its set of axioms (or the set of code numbers of its axioms) and rules of inference are recursive. This has nothing to do with validities. Nortexoid (talk) 13:30, 11 February 2008 (UTC)

Nevermind, I thought you were referring to just the introduction. I see what you mean. Nortexoid (talk) 13:33, 11 February 2008 (UTC)

(For everyone else - I was referring to the 4th paragraph). N., your point only underscores the large number of meanings of the term decidable that will need to be presented in this article. — Carl (CBM · talk) 13:36, 11 February 2008 (UTC)

Huh?!? In logic (and in this article, at least until the recent mess of edits and reverts), decidability of a system always means decidability of its set of validities (whether defined semantically or proof-theoretically). Mere decidability of the set of axioms and rules is not called decidability of the logical system, but recursive axiomatizability. (Or semidecidability/recursive enumerability/computable enumerability, as that's equivalent to it in most typical situations.)

If this were true at all (in fact it's not) then it would be true only in the case that the syntactic part of the logic is sound and complete wrt its semantics. According to your definition it is possible to have a logic be decidable even though its proof system is not recursively axiomatizable or its set of theorems not recursive.

But there is a deeper issue. There are logics with no validities yet non-empty consequence relations. (Some popular three-valued logics are like this.) Decidability in the sense you present is uninteresting in these cases. A general notion of 'decidability of a logic' means 'decidability of its consequence relation'. Nortexoid (talk) 14:56, 11 February 2008 (UTC)

I am not assuming anything about completeness or soundness. The term is applied in different contexts for both syntactically and semantically defined systems, and I used the word "validity" above as a generic name for either syntactic or semantic consequence, as demanded by the context. If there is a mismatch between a semantical and syntactical part of a logical system, then they actually make up two different systems, each with its own notion of decidability.

What you say about consequence relations is true, yet that's just a simple variation of the same concept. In all the situations you described, decidability is applied to a deductively closed system/consequence relation/what have you, not to a bare set of axioms as you claimed in your previous post[1]. According to that definition, first-order classical logic, Peano arithmetic, and other such systems are all decidable, which is contrary to the standard usage of the term. -- EJ (talk) 15:20, 11 February 2008 (UTC)

Speaking of consequence relations: the usage may differ in various fields of logic, but at least in modal logic the standard usage is that "decidable logic" refers to decidability of the set of theorems, whereas decidability of the full consequence relation is called in another way. The distinction is real, as there actually exist decidable normal modal logics with an undecidable consequence relation. -- EJ (talk) 16:01, 11 February 2008 (UTC)

I don't doubt that that is true; on the other hand, it means that you are including the deductive system as part of the logic, which is common in some areas but not in others. Could you work on improving the article regarding this issue? I don't have a good feel for what's normal in modal logic, or any references about out. A simple reference to a standard text goes a long way towards clarifying things. — Carl (CBM · talk) 16:06, 11 February 2008 (UTC)

Normal means normal modal logic, and it indeed amounts to fixing a deductive system except for a possible addition of axiom schemata. I am aware that there are different conventions in other areas, I just wanted to point out that it's not an entirely good idea to present decidability of the full consequence relation as the "general notion of decidability of a logic" as Nortexoid suggested, because it may conflict with the actual usage. -- EJ (talk) 16:25, 11 February 2008 (UTC)

Sorry, I missed the sentence about modal logic which you added to the article when I wrote the reply above. I suspect that we slightly misunderstand each other. The issue is not whether the logic is defined semantically or proof-theoretically (modal logic can be defined semantically just fine, provided one uses the right semantics; though there may be other logics where this is not possible). The issue is whether "decidable logic" means decidability of only the set of its theorems

$\{A\mid {}\vDash _{L}A\},$

or decidability of the consequence relation

$\{\langle B,A\rangle \mid B\vDash _{L}A\}.$

The former is what the article currently describes, and what is also common usage in modal logic (so I do not feel any urge to change the article). The latter is used in some other areas, such as some multivalued logics, as pointed out by Nortexoid. I am not sufficiently familiar with this usage to write up something about it in the article.

As for references on modal logic: Chagrov and Zakharyaschev is one of the standard reference works, and it discusses many problems pertaining to decidability in detail. (In particular, the counterexample I mentioned above is there.)

Thank you once again for your work on the article. -- EJ (talk) 17:03, 11 February 2008 (UTC)

It's no problem; I wouldn't be around if I didn't want to improve the articles. Thanks for the reference, which I added to the article. — Carl (CBM · talk) 17:15, 11 February 2008 (UTC)

Hmm. As I tried to explain above, modal logic is a bad example to illustrate the point being made in the context where it is used in the article. Likewise, I gave the reference to show something quite different from what is claimed in the article. I'll try to fix that. -- EJ (talk) 13:54, 13 February 2008 (UTC)

Yes, I misunderstood both you there. I was reading the word "theorem" to mean syntactic consequence, and "consequence relation" to mean semantic consequence. That gives your sentence "at least in modal logic the standard usage is that "decidable logic" refers to decidability of the set of theorems, whereas decidability of the full consequence relation is called in another way" a meaning you didn't intend. Thanks for fixing it; I think I understand your terminology now. — Carl (CBM · talk) 14:55, 13 February 2008 (UTC)

CBM, what might have confused you is that logics and theories are often identified with their sets of theorems. So, there is no difference between the two meanings you present, the wording "A is in T" in the lead is really supposed to mean "A is valid in T". This is another reason why I prefer Henning Makholm's version [2] of the article, which makes it explicit. -- EJ (talk) 14:05, 11 February 2008 (UTC)

My point is that these quotes from the article use different meanings of the word decidable:

• "Every complete recursively enumerable theory is decidable. "
• "Propositional logic is decidable"

The latter is about decidability of a logic, the former about decidability of a theory. I'm going to edit the article to explain both of them, but if this article is only meant to cover one or the other, my text can be moved somewhere else more appropriate. — Carl (CBM · talk) 14:40, 11 February 2008 (UTC)

I don't follow. The latter statement is about decidability of a logic as the set of its theorems, and the former statement is about decidability of a theory as the set of its theorems. It is thus exactly the same meaning, in one case applied to a system which happens to be a propositional logic, and in the other case to a system which happens to be a first-order theory. Why do you think that the article currently does not cover both cases, and which one is the supposedly uncovered one? -- EJ (talk) 14:52, 11 February 2008 (UTC)

I edited the article some. Let me know what you think, and feel free to improve my writing mercilessly. — Carl (CBM · talk) 15:15, 11 February 2008 (UTC)

Your rewrite is very nice, thanks for the work. -- EJ (talk) 15:35, 11 February 2008 (UTC)

References

essential undecidability

Feferman and Feferman's 2004 biography of Alfred Tarski (p. 193) seems to indicate that this concept was introduced in the 1953 book Undecidable Theories by Tarski, Mostowski, and Raphael Robinson. This might or might not be worth mentioning in the article. 66.127.52.47 (talk) 20:58, 18 March 2010 (UTC)

Undecidable or incomplete

Please someone make really sure that "undecidable" is not confused with "incomplete", especially in this sentence under "Some undecidable theories": "Gödel's incompleteness theorems show that many other sufficiently strong theories of arithmetic [are undecidable]." Doesn't Gödel show that all sufficently strong theories of arithmetic are incomplete (by constucting an "undecidable"/independent sentence (where undecidable here has another meaning))? – Kiewbra (talk) 12:29, 9 January 2013 (UTC)

Hmm. Undecidability of consistent extensions of Q is usually bundled together with incompleteness theorems, and in fact, it follows easily enough from the Gödel–Rosser incompleteness theorem, since every consistent decidable theory has a decidable complete extension (though the usual proof goes the other way round). However, you are right that strictly speaking, Gödel didn’t prove the undecidability theorem, and even predates the definition of recursive sets. I’m not sure who first formulated the undecidability theorem in this form. The formulation using the concept of essentially undecidable theories comes from was popularized by the Tarski, Mostowski, and Robinson monograph, though Robinson presented the essential undecidability of his arithmetic earlier in 1950, and I suppose the concept of essential undecidability itself is due to Tarski.—Emil J. 13:59, 9 January 2013 (UTC)

See also

What is the significance of the "See also" section? It seems to have names of logicians and years, but I can't match Quine's year to a specific event or paper. — Arthur Rubin (talk) 16:02, 21 January 2014 (UTC)

Redundant articles maybe?

I'm no illiterate on the subject, but aren't the Decision problem and Undecidable problem kinda dealing with the same stuff as this one? --uKER (talk) 22:52, 19 July 2018 (UTC)