14
$\begingroup$

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.

Improve this question
$\endgroup$
6
  • $\begingroup$ I can think of some examples involving the axiom of choice; e.g., theorems which can be proved in ZF if the hypothesis is "trivially" strengthened from "infinite" to "Dedekind-infinite." But it sounds like maybe you're interested in much weaker base theories than ZF? $\endgroup$
    – Timothy Chow
    Commented Dec 13, 2022 at 18:30
  • 1
    $\begingroup$ @TimothyChow: I actually wanted to add "examples from set theory are explicitly welcomed", but thought better of it. So by all means go ahead. $\endgroup$
    – Sam Sanders
    Commented Dec 13, 2022 at 20:06
  • $\begingroup$ If we take any case where a theorem is provable in a strong system S, but is not provable in a weaker system W, then as we step through a proof of this theorem in system S, we will find some primitive steps trivially licensed in system S but not in system W. Adding the specific license to infer those particular steps as "trivial" extra conditions (as these are indeed trivial one-step inferences in system S) will then make the theorem provable in system W. $\endgroup$
    – Sridhar Ramesh
    Commented Dec 13, 2022 at 22:00
  • $\begingroup$ In the sheaf topos $\operatorname{Sh}(\mathbb C)$ the statement "all complex numbers have a square root" is false, but the statement "all non-zero complex numbers have square roots" is true. More generally, the statement "all non-zero complex numbers have square roots" is true in every topos with a NNO. $\endgroup$
    – wlad
    Commented Dec 27, 2022 at 10:04
  • $\begingroup$ Another example - computability related - is finding the square root of a quaternion $q$ instead of a complex number. The problem is uncomputable. But add the condition $q$ is not in $\mathbb R^-$ (the negative part of the real line) and it's computable. $\endgroup$
    – wlad
    Commented Dec 27, 2022 at 10:07

2 Answers 2

Reset to default
7
$\begingroup$

There are various examples involving the axiom of choice. For example:

Theorem 1 (ZFC). Let $A$ be an infinite set (i.e., there is no bijection between $A$ and any finite von Neumann ordinal). Then $A$ contains a countably infinite subset.

Theorem 1 is not provable in ZF. However, if we add the "trivial" condition that $A$ be not just infinite, but Dedekind-infinite, then it becomes provable in ZF.

This is not a terribly interesting example of what you asked for. Maybe you need to say more about what you're really interested in?

Improve this answer
$\endgroup$
3
  • $\begingroup$ I would be interested in examples you could find in an analysis textbook. For instance, Bourbaki uses regulated functions to define (part of) the Riemann integral in real analysis. One of Bourbaki's theorems implies the following special case: if $\int_0^1 f(x)dx=0$ for $f:[0,1]\rightarrow [0,1]$, then $f(x)=0$ for at least one $x \in [0,1]$. If one adds the extra "Baire 1" condition, the latter theorem is provable in a fairly weak system; without the condition, this is not so. $\endgroup$
    – Sam Sanders
    Commented Dec 14, 2022 at 8:10
  • $\begingroup$ Here is another example, also involving AC: consider the theorem a regulated function on the unit interval is bounded. There are at least two proofs: the first proof needs a LOT of comprehension, while the second proof uses (only) weak K\"onig's lemma plus a non-trivial fragment of countable AC (called QF-AC$^{0,1}$ by Kohlenbach). Adding the extra condition "Baire 1", one can prove this boundedness theorem assuming only $\Sigma_1^1$-AC$_0$, i.e. not much comprehension and no choice beyond ZF. $\endgroup$
    – Sam Sanders
    Commented Dec 14, 2022 at 8:34
  • $\begingroup$ I see. It might be possible to extract some other AC examples from some other MO questions, e.g., Unique existence and the axiom of choice or Unnecessary uses of the axiom of choice. $\endgroup$
    – Timothy Chow
    Commented Dec 14, 2022 at 13:30
5
$\begingroup$

Consider König's theorem, which asserts that every infinite finitely branching tree has an infinite branch.

This is a theorem of ZFC, but in ZF alone, it is not provable. But meanwhile, if one adds the "trivial" assumption that the nodes of the tree admit a linear order, then it is provable in ZF, since from the linear order we can get a choice function of the successors of any node in the tree.

Improve this answer
$\endgroup$
1
  • $\begingroup$ I am not going to say that the Axiom of Choice is out (because it even plays a crucial/essential role in real analysis and regulated functions). I will say that I prefer "basic" examples, like the following special case of FTC: for regulated $f : [0, 1] → \mathbb{R}$ such that $ F (x) := λx. \int_0^x f (t)dt$ exists, there is $x_0 ∈ (0,1)$ where $F$ is differentiable with derivative $f(x_0)$. When adding the extra "Baire 1" condition, the latter theorem is provable in fairly weak system; not so without this condition. $\endgroup$
    – Sam Sanders
    Commented Dec 14, 2022 at 8:14

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .