- #1
darkchild
- 155
- 0
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
Δ[itex]\vdash[/itex][itex]\forall[/itex]vP.
(meaning [itex]\forall[/itex]vP is deduced from the set of statements Δ.)
There exists an axiom scheme
[itex]\vdash[/itex]\forall[/itex]vP[itex]\rightarrow[/itex](P(t/v).
Then modus ponens is applied to these two to prove that
Δ[itex]\vdash[/itex]P(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?
In the proof of a theorem, it is given that
Δ[itex]\vdash[/itex][itex]\forall[/itex]vP.
(meaning [itex]\forall[/itex]vP is deduced from the set of statements Δ.)
There exists an axiom scheme
[itex]\vdash[/itex]\forall[/itex]vP[itex]\rightarrow[/itex](P(t/v).
Then modus ponens is applied to these two to prove that
Δ[itex]\vdash[/itex]P(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?