I am looking for examples of theorems where adding a 'trivial' extra condition makes the theorem provable in weaker systems. By 'trivial' I mean that the extra condition is trivial in strong enough systems. An example may be helpful as follows:

A function $f:[0,1]\rightarrow \mathbb{R}$ is called *regulated* in case the left and right limits $f(x+)$ and $f(x-)$ exist everywhere.

A function $f:[0,1]\rightarrow \mathbb{R}$ is called *Baire 1* in case it is the pointwise limit of a sequence of continuous functions.

It is well-known from real analysis that regulated functions are Baire 1.

Now, the following is provable in Kohlenbach's system RCA$_0^\omega$ plus some induction:

*A regulated and Baire 1 function on the unit interval has a point of continuity*.

By contrast, the following theorem is **not** provable in the same system extended with $\Pi_1^1$-comprehension (and the same for much stronger systems):

*A regulated function on the unit interval has a point of continuity*.

false, but the statement "all non-zero complex numbers have square roots" istrue. More generally, the statement "all non-zero complex numbers have square roots" is true in every topos with a NNO. $\endgroup$1more comment