Exponential prefixed polynomial equations

TL;DR

This paper introduces exponential prefixed polynomial equations (EPPEs) that extend polynomial equations by allowing variables as exponents, and demonstrates their equivalence to significant combinatorial and number-theoretic independence results.

Contribution

It develops concise EPPEs equivalent to the Paris-Harrington theorem and Goodstein's theorem, advancing the understanding of their logical independence.

Findings

EPPEs can represent complex independence results.

New methods for eliminating bounded universal quantifiers in Diophantine predicates.

EPPEs provide a concise formalization of combinatorial independence theorems.

Abstract

A prefixed polynomial equation is an equation of the form $P(t_1,\ldots,t_n) = 0$, where $P$ is a polynomial whose variables $t_1,\ldots,t_n$ range over the natural numbers, preceded by quantifiers over some, or all, of its variables. Here, we consider exponential prefixed polynomial equations (EPPEs), where variables can also occur as exponents. We obtain a relatively concise EPPE equivalent to the combinatorial principle of the Paris-Harrington theorem for pairs (which is independent of primitive recursive arithmetic), as well as an EPPE equivalent to Goodstein's theorem (which is independent of Peano arithmetic). Some new devices are used in addition to known methods for the elimination of bounded universal quantifiers for Diophantine predicates.