Solution to the P − W problem

Anderson and Belnap asked in §8.11 of their treatise Entailment [1] whether a certain pure implicational calculus, which we will call P − W, is minimal in the sense that no two distinct formulas coentail each other in this calculus. We provide a positive solution to this question, variously known as The P − W problem, or Belnap's conjecture.We will be concerned with two systems of pure implication, formulated in a language constructed in the usual way from a set of propositional variables, with a single binary connective →. We use A, B,…, A1, B1, …, as variables ranging over formulas. Formulas are written using the bracketing conventions of Church [3].The first system, which we call S (in honour of its evident incorporation of syllogistic principles of reasoning), has as axioms all instances of (B) B → C →. A → B →. A → C (prefixing),(B) A → B →. B → C →. A → C (suffixing), and rules (BX) from B → C infer A → B →. A → C (rule prefixing),(B’X) from A → B infer B → C →. A → C (rule suffixing),(BXY) from A → B and B → C infer A → C (rule transitivity).The second system, P − W, has in addition to the axioms and rules of S the axiom scheme (I) A → A of identity.We write ⊢SA (⊣SA) to mean that A is (resp. is not) a theorem of S, and similarly for P − W.