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?

  • $\begingroup$ 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? $\endgroup$ – DORpapst May 11 at 17:19
  • 1
    $\begingroup$ @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. $\endgroup$ – Derek Elkins May 11 at 19:20
  • 1
    $\begingroup$ 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?" $\endgroup$ – DanielV May 12 at 14:01
  • $\begingroup$ @DanielV yes, that’s exactly what I meant here. $\endgroup$ – DORpapst May 14 at 12:10
  • $\begingroup$ 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$ $\endgroup$ – DanielV May 15 at 6:32

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

  • $\begingroup$ Hi, Thanks for your answer! I understand this semantical idea, that helps a lot. But my question actually deals more on the syntax. I have added some additional information and my thoughts in the question now. $\endgroup$ – DORpapst May 11 at 17:06

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.