Hostname: page-component-cd9895bd7-fscjk Total loading time: 0 Render date: 2024-12-22T20:46:36.425Z Has data issue: false hasContentIssue false
  • English
  • Français

A solution of the decision problem for the Lewis systems S2 and S4, with an application to topology

Published online by Cambridge University Press:  12 March 2014

J. C. C. McKinsey
Get access Rights & Permissions [Opens in a new window]

Extract

In this paper I shall give a solution of the decision problem for the Lewis systems S2 and S4; i.e., I shall establish a constructive method for deciding whether an arbitrary given sentence of one of these systems is provable. The method is laborious to apply, since, in order to decide by means of it whether a given sentence is provable, it is necessary to construct a (usually very large) finite matrix. The argument will perhaps be of general interest, however, because it does not seem to depend too closely on the special features of these particular systems, so that it may be possible to apply it in order to solve the decision problem for other such systems.

Section II presents the decision method for S2, and Section III for S4. In Section IV, I shall establish a certain correspondence between S4 and topology, which will provide a solution for a decision problem in topology; this correspondence also enables us to settle a previously unsolved problem with regard to the Lewis systems.

In treating of this system, I shall use the notation of Lewis, with the single exception that I shall use the symbol “≣”, instead of Lewis's symbol “=”, for strict equivalence. I shall use the symbol “=” to denote identity. Thus “p≣q” is a formula of S2, while “x=y” is the statement asserting that x and y are identical. I shall refer to the rules, primitive sentences and theorems of S2 by the names and numbers used by Lewis. Whenever a theorem stated by Lewis involves the symbol “=”, I shall of course suppose that this symbol has been replaced throughout by “≣”: thus, for example, I shall take 19.82 to be “(◇p∨◇q) ≣ ◇(p∨q)”, instead of “(◇p∨◇q) ≣ ◇(p∨q)”.

Type
Other
Information
The Journal of Symbolic Logic , Volume 6 , Issue 4 , December 1941 , pp. 117 - 124
Copyright
Copyright © Association for Symbolic Logic 1941

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

References

1 See Lewis, and Langford, , Symbolic logic, pp. 122–178, and pp. 492–502Google Scholar.

2 For a fuller explanation of this notion, see §2 of Tarski's, Der Aussagenkalkül und die Topologie, Fundamenta mathematicae, vol. 31 (1938), pp. 103–134CrossRefGoogle Scholar.

3 Throughout the paper I shall use symbols from the theory of aggregates as abbreviations for certain English expressions. Thus I write “D⊂K” as an abbreviation for “D is a subset of K,” and “x ϵ K” as an abbreviation for “x is a member of K.” I use “∧” for the empty set, and “∨” for the universal set. Later I shall use the symbol “∩” to indicate the intersection of two sets, and the symbol “∪” to indicate the join (logical sum) of two sets.

4 Essentially the same result as that formulated in this theorem will be found in Huntington's, E. V.Postulates for assertion, conjunction, negation, and equality, Proceedings of the American Academy of Arts and Sciences, vol. 72 (1937), pp. 1–44CrossRefGoogle Scholar.

5 These postulates can easily be shown to be equivalent to Huntington's first set of postulates for Boolean algebra (Transactions of the American Mathematical Society, vol. 5 (1904), pp. 288–309CrossRefGoogle Scholar), from which they were derived by some trivial modifications.

6 In his Note on a property of matrices for Lewis and Langford's calculi of propositions, this Journal, vol. 5 (1940), pp. 150–151Google Scholar.

7 This method is very general, and applies to any sentential calculus which has a rule of substitution for sentential variables. The method was explained to me by Professor Tarski, to whom I am also indebted for many other suggestions in connection with the present paper.

8 I am indebted to the referee for a suggestion leading to a considerable simplification of the proof of this theorem, as well as for other helpful criticisms.