Grounding rules for (relevant) implication

In Poggiolesi (2020a) a definition of the notion of complete and immediate formal grounding in the background of a relevant framework has been introduced; this definition generates some intuitively acceptable grounding principles for relevant implication. In the present paper our aim is to construct a logic for the notion of complete and immediate formal grounding in a relevant framework based on that definition. Our logic will have the form of a calculus of natural deduction and will formalize the relation of grounding both as a meta-linguistic relation and as a connective. The calculus will contain grounding rules for relevant implication and will be proved to be sound and complete with respect to the original definition. Finally we will prove the deduction theorem at the grounding level, i.e. we will show that grounding formalized as a metalinguistic relation is equivalent to grounding formalized as a connective.