= Solution
In the language of <first-order logic>, define
$$
\boxed{\operatorname{Bottom}(b)\;\equiv\;\forall y\;R(b,y),\qquad\operatorname{Minimal}(b)\;\equiv\;\forall y\;(R(y,b)\Rightarrow y=b).}
$$
Thus a <least element> lies below every element, whereas a <minimal element> merely has no distinct element below it. The latter definition allows multiple incomparable <minimal elements>.
Here is a formal <natural deduction> proof, with the antisymmetry axiom available as a premise. Assume $\operatorname{Bottom}(b)$ and take a fresh arbitrary variable $t$. Assume $R(t,b)$. By <universal elimination> applied to $\operatorname{Bottom}(b)$, obtain $R(b,t)$. By <conjunction introduction>, obtain $R(t,b)\land R(b,t)$. Instantiate antisymmetry at $t,b$, and use <modus ponens rule> to obtain $t=b$. Discharge the assumption $R(t,b)$ by <implication introduction>, obtaining $R(t,b)\Rightarrow t=b$. Since $t$ was arbitrary and is free in no undischarged assumption, <universal introduction> gives $\operatorname{Minimal}(b)$. Discharge the initial assumption and universally quantify $b$ to conclude
$$
\boxed{\forall b\;\bigl(\operatorname{Bottom}(b)\Rightarrow\operatorname{Minimal}(b)\bigr).}
$$
Only antisymmetry was needed for this implication; reflexivity and transitivity are part of the ambient <partial order> axioms.
Back to article page
