What combinatorial and number-theoretic propositions can $I\Delta_0$ prove? Obviously there are an infinitude of them, but what are some well known theorems that can be proved in $I\Delta_0$, if any?
5
-
2$\begingroup$ A good place to start learning about what can be done in $I\Delta_0$ is the book Metamathematics of First-Order Arithmetic by Petr Hájek and Pavel Pudlák, a free copy of which can be accessed via the link below (especially in Chapter V). Note the $I\Delta_0$ is referred to as $I\Sigma_0$ in the book. projecteuclid.org/euclid.pl/1235421926#toc $\endgroup$– Ali EnayatCommented Jan 27, 2021 at 16:43
-
$\begingroup$ I skimmed that chapter before I posted my question. All I could find was information about what kind of coding is possible for arithmetizing syntax in $I\Delta_0$, but no standard theorems about combinatorics or number theory. Did I miss something? $\endgroup$– BPPCommented Jan 29, 2021 at 1:09
-
$\begingroup$ The following thesis investigated the reverse mathematics of bounded arithmetic: andrew.cmu.edu/user/avigad/Students/ojakian.pdf $\endgroup$– Erfan KhanikiCommented Feb 9, 2021 at 3:49
-
$\begingroup$ users.math.cas.cz/~jerabek/papers/phd.pdf $\endgroup$– Erfan KhanikiCommented Feb 9, 2021 at 3:50
-
$\begingroup$ They considered several theorems in mathematics including some in the combinatorics and formalized them in essentially fragments of $I\Delta_0$ or its fragments with an additional axiom which says $x^{\log x}$ is a total function. $\endgroup$– Erfan KhanikiCommented Feb 9, 2021 at 3:53
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
4
Since no one else is biting, I'll answer, and thanks to comments I now this is accurate:
$I\Delta_0$ can prove several basic theorems:
- Every square equals 0 or 1 mod 4
- No prime has a rational square root
- The only solutions to $x^3+y^3=z^3$ or $x^4+y^4=z^4$ are trivial
- Every $x$ is divisible by a prime $p$ with $p \le x$
(The standard proofs can be reproduced in $I\Delta_0$, since they do not require any lists or sequences or products thereof. The last claim is proved in $I\Delta_0$ in a paper by D'Aquino.)
$I\Delta_0$ seems not to be able to prove that:
- there are arbitrarily large primes
- every prime of the form $4m+1$ can be written as $a^2+b^2$
(The first is a well-known open problem due to Wilkie)
$I\Delta_0$ cannot prove that:
- the functions $x^{\log x}$, $x!$, or $x^y$ are total
- there are solutions to the Pell equation $x^2-Ny^2=1$
(The $x^{\log x}$ is due to Parikh; the Pell equation result is due to D'Aquino.)
But $I\Delta_0(exp)$, i.e. the theory $I\Delta_0$ in the language with exponentiation, seems to prove
- every theorem published in the Annals of Mathematics whose statement involves only finitary mathematical objects
(This is a well-known conjecture due to Friedman.)
-
2$\begingroup$ $x^{\log x}$ is not provably total in $I\Delta_0$, by Parikh theorem. See: math.ucsd.edu/~sbuss/ResearchWeb/parikh/paper.pdf $\endgroup$ Commented Feb 9, 2021 at 3:43
-
$\begingroup$ As far as I am aware, $I\Delta_0$ is not known to prove Fermat’s two-square theorem. Its proofs require a counting argument to establish that $-1$ is a quadratic residue. (The theory can formalize the infinite descent argument that if $-1$ is a quadratic residue, then $m$ can be written as a sum of two squares.) $\endgroup$ Commented Feb 9, 2021 at 7:47
-
1$\begingroup$ To clarify the above, Fermat’s two-square theorem is equivalent over $I\Delta_0$ to the statement $\bigl(\frac{-1}p\bigr)=1$ for prime $p\equiv1\pmod4$. This is not known to be provable even in $I\Delta_0+\Omega_1$. See doi.org/10.1016/0168-0072(91)90096-5 and doi.org/10.1002/malq.200910009. The weakest extension of $I\Delta_0$ known to prove it is the theory $I\Delta_0+\mathrm{Count}_2(\Delta_0)$ with modulo-$2$ counting principles (actually, its subtheory $IE_1+\mathrm{Count_2}(\nabla_1)$ suffices), which actually proves the full quadratic reciprocity theorem. $\endgroup$ Commented Feb 9, 2021 at 8:26
-
$\begingroup$ @EmilJeřábek, let me know if this is good now $\endgroup$– user44143Commented Feb 9, 2021 at 12:51