Is every Formal system expressible as a Turing machine and vice versa?

Question

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.

Answer 1

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.