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

1 Answer 1

Reset to default
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.

$\endgroup$
10
  • $\begingroup$ Spectacular. Thank you very much, @Taroccoesbrocco. I wish I could accept this answer two times :-) $\endgroup$
    – F. Zer
    Commented May 28, 2020 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
    Commented May 28, 2020 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
    Commented May 28, 2020 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
    Commented May 28, 2020 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
    Commented May 28, 2020 at 21:43

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .