Independent axiom schemata for S5

1956 ◽  
Vol 21 (3) ◽  
pp. 255-256
Author(s):  
Alan Ross Anderson

Leo Simons has shown that H1—H6 below constitute a set of independent axiom schemata for S3, with detachment for material implication “→” as the only primitive rule. He also showed that addition of the scheme (◇ ◇ α ⥽ ◇ α) yields S4, and that these schemata for S4 are independent. The question for S5 was left open. We shall show (presupposing familiarity with Simons' paper) that H1—H6 and S, below, constitute a set of independent axiom schemata for S5, with detachment for material implication as the only primitive rule.Let S5′ be the system generated from H1—H6 and S with the help of the primitive rule. It is easy to see that Simons' derivations of the rules (a) adjunction, (b) detachment for strict implication, and (c) intersubstitutability of strict equivalents, may be carried out for S5′. We know that (1) (∼ ◇ ∼ α ⥽ ◇ α) is provable in S2, hence also in S3 and S5′; and (1) and S yield (2) (α ⥽ ∼ ◇ ∼ ◇ α). Perry has shown that addition of (2) to S3 yields S5, so S5 is a subsystem of S5′. And it is easy to prove S in S5; hence the systems are equivalent.

1953 ◽  
Vol 18 (1) ◽  
pp. 60-62 ◽  
Author(s):  
John Myhill

The sign ‘⊃’ (or ‘→’ or ‘C’) functions in many logical systems in a way which precludes its interpretation as either strict or material implication. For example, in the systems of Heyting, Johansson, Fitch and Bernays (positive logic), the following are theorems:Now if ‘⊃’ were interpreted as strict implication, ⊃2 would mean ‘if p is true, then p is strictly implied by every proposition’, i.e. ‘if p is true, it is necessarily true’, which is false for contingently true p. If on the other hand ‘⊃’ were interpreted as material implication, ⊃1 would reduce to ‘~p ∨ p’, i.e. to the law of excluded middle, which is conspicuously lacking in the systems mentioned. The reader is likely in practice to veer between these two interpretations. Thus in Fitch or Heyting on realizing that ‘~p⊃▪ p⊃q’ is a theorem, one thinks of it as meaning ‘a false proposition implies everything’ and regards the implication as material; but the presence of ‘p⊃p’ as a theorem, even for choices of p which do not satisfy excluded middle, inclines one again to the strict interpretation. This vacillation, while it need not lead to the commission of any formal fallacies, tends to hamstring one's intuition and thus waste time. The purpose of this paper is to suggest an interpretation of ‘⊃’ which will prevent such havering.Let two formulae A and B be called interdeducible if A ⊢ B and B ⊢ A.


1965 ◽  
Vol 30 (1) ◽  
pp. 65-68 ◽  
Author(s):  
M. J. Cresswell

I have argued in [1] that a concept bearing some resemblance to ‘p is the answer to d’ (p a proposition and d a question) can be defined wherever d has the form,‘For which a's is it the case that A (a)?’ (Qa)A(a)where a is a variable and A a wff containing a. To say that p is the true and complete answer to (Qa)A(a) is expressed as saying that p is logically equivalent to the true conjunction of A(a) or ~A(a) for each a. It is defined as;Such a concept of answer is like Belnap's [2] direct true answer to a complete list question, or like Harrah's use [3] (p. 43) of the notion of a state description. The main difference between my approach and that of Belnap and Harrah is that while they are concerned to develop a formal metalanguage for discussion of questions and answers I am concerned to express, as far as possible in existing systems, certain interrogative statements; in particular statements of the form ‘— is the (an) answer to —’.While the account in [1] does give a formal analysis of one ‘answer’ concept there are respects in which it is inadequate.1. Since it uses entailment (or strict implication) to define the relation between p the answer and d the question we can shew that if p is the answer to d and q is logically equivalent to p then q is the answer to d.


1951 ◽  
Vol 16 (2) ◽  
pp. 112-120 ◽  
Author(s):  
Schiller Joe Scroggs

Dugundji has proved that none of the Lewis systems of modal logic, S1 through S5, has a finite characteristic matrix. The question arises whether there exist proper extensions of S5 which have no finite characteristic matrix. By an extension of a sentential calculus S, we usually refer to any system S′ such that every formula provable in S is provable in S′. An extension S′ of S is called proper if it is not identical with S. The answer to the question is trivially affirmative in case we make no additional restrictions on the class of extensions. Thus the extension of S5 obtained by adding to the provable formulas the additional formula p has no finite characteristic matrix (indeed, it has no characteristic matrix at all), but this extension is not closed under substitution—the formula q is not provable in it. McKinsey and Tarski have defined normal extensions of S4* by imposing three conditions. Normal extensions must be closed under substitution, must preserve the rule of detachment under material implication, and must also preserve the rule that if α is provable then ~◊~α is provable. McKinsey and Tarski also gave an example of an extension of S4 which satisfies the first two of these conditions but not the third. One of the results of this paper is that every extension of S5 which satisfies the first two of these conditions also satisfies the third, and hence the above definition of normal extension is redundant for S5. We shall therefore limit the extensions discussed in this paper to those which are closed under substitution and which preserve the rule of detachment under material implication. These extensions we shall call quasi-normal. The class of quasi-normal extensions of S5 is a very broad class and actually includes all extensions which are likely to prove interesting. It is easily shown that quasi-normal extensions of S5 preserve the rules of replacement, adjunction, and detachment under strict implication. It is the purpose of this paper to prove that every proper quasi-normal extension of S5 has a finite characteristic matrix and that every quasi-normal extension of S5 is a normal extension of S5 and to describe a simple class of characteristic matrices for S5.


1948 ◽  
Vol 13 (3) ◽  
pp. 138-139 ◽  
Author(s):  
Sören Halldén

It has been shown by Lewis and Langford that the postulate B8,is not deducible in SI. From this it follows that neither are the paradoxes of strict implication deducible in that system. However, the following weaker—but perhaps philosophically equally important—analogues are deducible:


1957 ◽  
Vol 22 (3) ◽  
pp. 241-244
Author(s):  
Alan Ross Anderson

In this paper we show how a modification of results due to Simons ([6]) yields a set of independent axiom schemata for von Wright's M ([8], p. 85), with a single primitive rule of inference. We first describe a system M*, then show its equivalence with M, and finally show that our schemata are independent.1. Axiomatization ofM*. We adopt the notational conventions of McKinsey and Tarski ([4], p. 2), as amended by Simons ([6], p. 309), except that we take “(α ⊰ β)” as an abbreviation for “˜◇˜(α 0→ β)”, rather than for “˜◇(α ∧ ˜β)”. Our only rule of inference is:Rule. If ⊦ α and ⊦ (˜◇˜α → β). then ⊦ β.We have six axiom schemata:We require a number of theorems for the proof of equivalence of M* with M.Theorem 1. If ⊦ α and ⊦ (α → β), then ⊦ β.Theorem 2. If ⊦ α and ⊦ (α ⊰ β), then ⊦ β.Proof by hypothesis, A5, and Theorem 2 (twice).Theorem 3. If ⊦ (α ⊰ β), then (˜◇β → ˜ ◇α).Proof by hypothesis, A6, and Theorem 2.Theorem 4. If ⊦(α ⊰ β), then ⊦[˜˜(γ ∧ α) ⊰ ˜˜(β ∧ γ)].


1954 ◽  
Vol 19 (1) ◽  
pp. 37-40 ◽  
Author(s):  
Moh Shaw-Kwei

As we know, the system of material implication is led into an inconsistency by the Russellian class, defined as λx. Nϵxx. This class, however, does no harm to many other systems, for example, the three-valued system L3 given by J. Łukasiewicz. A natural question is whether or not there exist classes which affect some of these other logical systems. The main result of the present paper is to answer this question affirmatively. At the end of this paper we point out that the interpretation given by J. Łukasiewicz for the system L3 is not satisfactory, and propose a new interpretation.B. Russell deduced the mentioned inconsistency by the aid of the notion of negation. Later on, H. B. Curry pointed out that we could get the same result without the aid of that notion. None of these results affects the system L3 and other similar systems. But these systems may be involved.To show this, we need the following definitions.A function of two variables Cpq will be called an implication when the following “implication rule” is valid:Under this definition we should note that material equivalence Epq, for example, is an implication.Let C be such an implication. Then the symbol “(Cp)iq” is defined recursively byThe class an is defined as λx. (Cϵxx)np, where p is a propositional variable. The rule of absorption of order n, denoted by (An), is:


1939 ◽  
Vol 4 (4) ◽  
pp. 137-154 ◽  
Author(s):  
William Tuthill Parry

Professor C. I. Lewis, in Lewis and Langford's Symbolic logic, designates the system (S2) determined by the postulates used in Chapter VI—namely, 11.1–7 (B1–7) andas the system of strict implication. For certain reasons, he prefers it to either the earlier system (S3) determined by the stronger set of postulates of his Survey of symbolic logic, as emended, namely, A1–7 andor the system (S1) determined by the weaker set of postulates B1–7 or A1–7.But Lewis and others, following O. Becker, have also given consideration to systems which contain some additional principle effecting the reduction of complex modalities to simpler ones. Notable are the system (S4) determined by B1–7 pluswhich includes (is stronger than) S3; and the system (S5) determined by B1–7 pluswhich includes S4.It seems worth while to investigate further the system of the Survey (emended), S3, which is intermediate between S2 and S4. This is the purpose of the present paper. We first prove some additional theorems in S2 and S3. These enable us to reduce all the complex modalities in S3 to a finite number, viz. 42; and it is shown that no further reduction is possible. Finally, several systems which include S3 are considered.


Author(s):  
Eugenio Orlandelli ◽  
Guido Gherardi

This paper introduces the logics of super-strict implications, where  a super-strict implication is  a strengthening of  C.I. Lewis' strict implication that avoids not only the paradoxes of material implication but also those of strict implication. The semantics of super-strict implications is obtained by strengthening the (normal) relational semantics for strict implication. We consider all logics of super-strict implications that are based on relational frames for modal logics in the  modal cube. it is shown that all  logics of super-strict implications are connexive logics in that they validate Aristotle's Theses and (weak) Boethius's Theses. A proof-theoretic characterisation of logics of super-strict implications is given by means of G3-style labelled calculi, and it is proved that the structural rules of inference are admissible in these calculi. It  is also shown that validity in the $$\mathsf{S5}$$-based logic of super-strict implications is equivalent to validity in  G. Priest's negation-as-cancellation-based  logic. Hence, we also   give a cut-free calculus for Priest's logic.


1956 ◽  
Vol 21 (1) ◽  
pp. 60-62 ◽  
Author(s):  
A. N. Prior

In the first of her papers on functional calculi based on strict implication, Ruth Barcan Marcus takes as her starting point the Lewis systems S2 and S4, supplemented by one of the normal bases for quantification theory, and by one special axiom for the mixture, asserting that if possibly something φ's then something possibly φ's. In the symbolism of Łukasiewicz, which will be used here, this axiom is expressible as CMΣxφxΣxMφx. In the present note I propose to show that if S5 had been taken as a startingpoint rather than S2 or S4, this formula need not have been laid down as an axiom but could have been deduced as a theorem.It has been shown by Gödel that a system equivalent to S5 may be obtained if we add to any complete basis for the classical propositional calculus a pair of symbols for ‘Necessarily’ and ‘Possibly,’ which here will be ‘L’ and ‘M’; the axiomsthe ruleRL: If α is a thesis, so is Lα;and the definitionDf. M: M = NLN.


Sign in / Sign up

Export Citation Format

Share Document