The completeness of $S1$ and some related systems.
Maxwell J. Cresswell · Notre Dame Journal of Formal Logic · 1972
The system SI, although dating back to Lewis and Langford in 1932 [12] has proved singularly recalcitrant to the algebraic and semantic techniques applied so successfully to other modal logics.In this paper* we define Sl-algebras (section 2), use them to prove the finite model property for SI (section 3), introduce a semantical definition of Sl-validity (section 4) and make a few remarks about various other systems which seem amenable to the SI treatment (section 5).1 The system SI.We use the basis for SI given by Lemmon in [9, p. 178].Lemmon takes ~, =), and L as primitive with the definitions 1 :(a= β)= df ((a^β) .(β*a)) Def M: Ma =df~L~aThe axioms are:and the rules:If a is a PC-tautology or an axiom then La is a theorem.1.4 Uniform substitution for propositional variables.1.5Modus Ponens: ha, ha 3 β -* hβ 1.6Substitution of proved strict equivalents.In view of 1.3 and 1.6 the choice of primitives is immaterial.The following strict equivalences will frequently be tacitly assumed in what follows: *This paper was written in 1969 before the publication of A. Shukla's work on SI in [15].A comparison between his algebras and ours is instructive.I am indebted to Mr.