Re: An example of a complete but undecidable theory

From: David C. Ullrich (ullrich_at_math.okstate.edu)
Date: 07/05/04 

Date: Mon, 05 Jul 2004 15:02:29 -0500

On 5 Jul 2004 12:41:07 -0700, kramsay@aol.com (Keith Ramsay) wrote:

>David C. Ullrich <ullrich@math.okstate.edu> wrote in message news:<inkie0ttrsnf1kot8ujubldsskcl6442hs@4ax.com>...
>| Under various standard assumptions (the language is
>| countable so it's possible to enumerate all finite
>| sequences of wffs, there's an algorithm to decide
>| whether a given sequence of wffs is a proof)
>| complete imples decidable:
>|
>| If you want to decide whether P is a theorem,
>| enumerate all the valid proofs one by one;
>| eventually either a proof of P or a proof of
>| ~P will appear.
>
>The way to remember the conditions is to ask yourself
>when the little argument here applies. :-)

That's actually my method for remembering the hypotheses
to lots of things (including this).

>People planning to read mathematical logic should keep in mind
>that it's common to write about theories that aren't necessarily
>formal systems. The set of all sentences in first-order logic with
>=, +, * that are true of the natural numbers is sometimes called
>"true arithmetic". Many theorems in logic don't depend on whether
>the axioms are computably enumerable. True arithmetic is
>complete, but there is of course no algorithm for determining
>what sentences belong to it.

Indeed. Actually when I saw the question of whether complete
implies decidable my first impulse was to give exactly this
counterexample. Decided to give the proof instead of the
counterexample, this being usenet, where one tries to
determine and honor the poster's hidden assumptions...

Woulda been more fun if neither of us had been explicit
about the assumptions - then we'd actually have a proof
and a counterexample for the same statement.

>Keith Ramsay

************************

David C. Ullrich

Relevant Pages