Syntactical proof of universal instantiation rule

First: I am not mathematician but philosopher. I understand why the universal instantiation rule is working.

$$\frac{\vdash\forall xA}{\vdash A^x_t}$$

But is there actually a serious proof in a logical proof system (Hilbert etc.) ? I don't personally find the critical step on how to get rid of the universal quantifier from one to the next line.

An idea of a syntactical proof:

1: $$\vdash\forall A$$

2: $$\vdash\forall A\to A$$

3: $$\vdash A$$

The first is the assumption, the second is a fact which I found in a book and which seems serious and the third line is modus ponens on the first two. But now, I have got the same result, but without the substitution in A?

• So, does this mean, my proof is correct, if I just put (x/t) at the last A in line 2 and at the A in line 3? – DORpapst May 11 at 17:19
• @FranzFerdinand For the purposes of producing a formal proof, it does not make sense to pick particular "facts" (theorems) from books. A formal proof is relative to a proof system. It takes work to show that two proof systems produce the same set of theorems (and they don't need to!), and even when you know that, the proofs will still look different. In many proof systems the rule you want to "seriously prove" is taken as a basic rule of inference. I seriously doubt producing a proof in a Hilbert-style proof system is going to be particularly enlightening or convincing. – Derek Elkins May 11 at 19:20
• I think another way to say what you are asking is "is there an established logic where UI is provable but not a primitive rule of inference?" – DanielV May 12 at 14:01
• @DanielV yes, that’s exactly what I meant here. – DORpapst May 14 at 12:10
• Off the top of my head, Godel's paper where he introduced his incompleteness theorem used $\exists$ $\lor$ and $\lnot$ as primitives, so it might not have had UI as a primitive. I don't exactly recall. But if so, UI would have been derived from negation rules, $\exists$-intros, $\exists$-elim, and $\forall x.P \equiv \lnot \exists x.\lnot P$ – DanielV May 15 at 6:32

In other words, if property $$A$$ holds of every object in the "universe" (this means $$\forall x A(x)$$), then it holds also of the object named by $$t$$ (i.e. $$A(t)$$).
$$\forall x A \to A^x_t$$.