We begin by presenting a new kind of finite counting theorem which asserts that any function on vectors of natural numbers has few low values over finite sets of arbitrary size (Theorems 0.1 and 0.2 from the introduction).
This estimate on the low values (herein called regressive values) is linear in the sizes of the finite sets.
This basic counting theorem is extended to systems of finite functions, where it is shown that every system which is “decreasing” (in appropriate senses) includes functions which have even fewer low values over finite sets of arbitrary size. This improved estimate is a constant depending on the dimension and not on the sizes of the finite sets (see Proposition A from the introduction).
However, these extended results can only be proved by using additional axioms which go well beyond the currently accepted axioms for mathematics (as usually formalized by ZFC = Zermelo Frankel set theory with the axiom of choice). Furthermore, the extended results have obviously equivalent finite forms, which remove any mention of infinite sets (see Proposition B from the introduction). See Theorem 5.91 and Corollary 1.
The additional axioms used in the proof of these extended results are among the so called large cardinal axioms that have been extensively used in set theory since the 1960’s (see e.g., [Sc61], [MS89]). The proofs here illustrate in clear terms how one uses large cardinals in an essential and completely natural way in the integers. A conceptual overview of the method is described at the end of the introduction.
The quest for a simple meaningful finite mathematical theorem that can only be proved by going beyond the usual axioms for mathematics has been a goal in the foundations of mathematics since G6del’s work in the 1930’s [Go3l].
Prior relevant developments include the introduction of the forcing method in [Co66], which was used to establish the unprovability of the continuum hypothesis from the usual axioms of mathematics (the consistency having been previously established in [Go4O]). But for theoretical reasons, the forcing method cannot establish the independence of a finite statement, at least not directly (see [Fr92, p. 54] and “absoluteness” in [Je78, p. 101-108]).
Another relevant development was the first example of a simple meaningful finite mathematical theorem (in Ramsey theory) whose proof requires some weak use of infinite sets, in [PH77]. This was followed by a simple meaningful finite mathematical theorem in graph theory (related to J. B. Kruskal’s theorem) whose proof requires some weak use of uncountable sets, [Si85], and a further, simply stated theorem in graph theory (related to the graph minor theorem), [FRS87], whose proof requires stronger uses of uncountable sets.
Other relevant developments include the first example of a simple meaningful mathematical theorem involving Borel measurable functions whose proof requires use of uncountably many infinities, [FY71], and the first example of a simple meaningful mathematical theorem involving Borel measurable functions show that proof requires axioms going far beyond the usual axioms for mathematics, [Fr8l], [St85].
As is clear from the body of this abstract, the results – which are provable only by going well beyond the usual axioms for mathematics – are well connected with existing topics in finite and discrete combinatorics (Ramsey theory), and form a coherent body of examples. We anticipate that a variety of simple and basic examples will be found with increasingly strong connections to diverse areas of mathematics.