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 confounding 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 :)

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 :)

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 confounding 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 :)

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 confounding 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 :)