Proving the equivalence of two definitions of the supremum of a set

Question

Edit #1: I apologize to everyone who took their time to read and answer my question. In my book, the second definition actually states that there exists an $x$ that is GREATER than $k-\epsilon$, rather than equal to. The definitions were indeed not equivalent because of this typo.

Edit #2: The universe is the set of real numbers. I should have been more clear about this.

---

First of all, let's define the upper bound of a set:

k is an upper bound of set A $\iff \text{upperBound}(k, A) \iff \forall x\in A:k\geq x$

Next, I propose two definitions of least upper bound of a set:

Definition 1:

k is THE LEAST upper bound of set A $\iff \text{leastUpperBound}(k, A) \iff \text{upperBound}(k, A) \land \forall k_2(\text{upperBound}(k_2, A)\implies k\leq k_2)$

Definition 2:

k is THE LEAST upper bound of set A $\iff \text{leastUpperBound}(k, A) \iff \text{upperBound}(k, A) \land \forall \epsilon >0 \exists x\in A:x=k-\epsilon$

I have tried and failed to use the rules of first-order logic to prove the equivalence of the two definitions. Help is much appreciated!

Answer 1

Def 2 correctly reads as: $k$ is an upper bound of $A$ and $$ \forall\varepsilon >0,\quad \exists x\in A,\quad x>k-\varepsilon. $$

Def 1 implies Def 2. Let $\sup A =: s$ according to Def 1. Suppose there exists $\varepsilon_0 >0$ such that $x\leqslant s-\varepsilon_0$ for every $x\in A$. Then $s-\varepsilon_0$ is an upper bound of $A$, a contradiction.

Def 2 implies Def 1. Let $\sup A =: s$ according to Def 2. Let $t$ be an upper bound of $A$, that is, $x\leqslant t$ for every $x\in A$. Suppose $s>t$. Then by Def 2, there exists $x\in A$ such that $x>t$, a contradiction. Thus, $s\leqslant t$.

Answer 2

EDIT: This answers the original version of the OP (prior to its Edit #1).

Definition 1:

$\text{leastUpperBound}(k, A) \\\iff \text{upperBound}(k, A) \land \forall k_2(\text{upperBound}(k_2, A)\implies k\leq k_2)$

Correct.

Definition 2:

$\text{leastUpperBound}(k, A) \\\iff \text{upperBound}(k, A) \land \forall \epsilon{>}0 \;\exists x{\in}A\:\:x=k-\epsilon$

This definition requires $A$ to be $(-\infty,p]$ for some $p.$

Is your goal to formalise the right conjunct? If so: $$\text{leastUpperBound}(k, A) \\\iff \text{upperBound}(k, A) \quad\land\quad \forall y\;\exists x{\in}A\:\:(y<x \lor y\geq k).$$

Answer 3

After contemplating the problem for a while, I have come up with my own proof that is based purely on first-order logic. All of the following first-order sentences are equivalent to one another, so you can either read the proof from up to down or the other way around.

The "first half" of both definitions, i.e. $\forall x \in A(x\leq k)$ is already the same, so I'll try to show the equivalence of the remaining "second halves", i.e. that $\forall k_2(\forall x\in A(x\leq k_2)\implies k_2\geq k) \iff \forall\epsilon>0\exists x\in A(x>k-\epsilon)$. $T$ will symbolize a true statement and $F$ a false statement.

Starting with the second definition, we have:

$\forall\epsilon(\epsilon>0\implies\exists x\in A(x>k-\epsilon))$

$\forall\epsilon(T\implies(\epsilon>0\implies\exists x\in A(x>k-\epsilon)))$, from the definition of implication in propositional logic

$\forall\epsilon(\exists k_2(k_2=k-\epsilon)\implies(\epsilon>0\implies\exists x\in A(x>k-\epsilon)))$, $k_2$ exists because subtraction is closed under the set of real numbers

$\forall\epsilon\forall k_2(k_2=k-\epsilon\implies(\epsilon>0\implies\exists x\in A(x>k-\epsilon)))$

$\forall\epsilon\forall k_2(\epsilon=k-k_2\implies(\epsilon>0\implies\exists x\in A(x>k-\epsilon)))$

$\forall\epsilon\forall k_2(\epsilon=k-k_2\implies(k-k_2>0\implies\exists x\in A(x>k-(k-k_2))))$

$\forall k_2(\exists\epsilon(\epsilon=k-k_2)\implies(k>k_2\implies\exists x\in A(x>k_2)))$

$\forall k_2(T\implies(k>k_2\implies\exists x\in A(x>k_2)))$, because subtraction is closed under the set of real numbers

$\forall k_2(k>k_2\implies\exists x\in A(x>k_2))$

$\forall k_2(\forall x\in A(x\leq k_2)\implies k\leq k_2)$, by taking the contraposition of the implication

Thus, the equivalence of the definitions has been proved