Past exam of the year 1 of the computer science course of the University of Oxford / 2003 / Calculus, probability, linear algebra, discrete mathematics, logic and proof, and models of computation / 8 / c

In the language of first-order logic, defineThus 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 $\mathrm{Bottom}(b)$ and take a fresh arbitrary variable $t$. Assume $R(t,b)$. By universal elimination applied to $\mathrm{Bottom}(b)$, obtain $R(b,t)$. By conjunction introduction, obtain $R(t,b)\wedge 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 $\mathrm{Minimal}(b)$. Discharge the initial assumption and universally quantify $b$ to concludeOnly antisymmetry was needed for this implication; reflexivity and transitivity are part of the ambient partial order axioms.