Article contents
Solution to the P − W problem1
Published online by Cambridge University Press: 12 March 2014
Extract
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),
(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
We write ⊢SA (⊣SA) to mean that A is (resp. is not) a theorem of S, and similarly for P − W.
- Type
- Research Article
- Information
- Copyright
- Copyright © Association for Symbolic Logic 1982
Footnotes
The results of this paper formed part of the first author's doctoral thesis [7] presented to the Australian National University in 1978.
References
REFERENCES
- 36
- Cited by