Unprovable arithmetic statements in RCA0, WKL0

218 Views Asked by At

I was wondering what are typical examples of statements in elemntary number theory which are unprovable in the weak systems of reverse mathematics such as RCA0 and WKL0?

The wikipedia page (https://en.wikipedia.org/wiki/Reverse_mathematics) gives examples of classical theorems unprovable in these systems, but they are not statements of elementary number theory.

So I am wondering can these systems (RCA0, WKL0) prove basic things like fundamental theorem of arithmetic, Euclidean algorithm etc.

1

There are 1 best solutions below

0
On BEST ANSWER

The main texts on reverse mathematics are Subsystems of Second-Order Arithmetic by Simpson and Slicing the Truth by Hirschfeldt. Both of these are extremely good sources on what these systems do and don't prove, and while they focus on second-order consequences they also discuss first-order consequences. A text which focuses exclusively on first-order consequences is Metamathematics of First-Order Logic by Hajek and Pudlak.

Here are some facts:

  • WKL$_0$ is $\Pi^1_1$-conservative over RCA$_0$. This was proved by Harrington, and can be found e.g. in Simpson's book. This implies that the arithmetic consequences of RCA$_0$ and of WKL$_0$ are the same; and in particular, WKL$_0$ does not prove the consistency of RCA$_0$.

  • The first-order strength of RCA$_0$ (hence, of WKL$_0$ as well) is $I\Sigma_1$; this system is more than enough for most elementary number theory, including the fundamental theorem of arithmetic and the termination of the Euclidean algorithm. (Simpson's book talks a bit about this if I recall correctly.)

  • There are arithmetic principles beyond $I\Sigma_1$ and stronger systems, however; consistency statements give easy examples (of course RCA$_0$ doesn't prove Con(RCA$_0$), and this is an arithmetic statement), and for more natural examples versions of Ramsey's theorem are good places to look. (For instance, Goodstein's theorem is not provable in ACA$_0$, and in fact is equivalent to Con(ACA$_0$) over a weak base theory.) The standard hierarchy of first-order arithmetic systems is the Kirby-Paris hierarchy, given by the induction and bounding principles $$I\Sigma_1\leftarrow B\Sigma_2\leftarrow I\Sigma_2\leftarrow B\Sigma_3\leftarrow I\Sigma_3\leftarrow ...$$ (this is relative to the base theory PA$^-$+$I\Sigma_0$, and the implications above are strict); this hierarchy reaches all the way up through (first-order) Peano arithmetic. This paper by Slaman begins with a good survey of this hierarchy. Beyond that, first-order principles get more technical, and are often expressed in terms of appropriate transfinite induction principles.