Hostname: page-component-7b7567c8c-fvjsw Total loading time: 0 Render date: 2026-11-13T11:58:15.625Z Has data issue: false hasContentIssue false
  • English
  • Français

Solution to the P − W problem1

Published online by Cambridge University Press:  12 March 2014

E.P. Martin and
R.K. Meyer
E.P. Martin
Affiliation:
Australian National University, Canberra, Australia
R.K. Meyer
Affiliation:
Australian National University, Canberra, Australia
Get accessRights & Permissions [Opens in a new window]

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),

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.

Information

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 47 , Issue 4 , December 1982, pp. 869 - 887
Copyright
Copyright © Association for Symbolic Logic 1982

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Article purchase

Temporarily unavailable

Footnotes

1

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

[1]Anderson, A. R. and Belnap, N. D. Jr., Entailment: The logic of relevance and necessity, vol. 1, Princeton University Press, Princeton, N. J., 1975.Google Scholar
[2]Belnap, N. D. Jr., A formal analysis of entailment, Technical Report No. 7, Contract No. SAR/Nonr-609 (16), Office of Naval Research, New Haven, 1960.CrossRefGoogle Scholar
[3]Church, A., Introduction to mathematical logic, vol. 1, Princeton University Press, Princeton, N. J., 1956.Google Scholar
[4]Curry, H. B. and Feys, R., Combinatory logic, vol. 1, North-Holland, Amsterdam, 1958.Google Scholar
[5]Fine, K., Models for entailment, Journal of Philosophical Logic, vol. 3 (1974), pp. 347–372.CrossRefGoogle Scholar
[6]McRobbie, M. A., A proof theoretic investigation of relevant and modal logics, Ph. D. thesis, Australian National University, Canberra, 1979.Google Scholar
[7]Martin, E. P., The P − W problem, Ph.D. thesis, Australian National University, Canberra, 1978.Google Scholar
[8]Meyer, R. K., A general Gentzen system for implicational calculi, The Relevance Logic News-letter, vol. 1 (1976), pp. 189–201.Google Scholar