A general question: I came across a vague statement that 'a uniform version of a theorem is one where the existence of objects concerned only depends on few parameters’, but that gives little intuition. Is it only about using a principle multiple times? What exactly does one call a uniform theorem?
Examples. To see what I mean have a brief look at:
- http://arxiv.org/abs/1808.09783v6
- An excerpt from (https://doi.org/10.1007/978-3-031-11367-3, p. 145-6):
The lack of relationships between $\leq_{RCA_{0}}$ and $\leq_c$ [two notions of reducibility] is a motivation for considering both of these reducibilities in practice. We can use precisely defined reducibility notions to describe the aspects of computability, verification, and uniformity that we see when studying theorems. In some cases, the same proof method establishes both $P \leq_c Q$ (or even $P \leq_W Q$ [Weihrauch reducibility], say) and $P \leq_{RCA_{0}} Q$. This happens surprisingly often: many theorems have proofs that are both effective and uniform. In other cases, examining the proof that $P \leq_{RCA_{0}}Q$ reveals a nonuniformity. Often, nonuniformity appears through use of the law of the excluded middle in a situation where we cannot effectively decide which of a number of possible cases holds. We have seen examples of this in our dealings with $\leq_c$ and $\leq_W$. Here is another, using Ramsey’s theorem for singletons. Consider the following proof in $RCA_0$ that $RT^1_2$ implies $RT^1_3$. Given a coloring : → 3, if () = 0 for infinitely many then we are done. Otherwise, there is a number such that () > 0 for all > . Then ∗ () = ( + ) − 1 induces a coloring ∗ : → 2, and we can compute an infinite homogeneous set for from any such set for ∗. The nonuniformity here is in the question whether the first color is used infinitely often. Of course, there are many alternate proofs of a theorem – especially if we consider all the possible formal proofs. We might ask whether there is an alternate proof that avoids this kind of nonuniformity. If we can show that $|P|\nleq_W |Q|$, this shows in a precise way that nonuniformity cannot be avoided, in the sense that there is no proof uniform enough to give a uniform algorithm for reducing $P$ to $Q$.
A uniform version of a theorem is a proof of the existence of a constructive-ish choice function that provides witnesses for all instances of the theorem.
Typically the theorem involved will be of the form $$(\forall x\in A)\,(\exists y\in B)\,P(x,y).$$
A proof in general might be non-constructive, and it's interesting to ask how hard it is to actually produce a $y$ corresponding to a given $x.$
Toward that end, a uniform version of the theorem would say that there exists a function $f\colon A\to B$ with some nice definability property such that $$(\forall x\in A)\;P(x,f(x)).$$
Depending on the situation, the definability property might say that $f$ is recursive, or that $f$ belongs to some level of the arithmetical or analytical hierarchy, or something of that sort.
(In set theory without the axiom of choice, just the existence of such an $f$ would be sufficient for a uniformity result, even without $f$ having any definability property.)