Solution to the P − W problem
Errol P. Martin, R. Meyer · Journal of Symbolic Logic · 1982
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.