I teach an intro logic class. One intuitive way of translating 'there is at most one F' is
$(\forall x)(Fx \rightarrow (\forall y)(Fy \rightarrow x=y))$
A student came up with the following, which is equivalent and much more compact
$(\exists x)(\forall y)(Fy \rightarrow x=y)$
We can demonstrate equivalence via interderivability in a Fitch-style system:
$(\forall x)(Fx \rightarrow (\forall y)(Fy \rightarrow x=y)) \dashv \vdash (\exists x)(\forall y)(Fy \rightarrow x=y)$
Below are two derivations. Right to Left is pretty easy and short. Left to Right (second) is long and a bit of a bear. Here is the question: can that one be simplified, is there a more elegant derivation? I would like to help the less sophisticated students see the equivalence. Actually I found a shorter, clearer derivation. See below.
R to L Right to Left Derivation
L to R Left to Right Derivation, can this be shortened?
L to R Shorter L to R Shorter
