2
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – Brian Moehring May 28 at 18:06
  • $\begingroup$ Thanks for your remark, @Brian Moehring. $\endgroup$ – F. Zer May 28 at 20:19
2
$\begingroup$

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 \begin{equation}\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) \end{equation} 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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Spectacular. Thank you very much, @Taroccoesbrocco. I wish I could accept this answer two times :-) $\endgroup$ – F. Zer May 28 at 20:16
  • $\begingroup$ 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. $\endgroup$ – F. Zer May 28 at 20:19
  • $\begingroup$ @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. $\endgroup$ – Taroccoesbrocco May 28 at 20:26
  • $\begingroup$ Thank you so much ! It's a great method. I was studying your explanation and wondered about something. $\endgroup$ – F. Zer May 28 at 21:30
  • 1
    $\begingroup$ @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). $\endgroup$ – Taroccoesbrocco May 28 at 21:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.