0

So I'm reading the famous paper of Turing "On Computable Numbers, with an Application to the Entscheidungsproblem". At the beginning of his proof of the undecidability of first-order logic (FOL), he claims the following:

It should perhaps be remarked that what I shall prove is quite different from the well-known results of Gödel. Gödel has shown that (in the formalism of Principia Mathematica) there are propositions such that neither nor ¬ is provable. As a consequence of this, it is shown that no proof of consistency of Principia Mathematica (or of K) can be given within that formalism. On the other hand, I shall show that there is no general method which tells whether a given formula is provable in K, or, what comes to the same, whether the system consisting of K with ¬ adjoined as an extra axiom is consistent.

With K being the axiomatization of FOL given by Hilbert and Ackermann. Furthermore, he claims:

If the negation of what Gödel has shown had been proved, i.e. if, for each , either or ¬ is provable, then we should have an immediate solution of the Entscheidungsproblem. For we can invent a machine which will prove consecutively all provable formulae. Sooner or later will reach either or ¬. If it reaches , then we know that is provable. If it reaches ¬, then, since K is consistent (Hilbert and Ackermann, p. 65), we know that is not provable.

So at first hand and without further clarification on his part, he seems to be equating two different kinds of formal axiomatic systems: the ones which try to mechanize the notion of validity in logic and the ones which try to mechanize the notion of truth in arithmetic.

Probably, what he's trying to get at is that there is a way to encode in arithmetic the notion of being a provable sentence in K so that, if arithmetic was complete, then that sentence could be proved or disproved in arithmetic.

Any suggestions to make sense of what he's talking about here?

Thank's in advance :)

Javier Diego-Fernández
  • 1
  • 1
  • I do not think he is equating anything, he is making a trivial observation that all theorems in a recursively axiomatized system can be algortihmically generated. Hence if the system is also complete this yields a decision procedure for provability of any sentence. Because when we simply generate all theorems one by one either or ¬ is eventually generated and the procedure is guaranteed to terminate. – Conifold Jun 13 '20 at 01:56
  • Axiomatic systems of FOL are of a different nature than axiomatic systems for mathematics (codified as postulates of FOL).

    Let's take an axiomatic system of arithmetic. In arithmetic, any expression with no free variables is either true or false. So if there is complete system any expression will eventually appear in it (either affirmed or negated).

    In an axiomatization of FOL that is not the case, it outputs only valid expressions and an expression whose negation is valid is a contradiction not a tautology.

    Completeness only implies decidability in the case of arithmetic not in logic

     – Javier Diego-Fernández Jun 13 '20 at 02:12
  • This post goes into more detail at the difference between both of those kinds of systems.

    https://philosophy.stackexchange.com/questions/15525/how-is-first-order-logic-complete-but-not-decidable/15526

    A complete system of logic (that outputs every one of the valid expressions of that logic) does not implies decidability (since it tells you when an expression is valid or contradiction, but not when it is only satisfiable). When I say I think he's equating two different kinds of systems I'm referring precisely to this difference.

     – Javier Diego-Fernández Jun 13 '20 at 02:17
  • I do not think he cares about satisfiability. "Completeness" here just means that everything is provable or disprovable, so by definition it implies "decidability" for arithmetic and logic alike. – Conifold Jun 13 '20 at 02:27
  • Completeness in a logical system means that the system is able to output one by one every valid expression of the logic. Again, completeness in a logical system does not imply decidability. A "just satisfiable" expression will never appear on the proofs and one cannot know it since it could be a valid expression that simply hasn't appeared yet.

    Again the argument Turing is making applies to axiomatizations of arithmetic, but not for axiomatizations of logic.

     – Javier Diego-Fernández Jun 13 '20 at 02:37
  • Turing's paper is written in 1936. What is now meant by completeness in a logical system as distinct from a mathematical system is moot, only what he means matters. And "completeness", as Turing uses the word, does imply decidability. – Conifold Jun 13 '20 at 02:54
  • Let us continue this discussion in chat. – Javier Diego-Fernández Jun 13 '20 at 03:03
  • The two are strongly linked: if PA is the conjunction of axioms of first-order arithmetic and T is a formula of arithmetic, we have that PA proves T iff if PA, then T is a valid FO formula. – Mauro ALLEGRANZA Jun 13 '20 at 08:04
  • 1
    @MauroALLEGRANZA: That's false. PA is not finitely axiomatizable. However, see my answer; Robinson's arithmetic (and also TC) is finitely axiomatizable. – user21820 Jun 16 '20 at 08:16

2 Answers2

2

Probably, what he's trying to get at is that there is a way to encode in arithmetic the notion of being a provable sentence in K so that, if arithmetic was complete, then that sentence could be proved or disproved in arithmetic.

You are absolutely correct. Godel showed (via his β-lemma) that one can encode finite sequences of natural numbers as natural numbers, and manipulate them, all within PA (or equivalent). A proof in any computable FOL theory T is simply a sequence of formulae satisfying the inference rules, which can obviously be encoded as a finite sequence of natural numbers. Furthermore, whether or not a natural number encodes a proof over T is a Σ1-sentence (i.e. of the form "∃k ( ... )" where all quantifiers in "..." are bounded). Now PA is Σ1-complete, meaning that if a Σ1-sentence is true then PA can prove it. So if T proves something then PA can prove that fact!

Symbolically, for any computable formal system T and any sentence Q over T, if ( T ⊢ Q ) then ( PA ⊢ ProvT ), where Prov[T] is a predicate in the language of PA.

Now it should be clear that the problem lies in the case ( T ⊬ Q ); where we have no guarantee that ( PA ⊢ ¬ProvT ). (And in fact Godel showed that it is in general not true.)

But Turing's comment can be strengthened to saying that if there is a computable consistent extension E of PA that proves every true Σ1-sentence and disproves every false Σ1-sentence, then we can determine whether ( T ⊢ Q ) by simply enuerating all theorems of E until we find either a proof or disproof of ProvT.

His original weaker comment is simply that there is no computable consistent complete axiomatization of the natural numbers N (i.e. a model of PA). But even just asking for the ability to disprove every false Σ1-sentence is bad enough, as explained above. All this still relies on Godel's β-lemma, but the explanation is slightly simpler. One only needs that ( T ⊢ Q ) iff ( N ⊨ ProvT ).

Related to your question, I would also like to mention that one can directly prove the undecidability of FOL via the Godel-Rosser theorem applied to Robinson's arithmetic RA. RA is finitely axiomatizable, hence provability of a sentence Q over RA is equivalent to provability of a single sentence over pure FOL (i.e. the conjunction of RA's axioms implies Q). Since provability of RA is undecidable by Godel-Rosser, provability over pure FOL is also undecidable.

If you are interested in the Godel-Rosser incompleteness theorem fully generalized, see this post for a simple computability-based proof.

user21820
  • 456
  • 1
  • 7
  • 17
  • Thanks for your careful response, I will look into the blog post you kindly shared. Just one additional question, the last paragraph of your explanation was not entirely clear to me. I'm aware that, once stated as FOL sentences, the provability of an arithmetic sentence would be equivalent to the provability of an FOL sentence being valid. Nevertheless, that does not rule out the possibility of some notion of logical validity not being captured inside the specific model of RA. Why the necessity of it having to finitely axiomatizable. – Javier Diego-Fernández Jul 16 '20 at 03:25
  • 1
    @JavierDiego-Fernández: What you stated in your second sentence is not true. Provability is always over some specified formal system. You can't just say "provable". Provable over what? And it seems you have basic misconceptions about logical validity and models as well. Anyway here is what is true: RA is finitely axiomatized, so we have ( RA ⊢ Q ) iff ( ⊢ RAX⇒Q ), where RAX is the conjunction of RA's axioms. You cannot do this with PA because it has infinitely many axioms (and there is no such thing as an infinite conjunction). – user21820 Jul 16 '20 at 04:11
0

Probably, what he's trying to get at is that there is a way to encode in arithmetic the notion of being a provable sentence in K so that, if arithmetic was complete, then that sentence could be proved or disproved in arithmetic.

I don't think that's what he's getting at, actually. What he appears to be suggesting is that you could write a computer program that recursively enumerates every possible proof (for example using a breadth-first search algorithm over the tree of all possible proofs that you might compose out of the axioms, with some additional finessing to deal with axiom schemata). This is a general technique, that "doesn't care" what your axioms look like. If you know that the system, whatever it encodes, is complete (that it proves every statement or its negation) and consistent (that it never proves a statement and its negation), then this technique will always find a proof or disproof of any proposition you care to ask about.

However, as Turing acknowledges, Godel had already proven that any system which can encode arithmetic cannot be both complete and consistent, so this doesn't actually work. Turing's argument then proves the stronger claim that there is no algorithm which does work in this case.

Kevin
  • 2,028
  • 10
  • 18
  • Hello! I noticed your comment here and wish to reply to it, but don't want to attract undesirable attention from the cranks over there (I think you know who I am referring to). Your skepticism is incorrect, and presumably it's because you are actually unfamiliar with mathematical logic and ZFC. It is trivial to formalize and do substantial reasoning about TMs in a reasonably natural manner (i.e. without Godel encoding) in ACA, which is a clearly predicative fragment of second-order arithmetic Z2, which is way weaker than ZFC. – user21820 Jun 16 '20 at 07:35
  • In terms of strength, PA = ACA0 < ACA << ATR << Z2 << ZC << ZFC. With Godel encoding, one can actually 'do' reasoning about TMs in PA (and in any system that interprets PA). This is how we can get PA ⊢ Con(PA)⇒¬⬜Con(PA) where "⬜" is the provability predicate. You are correct that these theorems are merely diagonalization arguments (modulo coding and simulation issues), and that's precisely why Godel's incompleteness theorems are provable in so weak meta-systems. ACA proves that every computable subset of N that encodes a theory that interprets PA− is either inconsistent or incomplete. – user21820 Jun 16 '20 at 07:41
  • PA alone can prove the incompleteness theorem for any specific computable formal system that computably interprets PA− (i.e. given a computer program that is a proof verifier or a theorem generator for a formal system, and a program that is a translation of arithmetic sentences into that system that witnesses that it interprets PA−), we can construct a proof over PA that the associated theory is inconsistent or incomplete), and even do so computably (i.e. we can write down a single program that given the programs for the formal system and translation will output the desired proof). – user21820 Jun 16 '20 at 07:47
  • You may be interested in some other details about the incompleteness theorems in this post and about ACA here. If you wish to inquire more, you're welcome to this chat-room as well. – user21820 Jun 16 '20 at 07:49