Solution to the <i>P</i> − <i>W</i> problem

Abstract

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,…, A 1 , B 1 , …, 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 ⊢ S A (⊣ S A ) to mean that A is (resp. is not) a theorem of S , and similarly for P − W .