Return to Answer

Abstract. The consistency of a theory means that each of its formal derivations $D_0, D_1, D_2,\ldots$ is free of contradictions. For Peano Arithmetic $\textsf{PA}$, after the standard coding of derivations by numerals, $\textsf{PA}$-consistency is directly represented by the consistency scheme $\mathrm{Con}^S(\textsf{PA})$, which is a series of arithmetical statements "$n$ is not a code of a derivation of $(0=1)$" for numerals $n = 0,1,2,\ldots$ . We note that the consistency formula $\mathrm{Con}(\textsf{PA})$, $\forall x$ "$x$ is not a code of a derivation of $(0=1)$" is strictly stronger in $\textsf{PA}$ than $\textsf{PA}$-consistency and corresponds to some other property which we call "uniform consistency." When studying the provability of consistency in $\textsf{PA}$, we should work not with the consistency formula $\mathrm{Con}(\textsf{PA})$ but with the consistency scheme $\mathrm{Con}^S(\textsf{PA})$, which adequately represents $\textsf{PA}$ consistency.

July 27 addition: 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.)

Abstract. The consistency of a theory means that each of its formal derivations $D_0, D_1, D_2,\ldots$ is free of contradictions. For Peano Arithmetic $\textsf{PA}$, after the standard coding of derivations by numerals, $\textsf{PA}$-consistency is directly represented by the consistency scheme $\mathrm{Con}^S(\textsf{PA})$, which is a series of arithmetical statements "$n$ is not a code of a derivation of $(0=1)$" for numerals $n = 0,1,2,\ldots$ . We note that the consistency formula $\mathrm{Con}(\textsf{PA})$, $\forall x$ "$x$ is not a code of a derivation of $(0=1)$" is strictly stronger in $\textsf{PA}$ than $\textsf{PA}$-consistency and corresponds to some other property which we call "uniform consistency." When studying the provability of consistency in $\textsf{PA}$, we should work not with the consistency formula $\mathrm{Con}(\textsf{PA})$ but with the consistency scheme $\mathrm{Con}^S(\textsf{PA})$, which adequately represents $\textsf{PA}$ consistency.

I appreciate your interest in this work. The paper Serial properties, selector proofs and the provability of consistency passed a rigorous refereeing and has been accepted to JLC. I have just approved the proofs, and the paper will appear on the JLC website shortly. I promised not to publish the full text before that (though I am open to answering questions about Arxiv preprints).

Abstract. The consistency of a theory means that each of its formal derivations $D_0, D_1, D_2,\ldots$ is free of contradictions. For Peano Arithmetic $\textsf{PA}$, after the standard coding of derivations by numerals, $\textsf{PA}$-consistency is directly represented by the consistency scheme $\mathrm{Con}^S(\textsf{PA})$, which is a series of arithmetical statements "$n$ is not a code of a derivation of $(0=1)$" for numerals $n = 0,1,2,\ldots$ . We note that the consistency formula $\mathrm{Con}(\textsf{PA})$, $\forall x$ "$x$ is not a code of a derivation of $(0=1)$" is strictly stronger in $\textsf{PA}$ than $\textsf{PA}$-consistency and corresponds to some other property which we call "uniform consistency." When studying the provability of consistency in $\textsf{PA}$, we should work not with the consistency formula $\mathrm{Con}(\textsf{PA})$ but with the consistency scheme $\mathrm{Con}^S(\textsf{PA})$, which adequately represents $\textsf{PA}$ consistency.

This paper introduces the Hilbert-inspired notion of proof of an infinite series of formulas in a theory and proves $\textsf{PA}$-consistency in the form $\mathrm{Con}^S(\textsf{PA})$ in $\textsf{PA}$. These findings show that $\textsf{PA}$ proves its consistency, whereas, by Goedel's second incompleteness theorem, $\textsf{PA}$ cannot prove its uniform consistency.

Comments for the OF readers.

1. Picking $\mathrm{Con}(\textsf{PA})$ to represent the consistency of $\textsf{PA}$ has been a strengthening fallacy. $\textsf{PA}$-consistency as a property of formal derivations is fairly represented by the scheme $\mathrm{Con}^S(\textsf{PA})$, which is a property of numerals. The formula $\mathrm{Con}(\textsf{PA})$ is strictly stronger in $\textsf{PA}$ than the $\textsf{PA}$-consistency. So, the (un)provability of consistency analysis based on $\mathrm{Con}(\textsf{PA})$ is void, and we ought to consider $\mathrm{Con}^S(\textsf{PA})$ instead. This is not a matter of taste or aesthetic preferences but rather a solid mathematical necessity.

2. To analyze the provability of consistency, we need to agree on what counts as proof of a serial property, here $\mathrm{Con}^S(\textsf{PA})$, in $\textsf{PA}$. The paper offers a complete account of the choices and argues in favor of the one endorsed by Hilbert in the 1920s, which we call selector proofs. There is not much freedom here, either: selector proofs have been tacitly used in mathematics, and the time is ripe to formalize them officially.

3. The rest is a standard proof theoretical treatment of $\mathrm{Con}^S(\textsf{PA})$ with a modest technical contribution that the selector based on partial truth definitions an easily formalizable p.r. function.

A special comment for people who believe in $\mathrm{Con}(\textsf{PA})$ in the context of provability in $\textsf{PA}$: $\mathrm{Con}(\textsf{PA})$ is the wrong way to represent $\textsf{PA}$ consistency. If you try to check why $\mathrm{Con}(\textsf{PA})$ is equivalent to $\textsf{PA}$ consistency, you would need to refer to the standard model of $\textsf{PA}$ or similar notions requiring strong meta-assumptions that defeat the purpose of analyzing the provability of consistency in $\textsf{PA}$.

The right way to represent consistency property (which is a property of finite derivation strings) arithmetically is by a serial property/scheme $\mathrm{Con}^S(\textsf{PA})$, which is a series of claims "n is consistent" for numerals $n = 0,1,2,\ldots$. It is immediate that "$\textsf{PA}$ is consistent" is equivalent to $\mathrm{Con}^S(\textsf{PA})$ without any metamathematical assumptions about $\textsf{PA}$.

I appreciate your interest in this work. The paper Serial properties, selector proofs and the provability of consistency passed a rigorous refereeing and has been accepted to JLC. I have just approved the proofs, and the paper will appear on the JLC website shortly. I promised not to publish the full text before that (though I am open to answering questions about Arxiv preprints).

Abstract. The consistency of a theory means that each of its formal derivations $D_0, D_1, D_2,\ldots$ is free of contradictions. For Peano Arithmetic $\textsf{PA}$, after the standard coding of derivations by numerals, $\textsf{PA}$-consistency is directly represented by the consistency scheme $\mathrm{Con}^S(\textsf{PA})$, which is a series of arithmetical statements "$n$ is not a code of a derivation of $(0=1)$" for numerals $n = 0,1,2,\ldots$ . We note that the consistency formula $\mathrm{Con}(\textsf{PA})$, $\forall x$ "$x$ is not a code of a derivation of $(0=1)$" is strictly stronger in $\textsf{PA}$ than $\textsf{PA}$-consistency and corresponds to some other property which we call "uniform consistency." When studying the provability of consistency in $\textsf{PA}$, we should work not with the consistency formula $\mathrm{Con}(\textsf{PA})$ but with the consistency scheme $\mathrm{Con}^S(\textsf{PA})$, which adequately represents $\textsf{PA}$ consistency.

This paper introduces the Hilbert-inspired notion of proof of an infinite series of formulas in a theory and proves $\textsf{PA}$-consistency in the form $\mathrm{Con}^S(\textsf{PA})$ in $\textsf{PA}$. These findings show that $\textsf{PA}$ proves its consistency, whereas, by Goedel's second incompleteness theorem, $\textsf{PA}$ cannot prove its uniform consistency.

Comments for the OF readers.

1. Picking $\mathrm{Con}(\textsf{PA})$ to represent the consistency of $\textsf{PA}$ has been a strengthening fallacy. $\textsf{PA}$-consistency as a property of formal derivations is fairly represented by the scheme $\mathrm{Con}^S(\textsf{PA})$, which is a property of numerals. The formula $\mathrm{Con}(\textsf{PA})$ is strictly stronger in $\textsf{PA}$ than the $\textsf{PA}$-consistency. So, the (un)provability of consistency analysis based on $\mathrm{Con}(\textsf{PA})$ is void, and we ought to consider $\mathrm{Con}^S(\textsf{PA})$ instead. This is not a matter of taste or aesthetic preferences but rather a solid mathematical necessity.

2. To analyze the provability of consistency, we need to agree on what counts as proof of a serial property, here $\mathrm{Con}^S(\textsf{PA})$, in $\textsf{PA}$. The paper offers a complete account of the choices and argues in favor of the one endorsed by Hilbert in the 1920s, which we call selector proofs. There is not much freedom here, either: selector proofs have been tacitly used in mathematics, and the time is ripe to formalize them officially.

3. The rest is a standard proof theoretical treatment of $\mathrm{Con}^S(\textsf{PA})$ with a modest technical contribution that the selector based on partial truth definitions an easily formalizable p.r. function.

A special comment for people who believe in $\mathrm{Con}(\textsf{PA})$ in the context of provability in $\textsf{PA}$: $\mathrm{Con}(\textsf{PA})$ is the wrong way to represent $\textsf{PA}$ consistency. If you try to check why $\mathrm{Con}(\textsf{PA})$ is equivalent to $\textsf{PA}$ consistency, you would need to refer to the standard model of $\textsf{PA}$ or similar notions requiring strong meta-assumptions that defeat the purpose of analyzing the provability of consistency in $\textsf{PA}$.

The right way to represent consistency property (which is a property of finite derivation strings) arithmetically is by a serial property/scheme $\mathrm{Con}^S(\textsf{PA})$, which is a series of claims "$n$ is consistent" for numerals $n = 0,1,2,\ldots$. It is immediate that "$\textsf{PA}$ is consistent" is equivalent to $\mathrm{Con}^S(\textsf{PA})$ without any metamathematical assumptions about $\textsf{PA}$. Furthermore, it is easy to check that $\mathrm{Con}(\textsf{PA})$ is strictly stronger than $\mathrm{Con}^S(\textsf{PA})$ in $\textsf{PA}$ which makes Goedel's result about the unprovability of $\mathrm{Con}(\textsf{PA})$ not directly applicable to $\textsf{PA}$ consistency (which is equivalent to $\mathrm{Con}^S(\textsf{PA})$ in $\textsf{PA}$).

I appreciate your interest in this work. The paper Serial properties, selector proofs and the provability of consistency passed a rigorous refereeing and has been accepted to JLC. I have just approved the proofs, and the paper will appear on the JLC website shortly. I promised not to publish the full text before that (though I am open to answering questions about Arxiv preprints).

Abstract. The consistency of a theory means that each of its formal derivations $D_0, D_1, D_2,\ldots$ is free of contradictions. For Peano Arithmetic $\textsf{PA}$, after the standard coding of derivations by numerals, $\textsf{PA}$-consistency is directly represented by the consistency scheme $\mathrm{Con}^S(\textsf{PA})$, which is a series of arithmetical statements "$n$ is not a code of a derivation of $(0=1)$" for numerals $n = 0,1,2,\ldots$ . We note that the consistency formula $\mathrm{Con}(\textsf{PA})$, $\forall x$ "$x$ is not a code of a derivation of $(0=1)$" is strictly stronger in $\textsf{PA}$ than $\textsf{PA}$-consistency and corresponds to some other property which we call "uniform consistency." When studying the provability of consistency in $\textsf{PA}$, we should work not with the consistency formula $\mathrm{Con}(\textsf{PA})$ but with the consistency scheme $\mathrm{Con}^S(\textsf{PA})$, which adequately represents $\textsf{PA}$ consistency.

This paper introduces the Hilbert-inspired notion of proof of an infinite series of formulas in a theory and proves $\textsf{PA}$-consistency in the form $\mathrm{Con}^S(\textsf{PA})$ in $\textsf{PA}$. These findings show that $\textsf{PA}$ proves its consistency, whereas, by Goedel's second incompleteness theorem, $\textsf{PA}$ cannot prove its uniform consistency.

Comments for the OF readers.

1. Picking $\mathrm{Con}(\textsf{PA})$ to represent the consistency of $\textsf{PA}$ has been a strengthening fallacy. $\textsf{PA}$-consistency as a property of formal derivations is fairly represented by the scheme $\mathrm{Con}^S(\textsf{PA})$, which is a property of numerals. The formula $\mathrm{Con}(\textsf{PA})$ is strictly stronger in $\textsf{PA}$ than the $\textsf{PA}$-consistency. So, the (un)provability of consistency analysis based on $\mathrm{Con}(\textsf{PA})$ is void, and we ought to consider $\mathrm{Con}^S(\textsf{PA})$ instead. This is not a matter of taste or aesthetic preferences but rather a solid mathematical necessity.

2. To analyze the provability of consistency, we need to agree on what counts as proof of a serial property, here $\mathrm{Con}^S(\textsf{PA})$, in $\textsf{PA}$. The paper offers a complete account of the choices and argues in favor of the one endorsed by Hilbert in the 1920s, which we call selector proofs. There is not much freedom here, either: selector proofs have been tacitly used in mathematics, and the time is ripe to formalize them officially.

3. The rest is a standard proof theoretical treatment of $\mathrm{Con}^S(\textsf{PA})$ with a modest technical contribution that the selector based on partial truth definitions an easily formalizable p.r. function.

A special comment for people who believe in Con(PA) in the context of provability in PA: Con(PA) is the wrong way to represent PA consistency. If you try to check why Con(PA) is equivalent to PA consistency, you would need to refer to the standard model of PA or similar notions requiring strong meta-assumptions that defeat the purpose of analyzing the provability of consistency in PA.

The right way to represent consistency property (which is a property of finite derivation strings) arithmetically is by a serial property/scheme Con^S(PA), which is a series of claims "n is consistent" for numerals n = 0,1,2,... . It is immediate that "PA is consistent" is equivalent to Con^S(PA) without any metamathematical assumptions about PA.

I appreciate your interest in this work. The paper Serial properties, selector proofs and the provability of consistency passed a rigorous refereeing and has been accepted to JLC. I have just approved the proofs, and the paper will appear on the JLC website shortly. I promised not to publish the full text before that (though I am open to answering questions about Arxiv preprints).

Abstract. The consistency of a theory means that each of its formal derivations $D_0, D_1, D_2,\ldots$ is free of contradictions. For Peano Arithmetic $\textsf{PA}$, after the standard coding of derivations by numerals, $\textsf{PA}$-consistency is directly represented by the consistency scheme $\mathrm{Con}^S(\textsf{PA})$, which is a series of arithmetical statements "$n$ is not a code of a derivation of $(0=1)$" for numerals $n = 0,1,2,\ldots$ . We note that the consistency formula $\mathrm{Con}(\textsf{PA})$, $\forall x$ "$x$ is not a code of a derivation of $(0=1)$" is strictly stronger in $\textsf{PA}$ than $\textsf{PA}$-consistency and corresponds to some other property which we call "uniform consistency." When studying the provability of consistency in $\textsf{PA}$, we should work not with the consistency formula $\mathrm{Con}(\textsf{PA})$ but with the consistency scheme $\mathrm{Con}^S(\textsf{PA})$, which adequately represents $\textsf{PA}$ consistency.

This paper introduces the Hilbert-inspired notion of proof of an infinite series of formulas in a theory and proves $\textsf{PA}$-consistency in the form $\mathrm{Con}^S(\textsf{PA})$ in $\textsf{PA}$. These findings show that $\textsf{PA}$ proves its consistency, whereas, by Goedel's second incompleteness theorem, $\textsf{PA}$ cannot prove its uniform consistency.

Comments for the OF readers.

1. Picking $\mathrm{Con}(\textsf{PA})$ to represent the consistency of $\textsf{PA}$ has been a strengthening fallacy. $\textsf{PA}$-consistency as a property of formal derivations is fairly represented by the scheme $\mathrm{Con}^S(\textsf{PA})$, which is a property of numerals. The formula $\mathrm{Con}(\textsf{PA})$ is strictly stronger in $\textsf{PA}$ than the $\textsf{PA}$-consistency. So, the (un)provability of consistency analysis based on $\mathrm{Con}(\textsf{PA})$ is void, and we ought to consider $\mathrm{Con}^S(\textsf{PA})$ instead. This is not a matter of taste or aesthetic preferences but rather a solid mathematical necessity.

2. To analyze the provability of consistency, we need to agree on what counts as proof of a serial property, here $\mathrm{Con}^S(\textsf{PA})$, in $\textsf{PA}$. The paper offers a complete account of the choices and argues in favor of the one endorsed by Hilbert in the 1920s, which we call selector proofs. There is not much freedom here, either: selector proofs have been tacitly used in mathematics, and the time is ripe to formalize them officially.

3. The rest is a standard proof theoretical treatment of $\mathrm{Con}^S(\textsf{PA})$ with a modest technical contribution that the selector based on partial truth definitions an easily formalizable p.r. function.

A special comment for people who believe in $\mathrm{Con}(\textsf{PA})$ in the context of provability in $\textsf{PA}$: $\mathrm{Con}(\textsf{PA})$ is the wrong way to represent $\textsf{PA}$ consistency. If you try to check why $\mathrm{Con}(\textsf{PA})$ is equivalent to $\textsf{PA}$ consistency, you would need to refer to the standard model of $\textsf{PA}$ or similar notions requiring strong meta-assumptions that defeat the purpose of analyzing the provability of consistency in $\textsf{PA}$.

The right way to represent consistency property (which is a property of finite derivation strings) arithmetically is by a serial property/scheme $\mathrm{Con}^S(\textsf{PA})$, which is a series of claims "n is consistent" for numerals $n = 0,1,2,\ldots$. It is immediate that "$\textsf{PA}$ is consistent" is equivalent to $\mathrm{Con}^S(\textsf{PA})$ without any metamathematical assumptions about $\textsf{PA}$.