Solution to the P − W problem

• Published in: The Journal of symbolic logic 1982-12, Vol.47 (4), p.869-887
• Main Authors: Martin, E.P., Meyer, R.K.
• Format: Article
• Language: English
• Subjects: Circular logic; Entailment; Inductive reasoning; Logical theorems; Mathematical logic; Reasoning; Relevance logic; Semantic models; Terminology
• ISSN: 0022-4812; 1943-5886
• DOI: 10.2307/2273106

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 .