so I have read some topics on this but I am still in doubt. I am trying to solve some natural deduction exercices and I am not quite sure what is the difference in how I approach them and the difference in notation, in pratical terms is having ⊢ the same as implication?
For example I have this exercise ⊢ (p => q) => (r + p => r + q) which I resolved like this:
p => q
--assume r + p
------assume r
------r + q
------therefore r => r + q
------assume p
------q
------r + q
------therefore p=> r + q
--r + q
--r + p => r + q
(p => q) => r + p => r + q
Hopefully thats not too hard to understand since I dont know how to properly format here, anyways so I did that one like that and then I have these kinds of exercises :
p => q ⊢ ((p => (p & q)) & ((p & q) => q)
and that one but from the second expression to the first so
((p => (p & q)) & ((p & q) => q) ⊢ p => q
, my question is can I work with these as if the ⊢ is an implication, are they different? what's the approach here.
Unfortunately, implication is an ambiguous word...
The connective $\to$ into $p \to q$ is read : " if $p$, then $q$ ".
The symbol $⊢ \varphi$ means that we have proved (in the calculus) the formula $\varphi$.
In your proof, up to the last but one line, you have produced the derivation :
because the derivation has the open assumption $p \to q$.
In the last step you have used the rule $\to$-intro to perform the last step :
Thus, we have a "strong link" between the two, but they are different : $\to$ is a connective used in the calculus with sentences (i.e. with sentence letters standing for sentences) to generate "more complex" sentences, while $\vdash$ is a symbol (followed by the name of a formula) used in the theory to describe the basic property of the calculus : the existence of a derivation ending with the said formula.