Modus Ponens on A Statement of Deduction?

  • Context: Graduate 
  • Thread starter Thread starter darkchild
  • Start date Start date
Join the discussion
Registration is free. Ask a follow-up in this thread, or start your own.
3 replies · 2K views
darkchild
Messages
153
Reaction score
0
This is from a text on mathematical logic. The theorem to be proven (specialization):

If Δ [itex]\vdash[/itex] [itex]\forall[/itex]vP, then Δ [itex]\vdash[/itex] P(t/v), provided that P admits t for v.

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

Suppose that Δ [itex]\vdash[/itex] [itex]\forall[/itex]vP and P admits t for v. Then modus ponens applied to Δ [itex]\vdash[/itex] [itex]\forall[/itex]vP and [itex]\vdash \forall[/itex]vP [itex]\rightarrow[/itex]P(t/v) (Axiom Scheme A5) gives Δ [itex]\vdash[/itex] 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 [itex]vdash[/itex]. It seems the latter are simply ignored, yet they are crucial to the meaning of the statement.
 
Physics news on Phys.org
darkchild said:
This is from a text on mathematical logic. The theorem to be proven (specialization):

If Δ [itex]\vdash[/itex] [itex]\forall[/itex]vP, then Δ [itex]\vdash[/itex] P(t/v), provided that P admits t for v.

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

Suppose that Δ [itex]\vdash[/itex] [itex]\forall[/itex]vP and P admits t for v. Then modus ponens applied to Δ [itex]\vdash[/itex] [itex]\forall[/itex]vP and [itex]\vdash \forall[/itex]vP [itex]\rightarrow[/itex]P(t/v) (Axiom Scheme A5) gives Δ [itex]\vdash[/itex] 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 [itex]vdash[/itex]. 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.
 
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. Δ [itex]\vdash \forall[/itex]vP would correspond to S
2. [itex]\vdash[/itex][itex]\forall[/itex]vPP(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 Δ.
 
darkchild said:
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. Δ [itex]\vdash \forall[/itex]vP would correspond to S
2. [itex]\vdash[/itex][itex]\forall[/itex]vPP(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.