Return to Answer

Here is the answer (a quote from the paper): "Whereas our methods allow proving the consistency of a theory in itself, we don’t know how to prove in T the consistency of a theory S, which is strictly stronger than T. In particular, Kurahashi-Sinclaire’s observation that prohibits PA from proving the consistency scheme for PA+ConPA shows also that PA cannot prove the consistency of ZF.

This paper refutes the Unprovability of Consistency thesis, and these findings have their foundational value. Though this does not reach the goals of Hilbert’s consistency program, it removes a principal roadblock on its way."

Here is the answer (a quote from the paper):

Whereas our methods allow proving the consistency of a theory in itself, we don’t know how to prove in T the consistency of a theory S, which is strictly stronger than T. In particular, Kurahashi-Sinclaire’s observation that prohibits PA from proving the consistency scheme for PA+ConPA shows also that PA cannot prove the consistency of ZF.

This paper refutes the Unprovability of Consistency thesis, and these findings have their foundational value. Though this does not reach the goals of Hilbert’s consistency program, it removes a principal roadblock on its way.

Thank you for your interest and for advertising my work.

The answer to this specific question (as well as to most of the questions asked on my work in this venue) is given in the paper published in JLC: Sergei Artemov. Serial properties, selector proofs and the provability of consistency. Journal of Logic and Computation, https://doi.org/10.1093/logcom/exae034, Published: 26 July 2024. (Ask me if you have trouble downloading the paper from JLC.)

Here is the answer (a quote from the paper): "Whereas our methods allow proving the consistency of a theory in itself, we don’t know how to prove in T the consistency of a theory S, which is strictly stronger than T. In particular, Kurahashi-Sinclaire’s observation that prohibits PA from proving the consistency scheme for PA+ConPA shows also that PA cannot prove the consistency of ZF.

This paper refutes the Unprovability of Consistency thesis, and these findings have their foundational value. Though this does not reach the goals of Hilbert’s consistency program, it removes a principal roadblock on its way."

BTW, we don't need Hilbert's authority to show that Con(PA) is not equivalent to "PA is consistent" over PA. Here is a clean math argument with some obvious technical assumptions like "PA derivations are finite syntactic objects", "Goedel numbers of PA-derivations are numerals," "Godel numbering preserves the elementary computational structure of PA-derivations, e.g., D is not a proof of 0=1 iff the code of D is not a code of a sequence containing the line 0=1," etc.

Here is the argument

1. Consistency of PA is a property "no formal derivation in PA proves 0=1." This is a canonical textbook definition.

2. Godel numbering transliterates this property in its equivalent form (*): "for any numeral n, n is not a code of a PA-derivation containing the line 0=1."

3. Since quantification over numerals is not expressible in PA, we have to use some other means to equivalently represent "for any numeral n ... ". An obvious way to do this is by a p.r. string of sentences (which we call the consistency scheme Con^S(PA): "0 is not a code of a PA-derivation containing the line 0=1," "1 is not a code of a PA-derivation containing the line 0=1," "2 is not a code of a PA-derivation containing the line 0=1," etc. It is immediate that (*) is mathematically equivalent to Con^S(PA) without any meta-assumptions about PA.

4. Con(PA) is strictly stronger than Con^S(PA) in PA (an easy exercise), hence Con(PA) is strictly stronger than (*).

Thank you for your interest and for advertising my work.

The answer to this specific question (as well as to most of the questions asked on my work in this venue) is given in the paper published in JLC: Sergei Artemov. Serial properties, selector proofs and the provability of consistency. Journal of Logic and Computation, https://doi.org/10.1093/logcom/exae034, Published: 26 July 2024. (Ask me if you have trouble downloading the paper from JLC.)

Here is the answer (a quote from the paper): "Whereas our methods allow proving the consistency of a theory in itself, we don’t know how to prove in T the consistency of a theory S, which is strictly stronger than T. In particular, Kurahashi-Sinclaire’s observation that prohibits PA from proving the consistency scheme for PA+ConPA shows also that PA cannot prove the consistency of ZF.

This paper refutes the Unprovability of Consistency thesis, and these findings have their foundational value. Though this does not reach the goals of Hilbert’s consistency program, it removes a principal roadblock on its way."

So, my humble contribution to Hilbert’s program is mostly moral

1. It removes the widely accepted misconception that G2 killed Hilbert’s program.

2. Moreover, it shows that this misconception was unwarranted from the very beginning, the 1930s. The unprovability of consistency argument was based on the assumption that any PA-consistency proof in PA should be PA provably equivalent to Con(PA), which had no justification then (cf. the JLC paper for the details) and now is proven false.

BTW, we don't need Hilbert's authority to show that Con(PA) is not equivalent to "PA is consistent" over PA. Here is a clean math argument with some obvious technical assumptions like "PA derivations are finite syntactic objects", "Goedel numbers of PA-derivations are numerals," "Godel numbering preserves the elementary computational structure of PA-derivations, e.g., D is not a proof of 0=1 iff the code of D is not a code of a sequence containing the line 0=1," etc.

Here is the argument

1. Consistency of PA is a property "no formal derivation in PA proves 0=1." This is a canonical textbook definition.

2. Godel numbering transliterates this property in its equivalent form (*): "for any numeral n, n is not a code of a PA-derivation containing the line 0=1."

3. Since quantification over numerals is not expressible in PA, we have to use some other means to equivalently represent "for any numeral n ... ". An obvious way to do this is by a p.r. string of sentences (which we call the consistency scheme Con^S(PA): "0 is not a code of a PA-derivation containing the line 0=1," "1 is not a code of a PA-derivation containing the line 0=1," "2 is not a code of a PA-derivation containing the line 0=1," etc. It is immediate that (*) is mathematically equivalent to Con^S(PA) without any meta-assumptions about PA.

4. Con(PA) is strictly stronger than Con^S(PA) in PA (an easy exercise), hence Con(PA) is strictly stronger than (*).

Thank you for your interest and for advertising my work.

The answer to this specific question (as well as to most of the questions asked on my work in this venue) is given in the paper published in JLC: Sergei Artemov. Serial properties, selector proofs and the provability of consistency. Journal of Logic and Computation, https://doi.org/10.1093/logcom/exae034, Published: 26 July 2024. (Ask me if you have trouble downloading the paper from JLC.)

Here is the answer (a quote from the paper): "Whereas our methods allow proving the consistency of a theory in itself, we don’t know how to prove in T the consistency of a theory S, which is strictly stronger than T. In particular, Kurahashi-Sinclaire’s observation that prohibits PA from proving the consistency scheme for PA+ConPA shows also that PA cannot prove the consistency of ZF.

This paper refutes the Unprovability of Consistency thesis, and these findings have their foundational value. Though this does not reach the goals of Hilbert’s consistency program, it removes a principal roadblock on its way."

BTW, we don't need Hilbert's authority to show that Con(PA) is not equivalent to "PA is consistent" over PA. Here is a clean math argument with some obvious technical assumptions like "PA derivations are finite syntactic objects", "Goedel numbers of PA-derivations are numerals," "Godel numbering preserves the elementary computational structure of PA-derivations, e.g., D is not a proof of 0=1 iff the code of D is not a code of a sequence containing the line 0=1," etc.

Here is the argument

1. Consistency of PA is a property "no formal derivation in PA proves 0=1." This is a canonical textbook definition.

2. Godel numbering transliterates this property in its equivalent form (*): "for any numeral n, n is not a code of a PA-derivation containing the line 0=1."

3. Since quantification over numerals is not expressible in PA, we have to use some other means to equivalently represent "for any numeral n ... " and an obvious way to do this is by a p.r. string of sentences (which we call the consistency scheme Con^S(PA): "0 is not a code of a PA-derivation containing the line 0=1," "1 is not a code of a PA-derivation containing the line 0=1," "2 is not a code of a PA-derivation containing the line 0=1," etc. It is immediate that (*) is mathematically equivalent to Con^S(PA) without any meta-assumptions about PA.

4. Con(PA) is strictly stronger than Con^S(PA) in PA (an easy exercise), hence Con(PA) is strictly stronger than (*).

Thank you for your interest and for advertising my work.

The answer to this specific question (as well as to most of the questions asked on my work in this venue) is given in the paper published in JLC: Sergei Artemov. Serial properties, selector proofs and the provability of consistency. Journal of Logic and Computation, https://doi.org/10.1093/logcom/exae034, Published: 26 July 2024. (Ask me if you have trouble downloading the paper from JLC.)

Here is the answer (a quote from the paper): "Whereas our methods allow proving the consistency of a theory in itself, we don’t know how to prove in T the consistency of a theory S, which is strictly stronger than T. In particular, Kurahashi-Sinclaire’s observation that prohibits PA from proving the consistency scheme for PA+ConPA shows also that PA cannot prove the consistency of ZF.

This paper refutes the Unprovability of Consistency thesis, and these findings have their foundational value. Though this does not reach the goals of Hilbert’s consistency program, it removes a principal roadblock on its way."

BTW, we don't need Hilbert's authority to show that Con(PA) is not equivalent to "PA is consistent" over PA. Here is a clean math argument with some obvious technical assumptions like "PA derivations are finite syntactic objects", "Goedel numbers of PA-derivations are numerals," "Godel numbering preserves the elementary computational structure of PA-derivations, e.g., D is not a proof of 0=1 iff the code of D is not a code of a sequence containing the line 0=1," etc.

Here is the argument

1. Consistency of PA is a property "no formal derivation in PA proves 0=1." This is a canonical textbook definition.

2. Godel numbering transliterates this property in its equivalent form (*): "for any numeral n, n is not a code of a PA-derivation containing the line 0=1."

3. Since quantification over numerals is not expressible in PA, we have to use some other means to equivalently represent "for any numeral n ... ". An obvious way to do this is by a p.r. string of sentences (which we call the consistency scheme Con^S(PA): "0 is not a code of a PA-derivation containing the line 0=1," "1 is not a code of a PA-derivation containing the line 0=1," "2 is not a code of a PA-derivation containing the line 0=1," etc. It is immediate that (*) is mathematically equivalent to Con^S(PA) without any meta-assumptions about PA.

4. Con(PA) is strictly stronger than Con^S(PA) in PA (an easy exercise), hence Con(PA) is strictly stronger than (*).