Similarly, does There exist a Turing Machine which takes a Formal system and a string input and returns whether it is a wff or not? Ie it must be a decidable TM. I have heard there are Turing machines that correspond to formal systems, so this leads me to believe this is false, but im not sure. My intuition says you can construct a new formal system through a diagonal argument, proving this machine cannot exist.

  • $\begingroup$ What is your definition of "formal system," precisely? $\endgroup$ – Noah Schweber Jul 22 '19 at 1:36
  • $\begingroup$ A finite set of symbols known as the alphabet, A grammar, a set of axioms, and a set of inference rules. Basically just the standard formalization of "axiomatic system" $\endgroup$ – Connor Jul 22 '19 at 2:20
  • $\begingroup$ In general axiom systems are not required to be recursively enumerable - do you want your formal systems to be? $\endgroup$ – Noah Schweber Jul 22 '19 at 2:21
  • $\begingroup$ I want a TM that can take in a formal system and a string and tell if it is provable. Im just wondering if this is some halting problem or Accepts(A) problem in disguise. $\endgroup$ – Connor Jul 22 '19 at 2:26
  • $\begingroup$ How is a formal system presented to the Turing machine? Are you demanding that formal systems be somehow "finitely generated"? (Actually it's moot, the answer even for nice formal systems is no, but this is still a point you need to realize requires a precise definition.) $\endgroup$ – Noah Schweber Jul 22 '19 at 2:28

In a comment above, the OP clarifies:

I want a TM that can take in a formal system and a string and tell if it is provable.

First, note that this question is ill-posed: what is a "formal system" and what does it mean for a TM to "take [one] in"? Even if we take "formal system" to mean "first-order theory," which is reasonable, the second question is still problematic: a general first-order theory is a very infinite object, so there's no way in general to treat a theory as an input to a Turing machine.

So we need to restrict attention to "finitely describable" theories. One very good candidate notion is the finitely (equivalently, singly) axiomatizable theories; another significantly broader one is the recursively enumerable theories (here we really talk about codes for the theory rather than the theory itself).

Either way, however, the answer to your question is no. Indeed, this is true even for individual seemingly-nice formal systems, like (first-order) Peano arithmetic (or even much weaker theories of arithmetic): the set of theorems of Peano arithmetic is not computable.

This is a consequence of Godel's incompleteness theorem (or more precisely, its later improvement by Rosser).

Roughly speaking, Godel says that if $T$ is a consistent and recursively enumerable theory which is "strong enough to encode basic arithmetic" (this can be made precise, I'm just avoiding doing that), then $T$ is not complete. This isn't immediately what you're asking about; however, it does have as a quick corollary that if $T$ is such a theory then there is no algorithm for determining whether a given sentence is provable in $T$.

Why? Well, if there were, we could use a kind of greedy algorithm to build a recursive completion of $T$:

  • Enumerate the sentences in our language as $\varphi_i$ ($i\in\mathbb{N}$).

  • Define a sequence of sentences $\psi_i$ $(i\in\mathbb{N}$) inductively as follows:

    • If $\varphi_0$ is a theorem of $T$, then $\psi_0=\varphi_0$; otherwise $\psi_0=\neg\varphi_0$.

    • Having defined $\psi_i$ for all $i<n$: if $(\psi_0\wedge\psi_1\wedge...\wedge\psi_{n-1})\rightarrow\varphi_n$ is a theorem of $T$, then $\psi_n=\varphi_n$; otherwise $\psi_n=\neg\varphi_n$.

  • It's now easy to check that the theory $T\cup\{\psi_i:i\in\mathbb{N}\}$ is complete, consistent, recursively enumerable, and extends $T$; and this contradicts Godel.

That said, if $T$ is a recursively enumerable theory (equivalently, a recursively axiomatizable theory), then the set of $T$-theorems is recursively enumerable - not quite as good as recursive, but still much better than nothing. And here we do more-or-less have an equivalence: every r.e. set is of equivalent complexity to the set of theorems of some r.e. theory (indeed, of some finitely axiomatizable theory). So there is a "computations/theories connection," it's just a bit more complicated.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.