Omniscience principles and functions of bounded variation (Q2776815)

Omniscience principles are general statements that can be proved classically but not constructively. They are used to show that other, more subject-specific statements that imply some omniscience principle do not have a constructive proof. The strongest omniscience principle is the law of excluded middle itself. It is easier to derive a weaker omniscience principle from a given subject-specific statement, and in this context weaker omniscience principles are more useful. In this paper a very weak omniscience principle is formulated, related omniscience principles are considered, and the theorem that a function of bounded variation is the difference of two increasing functions is shown to be equivalent to the omniscience principle WLPO. It is also shown that an arbitrary function (not necessarily strongly extensional) with located variation on an interval is the difference of two increasing functions.