Post History
#5: Post edited
by
clemens
·
2026-05-06T15:07:54Z (4 months ago)
- > I suspect the answer is yes, so how can I convince myself of that fact? Do I need to specify my metatheory more precisely? Do I need to assume ZFC is consistent?
- You're on the right track. The correct assumption to make here is known as $\Sigma_1^0$-soundness. A $\Sigma_1^0$-sound theory is only able to prove true $\Sigma_1^0$-statements—statements of the form $\exists n^{\in \mathbb{N}} (P(n))$ where $P(n)$ is an arithmetical statement with bounded quantifiers (or, equivalently, a statement checkable in bounded time by a Turing machine).
- As Gödel showed, provability is a $\Sigma_1^0$-statement[^1]. Conversely, all $\Sigma_1^0$-statements can be thought of as provability statements [^2]. Hence $\Sigma_1^0$-soundness is exactly equivalent to proof of provability implying actual provability!
- ---
- Two tangential notes on this question:
- 1. Any arithmetic that is powerful enough to talk about addition and multiplication is incomplete. This was proven with the MRDP theorem that showed that universal computation (and hence self-referential statements, true-but-unprovable statements, etc.) can be implemented using Diophantine equations. However, the MRDP theorem itself I believe can be proven in PRA—a fragment of arithmetic in which only primitive-recursive functions can be defined.
- 2. *Nonstandard models of arithmetic* provide a nice illustrative counterexample to $\Sigma_1^0$-soundness. Remember that Gödel showed that no theory can prove its own consistency; this means that every theory is consistent with a statement affirming its own inconsistency. So take, say, $\text{PA} + ¬\text{Con(PA)}$ (which must be consistent). This theory proves that $\exists n (n \text{ is the length of a proof of $\bot$ in PA})$. But since this $\Sigma_1^0$-statement is clearly false and yet provable in $\text{PA} + ¬\text{Con(PA)}$, we see that $\text{PA} + ¬\text{Con(PA)}$ is consistent but not $\Sigma_1^0$-sound. In other words there is a "nonstandard number" $n$—the length of the shortest proof of $\bot$ in PA—which $\text{PA} + ¬\text{Con(PA)}$ proves to exist but also to be greater than any "standard" (actually existing) number!
- ---
[^1] In fact this, rather than his famous diagonalization argument, was the main difficulty in Gödel's proof of his incompleteness theorem![^2] (e.g. in a "theory" $T$ in which $T \vdash S$ simply means that there exists a "proof" $n \in \mathbb{N}$ such that $\phi_S(n)$ is true)
- > I suspect the answer is yes, so how can I convince myself of that fact? Do I need to specify my metatheory more precisely? Do I need to assume ZFC is consistent?
- You're on the right track. The correct assumption to make here is known as $\Sigma_1^0$-soundness. A $\Sigma_1^0$-sound theory is only able to prove true $\Sigma_1^0$-statements—statements of the form $\exists n^{\in \mathbb{N}} (P(n))$ where $P(n)$ is an arithmetical statement with bounded quantifiers (or, equivalently, a statement checkable in bounded time by a Turing machine).
- As Gödel showed, provability is a $\Sigma_1^0$-statement[^1]. Conversely, all $\Sigma_1^0$-statements can be thought of as provability statements [^2]. Hence $\Sigma_1^0$-soundness is exactly equivalent to proof of provability implying actual provability!
- ---
- Two tangential notes on this question:
- 1. Any arithmetic that is powerful enough to talk about addition and multiplication is incomplete. This was proven with the MRDP theorem that showed that universal computation (and hence self-referential statements, true-but-unprovable statements, etc.) can be implemented using Diophantine equations. However, the MRDP theorem itself I believe can be proven in PRA—a fragment of arithmetic in which only primitive-recursive functions can be defined.
- 2. *Nonstandard models of arithmetic* provide a nice illustrative counterexample to $\Sigma_1^0$-soundness. Remember that Gödel showed that no theory can prove its own consistency; this means that every theory is consistent with a statement affirming its own inconsistency. So take, say, $\text{PA} + ¬\text{Con(PA)}$ (which must be consistent). This theory proves that $\exists n (n \text{ is the length of a proof of $\bot$ in PA})$. But since this $\Sigma_1^0$-statement is clearly false and yet provable in $\text{PA} + ¬\text{Con(PA)}$, we see that $\text{PA} + ¬\text{Con(PA)}$ is consistent but not $\Sigma_1^0$-sound. In other words there is a "nonstandard number" $n$—the length of the shortest proof of $\bot$ in PA—which $\text{PA} + ¬\text{Con(PA)}$ proves to exist but also to be greater than any "standard" (actually existing) number!
- ---
- [^1]: In fact this, rather than his famous diagonalization argument, was the main difficulty in Gödel's proof of his incompleteness theorem!
- [^2]: (e.g. in a "theory" $T$ in which $T \vdash S$ simply means that there exists a "proof" $n \in \mathbb{N}$ such that $\phi_S(n)$ is true)
#4: Post edited
by
clemens
·
2026-05-06T15:07:36Z (4 months ago)
markdown footnotes
- > I suspect the answer is yes, so how can I convince myself of that fact? Do I need to specify my metatheory more precisely? Do I need to assume ZFC is consistent?
- You're on the right track. The correct assumption to make here is known as $\Sigma_1^0$-soundness. A $\Sigma_1^0$-sound theory is only able to prove true $\Sigma_1^0$-statements—statements of the form $\exists n^{\in \mathbb{N}} (P(n))$ where $P(n)$ is an arithmetical statement with bounded quantifiers (or, equivalently, a statement checkable in bounded time by a Turing machine).
As Gödel showed, provability is a $\Sigma_1^0$-statement<sup>1</sup>. Conversely, all $\Sigma_1^0$-statements can be thought of as provability statements<sup>2</sup>. Hence $\Sigma_1^0$-soundness is exactly equivalent to proof of provability implying actual provability!- ---
- Two tangential notes on this question:
- 1. Any arithmetic that is powerful enough to talk about addition and multiplication is incomplete. This was proven with the MRDP theorem that showed that universal computation (and hence self-referential statements, true-but-unprovable statements, etc.) can be implemented using Diophantine equations. However, the MRDP theorem itself I believe can be proven in PRA—a fragment of arithmetic in which only primitive-recursive functions can be defined.
- 2. *Nonstandard models of arithmetic* provide a nice illustrative counterexample to $\Sigma_1^0$-soundness. Remember that Gödel showed that no theory can prove its own consistency; this means that every theory is consistent with a statement affirming its own inconsistency. So take, say, $\text{PA} + ¬\text{Con(PA)}$ (which must be consistent). This theory proves that $\exists n (n \text{ is the length of a proof of $\bot$ in PA})$. But since this $\Sigma_1^0$-statement is clearly false and yet provable in $\text{PA} + ¬\text{Con(PA)}$, we see that $\text{PA} + ¬\text{Con(PA)}$ is consistent but not $\Sigma_1^0$-sound. In other words there is a "nonstandard number" $n$—the length of the shortest proof of $\bot$ in PA—which $\text{PA} + ¬\text{Con(PA)}$ proves to exist but also to be greater than any "standard" (actually existing) number!
- ---
<sup>1</sup> In fact this, rather than his famous diagonalization argument, was the main difficulty in Gödel's proof of his incompleteness theorem!<sup>2</sup> (e.g. in a "theory" $T$ in which $T \vdash S$ simply means that there exists a "proof" $n \in \mathbb{N}$ such that $\phi_S(n)$ is true)
- > I suspect the answer is yes, so how can I convince myself of that fact? Do I need to specify my metatheory more precisely? Do I need to assume ZFC is consistent?
- You're on the right track. The correct assumption to make here is known as $\Sigma_1^0$-soundness. A $\Sigma_1^0$-sound theory is only able to prove true $\Sigma_1^0$-statements—statements of the form $\exists n^{\in \mathbb{N}} (P(n))$ where $P(n)$ is an arithmetical statement with bounded quantifiers (or, equivalently, a statement checkable in bounded time by a Turing machine).
- As Gödel showed, provability is a $\Sigma_1^0$-statement[^1]. Conversely, all $\Sigma_1^0$-statements can be thought of as provability statements [^2]. Hence $\Sigma_1^0$-soundness is exactly equivalent to proof of provability implying actual provability!
- ---
- Two tangential notes on this question:
- 1. Any arithmetic that is powerful enough to talk about addition and multiplication is incomplete. This was proven with the MRDP theorem that showed that universal computation (and hence self-referential statements, true-but-unprovable statements, etc.) can be implemented using Diophantine equations. However, the MRDP theorem itself I believe can be proven in PRA—a fragment of arithmetic in which only primitive-recursive functions can be defined.
- 2. *Nonstandard models of arithmetic* provide a nice illustrative counterexample to $\Sigma_1^0$-soundness. Remember that Gödel showed that no theory can prove its own consistency; this means that every theory is consistent with a statement affirming its own inconsistency. So take, say, $\text{PA} + ¬\text{Con(PA)}$ (which must be consistent). This theory proves that $\exists n (n \text{ is the length of a proof of $\bot$ in PA})$. But since this $\Sigma_1^0$-statement is clearly false and yet provable in $\text{PA} + ¬\text{Con(PA)}$, we see that $\text{PA} + ¬\text{Con(PA)}$ is consistent but not $\Sigma_1^0$-sound. In other words there is a "nonstandard number" $n$—the length of the shortest proof of $\bot$ in PA—which $\text{PA} + ¬\text{Con(PA)}$ proves to exist but also to be greater than any "standard" (actually existing) number!
- ---
- [^1] In fact this, rather than his famous diagonalization argument, was the main difficulty in Gödel's proof of his incompleteness theorem!
- [^2] (e.g. in a "theory" $T$ in which $T \vdash S$ simply means that there exists a "proof" $n \in \mathbb{N}$ such that $\phi_S(n)$ is true)
#3: Post edited
by
clemens
·
2026-04-22T17:56:57Z (5 months ago)
- > I suspect the answer is yes, so how can I convince myself of that fact? Do I need to specify my metatheory more precisely? Do I need to assume ZFC is consistent?
- You're on the right track. The correct assumption to make here is known as $\Sigma_1^0$-soundness. A $\Sigma_1^0$-sound theory is only able to prove true $\Sigma_1^0$-statements—statements of the form $\exists n^{\in \mathbb{N}} (P(n))$ where $P(n)$ is an arithmetical statement with bounded quantifiers (or, equivalently, a statement checkable in bounded time by a Turing machine).
- As Gödel showed, provability is a $\Sigma_1^0$-statement<sup>1</sup>. Conversely, all $\Sigma_1^0$-statements can be thought of as provability statements<sup>2</sup>. Hence $\Sigma_1^0$-soundness is exactly equivalent to proof of provability implying actual provability!
Two other tangential notes on:- 1. Any arithmetic that is powerful enough to talk about addition and multiplication is incomplete. This was proven with the MRDP theorem that showed that universal computation (and hence self-referential statements, true-but-unprovable statements, etc.) can be implemented using Diophantine equations. However, the MRDP theorem itself I believe can be proven in PRA—a fragment of arithmetic in which only primitive-recursive functions can be defined.
- 2. *Nonstandard models of arithmetic* provide a nice illustrative counterexample to $\Sigma_1^0$-soundness. Remember that Gödel showed that no theory can prove its own consistency; this means that every theory is consistent with a statement affirming its own inconsistency. So take, say, $\text{PA} + ¬\text{Con(PA)}$ (which must be consistent). This theory proves that $\exists n (n \text{ is the length of a proof of $\bot$ in PA})$. But since this $\Sigma_1^0$-statement is clearly false and yet provable in $\text{PA} + ¬\text{Con(PA)}$, we see that $\text{PA} + ¬\text{Con(PA)}$ is consistent but not $\Sigma_1^0$-sound. In other words there is a "nonstandard number" $n$—the length of the shortest proof of $\bot$ in PA—which $\text{PA} + ¬\text{Con(PA)}$ proves to exist but also to be greater than any "standard" (actually existing) number!
- <sup>1</sup> In fact this, rather than his famous diagonalization argument, was the main difficulty in Gödel's proof of his incompleteness theorem!
- <sup>2</sup> (e.g. in a "theory" $T$ in which $T \vdash S$ simply means that there exists a "proof" $n \in \mathbb{N}$ such that $\phi_S(n)$ is true)
- > I suspect the answer is yes, so how can I convince myself of that fact? Do I need to specify my metatheory more precisely? Do I need to assume ZFC is consistent?
- You're on the right track. The correct assumption to make here is known as $\Sigma_1^0$-soundness. A $\Sigma_1^0$-sound theory is only able to prove true $\Sigma_1^0$-statements—statements of the form $\exists n^{\in \mathbb{N}} (P(n))$ where $P(n)$ is an arithmetical statement with bounded quantifiers (or, equivalently, a statement checkable in bounded time by a Turing machine).
- As Gödel showed, provability is a $\Sigma_1^0$-statement<sup>1</sup>. Conversely, all $\Sigma_1^0$-statements can be thought of as provability statements<sup>2</sup>. Hence $\Sigma_1^0$-soundness is exactly equivalent to proof of provability implying actual provability!
- ---
- Two tangential notes on this question:
- 1. Any arithmetic that is powerful enough to talk about addition and multiplication is incomplete. This was proven with the MRDP theorem that showed that universal computation (and hence self-referential statements, true-but-unprovable statements, etc.) can be implemented using Diophantine equations. However, the MRDP theorem itself I believe can be proven in PRA—a fragment of arithmetic in which only primitive-recursive functions can be defined.
- 2. *Nonstandard models of arithmetic* provide a nice illustrative counterexample to $\Sigma_1^0$-soundness. Remember that Gödel showed that no theory can prove its own consistency; this means that every theory is consistent with a statement affirming its own inconsistency. So take, say, $\text{PA} + ¬\text{Con(PA)}$ (which must be consistent). This theory proves that $\exists n (n \text{ is the length of a proof of $\bot$ in PA})$. But since this $\Sigma_1^0$-statement is clearly false and yet provable in $\text{PA} + ¬\text{Con(PA)}$, we see that $\text{PA} + ¬\text{Con(PA)}$ is consistent but not $\Sigma_1^0$-sound. In other words there is a "nonstandard number" $n$—the length of the shortest proof of $\bot$ in PA—which $\text{PA} + ¬\text{Con(PA)}$ proves to exist but also to be greater than any "standard" (actually existing) number!
- ---
- <sup>1</sup> In fact this, rather than his famous diagonalization argument, was the main difficulty in Gödel's proof of his incompleteness theorem!
- <sup>2</sup> (e.g. in a "theory" $T$ in which $T \vdash S$ simply means that there exists a "proof" $n \in \mathbb{N}$ such that $\phi_S(n)$ is true)
#2: Post edited
by
clemens
·
2026-04-22T16:26:35Z (5 months ago)
- > I suspect the answer is yes, so how can I convince myself of that fact? Do I need to specify my metatheory more precisely? Do I need to assume ZFC is consistent?
- You're on the right track. The correct assumption to make here is known as $\Sigma_1^0$-soundness. A $\Sigma_1^0$-sound theory is only able to prove true $\Sigma_1^0$-statements—statements of the form $\exists n^{\in \mathbb{N}} (P(n))$ where $P(n)$ is an arithmetical statement with bounded quantifiers (or, equivalently, a statement checkable in bounded time by a Turing machine).
- As Gödel showed, provability is a $\Sigma_1^0$-statement<sup>1</sup>. Conversely, all $\Sigma_1^0$-statements can be thought of as provability statements<sup>2</sup>. Hence $\Sigma_1^0$-soundness is exactly equivalent to proof of provability implying actual provability!
(By the way, *nonstandard models of arithmetic* provide a nice counterexample to $\Sigma_1^0$-soundness. Remember that Gödel showed that no theory can prove its own consistency; this means that every theory is consistent with a statement affirming its own inconsistency. So take, say, $\text{PA} + ¬\text{Con(PA)}$ (which must be consistent). This theory proves that $\exists n (n \text{ is the length of a proof of $\bot$ in PA})$. But since this $\Sigma_1^0$-statement is clearly false and yet provable in $\text{PA} + ¬\text{Con(PA)}$, we see that $\text{PA} + ¬\text{Con(PA)}$ is consistent but not $\Sigma_1^0$-sound.)- <sup>1</sup> In fact this, rather than his famous diagonalization argument, was the main difficulty in Gödel's proof of his incompleteness theorem!
- <sup>2</sup> (e.g. in a "theory" $T$ in which $T \vdash S$ simply means that there exists a "proof" $n \in \mathbb{N}$ such that $\phi_S(n)$ is true)
- > I suspect the answer is yes, so how can I convince myself of that fact? Do I need to specify my metatheory more precisely? Do I need to assume ZFC is consistent?
- You're on the right track. The correct assumption to make here is known as $\Sigma_1^0$-soundness. A $\Sigma_1^0$-sound theory is only able to prove true $\Sigma_1^0$-statements—statements of the form $\exists n^{\in \mathbb{N}} (P(n))$ where $P(n)$ is an arithmetical statement with bounded quantifiers (or, equivalently, a statement checkable in bounded time by a Turing machine).
- As Gödel showed, provability is a $\Sigma_1^0$-statement<sup>1</sup>. Conversely, all $\Sigma_1^0$-statements can be thought of as provability statements<sup>2</sup>. Hence $\Sigma_1^0$-soundness is exactly equivalent to proof of provability implying actual provability!
- Two other tangential notes on:
- 1. Any arithmetic that is powerful enough to talk about addition and multiplication is incomplete. This was proven with the MRDP theorem that showed that universal computation (and hence self-referential statements, true-but-unprovable statements, etc.) can be implemented using Diophantine equations. However, the MRDP theorem itself I believe can be proven in PRA—a fragment of arithmetic in which only primitive-recursive functions can be defined.
- 2. *Nonstandard models of arithmetic* provide a nice illustrative counterexample to $\Sigma_1^0$-soundness. Remember that Gödel showed that no theory can prove its own consistency; this means that every theory is consistent with a statement affirming its own inconsistency. So take, say, $\text{PA} + ¬\text{Con(PA)}$ (which must be consistent). This theory proves that $\exists n (n \text{ is the length of a proof of $\bot$ in PA})$. But since this $\Sigma_1^0$-statement is clearly false and yet provable in $\text{PA} + ¬\text{Con(PA)}$, we see that $\text{PA} + ¬\text{Con(PA)}$ is consistent but not $\Sigma_1^0$-sound. In other words there is a "nonstandard number" $n$—the length of the shortest proof of $\bot$ in PA—which $\text{PA} + ¬\text{Con(PA)}$ proves to exist but also to be greater than any "standard" (actually existing) number!
- <sup>1</sup> In fact this, rather than his famous diagonalization argument, was the main difficulty in Gödel's proof of his incompleteness theorem!
- <sup>2</sup> (e.g. in a "theory" $T$ in which $T \vdash S$ simply means that there exists a "proof" $n \in \mathbb{N}$ such that $\phi_S(n)$ is true)
#1: Initial revision
by
clemens
·
2026-04-22T16:18:23Z (5 months ago)
> I suspect the answer is yes, so how can I convince myself of that fact? Do I need to specify my metatheory more precisely? Do I need to assume ZFC is consistent?
You're on the right track. The correct assumption to make here is known as $\Sigma_1^0$-soundness. A $\Sigma_1^0$-sound theory is only able to prove true $\Sigma_1^0$-statements—statements of the form $\exists n^{\in \mathbb{N}} (P(n))$ where $P(n)$ is an arithmetical statement with bounded quantifiers (or, equivalently, a statement checkable in bounded time by a Turing machine).
As Gödel showed, provability is a $\Sigma_1^0$-statement<sup>1</sup>. Conversely, all $\Sigma_1^0$-statements can be thought of as provability statements<sup>2</sup>. Hence $\Sigma_1^0$-soundness is exactly equivalent to proof of provability implying actual provability!
(By the way, *nonstandard models of arithmetic* provide a nice counterexample to $\Sigma_1^0$-soundness. Remember that Gödel showed that no theory can prove its own consistency; this means that every theory is consistent with a statement affirming its own inconsistency. So take, say, $\text{PA} + ¬\text{Con(PA)}$ (which must be consistent). This theory proves that $\exists n (n \text{ is the length of a proof of $\bot$ in PA})$. But since this $\Sigma_1^0$-statement is clearly false and yet provable in $\text{PA} + ¬\text{Con(PA)}$, we see that $\text{PA} + ¬\text{Con(PA)}$ is consistent but not $\Sigma_1^0$-sound.)
<sup>1</sup> In fact this, rather than his famous diagonalization argument, was the main difficulty in Gödel's proof of his incompleteness theorem!
<sup>2</sup> (e.g. in a "theory" $T$ in which $T \vdash S$ simply means that there exists a "proof" $n \in \mathbb{N}$ such that $\phi_S(n)$ is true)