Does decidability of a theory imply completeness of the theory?

post by Noosphere89 (sharmake-farah) · 2023-07-29T23:53:08.166Z · LW · GW · No comments

This is a question post.

Contents

  Answers
    8 Algon
None
No comments

I know right now that completeness implies decidability of a theory, but the question is essentially the converse of this:

Given an arbitrary formal theory that is somehow decidable by a Turing Machines, in the sense that for any sentence in the theory, you can decide it's truth or falsity by some means, can you show that it will inevitably be a complete theory?

If it isn't universally the case that decidability of a theory implies the completeness of a theory, are there any conditions that are required to have decidability of a theory be equivalent to completeness of a theory?

Answers

answer by Algon · 2023-07-30T00:05:51.473Z · LW(p) · GW(p)

No. This answer to a related stack-overflow question explains why:

 

That is to say a first order logic without any predicate or function symbols is decidable. But you can have incomplete theories in such a signature. 

comment by Noosphere89 (sharmake-farah) · 2023-07-30T00:26:47.431Z · LW(p) · GW(p)

Thank you for answering the question quickly, it was nice to know that being decidable wasn't implying completeness like completeness implied decidability.

Replies from: Algon
comment by Algon · 2023-07-30T14:40:04.824Z · LW(p) · GW(p)

Completeness doesn't imply decidability though? Peano arithmetic is complete and undecidable. Maybe you meant completeness + semidecidability - > decidability?

Replies from: sil-ver, sharmake-farah
comment by Rafael Harth (sil-ver) · 2023-07-30T15:41:23.174Z · LW(p) · GW(p)

Peano arithmetic is not complete. I think the claim from my post is correct except that it misses having a computable set of axioms as a second requirement (which in the post more or less follows from context, though I should still probably add it explicitly) actually nvm I did say this in the post. (See e.g. https://math.stackexchange.com/questions/1280043/every-complete-axiomatizable-theory-is-decidable)

Replies from: Algon, sharmake-farah
comment by Algon · 2023-07-30T16:05:49.817Z · LW(p) · GW(p)

Sure, that's true. I should've said the theory of the standard model of Peano arithmetic. That's complete, undecidable and can't have a recursive axiom system.

Replies from: sharmake-farah
comment by Noosphere89 (sharmake-farah) · 2023-07-30T16:12:06.822Z · LW(p) · GW(p)

I'm going to ask a new question, different from the old question I asked: Given a halt oracle added to the Turing Machine, that is a magical oracle tape that can solve all problems Turing-reducible to the halting problem, can we nail down the standard interpretation/model of Peano Arithmetic?

Replies from: lbThingrb
comment by lbThingrb · 2023-07-30T17:03:39.165Z · LW(p) · GW(p)

The true first-order theory of the standard model of arithmetic has Turing degree . That is to say, with an oracle for true arithmetic, you could decide the halting problem, but also the halting problem for oracle Turing machines with a halting-problem-for-regular-Turing-machines oracle, and the halting problem for oracle Turing machines with a halting oracle for those oracle Turing machines, and so on for any finite number of iterations. Conversely, if you had an oracle that solves the halting problem for any of these finitely-iterated-halting-problem-oracle Turing machines, you could decide true arithmetic.

Replies from: sharmake-farah
comment by Noosphere89 (sharmake-farah) · 2023-07-30T17:12:51.732Z · LW(p) · GW(p)

So the answer is no, even a magical halt oracle cannot compute the true first order theory of the standard model of arithmetic, but there are machines in which you can compute the true first order theory of the standard model of arithmetic.

Replies from: lbThingrb
comment by lbThingrb · 2023-07-30T17:23:20.589Z · LW(p) · GW(p)

Correct. Each iteration of the halting problem for oracle Turing machines (called the "Turing jump") takes you to a new level of relative undecidability, so in particular true arithmetic is strictly harder than the halting problem.

comment by Noosphere89 (sharmake-farah) · 2023-07-30T16:08:11.768Z · LW(p) · GW(p)

Your post is below, so anyone else can follow this conversation if necessary.

https://www.lesswrong.com/posts/Tb4mJWh3FYGRyid6C/understanding-goedel-s-incompleteness-theorem [LW · GW]

comment by Noosphere89 (sharmake-farah) · 2023-07-30T14:50:09.175Z · LW(p) · GW(p)

Sort of, though I was thinking of this quote from Rafael Harth's post below:

However, if the theory of A is complete, then it is also decidable! This is so because: If A is complete, for each sentence F, either F or ¬F is valid. Thus, either F or ¬F is internally provable. (Gödel's completeness theorem.) Therefore, we can write a procedure that, given any sentence F, searches for internal proofs for F and ¬F in parallel and outputs 'YES' and 'NO', respectively, if it finds one. Since one of them is always internally provable, this always works.

I was trying to think of an answer to how this could work, or alternatively how this couldn't work.

Replies from: Algon
comment by Algon · 2023-07-30T15:25:26.257Z · LW(p) · GW(p)

Based off that passage, I don't see Rafael Harth's argument works either.

No comments

Comments sorted by top scores.