given $o(k), \neg o(n), \neg y(j), \forall x(y(x)\Rightarrow \neg o(x)), \exists x(y(x))$ prove $y(n)$ using Stanford university fitch system Context:
This is related to another question I've recently asked BUT it is a different formulation of the same problem.
The orihinal problem is given here.
Solving the puzzle is very easy, my goal is to see if I can prove the solution using first-order logic, specifically using the Stanford University style Fitch system.
My formulation (for this question) is more in line with the puzzle then the formulation in the previous question:
Kevin is the oldest hence $o(k)$
Nicholas is not the oldest hence $\neg o(n)$
Joseph is not the youngest hence $\neg y(j)$
I also added two axioms:


*

*$\forall x(y(x)\Rightarrow\neg o(x))$

*$\exists x(y(x))$
I was able to infer $\neg y(k)$, and I believe this, together with $\neg y(j)$ and with axiom 2 should prove $y(n)$ but I can't figure out a way to show that. I would appreciate any help.
 A: There is another implicit premise in the problem: the domain is made up of $j$, $k$, $n$ and nobody else. In a formula,
\begin{align}
\forall x (x = j \lor x = k \lor x = n)
\end{align}
A sketch of the proof in a Fitch-style natural deduction system that $j(n)$ is the following:


*

*By instantiating $\forall x(y(x) \to \neg o(x))$ with $k$ (universal elimination), you get $y(k) \to \neg o(k)$.

*From $y(k) \to \neg o(k)$ and the premise $o(k)$ you can easily derive $\lnot y(k)$.

*From the premises $\exists x \, y(x)$ and $\lnot y(j)$ and from the fact that $\lnot y(k)$ you can infer that $y(n)$, provided that you know that there are no other people in the domain (hence the need for the further premise $\forall x (x = j \lor x = k \lor x = n)$). 


Otherwise, suppose there a fourth person (without a name). From $\exists x \, y(x)$ and $\lnot y(j)$ and $\lnot y(k)$ you cannot infer $y(n)$, because the youngest person might be the fourth person and not $n$.
Note that the hypothesis $\lnot o(n)$ is not necessary in the argument to prove $y(n)$.
Unfortunately, Stanford's proof assistant does not seem able to manage sentences with the identity symbol $=$ (it has no inference rules for it). Therefore, you cannot formulate the further axiom and use it to formalize the argument.
But there are many other proofs assistants for Fitch-style natural deduction that allow you to use the identity symbol $=$ and its inference rules, so you can use them to formalize the argument (in particular step 3).
