Syntactical proof of universal instantiation rule

$\begingroup$

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?

$\endgroup$ 5

1 Answer

$\begingroup$

The rule of Universal instantiation simply formalizes the evident intuitive principle that "what holds of all, holds of any"

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)$).

In Natural Deduction it is one of the basic rules for quantifiers.

In Hilbert-style proof system we can derive it from the quantifier axiom :

$\forall x A \to A^x_t$.

$\endgroup$ 1

Your Answer

Sign up or log in

Sign up using Google Sign up using Facebook Sign up using Email and Password Submit

Post as a guest

Post Your Answer Discard

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy