Is it possible to "hide" auxiliary statements introduced by universal and existential instantiations in Hilbert's system? Let's consider a simple derivation in Hilbert's style. We start from two statements that we treat as "axioms":
$\forall x : [P(x) \implies Q(x)] $
$\forall x : P(x)$
We want to prove the following "theorem" (which is an obvious consequence of the two "axioms"):
$\forall x : Q(x)$
First, we apply the rule of "universal instantiation" to the first axiom and get the following statement:
$P(y) \implies Q(y)$
Second, we apply the rule of "universal instantiation" the second axiom and get:
$P(y)$
Now we combine the last two statements using "Modus ponens" and get the following statement:
$Q(y)$
Now we apply "generalization" the last statement to finally get what we wanted to prove:
$\forall x : Q(x)$
My problem with this proof is that between the two axioms and the final statement in the proof we have some "intermediate" statements that do not look to me like "valid" statements because they have some auxiliary variable $y$.
In other words, my expectation was that by applying derivation rules to "valid" statements (axioms of proven theorems) we always get some other "valid" statements. But it looks like it is not always the case.
So, my question is if the Hilbert's style derivation system can be "modified" a bit such that we "hide" those statements such that a proof is a directed acyclic graph with axiom being "input nodes" and the proven theorem is "output node" and, what is important, all the intermediate nodes correspond to some "valid" expressions that make sense (meaning) out of the context of the proof (by themselves).
ADDED:
The proof is taken from here.
 A: In your previous question, you seem to have been seeking a proof system where each proof consists of a list of sentences of first-order classical logic, such that every element of the list is in fact validated by the usual semantics of first-order classical logic (i.e. it holds under all assignments). Here you seek something very similar, except you wish to allow additional mathematical axioms as well. I'll focus on your previous question, since you can freely pass between the two perspectives via a deduction theorem in any Hilbert-style proof system.
The usual Hilbert system H fails your requirement only because of two perceived issues:

*

*each H-proof consists of a list of formulae, as opposed to sentences, and

*you cannot interpret what it means for a formula to be semantically valid, due to the presence of free variables.

The second is not an issue in practice. We call a sentence semantically valid if it holds under every assignment. As Eric Towers noted in the comments, the very same definition applies to formulae. Each assignment assigns values to free variables, so the formula $P(y)$ with only $y$ free in $P$ holds under every assignment precisely if its universal closure, the sentence $\forall y. P(y)$ holds under every assignment. This fact is often summarized (badly) as "free variables are implicitly universally quantified".
So if you dispense with your first requirement (that each proof consist of sentences only), the usual Hilbert system H satisfies your second one.
This leaves your first requirement only, which can now be reformulated as follows: is there a Hilbert-style proof system that generates only sentences? The answer is positive, e.g. the book Introduction to Mathematical Logic by Elliott Mendelson constructs such a Hilbert system in the section "Properties of First-order Theories" of Chapter 2 (in my edition the axioms are given in the statement of Exercise 2.28, but each edition is different).
