Prologue: To borrow straight out of SEP:
The moon is made of green cheese. Therefore, either it is raining in Ecuador now or it is not.
In order to prevent explosion relevant logic is introduced which has prompted Anderson and Belnap's magnum opus Entailment (1975).
As the example below from SEP shows:
$ 1. A_{\{1\}}$ Hyp
$ 2. (A → B)_{\{2\}} $ Hyp
$ 3. B_{\{1,2\}} $ 1,2, → E
Now to prevent irrelevant premises "to creep in" Anderson and Belnap introduced the following rule:
From $A_{\{i\}}$ and $B_{\{i\}}$ to infer $(A\&B)_{i}.$
where i is the index and,
This rule says that two formulae to be conjoined must have the same index before the rule of conjunction introduction can be used.
My Question: As an undergraduate before tackling the mammoth two part editions of the authors I am curious as to the juicy synopsis of their work. How does R actually resolve the entailment paradox with introduction of index because superficially it seems that it must work under assumption of $\mathbb{N}$ to use for index when $\mathbb{N}$ itself must be constructed from primitive recursion using entailment operator?
Intuitively it seems that there must be a hidden tautology inside somewhere. How can I see the big picture or a bit more precisely, how is entailment defined formally?
Thank you.
