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

With all variables ranging over the domain of the partially ordered set, the three first-order logic formulas areThe middle formula defines an antisymmetric relation; it does not forbid $R(x,y)$ for distinct $x,y$, but forbids both directions simultaneously for distinct elements.

Let $\mathbf{A}$ be the one-element partially ordered set $\{a\}$ with $R(a,a)$. Taking $x=a$ witnesses the existential quantifier, and the only $y$ is comparable with $a$. Thus $\mathbf{A}\models \phi$.

Let $\mathbf{B}$ be the two-element antichain $\{a,b\}$, with $R$ consisting only of $(a,a)$ and $(b,b)$. This is a partial order. If $x=a$, choose $y=b$, and if $x=b$, choose $y=a$. In either case both $R(x,y)$ and $R(y,x)$ are false. Therefore no witness for the existential quantifier exists:

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.