 Implies here is a logical notion, though just which one, and what the options are, depends on what background logic is assumed. For our discussion, we think of it in so-called rule form: that the argument from \(A\) to \(B\) is valid, which we record (as above) via the turnstile. In some logical settings (e.g., classical logic, in which a certain so-called deduction theorem holds), this is equivalent to the provability of a conditional, but in some settings, it is not. Either way, capture and release jointly make \(A\) and \(\Tr(\left\ulcorner A\right\urcorner)\) logically equivalent in the sense of being inter-derivable. In strong forms, capture and release can lead to the full intersubstitutability of \(A\) and \(\Tr(\left\ulcorner A\right\urcorner)\) in extensional contexts. As we discuss more in  section 4.1,  this is important to some views of the nature of truth. Thus, \(\vdash\) is being used here as a schematic placeholder for a range of different logical notions, each of which will provide some notion of valid inference in some logical theory.