Is Modus Ponens Applicable in Logical Deductions Involving Quantifiers?

[darkchild]

P is a one-place predicate, t is a constant, v is a variable of P. P(t/v) denotes replacing v by t in P.

In the proof of a theorem, it is given that

Δ\vdash\forallvP.
(meaning \forallvP is deduced from the set of statements Δ.)

There exists an axiom scheme

\vdash\forall[/itex]vP\rightarrow(P(t/v).

Then modus ponens is applied to these two to prove that

Δ\vdashP(t/v).

I've never seen modus ponens applied to a deduction and it is used with so I scarcely know what to ask...how is this permissible? How does it work...same as regular modus ponens? Is there a proof that this is shows this is the same as modus ponens, or a definition that describes it?

 

[darkchild]

The axiom scheme should be

\vdash\forallv→P(t/v).

Also, the last paragraph of my original post should say "it is used without explanation, so I scarcely know what to ask." Meaning give me whatever relevant information you've got.

 

[MLP]

This is a day late and a dollar short since your question is from November but ...

I think the axiom scheme should be ∀vP→P(t/v) so we are given the following as premises:

∀vP
∀vP→P(t/v)

notice that this has the form
1. A
2. A→B

Modus ponens is the rule that says that given 1 and 2 we may infer B, i.e., P(t/v)