Fix a proof system for first-order arithmetic and let $\text{Con}(T,k)$ be an encoding of the statement that there is no proof of a contradiction in theory $T$ shorter than $k$ bits.

Now define $U_k = \text{PA} + \text{Con}(U_k, k)$ using Gödel's fixed point theorem. So each $U_k$ is the theory of PA with an additional axiom claiming that $U_k$ is consistent up to $k$-bit proofs.

Let's use ZFC as a meta-theory, so we know that PA is consistent. Are all the $U_k$ also consistent?

  • 2
    $\begingroup$ Maybe I'm missing something, but if PA is consistent, then for each individual $k\in\mathbb{N}$ PA proves "there is no contradiction in me of length $<k$" (since there are only finitely many proofs of length $<k$ in the first place, and PA can enumerate them and check that each one isn't a proof of $0=1$). So isn't it provable in ZFC that PA and $U_k$ are equivalent? $\endgroup$ Commented Apr 11, 2017 at 18:28
  • $\begingroup$ Noah, the theory $PA + Con(PA, k)$ is consistent and equivalent to PA, but I'm not so sure about $U_k = PA + Con(U_k, k)$. $\endgroup$ Commented Apr 11, 2017 at 19:54
  • 1
    $\begingroup$ Rob, $\text{Con}(U_k,k)$ is a sentence that encodes "there is no proof of a contradiction shorter than $k$ in the theory whose axioms are the axioms of PA plus this sentence", I think it is possible to construct this, although not in a unique way. I don't see an issue with PA being infinite, all we need is a way to tell if a sentence is an axiom. $\endgroup$ Commented Apr 14, 2017 at 16:41
  • 1
    $\begingroup$ @RobArthan The fixed point theorem is only being applied to a single formula here. Specifically, there's a formula $\varphi(x)$ asserting that $x$ is the Goedel number of a sentence which, when appended to PA, yields a $k$-consistent theory. By the fixed point theorem, we get a sentence $\psi$ with Goedel number $n$ such that PA proves $\psi\iff\varphi(n)$; the theory $U_k$ is just PA+$\psi$. $\endgroup$ Commented Apr 14, 2017 at 16:51
  • 2
    $\begingroup$ @NoahSchweber: &@Dan: thanks for the clarifications. I think it would have been clearer if Dan had written $U_k = Con(PA + U_k, k)$ rather than making it look as if $U_k$ were a sentence that implies each axiom of $PA$. $\endgroup$
    – Rob Arthan
    Commented Apr 14, 2017 at 19:08

1 Answer 1


It depends on the particular fixed-point that you use.

First, on the negative side, I claim that for some fixed points and large enough $k$, the answer is no, they can be inconsistent.

For example, let $\psi$ be any statement that can be refuted by PA in many fewer than $k$ bits, such as the statement $1\neq 1$. In this case, PA proves that $\psi$ is false, and it also proves that $\text{PA}+\psi$ proves a contradiction, and for large enough $k$ this proof will use fewer than $k$ bits. So PA proves that $\psi$ and $\text{Con}(\text{PA}+\psi,k)$ are equivalent, both being false. So it is one of the fixed points asserted to exist by the fixed-point lemma. But it is not consistent.

Meanwhile, on the positive side, let us assume that PA is consistent. Let $\psi$ be the sentence $1=1$, which is provable in PA and consistent with PA. For any fixed $k$, it follows that there will be no proof of a contradiction from $\text{PA}+\psi$ in fewer than $k$ bits (since we assumed PA is consistent), and furthermore PA will prove this for each particular $k$, since it can note the fact specifically about each of the finitely many proofs. So PA proves that $\psi$ is true and also that $\text{Con}(\text{PA}+\psi,k)$ is true, and so it is a fixed point. And for this fixed point, we have consistency.

Thinking about it a little more, I've come to realize that what is going on is the following:

Theorem. If PA proves or refutes $\psi$, then for any sufficiently large $k$, PA proves that $\psi$ is equivalent to $\text{Con}(\text{PA}+\psi,k)$, and so all such statements are fixed points.

Proof. If PA refutes $\psi$, then that proof has some length, and so for $k$ large enough, PA also proves that PA+$\psi$ is inconsistent, and thus PA proves $\psi\leftrightarrow \text{Con}(\text{PA}+\psi,k)$, since both sides are proven false.

If PA proves $\psi$, and without loss is consistent, then for any $k$ there will be no proof of a contradiction from PA+$\psi$ using fewer than $k$ bits, and PA will prove that by verifying each of those proofs. So in this case, PA proves $\psi\leftrightarrow \text{Con}(\text{PA}+\psi,k)$.

So in either case, $\psi$ is a fixed point. QED

Update. Although one might be disappointed by the fixed-points provided by the previous theorem, I've now realized that all fixed points are exactly like that.

Theorem. The following are equivalent for any sentence $\psi$:

  1. $\text{PA}\vdash\psi\leftrightarrow\text{Con}(\text{PA}+\psi,k)$ for some $k$.
  2. $\text{PA}\vdash\psi\leftrightarrow\text{Con}(\text{PA}+\psi,k)$ for all sufficiently large $k$.
  3. $\psi$ is provable or refutable in PA.

Proof. I've already proved that if $\psi$ is provable or refutable, then $2$ holds, and this implies $1$. Conversely, suppose that $1$ holds. Since there are only finitely many possible proofs using $k$ at most $k$ bits, it follows for any particular $k$ that PA either proves or refutes $\text{Con}(\text{PA}+\psi,k)$, simply by inspecting the finitely many proofs. So PA proves or refutes $\psi$, since $\psi$ is equivalent to that statement. So all three statements are equivalent. QED

In particular, there are no fixed points that are themselves independent of PA.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .