Modus Ponens on A Statement of Deduction?

[darkchild]

This is from a text on mathematical logic. The theorem to be proven (specialization):

If Δ \vdash \forallvP, then Δ \vdash P(t/v), provided that P admits t for v.

My confusion concerns the use of modens ponens in the proof:

Suppose that Δ \vdash \forallvP and P admits t for v. Then modus ponens applied to Δ \vdash \forallvP and \vdash \forallvP \rightarrowP(t/v) (Axiom Scheme A5) gives Δ \vdash P(t/v).

I have never seen this before and do not understand how it is legal or exactly what it means to use modus ponens on statements containing Δ (a set of formulas used as premises) and vdash. It seems the latter are simply ignored, yet they are crucial to the meaning of the statement.

 

[gopher_p]

This is from a text on mathematical logic. The theorem to be proven (specialization):

If Δ \vdash \forallvP, then Δ \vdash P(t/v), provided that P admits t for v.

My confusion concerns the use of modens ponens in the proof:

Suppose that Δ \vdash \forallvP and P admits t for v. Then modus ponens applied to Δ \vdash \forallvP and \vdash \forallvP \rightarrowP(t/v) (Axiom Scheme A5) gives Δ \vdash P(t/v).

I have never seen this before and do not understand how it is legal or exactly what it means to use modus ponens on statements containing Δ (a set of formulas used as premises) and vdash. It seems the latter are simply ignored, yet they are crucial to the meaning of the statement.

I looks like what is intended is that the deduction of $\forall Pv$ from $\Delta$ and modus ponens applied to $\forall Pv$ and $\forall Pv\rightarrow P(t/v)$ gives a deduction of $P(t/v)$ from $\Delta$. I would agree that the wording is a bit wonky, though.

 

[darkchild]

What I don't understand is the role played by the symbol Δ. I understand modus ponens as

1. S
2. S → T
∴ T

That cannot be neatly applied to this proof:

1. Δ \vdash \forallvP would correspond to S
2. \vdash\forallvP → P(t/v) should correspond to S → T

However, the formula that corresponds to S in step one is different than the formula that corresponds to S in step 2. It's missing Δ.

 

[gopher_p]

What I don't understand is the role played by the symbol Δ. I understand modus ponens as

1. S
2. S → T
∴ T

That cannot be neatly applied to this proof:

1. Δ \vdash \forallvP would correspond to S
2. \vdash\forallvP → P(t/v) should correspond to S → T

However, the formula that corresponds to S in step one is different than the formula that corresponds to S in step 2. It's missing Δ.

$\forall vP$ corresponds to $S$ and $P(t/v)$ corresponds to $T$.

Again, the wording of the text is a little bit off in my opinion. They aren't applying "informal" modus ponens to the meta-mathematical statements $\Delta\vdash \forall vP$ and $\vdash \left(\forall vP\rightarrow P(t/v)\right)$; they're applying "formal" modus ponens to the formal sentences $\forall vP$ and $\forall vP\rightarrow P(t/v)$.

Note that this is an informal proof that there is a formal deduction of $P(t/v)$ from $\Delta$ given the fact that there is a formal deduction of $\forall vP$ from $\Delta$. It's basically a proof about proofs, and it's more than a little bit meta.