Non-upper bounds without excluded middle

Question

Motivated by an earlier question, I'm curious if we can prove the following statement without the law of excluded middle:

Let $E$ be a set of real numbers. A number $x$ is said to be an upper bound for $E$ if $e\leq x$ for all $e\in E$. Prove that $y$ is not an upper bound for $E$ if and only if there exists $e\in E$ such that $e > y$.

To prove the statement, it seems necessary to invert a quantifier and an order relation, and both steps feel dubious. I don't have a reference work, but Wikipedia indicates that trichotomy isn't guaranteed in intuitionistic logic, and this bit doesn't mention any allowed implication of the form $\neg(\forall e \phi(e))\to(\bullet)$. So:

1. Is only one direction of the statement true/provable without excluded middle?
2. Is there a standard way to weaken the statement so that the weaker version holds in both directions?
3. What if we replace the real numbers with a simpler set, like the rational numbers or integers?

My question isn't necessarily limited to intuitionistic logic. Feel free to answer for your favorite logical system!

Answer 1

The principle "if $a$ is not an upper bound for $E$, then there is an element of $E$ that is greater than $a$" is expressed formally as $$ \lnot [ (\forall x \in E) ( x < a \lor x = a) ] \to (\exists x \in E)(a < x). $$

This principle is not provable in the standard formal system called "intuitionistic first-order predicate logic" which I will call IFOL. In fact, even the weaker formula $$ (1) \quad \lnot [ ( \forall x) ( x < a \lor x = a)] \to (\exists x)(a < x) $$ is not provable in IFOL from the axioms of a linear order (reflexivity, antisymmetry, and transitivity of $<$). I want to focus on that weaker principle (1), because it avoids any unnecessary distractions with sets. So we work in a theory that has only one type of object, and only two binary relations: equality and a linear order $<$.

My claim is that (1) is not provable in IFOL from the axioms of a linear ordering. The way to prove this, as might be expected, is to produce a countermodel. But this must necessarily be a nonclassical countermodel, because principle (1) is provable from the axioms of a linear order in classical logic. Before I describe a formal countermodel, let me describe the intuition behind it.

Intuition

The intuition why principle (1) is not provable in IFOL is related to the different relationship between universal and existential quantifiers in constructive logic. It also relates to an intuition in constructive logic that "more elements may appear at any time". In classical logic, we treat $\forall$ and $\exists$ as dual to each other. In constructive systems, it is often better to view $\forall$ as making a promise and $\exists$ as producing a witness:

• $(\forall x)[x < a \lor x = a]$ can be viewed as a promise that, whenever we find another element $x$, it will be equal to $a$ or less than $a$.

• $(\exists x)[a < x]$ asserts that we already have a specific witness $x_0$ with $a < x_0$.

Imagine I am constructing a model, adding elements one at a time, and I have not yet made up my mind whether I want $a$ to be an upper bound. We can view $\lnot (\forall x)[x = a \lor x < a]$ as saying that, although $a$ might be an upper bound for the elements I have already added, I am not willing to promise that $a$ will be an upper bound for all elements I might add later. Maybe $a$ will end up as an upper bound, maybe not. But $(\exists x)[a < x]$ means I have already chosen an element to be less than $a$.

I can certainly reserve the right to later add an element larger than $a$, without adding that element at the present time: formalizing this situation gives a model in which principle (1) fails.

Formal countermodel

One type of nonclassical model is called a Kripke frame; these are briefly described at the Stanford Encyclopedia article on intuitionistic logic. It is important to remember that "intuitionistic logic" here means the particular formal deductive system IFOL.

Now, assuming some familiarity with Kripke frames: the desired Kripke frame has just two nodes, $p$ and $p'$. In node $p$ we have the linear ordering with just one element $a$. In node $p'$ we have the linear ordering with two elements $a,b$ and $a < b$. Node $p$ does not force that $a$ is an upper bound, in fact $p$ forces $\lnot [ (\forall x)(x < a \lor x = a)]$. But $p$ does not force any witness for $(\exists x)[a < x]$. So node $p$ does not force formula (1). Because a formula is provable in IFOL if and only if it is forced by every node of every Kripke frame, principle (1) is not provable in intuitionistic logic.

Answers to the remaining parts of the question

The converse of (1) is provable in IFOL.

One way to weaken (1) is to use a translation that maps provable formula of classical first-order logic to classically equivalent formulas provable in IFOL. The double-negation translations do this, for example. These add enough additional double-negations to the formula to make it intuitionistically provable, while preserving classical equivalence.

Answer 2

Constructively, negations are superfluous. Ordinarily one would give a positive definition of negative concepts like "is not an upper bound" and the natural definition in this case would turn the statement under discussion into a tautology. It would assert that $A \leftrightarrow B$, where $A$ was previously defined to be true if and only if $B$ holds.