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

Question

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:

1. $\forall x(y(x)\Rightarrow\neg o(x))$
2. $\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.

Answer 1

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:

1. By instantiating $\forall x(y(x) \to \neg o(x))$ with $k$ (universal elimination), you get $y(k) \to \neg o(k)$.
2. From $y(k) \to \neg o(k)$ and the premise $o(k)$ you can easily derive $\lnot y(k)$.
3. 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).