MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|cite|improve this question
Perhaps I am being slow, but what is R? The software package? the real numbers in standard mathematics? The real numbers in some constructive proof assistant? Or is it some flavour of logic? – David Roberts Jan 8 '12 at 8:25
I should've made it more clear. R is indeed a flavor of logic. – Sniper Clown Jan 8 '12 at 8:35

You could also read something more recent about substructural logics, of which relevant logic is an example, it doesn't have to be a 1970's text (see section 2.1 of SEP's article on substructural logics).

share|cite|improve this answer

Your Answer


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.