What formal proof systems are capable of proving $\forall x \exists y x = y$ without needing to apply $\forall$-I to $\exists y x = y$?

Question

I am interested in some philosophical questions that depend on whether the open formula $\exists y x = y$ is a logical truth. I'm making the assumption that some logical systems are intended, in the sense that conclusions of those logical systems are ones that ought to be philosophically endorsed. On that assumption, I can clarify what I mean by "logical truth." A logical truth is a statement for which there is a proof in a logical system that is intended (in the sense above). Thus, if standard predicate logic is intended, then the following proof shows that $\exists y x = y$ is a logical truth:

1. $x = x$ (axiom)
2. $\exists y x = y$ (1, $\exists$-I)

This conclusion is philosophically problematic for me. Since I think that all logical truths ought to be considered metaphysically necessary, this commits me to the conclusion that $\Box \exists y x = y$ is a necessary truth, which further leads to the conclusion that $\Box \forall x \Box \exists y x = y$ is a a logical truth. Properly understood, this is the sort of radical conclusion philosophers/logicians should avoid. It has the consequence, for example, that there is nothing that could have failed to be something.

So, I want a logical system in which $\exists y x = y$ never appears as a line in any proof. But there were reasons why it was needed in standard predicate logic. The primary example is in the question's titled. Usually one must prove $\exists y x = y$ "on the way" to proving $\forall x \exists y x = y$, which is harmless, philosophically speaking.

Answer 1

What formal proof systems are capable of proving ∀x∃yx=y without needing to apply ∀ -I to ∃yx=y?

Formal proof by contradcition in DC Proof system: