2

Let S and T be subsets of $\mathbb R$ such that s < t for each s ∈ S and each t ∈ T. Prove carefully that sup S ≤ inf T.

Now I understand how to prove this as a natural language proof like, a = sup S, b = inf T For all t in T, t is an upper bound of S. Hence, a being the least of the upper bounds, a ≤ t, for all t in T. But then a is a lower bound of T. Hence, b being the greatest of the lower bounds, b ≥ a. Thus, sup S ≤ inf T

But I am struggling to write this as a step by step predicate logic proof while justifying each step.

Can someone please help?

MarnixKlooster ReinstateMonica
  • 5,576
harold
  • 311
  • 1
  • 11

2 Answers2

1

As a really really late answer, here is an alternative way of writing down this proof, which certainly is "a step by step predicate logic proof while justifying each step".$ \newcommand{\calc}{\begin{align} \quad &} \newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}} \newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} } \newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & } \newcommand{\endcalc}{\end{align}} \newcommand{\Ref}[1]{\text{(#1)}} \newcommand{\then}{\Rightarrow} \newcommand{\when}{\Leftarrow} \newcommand{\true}{\text{true}} \newcommand{\false}{\text{false}} $

As a commenter said, let's start by making the definitions explicit. The simplest definitions for $\;\sup\;$ and $\;\inf\;$ I know are that \begin{align} \tag{0} \sup S \le z &\;\equiv\; \langle \forall s : s \in S : s \le z \rangle \\ \tag{1} z \le \inf T &\;\equiv\; \langle \forall t : t \in T : z \le t \rangle \\ \end{align} for every $\;z\;$, for any non-empty upper-bounded $\;S\;$ and non-empty lower-bounded $\;T\;$.

Now we can start to calculate, starting from the statement we need to prove, working to expand the definitions, and seeing where this leads us:

$$\calc \sup S \le \inf T \op\equiv\hints{ordering -- the simplest way I see to allow}\hint{using the above definitions} \langle \forall z : z \le \sup S : z \le \inf T \rangle \op\equiv\hint{definition $\Ref{1}$ of $\;\inf\;$ -- the only definition which applies} \langle \forall z : z \le \sup S : \langle \forall t : t \in T : z \le t \rangle \rangle \op\equiv\hints{exchange quantifications -- to bring the $\;z\;$'s back}\hint{together} \langle \forall t : t \in T : \langle \forall z :: z \le \sup S : z \le t \rangle \rangle \op\equiv\hint{ordering -- simplify again} \langle \forall t : t \in T : \sup S \le t \rangle \op\equiv\hint{definition $\Ref{0}$ of $\;\sup\;$} \langle \forall t : t \in T : \langle \forall s : s \in S : s \le t \rangle \rangle \op\when\hint{weaken using $\;\lt \;\then\; \le\;$ -- to achieve the desired goal} \langle \forall t : t \in T : \langle \forall s : s \in S : s \lt t \rangle \rangle \endcalc$$

This completes the proof.

MarnixKlooster ReinstateMonica
  • 5,576
1

We know that sup and inf exist and are unique for bounded-from-the-right-side subsets of $\mathbb{R}$, let's call this property $\star$, so it's ok to name them (sup and inf) like you did (a and b), but let's just prove that $S$ and $T$ really are bounded above and below, respectively. We do need an additional assumption: that these subsets are not empty. Our domain is $\mathbb{R}$

  1. $\forall s(s \in S \rightarrow \forall t(t \in T \rightarrow s < t))$ (assume)

  2. $\exists x(x \in S) \land \exists x(x \in T)$ (assume)

  3. $\exists x(x \in S)$ (from 2)

  4. $s_0 \in S$ (special as.)

  5. $s_0 \in S \rightarrow \forall t(t \in T \rightarrow s_0 < t)$ (from 1)

  6. $\forall t(t \in T \rightarrow s_0 < t)$ (from 4, 5)

  7. $\exists x \forall t(t \in T \rightarrow x < t)$ (existential elimination of 3, by 4-6)

Similarly for $S$. The first two steps in the proof below are by 7th steps in the proof above and its $S$-version, by $\star$.

  1. $\forall s (s \in S \rightarrow s \leq a) \land \forall a' (a' < a \rightarrow \neg \forall s (s \in S \rightarrow s \leq a'))$

  2. $\forall t (t \in T \rightarrow b \leq t) \land \forall b' (b < b' \rightarrow \neg \forall t (t \in T \rightarrow b' \leq t))$

  3. $\forall s(s \in S \rightarrow \forall t(t \in T \rightarrow s < t))$ (assume)

  4. b < a (assume for reductio ad absurdum)

  5. $\forall a' (a' < a \rightarrow \neg \forall s (s \in S \rightarrow s \leq a'))$ (from 1)

  6. $b < a \rightarrow \neg \forall s (s \in S \rightarrow s \leq b)$ (from 5)

  7. $\neg \forall s (s \in S \rightarrow s \leq b)$ (from 4, 6)

  8. $\exists s(s \in S \land b \lt s)$ (from 7)

  9. $s_0 \in S \land b \lt s_0$ (special as.)

  10. $\forall b' (b < b' \rightarrow \neg \forall t (t \in T \rightarrow b' \leq t))$ (from 2)

  11. $b < s_0 \rightarrow \neg \forall t (t \in T \rightarrow s_0 \leq t)$ (from 10)

  12. $b \lt s_0$ (from 9)

  13. $\neg \forall t (t \in T \rightarrow s_0 \leq t)$ (from 11, 12)

  14. $\exists t (t \in T \land t \lt s_0)$ (from 13)

  15. $s_0 \in S$ (from 9)

  16. $s_0 \in S \land \exists t (t \in T \land t \lt s_0)$ (from 14, 15)

  17. $\exists s (s \in S \land \exists t (t \in T \land t \lt s))$ (existential elimination of 8 by 9-16)

  18. $\neg (b < a)$ (3, 17 contradiction)

Luka Mikec
  • 795
  • Thank you so much! just want to clarify what you mean by "s0" – harold Sep 12 '13 at 15:43
  • That is a way to prove things from formula of ExP(x) form. Basically you assume that P holds for some pseudoconstant (e.g. s0), for example P(s0), deduce something from P(s0) like P(s0) or Q(s0), and then get rid of s0 by, for example, deducing Ex(P(x) or Q(x)) (s0 doesn't represent a specific object, that is why it's called a pseudoconstant). This rule of inference is called "existent. quant. elimination", and it's valid because the only thing we know about pseudoconstant is that P holds; you might say pseudoconstant refers to "any" object for which P holds. – Luka Mikec Sep 12 '13 at 16:02