Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

I trying to proove this: For a set of verses $\Sigma$ and a function $s:Var\rightarrow WFF$ : Defenition: subst($\Sigma$,s)={subst($\alpha$,s)|$\alpha\in\Sigma$} . Proove that for every $\varphi$ : if $\Sigma\vdash\varphi$ than $subst(\Sigma,s)\vdash subst(\varphi,s)$.

I started from the basic: if $ \varphi\in\Sigma $ than $\Sigma\vdash\varphi $ and by defention of subst, $subst(\varphi,s)\in subst(\Sigma,s) $ than $subst(\Sigma,s)\vdash subst(\varphi,s) $. Now, i am trying to find the next untrivial movement to proove it for every $\varphi$ that $\Sigma\vdash\varphi$ but can't see it.

share|improve this question
1  
This notation and terminology is unfamiliar to myself. What is meant by a verse? What is $\mathrm{substr}$ supposed to represent? substitution? Given a verse $\alpha$, how is $\mathrm{substr} ( \alpha , s )$ defined? –  Arthur Fischer Jan 1 '13 at 13:17
    
the defenition of subst: for $i\in N$ subst($p_i$,s)=s($p_i$). for $\alpha,\beta\in WFF$ subst($(\neg\alpha)$,s)=$(\neg subst(\alpha,s))$ and $subst((\alpha\circ\beta),s)=(subst(\alpha,s)\circ subst(\beta,s))$ –  Michael Cohen Jan 1 '13 at 13:26
    
While $\circ\in${$\vee,\wedge,\rightarrow$}. And subst(O,s)=O , if $O\in{T,F}$. –  Michael Cohen Jan 1 '13 at 13:33
add comment

1 Answer

Which deducibility relation (expressed by '$\vdash$') is in question here? After all, we can easily concoct deviant deducibility relations which don't respect substitution. So it matters crucially which deduction system you are working with.

To show that a particular deducibility relation respects substitution, you'll need therefore to look at the definition of that relation. If what is in question is deducibility in e.g. a given system of first-order logic, then how the proof goes it will depend on how that system is presented. E.g. is it an old-fashioned axiomatic system with a built-in substitution rule?

Suppose it is a natural deduction system. Then the individual rules $R$ are usually presented in such a way that if you can readily check that if $\varphi$ follows immediately from assumptions $\Sigma$ by the rule $R$, then $subst(\varphi,s)$ follows from $subst(\Sigma,s)$. And then you can argue by induction on the size of proofs that if $\Sigma \vdash \varphi$ then $subst(\Sigma,s)\vdash subst(\varphi,s)$.

But the details must depend on the particular deduction system you are working with. You can't argue entirely in the abstract.

share|improve this answer
    
So you saying that the induction must be on the size of the proof? I am working with the natural deduction system. –  Michael Cohen Jan 1 '13 at 13:40
    
@MichaelCohen Yes, I guess so! –  Peter Smith Jan 1 '13 at 14:27
    
Can you show me you induction move? i have a problem to define it correctly. –  Michael Cohen Jan 1 '13 at 15:30
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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