Suppose $b$ is the smallest element of $B$. Then $b$ is also a minimal element of $B$, and it is the only minimal element.

Question

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

Suppose $R$ is a partial order on a set $A$, and $B \subseteq A$. Suppose $b$ is the smallest element of $B$. Then $b$ is also a minimal element of $B$, and it is the only minimal element.

I proved that $b$ is a minimal element of $B$ using the property of antisymmetry ($R$ is a partial order). Now, I will prove uniqueness using Fitch-style Natural Deduction system.

$ \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.\, b \in B \land \forall x(x \in B \to bRx) \qquad \textit{b is the smallest element of B}\\ 2.\,b \in B \land \neg \exists x(xRb \land x \neq b) \qquad \textit{b is a minimal element of B} }{ 3.\,\neg \exists x(xRb \land x \neq b) \ce{2} \fitch{4.\, c \in B \land \neg \exists x(xRc \land x \neq c)}{ 5.\,c \in B \ce{4} 6.\,\neg \exists x(xRc \land x \neq c) \ce{4} \fitch{7.\, b \neq c}{ 8.\,\forall x(x \in B \to bRx) \ce{1} 9.\,c \in B \to bRc \Ae{8} 10.\,bRc \ie{9,5} 11.\,bRc \land b \neq c \ci{10,7} 12.\,\exists x(xRc \land x \neq c) \Ei{11} 13.\,\bot \ne{6,12} }\\ 14.\,b = c \IP{7-13} }\\ 15.\, \forall z((z \in B \land \neg \exists x(xRz \land x \neq z)) \to b = z) \Ai{14} 16.\,b \in B \land \neg \exists x(xRb \land x \neq b) \land \forall z(z \in B \land \neg \exists x(xRz \land x \neq z)) \to b = z) \ci{2,15} } $

Is my uniqueness proof correct ?

EDIT: This rules of inference can be found in Appendix C of this book: forallx: An Introduction to Formal Logic

Answer 1

$ \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 \\} $

Your formal proof is essentially correct except few (negligible) errors.

1. In line $9$ you applied the rule $\forall \mathbf{E} \ {8}$ (elimination of the universal quantifier from line $8$), not $\land \mathbf{E}$.

2. The formula formalizing the sentence "$b$ is a minimal element of $B$" is $\lnot \exists x (x \in B \land xRb \land x \neq b)$. It is important to specify that $x \in B$, because without it the formula means that $b$ is a minimal element of $A$ (which is the domain of the quantification) and clearly this is false: for instance, if $A = \{0, 1\}$ and $B = \{1\}$, then $1$ is the smallest (and minimal) element of $B$ but not of $A$. So, in your proof that line $2$ derives from line $1$ there is a bug, if you show it we can fix it.

3. Line $3$ is superfluous. It is not surprising that you don't need the hypothesis of minimality for $b$, because in fact you have a stronger hypothesis in line $1$: $b$ is the smallest element of $B$.

4. The formula formalizing the sentence "any minimal element in $B$ is equal to $b$" is $\forall z \big((z \in B \land \neg \exists x(x \in B \land xRz \land x \neq z)) \to b = z \big)$ (pay attention to parentheses, you forgot one).

5. (Maybe as a consequence of the previous error) After line $14$, you first have to introduce the implication, discharging line $4$, and then you have to introduce the universal quantifier. Note that without discharging line $4$, you cannot introduce the universal quantifier because $c$ is a free variable in your hypotheses.

So, a correct proof in Fitch-style natural deduction fixing the aforementioned errors is the following:

$ \fitch{ 1.\, b \in B \land \forall x(x \in B \to bRx) \qquad \textit{b is the smallest element of B}\\ 2.\,b \in B \land \neg \exists x(x \in B \land xRb \land x \neq b) \qquad \textit{b is a minimal element of B} }{ \fitch{3.\, c \in B \land \neg \exists x(x \in B \land xRc \land x \neq c)}{ 4.\,c \in B \ce{3} 5.\,\neg \exists x(x \in B \land xRc \land x \neq c) \ce{3} \fitch{6.\, b \neq c}{ 7.\,\forall x(x \in B \to bRx) \ce{1} 8.\,c \in B \to bRc \Ae{8} 9.\,bRc \ie{9,4} 10.\,bRc \land b \neq c \ci{10,7} 11.\, b \in B \ce{1} 12.\, b \in B \land bRc \land b \neq c \ci{11,10} 13.\,\exists x(x \in B \land xRc \land x \neq c) \Ei{12} 14.\,\bot \ne{5,13} }\\ 15.\,b = c \IP{6-14} }\\ 16.\, (c \in B \land \neg \exists x(x \in B \land xRc \land x \neq c)) \to b = c \ii{3{-15}} 17. \, \forall z((z \in B \land \neg \exists x(x \in B \land xRz \land x \neq z)) \to b = z) \Ai{16} 18.\,b \in B \land \neg \exists x(x \in B \land xRb \land x \neq b) \land \forall z((z \in B \land \neg \exists x(x \in B \land xRz \land x \neq z)) \to b = z) \ci{2,17} } $

---

Note that if you formalize the sentence "$b$ is a minimal element of $B$" as $\forall z ((z \in B \land zRb) \to z = b)$ (which is logically equivalent to your formalization $\lnot \exists z (z \in B \land zRb \land z \neq b)$), then the proof becomes easier, without the need for reductio ad absurdum ($\mathbf{IP}$). Indeed: $ \fitch{ 1.\, b \in B \land \forall x(x \in B \to bRx) \qquad \textit{b is the smallest element of B}\\ 2.\,b \in B \land \forall x((x \in B \land xRb) \to x = b) \qquad \textit{b is a minimal element of B} }{ 3.\,\forall x(x \in B \land xRb \to x = b) \ce{2} \fitch{4.\, c \in B \land \forall x((x \in B \land xRc) \to x = c)}{ 5.\,c \in B \ce{4} 6.\,\forall x((x \in B \land xRc) \to x = c) \ce{4} 7.\, (b \in B \land bRc) \to b = c \Ae{6} 8.\,\forall x(x \in B \to bRx) \ce{1} 9.\, c \in B \to bRc \Ae{8} 10.\, bRc \ie{9,5} 11.\, b \in B \ce{1} 12.\, b \in B \land bRc \ci{11,10} 13.\,b = c \ie{7,12} }\\ 14.\, (c \in B \land \forall x((x \in B \land xRc) \to x = c)) \to b = c \ii{4{-}13} 15. \, \forall z((z \in B \land \forall x((x \in B \land xRz) \to x = z)) \to b = z) \Ai{14} 16.\,b \in B \land \forall x((x \in B \land xRb) \to x = b) \land \forall z((z \in B \land \forall x((x \in B \land xRz) \to x = z)) \to b = z) \ci{2,15} } $