How to prove (and which deduction systems are necessary/sufficient) the formula $\forall x\exists y f(x)=y$

Question

Let $\mathcal M=\langle M,f\rangle$ be an $\mathcal L$-structure of language $\mathcal L$ that contains $\{=\}$. $f$ is a unary function symbol ($f\subset M\times M$, and $f$ is well defined: $\forall x,y\in M\ x=y\implies f(x)=f(y)$)

The formula $\forall x\exists y\ f(x)=y$ is equivalent to $\forall x\exists y\ \varphi[x,y]$, where $\varphi[x,y]=f(x)=y$

For example using natural deduction:

The first two operations are obvious: starting from the bottom going up ()starting from waht we want to prove, aiming to arrive to an axiom) we use the introduction of $\forall$ and then the introduction of $\exists$.

Then we get the sequent $\vdash\varphi[\tilde y/x,\tilde t/y]$

But this is just an atomic formula.

I am only getting familiar with sequent calculus and natural deduction so I don't know if what I'm asking really makes sense...

If possible I'd also be interested in knowing what type of logical deduction system would be necessary/sufficient for this type of proof.

Answer 1

Every sound and complete proof system for FOL with equality will do.

With Natural Deduction we have:

1) $f(x)=f(x)$ --- by $=$-Intro (the rule has no assumptions)

2) $\exists y (f(x)=y)$ --- from 1) by $\exists$-Intro

$\forall x \ \exists y (f(x)=y)$ --- from 3) by $\forall$-Intro.

---

Very similar with Sequent Calculus:

1) $\to \ f(x)=f(x)$ --- initial sequent

2) $\to \ \exists y (f(x)=y)$ --- from 1) by $\exists$-right

$\to \ \forall x \ \exists y (f(x)=y)$ --- from 2) by $\forall$-right