Prove if $B$ has a smallest element, then this element is unique.

Working on the book: Daniel J. Velleman. "HOW TO PROVE IT: A Structured Approach, Second Edition" (p. 206)

Theorem 4.4.6. Suppose $$R$$ is a partial order on a set $$A$$, and $$B \subseteq A$$.

If $$B$$ has a smallest element, then this smallest element is unique. Thus, we can speak of the smallest element of $$B$$ rather than a smallest element.

I symbolized "$$B$$ has a smallest element", as: $$\exists y\forall x(x \in B \to (y,x) \in R)$$

"$$B$$ smallest element is unique", as: $$\exists y(\forall x(x \in B \to (y,x) \in R) \land \forall z(\forall x(x \in B \to (z,x) \in R) \to y = z))$$

My proof skeleton using Fitch-style natural deduction:

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ci#1{\qquad\mathbf{\land I} \: #1 \\} \def\ce#1{\qquad\mathbf{\land E} \: #1 \\} \def\oi#1{\qquad\mathbf{\lor I} \: #1 \\} \def\oe#1{\qquad\mathbf{\lor E} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\} \def\qi#1{\qquad\mathbf{=I}\\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\ni#1{\qquad\mathbf{\neg I} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\}$$

$$\fitch{1.\, \exists y\forall x(x \in B \to (y,x) \in R)}{ \fitch{2.\, \forall x(x \in B \to (b',x) \in R)}{ \fitch{3.\, \forall x(x \in B \to (b,x) \in R)}{ 4.\,b \in B \to (b',b) \in R \Ae{2} 5.\,b \in B \to (b,b') \in R \Ae{3} \vdots\\ }\\ b=b'\\ }\\ \forall x(x \in B \to (z,x) \in R) \to y = z) }$$

As $$R$$ is a partial order, I would need to use antisymmetry property. But I do not know how to use it in lines 4,5 to infer that $$(b',b) \in R \land (b,b') \in R$$.

How can I fill the dots ? Am I missing some premise or step?

• Your representation of "$B$ has a smallest element" is missing an important part. It should be $$\exists y(y \in B \land \forall x(x \in B \to (y,x) \in R))$$ Using your representation, there's no reason such a $y$ would be unique. – Brian Moehring May 28 at 18:06
• Thanks for your remark, @Brian Moehring. – F. Zer May 28 at 20:19

1 Answer

Preliminary: I use the notation $$xRy$$ for $$(x,y) \in R$$.

Remark: The correct formalization of "$$B$$ has a smallest element" is $$\exists y(y \in B \land \forall x(x \in B \to yRx))$$ It is important that smallest element of $$B$$ is in $$B$$, otherwise you lose uniqueness. Indeed, let $$A = \{a_1, a_2, b\}$$ and $$B = \{b\}$$ with $$a_1 < b$$ and $$a_2 < b$$ and $$a_1 \neq a_2$$: both $$a_1$$ and $$a_2$$ (which are distinct) satisfy $$\exists y \forall x (x \in B \to yRx)$$ (I assume the domain of quantifications is $$A$$).

Solution: First, consider the following proof $$\pi$$ in Fitch-style natural deduction of the fact that if $$R$$ is a antisymmetric relation (on the domain $$A$$, premise $$0$$) and if $$y$$ is a smallest element of $$B$$ (premise $$1$$), then any other smallest element of $$B$$ is equal to $$y$$.

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ci#1{\qquad\mathbf{\land I} \: #1 \\} \def\ce#1{\qquad\mathbf{\land E} \: #1 \\} \def\oi#1{\qquad\mathbf{\lor I} \: #1 \\} \def\oe#1{\qquad\mathbf{\lor E} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\} \def\qi#1{\qquad\mathbf{=I}\\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\ni#1{\qquad\mathbf{\neg I} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\}$$

$$\fitch{0. \, \forall y \forall z (yRz \land zRy \to y = z) \\ 1.\, y \in B \land \forall x (x \in B \to yRx)} { \fitch{2.\, z \in B \land \forall x (x \in B \to zRx)} {3. \, \forall x (x \in B \to zRx) \ce{2} 4. \, y \in B \to z R y \Ae{3} 5. \, y \in B \ce{1} 6. \, zRy \ie{4,5} 7. \, \forall x (x \in B \to yRx) \ce{1} 8. \, z \in B \to yRz \Ae{7} 9. \, z \in B \ce{2} 10. \, yRz \ie{8,9} 11. \, yRz \land zRy \ci{10, 6} 12. \, yRz \land zRy \to y = z \Ae{0} 13. \, y = z \ie{12,11} }\\ 14. \, (z \in B \land \forall x (x \in B \to zRx)) \to y = z \ii{2{-}13} 15. \, \forall z \big((z \in B \land \forall x (x \in B \to zRx)) \to y = z \big) \Ai{14} }$$

Given the proof $$\pi$$ above, it is immediate to write a proof in Fitch-style natural deduction of $$$$\tag{*} \exists y \big( y \!\in\! B \land \forall x (x \!\in\! B \to yRx) \land \forall z ((z \!\in\! B \land \forall x (x \!\in\! B \to zRx)) \to y = z) \big)$$$$ under the assumptions that $$R$$ is antisymmetric (premise $$0$$ below) and that $$B$$ has a smallest element (premise $$1$$ below):

$$\fitch{0. \, \forall y \forall z (yRz \land zRy \to y = z) \\ 1.\, \exists y (y \in B \land \forall x (x \in B \to yRx))} { \fitch{2.\, y \in B \land \forall x (x \in B \to yRx)}{ \vdots \ \pi \\ 16. \, \forall z \big((z \in B \land \forall x (x \in B \to zRx)) \to y = z \big) \\ 17. \, (y \!\in\! B \land \forall x (x \!\in\! B \to yRx)) \land \forall z \big((z \!\in\! B \land \forall x (x \!\in\! B \to zRx)) \to y = z \big) \ci{2, 16} 18. \, \exists y \big( (y \!\in\! B \land \forall x (x \!\in\! B \to yRx)) \land \forall z \big((z \!\in\! B \land \forall x (x \!\in\! B \to zRx)) \to y = z \big) \big) \Ei{17} }\\ 19. \, \exists y \big( (y \!\in\! B \land \forall x (x \!\in\! B \to yRx)) \land \forall z \big((z \!\in\! B \land \forall x (x \!\in\! B \to zRx)) \to y = z \big) \big) \Ee{1, 2{-}18} }$$

Note that formula $$(*)$$ above formalizes the sentence "$$B$$ has a unique smallest element".

Final remark: Actually the derivation above shows that only antisymmetry of $$R$$ is required to prove the uniqueness of the smallest element. Transitivity and reflexivity of $$R$$ play no role.

• Spectacular. Thank you very much, @Taroccoesbrocco. I wish I could accept this answer two times :-) – F. Zer May 28 at 20:16
• I really liked how you “modularised” this proof. Could you tell me what is needed to do it ? In order to insert a proof into a bigger proof, do I need to have exact premises ? I will appreciate if you could elaborate a little on this. – F. Zer May 28 at 20:19
• @F.Zer - You're welcome! The symbol $\vdots \ \pi$ means the you have to take the proof $\pi$ above and replace the vertical dots in the second derivation with $\pi$. Note that above $\vdots$ you have exactly premise $1$ in $\pi$ and above $\vdots$ you have exactly the conclusion of $\pi$ (otherwise you couldn't plug $\pi$ into the second derivation). To be more precise, you just have to plug the part of $\pi$ from premise $1$ to conclusion $15$ (discarding premise $0$ of $\pi$) into the second derivation, since premise $0$ of $\pi$ is exactly premise $0$ of the second derivation. – Taroccoesbrocco May 28 at 20:26
• Thank you so much ! It's a great method. I was studying your explanation and wondered about something. – F. Zer May 28 at 21:30
• @F.Zer - Yes and no. Sure, a modular approach is good when you have to use the same subproof several times, or if you want to "enucleate" a piece of proof from the rest to stress something. But in this case there is a technical problem: a premise of $\pi$ is open ($y$ is not bound to any quantifier), hence the proof $\pi$ talks about a generic $y$. So, if you want to combine $\pi$ with another existential axiom, you have to be careful (remember the constraint about the elimination of the existential quantifier). – Taroccoesbrocco May 28 at 21:43