Can someone demonstrate a very simple proof in Hilbert for FOL?

[Roman]

Can someone demonstrate a very simple proof in Hilbert for FOL? I'm
confused with how the quantifiers in front of the axioms work...

[Curtis Bright]

Post by Roman
Can someone demonstrate a very simple proof in Hilbert for FOL? I'm
confused with how the quantifiers in front of the axioms work...

In the simplest case the "∀*" (finite sequence of universal quantifiers)
is empty.

A quick proof that |-(∀x.P->∀x.P), where P is a 0-ary relation symbol:

1. ∀x.P->P (Ax5)
2. P->∀x.P (Ax6)
3. ∀x.P->∀x.P (Transitivity on 1, 2)

However, you should still give a justification of why the transitivity
property holds in the first-order system, since it is not a formal rule
of the system and I believe you've only seen it proved for propositional
logic.

Curtis