1 Introduction

1.1 The Sentential Calculus with Identity \( SCI \)

Roman Suszko’s introduction (Bloom & Suszko, 1972) of the Sentential Calculus with Identity (\( SCI \)), was a consequence of his work on non-Fregean logics (see, e.g. Suszko, 1975). According to Gottlob Frege, the denotation (referent, Bedeutung) of a sentence (a formula) is nothing but a truth-value. This principle, called by Suszko the Fregean Axiom, can be formalized as \((\varphi \leftrightarrow \psi )\rightarrow (\varphi \equiv \psi )\) where \(\varphi \equiv \psi \) reads: ‘\(\varphi \) and \(\psi \) have the same denotation’. The essential feature of a non-Fregean logic is the failure of that Fregean Axiom: even if two formulas \(\varphi ,\psi \) have the same truth-value in a given model, i.e. \(\varphi \leftrightarrow \psi \) is satisfied, they may have different denotations, i.e. \(\varphi \not \equiv \psi \). \( SCI \) can be seen as a basic non-Fregean logic that extends classical propositional logic \( CPC \) by an identity connective \(\equiv \) along with corresponding axioms. More precisely, the set \(Fm_\equiv \) of formulas of \( SCI \) is inductively defined over an infinite set V of propositional variables \(x_0, x_1,\ldots \), logical (i.e. truth-functional) connectives \(\bot \), \(\top \), \(\lnot \), \(\vee \), \(\wedge \), \(\rightarrow \) and an identity connective \(\equiv \) for formulas of the form \((\varphi \equiv \psi )\). The axioms of \( SCI \) then are given by all formulas having the form of a theorem of \( CPC \) or are axioms of (propositional) identity according to the following schemes:

  • (id1) \(\varphi \equiv \varphi \)

  • (id2) \((\varphi \equiv \psi )\rightarrow (\varphi \rightarrow \psi )\)

  • (id3) \((\varphi \equiv \psi )\rightarrow (\lnot \varphi \equiv \lnot \psi )\)

  • (id4)–(id7) \(((\varphi _1\equiv \psi _1)\wedge (\varphi _2\equiv \psi _2))\rightarrow ((\varphi _1*\varphi _2)\equiv (\psi _1 *\psi _2))\), where \(*\in \{\vee , \wedge , \rightarrow , \equiv \}\), respectively.

With Modus Ponens MP as the only inference rule, the notion of derivation is defined in the usual way. We write \(\varPhi \vdash _{ SCI }\varphi \) if there is a derivation of \(\varphi \in Fm_\equiv \) from a set \(\varPhi \subseteq Fm_\equiv \).

There are slightly different axiomatizations of \( SCI \) in the literature, and the particular choice of classical connectives for the underlying object language has a certain impact on its expressiveness [the language given in our main reference Bloom and Suszko (1972) is based on \(\lnot \), \(\rightarrow \) besides the identity connective]. For example, \((\varphi \vee \psi ) \equiv (\lnot \varphi \rightarrow \psi )\) is not a theorem, i.e. \(\varphi \vee \psi \) and \(\lnot \varphi \rightarrow \psi \) may have different semantics although they are logically equivalent. However, all relevant results on logic \( SCI \) are independent from the actual choice of logical connectives, see also footnote 2 of Bloom and Suszko (1972). We will therefore assume that logic \( SCI \) is generally defined as in the present paper.

The identity axioms ensure that propositional identity \(\equiv \) forms a congruence relation on formulas which refines material equivalence \(\leftrightarrow \). Indeed, \((\varphi \equiv \psi )\rightarrow (\varphi \leftrightarrow \psi )\) as well as \((\varphi \equiv \psi )\rightarrow (\psi \equiv \varphi )\) and \(((\varphi \equiv \psi )\wedge (\psi \equiv \chi ))\rightarrow (\varphi \equiv \chi )\) are derivable. The ‘compatibility’ of the defined equivalence relation with all connectives of the language is expressed by axioms (id3) and (id4)–(id7). As already observed in Bloom and Suszko (1972), replacing (id3)–(id7) by the single schemeFootnote 1

$$\begin{aligned} (\varphi \equiv \psi )\rightarrow (\chi [x:=\varphi ]\equiv \chi [x:=\psi ]), \end{aligned}$$
(1)

which we call the Substitution Principle SP, results in a deductively equivalent system. SP essentially says that formulas with the same denotation can be replaced by each other in any context. This principle can be seen as a particular instance of a general ontological law known in the literature as the indiscernibility of identicals or Leibniz’s law. SP also represents a necessary condition for the existence of a natural propositional semantics. In fact, if we interpret logical connectives and further operators of the object language semantically as functions on propositions, then SP says that all these functions are well-defined: identical arguments yield identical function values. For instance, SP holds in classical and intuitionistic propositional logic if we interpret propositional identity \(\varphi \equiv \psi \) by \(\varphi \leftrightarrow \psi \). In the language of modal logic, we can introduce an identity connective defining \((\varphi \equiv \psi ):= \square (\varphi \leftrightarrow \psi )\). Under this assumption, SP then holds in the Lewis modal systems \( S3 \), \( S4 \) and \( S5 \) though it is not valid in the weaker Lewis systems \( S1 \) and \( S2 \), cf. (Lewitzka, 2015, 2016; Suszko, 1971). We shall discuss that point in more detail in chapter 4 [Lewis modal logics \( S1 \)\( S5 \) were introduced as axiomatic systems in Lewis and Langford (1959); a study of these systems, including semantic aspects, can be found in Hughes and Cresswell (1996)].

1.2 Intensionality as a Measure for the Discernibility of Propositions

We strictly distinguish between formulas (as syntactic objects of the underlying formal language) and propositions (as semantic objects given as elements of some model-theoretic universe). Formulas denote propositions, i.e. the semantics (denotation) of a formula is a proposition. When we say “proposition \(\varphi \)”, then we actually mean “the proposition denoted by \(\varphi \)”. In the case of classical propositional logic \( CPC \), there are only two propositions, the True and the False, and the denotation of a formula can be identified with its truth-value (this corresponds to Frege’s view). In the opposite extreme, any two different formulas denote different propositions. In this case, the denotation of a formula can be identified with its intension (cf. Examples 2.13 and 2.14 below).Footnote 2

The phenomena of extensionality, intensionality and hyperintensionality are often explained in the following way (we consider here only classical logics, i.e. the classical interpretation of logical connectives), cf. Leitgeb (2019). An operator is extensional (or creates an extensional context) if its application to formulas with the same truth-value (extension) results again in formulas having the same truth-value. Considering the scenario of possible worlds semantics, an operator is viewed as intensional if it is not extensional and if additionally its application to formulas having the same truth-values at all accessible worlds results in formulas with the same truth-value at the given world. If the latter condition is not satisfied, then the operator is regarded as hyperintensional [the notion of hypterintensionality was originally introduced by Cresswell (1975)]. For instance, the modal operator \(\square \) of normal modal logics creates an intensional context: the fact that two formulas \(\varphi \) and \(\psi \) have the same truth-value at a given world does not imply that the truth-values of \(\square \varphi \) and \(\square \psi \) are equal, too; however, if \(\square (\varphi \leftrightarrow \psi )\) is true at the given world, i.e. \(\varphi \) and \(\psi \) have the same truth-values at all accessible worlds, then \(\square \varphi \) and \(\square \psi \) have the same truth-value at the given world – this is ensured by axiom K of normal modal logics. It follows that \(\square \) is not hyperintensional. Hyperintensionality is particularly given if the application of an operator to two logically equivalent formulas may result in formulas with different truth-values; in Cresswell’s words (Cresswell, 1975): “Hyperintensional contexts are simply contexts which do not respect logical equivalence”. Intuitively, in a hyperintensional context there exist more denotations, i.e. propositions, than in the context described by standard possible worlds semantics: in fact, if the application of an operator to \(\varphi \) and \(\psi \) results in formulas with different truth-values, then we may assume that \(\varphi \) and \(\psi \) refer to different propositions.Footnote 3

We propose here an explanation of the three contexts by means of the discernibility of propositions. An extensional context is given if only two propositions can be distinguished, namely the two classical truth-values (extensions): the True and the False. The operators of the language then are extensional in the above sense and can be interpreted as Boolean functions on two truth-values. In normal modal logics, a proposition is given as a set of possible worlds: the proposition denoted by \(\varphi \) is the set of those worlds which are accessible from the given world and where \(\varphi \) is satisfied. Then more than two (actually, infinitely many) propositions can be distinguished: \(\varphi \) and \(\psi \) denote the same proposition iff \(\square (\varphi \leftrightarrow \psi )\) is true at the given world (i.e. \(\varphi \) and \(\psi \) are true at exactly the same accessible worlds). Of course, logically equivalent formulas always denote the same proposition. The context is hyperintensional if more propositions can be discerned than in the framework of standard possible worlds semantics. This happens in the case of \( SCI \) where, for instance, logically equivalent formulas may denote different propositions: e.g. \(\lnot \lnot x\equiv x\) is not valid in \( SCI \), i.e. there is a model where \(\lnot \lnot x\) and x denote different propositions (different elements of the model-theoretic universe).

An intension (or sense) refers to a mental content (which is more than a truth-value), and we understand intensionality as the possibility or capability of a system to deal semantically with intensions. We regard hyperintensionality here as a strong form of intensionality (this interpretation slightly deviates from the usual view where hyperintensionality is regarded as something that goes beyond intensionality). We assume the existence of different degrees of intensionality: the more propositions can be discerned the higher is the degree of intensionality. In the extensional case of \( CPC \), there are only two propositions (cf. Example 2.13 below), the Fregean Axiom \((\varphi \equiv \psi )\leftrightarrow (\varphi \leftrightarrow \psi )\) is valid. Whenever the Fregean axiom fails, we have a certain degree of intensionality as it is the case in normal modal logics. However, normal modal logics still validate the principle \((\varphi \equiv \psi )\leftrightarrow \square (\varphi \leftrightarrow \psi )\) which can be restored in certain extensions of \( SCI \) (see Sect. 4). If this principle also fails and more propositions can be discerned than in modal logic where propositional identity is given by strict equivalence \(\square (\varphi \leftrightarrow \psi )\), then we have a hyperintensional context, a high degree of intensionality. The highest degree of intensionality is achieved if the intension of any formula can be identified with its denotation. In our basic propositional language, that is the case if any two different formulas denote different propositions, a context which also can be represented in \( SCI \) by an intensional model, cf. Example 2.14 below. Thus, in an intensional model, the intension of a formula (i.e. a mental content expressed by the formula’s syntax) is in one-to-one correspondence with the formula’s semantics. We assume the existence of further degrees of intensionality which can be formalized either by appropriate axiomatic extensions of \( SCI \) or by similar logics having an identity connective such as studied in Ishii (1998).

1.3 Some Lewis-Style Modal Logics as Examples of Intensional Logics Modeled as Specific \( SCI \)-Extensions

We review and study some Lewis-style modal logics as particular examples of intensional logics that can be modeled in the object language of \( SCI \) as axiomatic extensions of the logic \( SCI \). We shall refer to such extensions as \( SCI \)-extensions. As already mentioned above, in the language of propositional modal logic, scheme SP of \( SCI \) is valid in Lewis modal logics \( S3 \)\( S5 \) if the identity connective is defined as strict equivalence: \((\varphi \equiv \psi ):= \square (\varphi \leftrightarrow \psi )\). Adding SP to Lewis modal system \( S1 \) results in a logic introduced in Lewitzka (2016) under the name \( S1 \)+\( SP \). In the present paper, we will refer to it as \( S1SP \). We then get the hierarchy \( S1SP \subsetneq S3 \subsetneq S4 \subsetneq S5 \) of Lewis (-style) modal logics for which there is a unifying framework of algebraic semantics based on Boolean algebras. We shall explore that semantics in some detail in Sect. 4. The strong connection between certain \( SCI \)-extensions and Lewis modal systems was already observed in Suszko (1971); Bloom and Suszko (1972) where a correspondence between specific extensions of \( SCI \) and the modal logics \( S4 \) and \( S5 \) is established.

In the present paper, we study a kind of equivalences between \( SCI \)-extensions and Lewis-style modal systems (not restricted to \( S4 \) and \( S5 \)) in a systematic way and establish precise criteria for these equivalences. We consider here both object languages separately – the language of \( SCI \) versus the language of propositional modal logic – and define appropriate translations between them. Results due to Suszko (1971) then can be interpreted as special cases of our general approach.

The main aim of this investigation is to present the logic \( SCI \) as a general framework for the modeling of (hyper-) intensional semantics. For this purpose, we reformulate Suszko’s original semantics and define \( SCI \)-models explicitly as Boolean prealgebras (Boolean prelattices). Such structures are defined in different ways in the literature and are considered appropriate for the modeling of (hyper-) intensional reasoning: see, e.g. Fox and Lappin (2005), Pollard (2008), also Lewitzka (2015). Our presentation then establishes an explicit connection between \( SCI \) and recent research on intensional semantics.

2 Boolean Prealgebras as Models of \( SCI \)

Recall that a preorder on a set M is a binary relation on M satisfying reflexivity and transitivity (if the relation is in addition antisymmetric, then we are dealing with a partial order). We also expect the reader to be familiar with basic concepts concerning Boolean algebras such as filters and ultrafilters and quotient algebras.

Definition 2.1

A structure

$$\begin{aligned} {\mathcal {B}}=(B, \vee ^{\mathcal {B}}, \wedge ^{\mathcal {B}}, \lnot ^{\mathcal {B}}, \bot ^{\mathcal {B}}, \top ^{\mathcal {B}}, \rightarrow ^{\mathcal {B}}, \preceq ^{\mathcal {B}}) \end{aligned}$$

of type (2, 2, 1, 0, 0, 2) with a preorder \(\preceq ^{\mathcal {B}}\) on universe B is a Boolean prealgebra if the following two conditions are satisfied:

  • The relation \(\approx \) defined by \(a\approx b\) \(:\Leftrightarrow \) (\(a\preceq ^{\mathcal {B}} b\) and \(b\preceq ^{\mathcal {B}} a\)) is a congruence relation on B such that the quotient

    $$\begin{aligned} {\mathcal {B}}/{\approx }=(B/{\approx }, \vee ^{{\mathcal {B}}/\approx }, \wedge ^{{\mathcal {B}}/\approx }, \lnot ^{{\mathcal {B}}/\approx }, \bot ^{{\mathcal {B}}/\approx }, \top ^{{\mathcal {B}}/\approx }, \rightarrow ^{{\mathcal {B}}/\approx }) \end{aligned}$$

    is a Boolean algebra, where \(B/{\approx }=\{\overline{a}\mid a\in B\}\) is the universe of congruence classes \(\overline{a}\) of elements \(a\in B\) modulo \(\approx \), and the operations \(\vee ^{{\mathcal {B}}/\approx }\), \(\wedge ^{{\mathcal {B}}/\approx }\), etc. are defined in the usual way.

  • For all \(a,b\in B\):

    $$\begin{aligned} a\preceq ^{\mathcal {B}} b\Leftrightarrow \overline{a}\le ^{{\mathcal {B}}/\approx }\overline{b}, \end{aligned}$$

    where \(\le ^{{\mathcal {B}}/\approx }\) is the underlying lattice order of Boolean algebra \({\mathcal {B}}/{\approx }\).

Given a Boolean prealgebra \({\mathcal {B}}\), we refer to the quotient \({\mathcal {B}}/{\approx }\) as the associated Boolean algebra. If the context is clear, we usually omit superscripts and write \(\vee \) instead of \(\vee ^{\mathcal {B}}\) etc.

Of course, every Boolean algebra together with its lattice order (regarded as a preorder) is trivially a Boolean prealgebra. However, even if a given Boolean prealgebra with given preorder \(\preceq \) is a Boolean algebra, its lattice order \(\le \) may differ from \(\preceq \) (cf. Lemma 2.4 below). Recall that every Boolean algebra is a Heyting algebra. Those Heyting algebras which are not Boolean algebras are non-trivial, natural examples of Boolean prealgebras. In order to see this, consider any designated ultrafilter U of a given Heyting algebra (which exists by Zorn’s Lemma) and the preorder \(a\preceq b\) \(:\Leftrightarrow a\rightarrow b\in U\), where \(a\rightarrow b\) is the relative pseudo-complement of a w.r.t. b. Then the resulting quotient algebra modulo \(\approx \) is the two-element Boolean algebra (of course, there may exist further congruence relations on a given Heyting algebra that result in a Boolean quotient algebra). Finally, one easily verifies that also the condition \(a\preceq b\Leftrightarrow \overline{a}\le \overline{b}\) holds for all elements ab of the Heyting algebra, where \(\le \) is here the lattice order of the two-element quotient algebra.

Note that we cannot do without the second condition of Definition 2.1 since it is not implied by the first condition. Consider, for instance, the 4-element Boolean algebra Pow(2) with the preorder \(\preceq \) given by set-theoretic inclusion on Pow(2) extended by the tuple \((\{1\},\{2\})\). So we have in particular \(\{1\}\preceq \{2\}\). Relation \(\approx \) is the identity on Pow(2) and the resulting quotient algebra is, of course, again the Boolean algebra Pow(2) with lattice order \(\subseteq \). However, the second condition of Definition 2.1 fails since we have \(\{1\}\preceq \{2\}\), though \(\{1\}\nsubseteq \{2\}\).

If one deals with Boolean algebras, then one usually works with a reduced (‘functionally complete’) set of operations since others are definable such as in the case of implication: \(a \rightarrow b:= \lnot a\vee b\). This, however, does not hold in general in Boolean prealgebras. For instance, although \(a \rightarrow b\approx \lnot a \vee b\) is valid in the class of Boolean prealgebras, there exist Boolean prealgebras where \(a\rightarrow b \ne \lnot a \vee b\) holds true. Considering such structures as semantic domains for (classical) propositional logics enables us to assign different denotations to logically equivalent formulas such as \(\varphi \rightarrow \psi \) and \(\lnot \varphi \vee \psi \). This results in a hyperintensional semantics.

Definition 2.2

Let \({\mathcal {B}}\) be a Boolean prealgebra with associated Boolean algebra \({\mathcal {B}}/{\approx }\), and let \(F\subseteq B\) be closed under \(\approx \), i.e. \(a\in F\Leftrightarrow b\in F\) whenever \(a\approx b\), for any \(a,b\in B\). Then we say that F is a filter of \( B \) if the set \(F^{{\mathcal {B}}/{\approx }}=\{\overline{a}\mid a\in F\}\) is a filter (in the usual sense) of Boolean algebra \({\mathcal {B}}/{\approx }\). The notions of proper filter and ultrafilter of a Boolean prealgebra are defined analogously.

The statements of the following Corollary are immediate consequences from the definitions and known facts about filters in Boolean (or Heyting) algebras (cf. Chagrov & Zakharyaschev, 1997).

Corollary 2.3

Let \({\mathcal {B}}\) be a Boolean prealgebra and let \(F\subseteq B\) be closed under \(\approx \). Then the following conditions are equivalent.

  • F is a filter of \({\mathcal {B}}\).

  • For all \(a,b\in B\), the following two conditions are satisfied. If \(a,b\in F\), then \(a\wedge b\in F\). If \(a\in F\) and \(a\preceq b\), then \(b\in F\).

  • \(F\ne \varnothing \), and for all \(a,b\in B\), if \(a\in F\) and \(a \rightarrow b\in F\), then \(b\in F\).

Let F be a filter. Then F is a proper filter iff \(F\ne B\) iff \(\bot \notin F\). Furthermore, F is an ultrafilter iff F is a maximal element (w.r.t. set-theoretic inclusion) among all proper filters iff \(a\in F\) or \(\lnot a\in F\), for any \(a\in B\).

Lemma 2.4

Let \({\mathcal {B}}\) be a Boolean prealgebra. If \({\mathcal {B}}\) is itself a Boolean algebra, then its lattice order \(\le \) refines the given preorder \(\preceq \), i.e. for all \(a,b\in B\): \(a\le b\) implies \(a\preceq b\).

Proof

Suppose the Boolean prealgebra \({\mathcal {B}}\) is a Boolean algebra. Then applying Definition 2.1 and facts about Boolean algebras, we get for all \(a,b\in B\): \(a\le b\) \(\Leftrightarrow \) \(a= a\wedge b\) \(\Rightarrow \) \(a\approx a\wedge b\) \(\Leftrightarrow \) \(\overline{a}=\overline{a\wedge b}\) \(\Leftrightarrow \) \(\overline{a}\le ^{{\mathcal {B}}/{\approx }}\overline{b}\) \(\Leftrightarrow \) \(a\preceq b\). \(\square \)

The concept of \( SCI \)-model was originally introduced in Bloom and Suszko (1972). We are now able to present a different definition based on our notion of Boolean prealgebra.

Definition 2.5

An \( SCI \)-model is a structure

$$\begin{aligned} {\mathcal {M}}=(M, TRUE , \vee ^{\mathcal {M}}, \wedge ^{\mathcal {M}}, \lnot ^{\mathcal {M}}, \bot ^{\mathcal {M}}, \top ^{\mathcal {M}}, \rightarrow ^{\mathcal {M}}, \equiv ^{\mathcal {M}}, \preceq ^{\mathcal {M}}) \end{aligned}$$

such that the reduct \((M, \vee ^{\mathcal {M}}, \wedge ^{\mathcal {M}}, \lnot ^{\mathcal {M}}, \bot ^{\mathcal {M}}, \top ^{\mathcal {M}}, \rightarrow ^{\mathcal {M}}, \preceq ^{\mathcal {M}})\) is a Boolean prealgebra with some (designated) ultrafilter \( TRUE \subseteq M\), and \(\equiv ^{\mathcal {M}}\) is a binary operation such that for all \(m,m'\in M\) the following holds:

$$\begin{aligned} m\equiv ^{\mathcal {M}} m'\in TRUE \Leftrightarrow m = m'. \end{aligned}$$

The elements of universe M are called propositions, and \( TRUE \) is the designated set of true propositions. (As before, we usually omit superscripts if the context is clear.)

An assignment (or valuation) of an \( SCI \)-model \({\mathcal {M}}\) is a function \(\gamma :V\rightarrow M\). Its canonical extension from \(Fm_\equiv \) to M, to which we refer again as \(\gamma \), satisfies the following: \(\gamma (\bot )=\bot ^{\mathcal {M}}\), \(\gamma (\top )=\top ^{\mathcal {M}}\), and \(\gamma (\varphi * \psi )=\gamma (\varphi ) *^{\mathcal {M}} \gamma (\psi )\) for \(*\in \{\vee , \wedge , \rightarrow , \equiv \}\), i.e., \(\gamma :Fm_\equiv \rightarrow M\) can be seen as an ‘homomorphism’ from the object language to a given \( SCI \)-model \({\mathcal {M}}\).

Definition 2.6

If \({\mathcal {M}}\) is an \( SCI \)-model and \(\gamma \) is an assignment of \({\mathcal {M}}\), then we call the tuple \(({\mathcal {M}},\gamma )\) an \( SCI \)-interpretation. The satisfaction relation between interpretations and formulas is defined as follows:

$$\begin{aligned} ({\mathcal {M}},\gamma )\vDash \varphi :\Leftrightarrow \gamma (\varphi )\in TRUE . \end{aligned}$$

If \(({\mathcal {M}},\gamma )\vDash \varphi \) for all assignments \(\gamma \in M^V\), then we write \({\mathcal {M}}\vDash \varphi \) and say that \({\mathcal {M}}\) validates \(\varphi \) (or \(\varphi \) is valid in \({\mathcal {M}}\)). As usual, a set of formulas is satisfied (validated) if all its elements are satisfied (validated). The relation of logical consequence is defined in the standard way: \(\varPhi \Vdash _{ SCI }\varphi :\Leftrightarrow Mod(\varPhi )\subseteq Mod(\{\varphi \})\), where \(Mod(\varPsi )\) is the class of all \( SCI \)-interpretations satisfying \(\varPsi \).

Corollary 2.7

The connective of propositional identity has the intended meaning, i.e. for any interpretation \(({\mathcal {M}},\gamma )\) and any \(\varphi ,\psi \in Fm_\equiv \): \(({\mathcal {M}},\gamma )\vDash \varphi \equiv \psi \) iff \(\gamma (\varphi )=\gamma (\psi )\) iff \(\varphi \) and \(\psi \) denote the same proposition in \(({\mathcal {M}},\gamma )\).

Proof

\(({\mathcal {M}},\gamma )\vDash \varphi \equiv \psi \) iff \(\gamma (\varphi \equiv \psi )\in TRUE \) iff \(\gamma (\varphi )\equiv ^{\mathcal {M}} \gamma (\psi )\in TRUE \) iff \(\gamma (\varphi )=\gamma (\psi )\), by definition of operation \(\equiv ^{\mathcal {M}}\). \(\square \)

In Bloom and Suszko (1972), the authors consider only the logical connectives \(\lnot \) and \(\rightarrow \), and consequently they define an \( SCI \)-model as a structure \({\mathcal {A}}=(A,\lnot , \rightarrow , \equiv )\) that satisfies certain conditions according to Bloom and Suszko (1972, Definition 1.6). In the following, we adapt that definition to our notation in order to show that the original definition from Bloom and Suszko (1972) is equivalent to our notion presented in Definition 2.5 above. The equivalence is not obvious since both definitions are conceptually different. In particular, the original approach of Bloom and Suszko (1972) hides the prelattice structure which is an essential aspect of our notion of \( SCI \)-model and crucial for modeling (hyper-) intensionality explicitly.

The original concept of \( SCI \)-model from Bloom and Suszko (1972), adapted to our notations, can be defined in the following way:

Definition 2.8

Let us call a structure

$$\begin{aligned} {\mathcal {M}}=(M, TRUE , \vee ,\wedge , \lnot , \bot , \top , \rightarrow ,\equiv ) \end{aligned}$$

an original \( SCI \)-model if it is an algebra of type (2, 2, 1, 0, 0, 2, 2) with a proper subset \( TRUE \subsetneq M\) of its universe such that the following conditions are satisfied.

  • The set \( TRUE \) is admissible, i.e. for any valuation \(\gamma :Fm_\equiv \rightarrow M\) and any axiom \(\varphi \) of \( SCI \), it holds that \(\gamma (\varphi )\in TRUE \).Footnote 4

  • \( TRUE \) is closed, i.e. for any \(a,b\in M\): \(a\in TRUE \) and \(a\rightarrow b\in TRUE \) implies \(b\in TRUE \).

  • \( TRUE \) is prime, i.e. for any \(a\in M\): \(a\in TRUE \) or \(\lnot a \in TRUE \).

  • \( TRUE \) is normal, i.e. for any \(a,b\in M\): \(a\equiv b\in TRUE \) iff \(a=b\).

In terms of the original definition (Bloom & Suszko, 1972, Definition 1.6), the conditions of the above Definition 2.8 express that \( TRUE \) is a prime, normal filter of the underlying \( SCI \)-algebra, where a filter is defined as a proper subset that is admissible and closed. Thus, Definition 2.8 restores precisely the concept of a model of \( SCI \) originally introduced in Bloom and Suszko (1972, Definition 1.6). The fact that we are working with a richer propositional language (the object language in Bloom and Suszko (1972) is based on the smaller set of logical connectives \(\lnot ,\rightarrow \)) is not really relevant: all definitions and results can be adapted in the obvious way to the actually given set of primitive connectives.

The following remark emphasizes that a prime, normal filter has the expected properties of an ultrafilter. The first two properties are stated in (Proposition 1.15(a), Bloom and Suszko 1972), and the remaining two follow similarly using classical propositional logic and the fact that \( TRUE \) is admissible and closed.

Remark 2.9

In every original \( SCI \)-model, any prime, normal filter \( TRUE \) has the following properties. For all elements ab:

  • \(a\rightarrow b\in TRUE \) \(\Leftrightarrow \) \(a\in TRUE \) implies \(b\in TRUE \).

  • \(a\notin TRUE \Leftrightarrow \lnot a\in TRUE \).

  • \(a\vee b\in TRUE \Leftrightarrow a\in TRUE \) or \(b\in TRUE \).

  • \(a\wedge b\in TRUE \Leftrightarrow a\in TRUE \) and \(b\in TRUE \).

Theorem 2.10

(Equivalence of the two semantics) The semantics based on Boolean prealgebras is equivalent to the original semantics given in Bloom and Suszko (1972) in the following sense.

  1. (i)

    If \({\mathcal {M}}=(M, TRUE , \vee , \wedge , \lnot , \bot , \top , \rightarrow , \equiv , \preceq )\) is an \( SCI \)-model according to Definition 2.5, then the reduct \({\mathcal {M}}^-=(M, TRUE , \vee , \wedge , \lnot , \bot , \top , \rightarrow , \equiv )\) is an original \( SCI \)-model according to Definition 2.8, i.e. an \( SCI \)-model in the sense of Bloom and Suszko (1972) (with operators for the additional connectives \(\vee \), \(\wedge \), \(\bot \), \(\top \)).

  2. (ii)

    If \({\mathcal {M}}^-=(M, TRUE , \vee , \wedge , \lnot , \bot , \top , \rightarrow , \equiv )\) is an original \( SCI \)-model according to Definition 2.8 [i.e. a model in the sense of Bloom and Suszko (1972)], then the expansion \({\mathcal {M}}\) which extends \({\mathcal {M}}^-\) by the relation \(\preceq \) defined by \(a\preceq b:\Leftrightarrow a\rightarrow b\in TRUE \), is an \( SCI \)-model according to Definition 2.5.

  3. (iii)

    The models \({\mathcal {M}}\) and \({\mathcal {M}}^-\) in (i) and in (ii) satisfy exactly the same formulas. That is, for the models in both items (i) and (ii), the following holds: \(({\mathcal {M}},\gamma )\vDash \varphi \Leftrightarrow ({\mathcal {M}}^-,\gamma )\vDash \varphi \), for any \(\varphi \in Fm_\equiv \) and any valuation \(\gamma :V\rightarrow M\).

Proof

(i): Let \({\mathcal {M}}=(M, TRUE , f_\vee , f_\wedge , f_\lnot , f_\bot , f_\top , f_\rightarrow , f_\equiv , \preceq )\) be an \( SCI \)-model in our sense. Then one easily checks that the set \( TRUE \) satisfies all the conditions given in Definition 2.8 (one has to switch between the Boolean prealgebra \({\mathcal {B}}\) underlying \({\mathcal {M}}\) and the associated Boolean algebra \({\mathcal {B}}/{\approx }\)). For instance, towards admissibility, we show for the identity axiom (id2) that \(\gamma ((\varphi \equiv \psi )\rightarrow (\varphi \rightarrow \psi ))\in TRUE \), for any given valuation \(\gamma \). It is enough to show that \(\overline{\gamma ((\varphi \equiv \psi )\rightarrow (\varphi \rightarrow \psi ))}\) belongs to the corresponding ultrafilter \( TRUE ^{{\mathcal {B}}/{\approx }}\) of the associated Boolean algebra. But if \(\overline{\gamma (\varphi \equiv \psi )}\) belongs to that ultrafilter, then \(\gamma (\varphi \equiv \psi )\in TRUE \), i.e. \(\gamma (\varphi )=\gamma (\psi )\), and thus \(\gamma (\varphi )\rightarrow \gamma (\psi )\in TRUE \). The latter implies \(\overline{\gamma (\varphi \rightarrow \psi )}\in TRUE ^{{\mathcal {B}}/{\approx }}\), whence the claim follows. The remaining conditions follow in a similar way or from properties of (ultra-) filters, see also Corollary 2.3. Thus, \({\mathcal {M}}^-\) is an original \( SCI \)-model.

(ii): Let \({\mathcal {M}}^-=(M, TRUE , \vee , \wedge , \lnot , \bot , \top , \rightarrow , \equiv )\) be an original \( SCI \)-model according to Definition 2.8. For \(a,b\in M\), we define \(a\preceq b:\Leftrightarrow a\rightarrow b\in TRUE \). Furthermore, \(a\approx b:\Leftrightarrow \) (\(a\preceq b\) and \(b\preceq a\)). Since \( TRUE \) satisfies the conditions of Definition 2.8, one recognizes that \( TRUE \) is ‘deductively closed’, i.e. if \(\gamma (\varPhi )\subseteq TRUE \) and \(\varPhi \vdash _{ SCI }\varphi \), then \(\gamma (\varphi )\in TRUE \), for any set \(\varPhi \cup \{\varphi \}\) of formulas and any valuation \(\gamma \) of \({\mathcal {M}}^-\). It follows that \(\preceq \) is reflexive and transitive, i.e. a preorder on M, and \(\approx \) is a congruence. In particular, for any propositional formulas \(\varphi ,\psi \) (without identity connective), if \(\varphi \leftrightarrow \psi \) is a theorem of \( CPC \), then \(\gamma (\varphi )\approx \gamma (\psi )\), for any valuation \(\gamma \). Thus, all Boolean equations are valid in the quotient structure \({\mathcal {M}}^-/{\approx }\) which therefore is a Boolean algebra (actually, it is the two-element Boolean algebra with top element \(\overline{\top }= TRUE \)). In order to verify the second condition of Definition 2.1, it is enough to show that the equivalence

$$\begin{aligned} a\preceq b\Leftrightarrow a\wedge b\approx a \end{aligned}$$

is valid.

\(\Rightarrow \)”: Suppose \(a\preceq b\). Of course, \(a\wedge b\preceq a\) is always true since the formula \((x\wedge y)\rightarrow x\) is a classical tautology and therefore denotes an element of \( TRUE \) under any valuation, in particular under \(x\mapsto a\), \(y\mapsto b\). Now let us verify \(a\preceq a\wedge b\), i.e. \(a\rightarrow (a\wedge b)\in TRUE \). From hypothesis \(a\preceq b\), i.e. \(a\rightarrow b\in TRUE \), and condition (ii) of Definition 2.8 it follows that \(a\in TRUE \) implies \(\{a, b\}\subseteq TRUE \). Since \( TRUE \) is ‘deductively closed’, we get that \(a\in TRUE \) implies \(a\wedge b\in TRUE \). By Remark 2.9(a), we conclude \(a\rightarrow (a\wedge b)\in TRUE \), i.e. \(a\preceq a\wedge b\).

\(\Leftarrow \)”: Suppose \(a\wedge b\approx a\), in particular, \(a\rightarrow (a\wedge b)\in TRUE \). Since \( TRUE \) is ‘deductively closed’, we get \(a\rightarrow b\in TRUE \), i.e. \(a\preceq b\).

Hence, \({\mathcal {M}}^-\) together with relation \(\preceq \) is a Boolean prealgebra according to Definition 2.1. Finally, the equivalence \(a\equiv b\in TRUE \Leftrightarrow a=b\) is ensured by condition (iii) of Definition 2.8. Thus, the structure \({\mathcal {M}}\) which results from \({\mathcal {M}}^-\) by adding relation \(\preceq \) is an \( SCI \)-model according to Definition 2.5 above.

(iii): This follows immediately from the definitions of satisfaction:

\(({\mathcal {M}},\gamma )\vDash \varphi \Leftrightarrow \gamma (\varphi )\in TRUE \Leftrightarrow ({\mathcal {M}}^-,\gamma )\vDash \varphi \). \(\square \)

Remark 2.11

(a) Theorem 2.10 shows that for every original \( SCI \) model [a model in the sense of Bloom and Suszko (1972)] there is an \( SCI \)-model in the sense of our Definition 2.5, and vice-versa, such that exactly the same formulas are satisfied by both models. Actually, the models of both semantics are essentially the same algebraic structures interpreted in different ways. Our approach emphasizes the view on \( SCI \)-models as Boolean prealgebras with an explicitly given preorder. Such objects are crucial for our understanding and modeling of (hyper-) intensional semantics. In general, a Boolean prealgebra can be a free algebraic structure in the sense that no equations between formulas are satisfied a priori: if \(\varphi \ne \psi \), then \(\varphi \equiv \psi \) is false, i.e. \(\varphi \) and \(\psi \) denote different propositions (see Example 2.14 below for such a model). Nevertheless, constraints in form of equations may be imposed and (intensional) semantics can be modeled in a flexible way (e.g. one could require that formulas \(\varphi \) and \(\lnot \lnot \varphi \) always have the same semantics, or that all tautologies denote the same proposition in every model). Theorem 2.10 particularly shows that original \( SCI \)-models are essentially Boolean prealgebras.

(b) Note that the translations between models given in (i) and (ii) of Theorem 2.10 are in general not inverse to each other since the underlying preorders may change. For example, if \({\mathcal {M}}\) is an \( SCI \)-model in our sense, then the reduct \({\mathcal {M}}^-\) according to (i) is an original \( SCI \)-model. However, if we consider the expansion \({\mathcal {M}}^*\) of \({\mathcal {M}}^-\) according to (ii), then the preorder \(\preceq ^*\) of \({\mathcal {M}}^*\) may be strictly coarser than the preorder \(\preceq \) of \({\mathcal {M}}\) although both models are based on the same algebraic structure. In any case, \(\preceq \) refines \(\preceq ^*\). In fact, \(a\preceq b\) implies \(\overline{a}\le \overline{b}\) implies \(\overline{a}\overline{\rightarrow }\overline{b} = \overline{\top }\) implies \(a\rightarrow b \in TRUE \) implies \(a\preceq ^* b\), where \(\le \) is the lattice order, \(\overline{\rightarrow }\) is the implication and \(\overline{\top }\) is the top element of the associated Boolean algebra. This proves in particular that the preorder defined in (ii) of the above theorem is always the coarsest (the largest) possible preorder for a Boolean prealgebra.Footnote 5

As \( SCI \) is sound and complete with respect to the original semantics presented in Bloom and Suszko (1972), Theorem 2.10 yields the corresponding result w.r.t. our equivalent semantics.

Corollary 2.12

(Soundness and Completeness) For any set \(\varPhi \cup \{\varphi \}\subseteq Fm_\equiv \), the following holds: \(\varPhi \Vdash _{ SCI }\varphi \Leftrightarrow \varPhi \vdash _{ SCI }\varphi \).

In the following, we are going to sketch out a direct proof of completeness which will be useful below. Following the usual strategy, it is enough to show that every consistent set of formulas has a model. Suppose \(\varPhi \) is consistent in \( SCI \). By Zorn’s Lemma, there is an extension \(\varPsi \supseteq \varPhi \) which is maximal consistent in the logic \( SCI \). By the axioms of propositional identity, the relation \(\cong \) defined by

$$\begin{aligned} \varphi \cong \psi :\Leftrightarrow (\varphi \equiv \psi )\in \varPsi \end{aligned}$$

is a congruence relation on \(Fm_\equiv \) (symmetry, transitivity and compatibility with operations follow from applications of (1), i.e. the Substitution Property SP). Moreover, by (id2), \(\varphi \cong \psi \) implies: \(\varphi \in \varPsi \Leftrightarrow \psi \in \varPsi \). For \(\varphi \in Fm_\equiv \), let \([\varphi ]\) be the congruence class of \(\varphi \) modulo \(\cong \). Then we put \(M:=\{[\varphi ]\mid \varphi \in Fm_\equiv \}\), \( TRUE :=\{[\varphi ]\mid \varphi \in \varPsi \}\) and define operations \(\lnot [\varphi ]:=[\lnot \varphi ]\), \(([\varphi ]*[\psi ]):=[\varphi * \psi ]\), for \(*\in \{\vee , \wedge , \rightarrow , \equiv \}\), and \(\bot :=[\bot ]\), \(\top :=[\top ]\). The relation \(\preceq \) on M defined by

$$\begin{aligned} {[}\varphi ]\preceq [\psi ] :\Leftrightarrow \varphi \rightarrow \psi \in \varPsi \end{aligned}$$

is a preorder on M. By SP, \(\preceq \) is well-defined. Next we show that the structure

$$\begin{aligned} \mathcal {M'}=(M, \vee , \wedge , \lnot , \bot , \top , \rightarrow , \preceq ) \end{aligned}$$

is a Boolean prealgebra. The relation \(\approx \) given by

$$\begin{aligned} {[}\varphi ]\approx [\psi ] :\Leftrightarrow \varphi \leftrightarrow \psi \in \varPsi \Leftrightarrow ([\varphi ]\preceq [\psi ]\text { and }[\psi ]\preceq [\varphi ]) \end{aligned}$$

is obviously a congruence relation of \(\mathcal {M'}\). Since \(\varPsi \) is maximal consistent, it contains in particular all equivalences \(\varphi \leftrightarrow \psi \) which are valid in \( CPC \). These equivalences axiomatize as equations ‘\(\varphi =\psi \)’ the class of Boolean algebras. It follows that the quotient of \(\mathcal {M'}\) modulo \(\approx \) is a Boolean algebra whose elements are the congruence classes \(\overline{[\varphi ]}\) of the elements \([\varphi ]\in M\) modulo \(\approx \). Moreover, for any elements \([\varphi ],[\psi ]\) we have: \([\varphi ]\preceq [\psi ]\) iff \(\varphi \rightarrow \psi \in \varPsi \) iff \((\varphi \wedge \psi )\leftrightarrow \varphi \in \varPsi \) iff \([\varphi ]\wedge [\psi ]\approx [\varphi ]\) iff \(\overline{[\varphi ]\wedge [\psi ]} = \overline{[\varphi ]}\) iff \(\overline{[\varphi ]} \le \overline{[\psi ]}\), where \(\le \) is the lattice order of the associated Boolean algebra. Hence, \({\mathcal {M}}'\) is a Boolean prealgebra.Footnote 6 By construction, we have for any elements \([\varphi ]\), \([\psi ]\): \([\varphi ] = [\psi ]\) iff \(\varphi \cong \psi \) iff \(\varphi \equiv \psi \in \varPsi \) iff \([\varphi \equiv \psi ]=[\varphi ]\equiv [\psi ]\in TRUE \). Thus,

$$\begin{aligned} {\mathcal {M}}:=(M, TRUE , \vee , \wedge , \lnot , \bot , \top , \rightarrow , \equiv , \preceq ) \end{aligned}$$

is an \( SCI \)-model. We consider the assignment \(\gamma \in M^V\) defined by \(x\mapsto [x]\). By induction on formulas, it follows that \(\gamma (\varphi )=[\varphi ]\). Then we have

$$\begin{aligned} ({\mathcal {M}},\gamma )\vDash \varphi \Leftrightarrow \gamma (\varphi )=[\varphi ]\in TRUE \Leftrightarrow \varphi \in \varPsi . \end{aligned}$$

In particular, \(({\mathcal {M}},\gamma )\vDash \varPhi \) and whence \(\varPhi \) is satisfiable. Applying standard arguments and classical propositional logic, it follows that \( SCI \) is complete w.r.t. the semantics given by the class of our \( SCI \)-models. \(\square \)

Classical propositional logic \( CPC \) is extensional in the sense that the denotation (reference, Bedeutung) of any formula is already determined by its truth-value relative to the underlying assignment: either true or false. Consequently, the Fregean Axiom holds: \((\varphi \leftrightarrow \psi )\leftrightarrow (\varphi \equiv \psi )\). It is known that this situation can be modeled in \( SCI \) by presenting a two-element model where all true formulas denote one element (the true proposition) and all false formulas denote the other one (the false proposition).

Example 2.13

There exists an extensional \( SCI \)-model, i.e. a two-element model \({\mathcal {M}}\) where the denotation of a formula is nothing but a classical truth-value: for every assignment \(\gamma :V\rightarrow \{0,1\}\) and all \(\varphi ,\psi \in Fm\), \(({\mathcal {M}},\gamma )\vDash \varphi \equiv \psi \) iff \(({\mathcal {M}},\gamma )\vDash \varphi \leftrightarrow \psi \) iff \(\varphi \) and \(\psi \) have the same classical truth-value.

Proof

Of course, the desired extensional model will be based (up to isomorphism) on the two-element Boolean algebra \({\mathcal {B}}\) with universe \(\{0,1\}\). Let \(\preceq \) be the natural total order on \(\{0,1\}\). The resulting relation \(\approx \) is the identity and the associated quotient algebra is \({\mathcal {B}}\) itself. We define an additional Boolean operation \(\equiv :\{0,1\}\times \{0,1\}\rightarrow \{0,1\}\) by \((x\equiv y)=1\) \(:\Leftrightarrow \) \(x=y\) (as usual, we consider infix notation for the operation \(\equiv \)). Then \({\mathcal {B}}\) together with \(\equiv \) and \(\preceq \) and the unique ultrafilter \( TRUE :=\{1\}\) yields an \( SCI \)-model \({\mathcal {M}}\). Obviously, for any assignment \(\gamma :V\rightarrow \{0,1\}\) and for any formulas \(\varphi ,\psi \in Fm_\equiv \), we have \(({\mathcal {M}},\gamma )\vDash \varphi \equiv \psi \) iff \(\gamma (\varphi )=\gamma (\psi )\) iff \(\varphi \) and \(\psi \) have the same classical truth-value. \(\square \)

It is clear that the above two-valued \( SCI \)-model along with all possible assignments yields the standard two-valued semantics of classical propositional logic \( CPC \). In fact, \( CPC \) is represented by the \( SCI \)-extension \( SCI ^{ext}\) that results from \( SCI \) by adding the Fregean Axiom \((\varphi \leftrightarrow \psi )\rightarrow (\varphi \equiv \psi )\). The extension \( SCI ^{ext}\) contains \((\varphi \leftrightarrow \psi )\leftrightarrow (\varphi \equiv \psi )\) and thus \((\varphi \leftrightarrow \psi )\equiv (\varphi \equiv \psi )\) as theorems. By SP, \((\varphi \leftrightarrow \psi )\) and \((\varphi \equiv \psi )\) then can be replaced by each other in every context. One easily shows that \( SCI ^{ext}\) is sound and complete w.r.t. the class of all extensional (i.e. two-element) \( SCI \)-models. We have for any \(\varphi \in Fm_\equiv \):

$$\begin{aligned} \vdash _{ SCI ^{ext}}\varphi \text { }\Leftrightarrow \text { } \vdash _{ CPC }\varphi ^*, \end{aligned}$$

where \(\varphi ^*\) is the result of replacing every subformula of the form \(\psi \equiv \chi \) in \(\varphi \) by \(\psi \leftrightarrow \chi \).

Another important example of \( SCI \)-model, as opposed to an extensional model, is an intensional model where the denotation of a formula is determined by its intension, i.e. essentially by its syntax.Footnote 7 In such a model, any two (syntactically) different formulas have different denotations, so the denotation of a formula can be identified with its intension. In the following, we present a construction of such a model. Intensional models have also been constructed for a logic that extends \( SCI \) by propositional quantifiers and a truth predicate [see, e.g. the discussion and a construction presented in Lewitzka (2012)].Footnote 8

Example 2.14

There exists an intensional \( SCI \)-model, i.e. a model \({\mathcal {M}}\) along with an assignment \(\gamma \) such that for all \(\varphi ,\psi \in Fm_\equiv \),

$$\begin{aligned} ({\mathcal {M}},\gamma )\vDash \varphi \equiv \psi \Leftrightarrow \varphi =\psi . \end{aligned}$$

Proof

In order to construct the model \({\mathcal {M}}\), we define a rank \(R:Fm_\equiv \rightarrow {\mathbb {N}}\) on formulas as follows:

  • \(R(x)=R(\bot )=R(\top )=R(\varphi \equiv \psi )=0\), for any \(x\in V\) and \(\varphi ,\psi \in Fm_\equiv \).

  • If \(\varphi ,\psi \in Fm_\equiv \) such that \(R(\varphi )\) and \(R(\psi )\) are already defined, then \(R(\lnot \varphi )=R(\varphi )+1\) and \(R(\varphi *\psi )=max\{R(\varphi ), R(\psi )\}+1\), where \(*\in \{\vee , \wedge ,\rightarrow \}\).

We consider the given enumeration of the set of variables \(V=\{x_0, x_1, x_2,\ldots \}\) and define the set \( TRUE \) by induction on rank R as the smallest set such that the following conditions are satisfied:

  • For formulas of rank 0, we have: \(\bot \not \in TRUE \), \(\top \in TRUE \), \(x_i\in TRUE \) iff i is an even index, \(\varphi \equiv \psi \in TRUE \) iff \(\varphi =\psi \).

  • Suppose membership of all formulas of rank \(\le n\in {\mathbb {N}}\) w.r.t. \( TRUE \) is already determined. Let \(\varphi \), \(\psi \) be formulas such that \(max\{R(\varphi ), R(\psi )\} = n\). Then:

    • \(\varphi \wedge \psi \in TRUE \) if \(\varphi \in TRUE \) and \(\psi \in TRUE \)

    • \(\varphi \vee \psi \in TRUE \) if \(\varphi \in TRUE \) or \(\psi \in TRUE \)

    • \(\lnot \varphi \in TRUE \) if \(\varphi \notin TRUE \)

    • \(\varphi \rightarrow \psi \in TRUE \) if \(\varphi \notin TRUE \) or \(\psi \in TRUE \)

Membership of \( TRUE \) then determines classical truth-values for all formulas. The relation \(\preceq \) on \(M:=Fm_\equiv \) defined by \(\varphi \preceq \psi :\Leftrightarrow \) \(\varphi \rightarrow \psi \in TRUE \) is a preorder. Moreover, the relation \(\approx \) defined by \(\varphi \approx \psi \) \(:\Leftrightarrow \) (\(\varphi \preceq \psi \) and \(\psi \preceq \varphi \)) \(\Leftrightarrow \) ‘both \(\varphi \) and \(\psi \) belong to \( TRUE \) or both \(\varphi \) and \(\psi \) belong to \(M\smallsetminus TRUE \)’ is a congruence relation on the structure \((M,\vee ,\wedge ,\lnot ,\bot ,\top ,\rightarrow )\). The associated quotient algebra is the two-element Boolean algebra \(\{0,1\}\) where 1 is the image of \( TRUE \) under the canonical homomorphism. Thus, any congruence class \(\overline{\varphi }\) equals 0 or 1. Moreover, \(\varphi \preceq \psi \) \(\Leftrightarrow \) \(\varphi \rightarrow \psi \in TRUE \) \(\Leftrightarrow \) [\((\varphi \wedge \psi )\rightarrow \varphi \in TRUE \) and \(\varphi \rightarrow (\varphi \wedge \psi )\in TRUE \)] \(\Leftrightarrow \) \((\varphi \wedge \psi )\approx \varphi \) \(\Leftrightarrow \) \(\overline{\varphi }\le \overline{\psi }\). Hence,

$$\begin{aligned} \mathcal {M'}=(M,\vee ,\wedge ,\lnot ,\bot ,\top ,\rightarrow ,\preceq ) \end{aligned}$$

is a Boolean prealgebra. Together with ultrafilter \( TRUE \) and the operation \(\equiv \) on \(M=Fm_\equiv \) defined by the identity connective itself, we then obtain the \( SCI \)-model

$$\begin{aligned} {\mathcal {M}}=(M, TRUE ,\vee , \wedge ,\lnot ,\bot ,\top ,\rightarrow ,\equiv ,\preceq ). \end{aligned}$$

Consider the assignment \(\gamma :V\rightarrow Fm_\equiv \), \(x\mapsto x\). Then, by induction on formulas, \(\gamma (\varphi )=\varphi \) for any \(\varphi \in Fm_\equiv \). Furthermore, for all \(\varphi ,\psi \in Fm_\equiv \):

$$\begin{aligned} ({\mathcal {M}},\gamma )\vDash \varphi \equiv \psi \Leftrightarrow \gamma (\varphi \equiv \psi )=\varphi \equiv \psi \in TRUE \Leftrightarrow \varphi =\psi . \end{aligned}$$

\(\square \)

As a consequence, already derived in a different way in (Corollary 2.14, Bloom and Suszko 1972), we conclude that only trivial equations are theorems:

Corollary 2.15

For all \(\varphi ,\psi \in Fm_\equiv \), \(\vdash _{ SCI }\varphi \equiv \psi \Leftrightarrow \varphi =\psi \).

Proof

If \(\varphi =\psi \), then by identity axiom (id1): \(\vdash _{ SCI }\varphi \equiv \psi \). Now, we suppose \(\varphi \ne \psi \). Then we have \(({\mathcal {M}},\gamma )\nvDash \varphi \equiv \psi \) for the intensional model constructed above and thus \(\varphi \equiv \psi \) is not logically valid. Soundness yields \(\nvdash _{ SCI }\varphi \equiv \psi \). \(\square \)

In the remainder of this section, we show that some relevant modal principles can be restored in \( SCI \) without additional axioms. The representation of certain Lewis-style modal systems by means of appropriate \( SCI \)-extensions will be the topic of the next section.

For \(\varphi \in Fm_\equiv \), we define

$$\begin{aligned} \square \varphi := (\varphi \equiv \top ). \end{aligned}$$
(2)

Theorem 2.16

Let \({\mathcal {M}}\) be an \( SCI \)-model. Then the following are equivalent:

  1. (i)

    \({\mathcal {M}}\) is based on a Boolean algebra, i.e. the \(\{\vee ,\wedge ,\lnot ,\bot ,\top ,\rightarrow \}\)-reduct of \({\mathcal {M}}\) is a Boolean algebra.

  2. (ii)

    For all formulas \(\chi \) having the form of a theorem of \( CPC \), and for all formulas \(\varphi \) and \(\psi \), model \({\mathcal {M}}\) validates \(\square \chi \) and \((\varphi \equiv \psi )\leftrightarrow \square (\varphi \leftrightarrow \psi )\).

Proof

If \({\mathcal {M}}\) is a Boolean algebra, then all theorems of \( CPC \), as well as their substitution instances, are evaluated by the top element \(\top \) under any assignment. It is also known that the equivalence \(m\rightarrow m'=\top \) \(\Leftrightarrow \) \(m\le m'\) holds in every Boolean algebra (actually, in every Heyting algebra). Then it is clear that (i) implies (ii). Now, suppose (ii) holds true. Then \({\mathcal {M}}\) validates in particular \(\square (\varphi \leftrightarrow \psi )\) whenever \(\varphi \leftrightarrow \psi \) is a classical tautology. Since \((\varphi \equiv \psi )\leftrightarrow \square (\varphi \leftrightarrow \psi )\) is valid in \({\mathcal {M}}\), we have \({\mathcal {M}}\vDash \varphi \equiv \psi \) for all Boolean equations \(\varphi \equiv \psi \) that axiomatize the class of Boolean algebras. Hence, \({\mathcal {M}}\) itself is based on a Boolean algebra. \(\square \)

Definition 2.17

\( SCI ^+\) is the logic that results from \( SCI \) by adding the following axioms:

  • \(\square \chi \) whenever \(\chi \) has the form of a classical tautology (theorem of \( CPC \)),

  • \((\varphi \equiv \psi )\leftrightarrow \square (\varphi \leftrightarrow \psi )\).

The next result then follows from Theorem 2.16.

Corollary 2.18

The \( SCI \)-extension \( SCI ^+\) is sound and complete w.r.t. the class of those \( SCI \)-models which are based on Boolean algebras.

As a consequence, \( SCI ^+\) coincides with the known \( SCI \)-extension \( WB \) which is discussed as a specific theory of \( SCI \) in some works on non-Fregean logic [see, e.g. Wawrzynczak (1973) for a detailed presentation].

The question arises whether the extension \( SCI ^+\) implies further interesting modal laws. Using Corollary 2.18, we may argue semantically showing that the following formulas are theorems of \( SCI^+ \):

  • \(\square \varphi \rightarrow \varphi \)

  • \(\square (\varphi \rightarrow \psi )\rightarrow (\square \varphi \rightarrow \square \psi )\).

In fact, given a Boolean algebra, the top element \(\top \) is contained in every ultrafilter; and for any elements \(m,m'\): if \(m\le m'\), then \(m=\top \) implies \(m'=\top \). Thus, the above formulas are valid in \( SCI ^+\). However, some principles of normal Lewis systems are not valid. For instance, the full necessitation rule does not hold. As a counter-example, we consider the Boolean algebra \(2^2\) with elements \(\varnothing \), \(\{0\}\), \(\{1\}\), \(\{0,1\}\) and set-theoretic inclusion as lattice order, along with the ultrafilter \( TRUE =\{\{0\},\{0,1\}\}\) and operation \(\equiv \) defined by \((m\equiv m'):=\{0\}\in TRUE \) if \(m=m'\), and \((m\equiv m')=\{1\}\notin TRUE \) otherwise. Then \(\square \{0\}=(\{0\}\equiv \top )=\{1\}\not \le \{0\}\). Thus, \(\square (\square \varphi \rightarrow \varphi )\) is not valid.

Definition 2.19

In some analogy to Lewis modal system \( S3 \), we define the following extension of \( SCI ^+\): \( SCI _3\) is the logic that results from \( SCI ^+\) by adding all formulas of the form \(\square (\varphi \rightarrow \psi )\rightarrow \square (\square \varphi \rightarrow \square \psi )\) as theorems.

Note, however, that the alleged analogy to Lewis system \( S3 \) is rather weak. For instance, \(\square (\square (\varphi \rightarrow \psi )\rightarrow \square (\square \varphi \rightarrow \square \psi ))\) is a theorem of \( S3 \) but not of \( SCI _3\).

Definition 2.20

An \( SCI \)-model \({\mathcal {M}}\) is called an \( SCI _3\)-model if \({\mathcal {M}}\) is based on a Boolean algebra and satisfies the following condition for all \(m,m'\in M\):

$$\begin{aligned} m\le m' \Rightarrow \square m\le \square m', \end{aligned}$$

where \(\square m:=(m\equiv \top )\). That is, \(\square \) is a monotonic operation on M.

Corollary 2.21

Logic \( SCI _3\) is sound and complete w.r.t. the class of \( SCI _3\)-models.

Proof

One easily checks that every \( SCI _3\)-model validates formulas of the form \(\square (\varphi \rightarrow \psi )\rightarrow \square (\square \varphi \rightarrow \square \psi )\). In order to prove completeness, it is enough to show that the constructed model in our direct completeness proof above satisfies the condition of monotonicity of \(\square \). Since \( SCI _3\) contains \( SCI ^+\), we already know that that model is a Boolean algebra. So for two elements \([\varphi ]\) and \([\psi ]\), suppose \([\varphi ]\le [\psi ]\) (where \(\le \) is the lattice order). Then \((\varphi \rightarrow \psi ) \equiv \top \in \varPsi \). That is, \(\square (\varphi \rightarrow \psi )\in \varPsi \) and thus \(\square (\square \varphi \rightarrow \square \psi )\in \varPsi \). But then \((\square \varphi \rightarrow \square \psi )\equiv \top \in \varPsi \) and thus \([\square \varphi \rightarrow \square \psi ]=[\top ]\), i.e. \(\square [\varphi ]=[\square \varphi ]\le [\square \psi ]=\square [\psi ]\). \(\square \)

We are interested in conditions that ensure, in some precise sense, complete restorations of some Lewis-style modal systems, in particular of \( S3 \)\( S5 \). It turns out that principle \((\varphi \equiv \psi )\leftrightarrow \square (\varphi \leftrightarrow \psi )\), valid in \( SCI ^+\), is too weak for this purpose. In fact, we must postulate the equation \((\varphi \equiv \psi )\equiv \square (\varphi \leftrightarrow \psi )\), i.e. we must identify propositional identity with strict equivalence. These topics will be studied in Sect. 4.

3 Some Lewis-Style Modal Systems and Their Algebraic Semantics

The goal of this section is to review some Lewis-style modal systems in the vicinity of \( S3 \) (more precisely, systems based on a logic called \( S1SP \)) which in the subsequent section then will be shown to be equivalent, in some precise sense, to certain axiomatic extensions of logic \( SCI \). Our object language is now the language of propositional modal logic \(Fm_\square \), i.e. the set of formulas inductively defined over the set of variables \(V=\{x_0,x_1,\ldots \}\), logical connectives \(\bot , \top , \vee , \wedge , \lnot , \rightarrow \) and the modal operator \(\square \). Thus, the languages \(Fm_\equiv \) and \(Fm_\square \) share the ‘pure’ propositional part based on the logical connectives. We introduce an ‘identity connective’ defined by strict equivalence:

$$\begin{aligned} (\varphi \equiv \psi ) := (\square (\varphi \rightarrow \psi )\wedge \square (\psi \rightarrow \varphi )). \end{aligned}$$
(3)

It is evident that under this interpretation, all Lewis modal systems \( S1 \)\( S5 \) satisfy Suszko’s identity axioms (id1) \(\varphi \equiv \varphi \) and (id2) \((\varphi \equiv \psi )\rightarrow (\varphi \rightarrow \psi )\). Moreover, \( S3 \) also satisfies the remaining identity axioms, i.e. SP ( where, of course, identity is given as strict equivalence according to (3) above). \( S3 \) is the weakest Lewis modal system containing SP (cf. (Lewitzka, 2016, 2015)). In the following, we recall definitions of some relevant Lewis-style modal systems and consider an algebraic semantics which can be immediately translated into \( SCI \)-semantics, and vice-versa. We adopt that particular approach to algebraic semantics from Lewitzka (2016).

Lewis system \( S1 \) can be defined in the following way (see, e.g. Hughes & Cresswell, 1996). All formulas of the following form are axioms:

  • tautologies of \( CPC \) (and their substitution-instances in the modal language)

  • \(\square \varphi \rightarrow \varphi \)

  • \((\square (\varphi \rightarrow \psi )\wedge \square (\psi \rightarrow \chi ))\rightarrow \square (\varphi \rightarrow \chi )\) (transitivity of strict implication)

The inference rules are Modus Ponens MP, Axiom Necessitation AN “If \(\varphi \) is an axiom, then \(\square \varphi \) is a theorem”, and Substitution of Proved Strict Equivalents SPSE “If \(\varphi \equiv \psi \) is a theorem, then so is \(\chi [x:=\varphi ]\equiv \chi [x:=\psi ]\)”. Lewis system \( S3 \) results from \( S1 \) by adding

  1. (S3)

    \(\square (\varphi \rightarrow \psi )\rightarrow \square (\square \varphi \rightarrow \square \psi )\) as an axiom scheme to \( S1 \). Of course, rule AN now applies also to (S3). Rule SPSE can be ignored since it is derivable from the rest. Lewis system \( S4 \) results from \( S3 \) by adding

  2. (S4)

    \(\square \varphi \rightarrow \square \square \varphi \) as an axiom scheme (rule AN now applies also to (S4)). Finally, \( S5 \) results from \( S4 \) by adding

  3. (S5)

    \(\lnot \square \varphi \rightarrow \square \lnot \square \varphi \)

as an axiom scheme (of course, rule AN now extends to instances of (S5)). We do not consider system \( S2 \) here since it seems to be not susceptible to our style of algebraic semantics [however, it is known that \( S2 \) can be captured by a non-normal Kripke-style semantics, cf. Hughes and Cresswell (1996)]. There is no known natural semantics for system \( S1 \), cf. Hughes and Cresswell (1996). If we add SP, \((\varphi \equiv \psi )\rightarrow (\chi [x:=\varphi ]\equiv \chi [x:=\psi ])\), as a theorem scheme to \( S1 \) (recall that rule AN is not applicable to theorems, also note that SP is stronger than the \( S1 \)-rule SPSE), then we obtain modal system \( S1+SP \) which was introduced and studied in Lewitzka (2016). Simplifying notation, we will refer to that system as \( S1SP \) instead of \( S1+SP \). In contrast to \( S1 \), the stronger system \( S1SP \) has a natural model-theoretic semantics which we will recall below.

In system \( S1 \), derivations from the empty set, i.e. derivations of theorems, are defined as usual. For \({\mathcal {L}}\in \{ S1SP , S3 , S4 , S5 \}\) and \(\varPhi \cup \{\varphi \}\subseteq Fm_\square \), we write \(\varPhi \vdash _{\mathcal {L}}\varphi \) if there is a derivation of \(\varphi \) from \(\varPhi \), i.e. a finite sequence \(\varphi _1,\ldots ,\varphi _n=\varphi \) such that for each \(\varphi _i\), \(1\le i\le n\), the following holds: \(\varphi _i\in \varPhi \) or \(\varphi _i\) is an axiom of \({\mathcal {L}}\) or \(\varphi _i\) is obtained by AN (i.e. \(\varphi _i = \square \psi \) for some axiom \(\psi \) of \({\mathcal {L}}\)) or \(\varphi _i\) is obtained by MP applied to preceding formulas of the sequence. Note that we can do without the full Necessitation Rule “If \(\varphi \) is a theorem, then so is \(\square \varphi \)”. In fact, by induction on derivations one shows that the full Necessitation Rule is derivable in \( S4 \).

The following result was originally shown in the context of logic \( S1SP \), cf. Lewitzka (2016, Lemma 2.3). The proof given there makes use of SP. However, one recognizes that SP can be replaced by the \( S1 \)-rule SPSE in the proof. Hence, the result also holds in the weaker system \( S1 \).

Lemma 3.1

(Lewitzka, 2016) Every instance of the following principle N is a theorem of \( S1 \):

$$\begin{aligned} \square \varphi \leftrightarrow (\varphi \equiv \top ). \end{aligned}$$

N expresses the fact that there exists exactly one necessary proposition, namely the proposition denoted by \(\top \). N would easily follow from distribution principle K, \(\square (\varphi \rightarrow \psi )\rightarrow (\square \varphi \rightarrow \square \psi )\).Footnote 9 However, K is not available in \( S1 \). Nevertheless, using N and SP we are able to show the following, cf. (Lewitzka 2016, Lemma 2.4):

Lemma 3.2

(Lewitzka, 2016) Distribution principle K holds in \( S1SP \), i.e. formulas of the form

$$\begin{aligned} \square (\varphi \rightarrow \psi )\rightarrow (\square \varphi \rightarrow \square \psi ) \end{aligned}$$

are theorems of \( S1SP \).

Lemma 3.3

\(\square (\varphi \wedge \psi )\leftrightarrow (\square \varphi \wedge \square \psi )\) is a theorem of \( S1SP \).

Proof

We obtain the following sequence of theorems:

\(\square (\varphi \wedge \psi )\leftrightarrow ((\varphi \wedge \psi )\equiv \top )\), i.e. \(\square (\varphi \wedge \psi )\rightarrow \square (\top \rightarrow (\varphi \wedge \psi ))\), by Lemma 3.1

\((\square (\top \rightarrow (\varphi \wedge \psi ))\wedge \square ((\varphi \wedge \psi )\rightarrow \varphi ))\rightarrow \square (\top \rightarrow \varphi )\), by the transitivity axiom of strict implication of \( S1 \)

\(\square ((\varphi \wedge \psi )\rightarrow \varphi ))\), by rule AN

\(\square (\varphi \wedge \psi )\rightarrow \square (\top \rightarrow \varphi )\), i.e. \(\square (\varphi \wedge \psi )\rightarrow (\varphi \equiv \top )\), by transitivity of implication

\(\square (\varphi \wedge \psi )\rightarrow \square \varphi \), by the last derivation and principle N, i.e. Lemma 3.1

\(\square (\varphi \wedge \psi )\rightarrow \square \psi \) is obtained similarly

(A) \(\square (\varphi \wedge \psi )\rightarrow (\square \varphi \wedge \square \psi )\), follows from the above

\(\square \psi \leftrightarrow (\psi \equiv \top )\), instance of principle N

\((\psi \equiv \top )\rightarrow \square (\varphi \wedge y)[y:=\psi ]\equiv \square (\varphi \wedge y)[y:=\top ]\), instance of SP (where y is a fresh variable)

\(\square \psi \rightarrow (\square (\varphi \wedge \psi )\equiv \square (\varphi \wedge \top ))\), by transitivity of implication

\(\square \psi \rightarrow (\square (\varphi \wedge \top )\rightarrow \square (\varphi \wedge \psi ))\), follows from the above along with propositional logic

\(\varphi \equiv (\varphi \wedge \top )\), by rule AN

\(\square \psi \rightarrow (\square \varphi \rightarrow \square (\varphi \wedge \psi ))\), by applying \( S1 \)-rule SPSE (or the stronger SP)

(B) \((\square \varphi \wedge \square \psi )\rightarrow \square (\varphi \wedge \psi )\), by propositional logic

\(\square (\varphi \wedge \psi )\leftrightarrow (\square \varphi \wedge \square \psi )\), by combining (A) and (B). \(\square \)

By Lemma 3.3, we may write strict equivalence \(\square (\varphi \rightarrow \psi )\wedge \square (\psi \rightarrow \varphi )\) equivalently and shorter as \(\square (\varphi \leftrightarrow \psi )\) in systems containing \( S1SP \). In \( S1SP \), we may also strengthen the result of Lemma 3.1 as follows.

Lemma 3.4

The following scheme \(\square N\) is derivable in \( S1SP \):

$$\begin{aligned} \square \varphi \equiv (\varphi \equiv \top ). \end{aligned}$$

Proof

Consider the following sequence of theorems:

\(\varphi \leftrightarrow (\varphi \leftrightarrow \top )\) is a propositional tautology.

\(\Box (\varphi \leftrightarrow (\varphi \leftrightarrow \top ))\), i.e. \(\varphi \equiv (\varphi \leftrightarrow \top )\), results from rule AN.

\((\varphi \equiv (\varphi \leftrightarrow \top ))\rightarrow (\square x[x:=\varphi ]\equiv \square x[x:=(\varphi \leftrightarrow \top )]\) is an instance of SP.

\(\square \varphi \equiv \square (\varphi \leftrightarrow \top )\) then results from Modus Ponens. \(\square \)

Definition 3.5

By a Boolean model we mean a Boolean algebra with a designated ultrafilter \( TRUE \) and an additional unary operation \(\square \). As before, the underlying lattice order is denoted by \(\le \).

Definition 3.6

Let \({\mathcal {M}}\) be a Boolean model satisfying the following conditions for all \(a,b,c\in M\):

  1. (1)

    \(\square a\in TRUE \Leftrightarrow a=\top \)

  2. (2)

    \(\square a\le a\)

  3. (3)

    \(\square (a\rightarrow b)\wedge \square (b\rightarrow c)\le \square (a\rightarrow c)\)

Then we call \({\mathcal {M}}\) an \( S1SP \)-model.

Note that conditions (2) and (3) reflect corresponding axioms of \( S1 \).

Lemma 3.7

In every \( S1SP \)-model it holds that

$$\begin{aligned} \square (a \wedge b)\in TRUE \Leftrightarrow (\square a\wedge \square b)\in TRUE , \end{aligned}$$

for all elements ab, i.e. formulas of the form \(\square (\varphi \wedge \psi )\leftrightarrow (\square \varphi \wedge \square \psi )\) are valid in the class of \( S1SP \)-models. Moreover, principle K, \(\square (\varphi \rightarrow \psi )\rightarrow (\square \varphi \rightarrow \square \psi )\), is valid in the class of \( S1SP \)-models.

Proof

By (1), \(\square (a \wedge b)\in TRUE \) \(\Leftrightarrow \) \(a=\top \) and \(b=\top \) \(\Leftrightarrow \) \(\square a\in TRUE \) and \(\square b\in TRUE \) \(\Leftrightarrow \) \(\square a\wedge \square b \in TRUE \). The second assertion can be shown as follows: For a given \( S1SP \)-model, suppose \(\square (a\rightarrow b)\in TRUE \) and \(\square a\in TRUE \). The former implies \(a\rightarrow b=\top \), i.e. \(a\le b\). The latter implies \(a=\top \). It follows \(b=\top \) and thus \(\square b\in TRUE \). \(\square \)

Notice that validity of modal principle K in the class of \( S1SP \)-models does not mean that all instances of K are interpreted by the top element of the given Boolean algebra (as it is the case in normal modal logics). It only means that such instances are interpreted by some element of the ultrafilter \( TRUE \), a designated ultrafilter that contains in particular the element \(\square \top \). Actually, we cannot choose an arbitrary ultrafilter \( TRUE \) of the Boolean algebra because (1) of Definition 3.6 must be fulfilled. In this aspect, our semantic approach differs from the standard one where the class of modal algebras usually forms an equational class, i.e. a variety of algebras. Recall that a modal algebra, in the usual sense, is a Boolean algebra with an operator \(\square \) satisfying the following stronger conditions for all elements ab:

$$\begin{aligned} \begin{aligned}&\square (a \wedge b) = \square a\wedge \square b,\text { and }\\&\quad \square \top =\top . \end{aligned} \end{aligned}$$

The variety of all modal algebras, given in this way, forms the standard algebraic semantics for normal modal logic \( K \).

Given the modal language \(Fm_\square \) and an \( S1SP \)-model \({\mathcal {M}}\), the notion of an assignment (valuation) \(\gamma :V\rightarrow M\) is defined as before as a ‘homomorphism’ from \(Fm_\square \) to \({\mathcal {M}}\), in particular: \(\gamma (\square \varphi )=\square (\gamma (\varphi ))\). Also the notion of satisfaction is given in the same way: \(({\mathcal {M}},\gamma )\vDash \varphi \Leftrightarrow \gamma (\varphi )\in TRUE \). \( S1SP \)-models were introduced in Lewitzka (2016) (using another terminology) to provide a kind of algebraic semantics for Lewis-style modal logic \( S1SP \):

Theorem 3.8

(Lewitzka, 2016) \( S1SP \) is (strongly) sound and complete with respect to the class of all \( S1SP \)-models.

Definition 3.9

We call a Boolean model \({\mathcal {M}}\) an \( S3 \)-model if the following hold for all \(a,b\in M\):

  1. (1)

    \(\square a\in TRUE \Leftrightarrow a=\top \)

  2. (2)

    \(\square a\le a\)

  3. (S3)

    \(\square (a\rightarrow b)\le \square (\square a\rightarrow \square b)\)

Lemma 3.10

Every \( S3 \)-model is an \( S1SP \)-model, i.e. condition (3) of Definition 3.6 is satisfied. Moreover, in every \( S3 \)-model, modal operator \(\square \) is a monotone function and the following holds for all elements ab:

$$\begin{aligned} \square (a\wedge b) = \square a \wedge \square b. \end{aligned}$$

Proof

Condition (S3) ensures that \(\square \) is a monotone function: \(a\le b\) iff \(a\rightarrow b=\top \) iff \(\square (a\rightarrow b)\in TRUE \) \(\overset{(S3)}{\Rightarrow }\) \(\square (\square a\rightarrow \square b)\in TRUE \) iff \(\square a\rightarrow \square b=\top \) iff \(\square a\le \square b\). Note that \(a\wedge b\le a\) and \(a\wedge b\le b\). Monotonicity implies

$$\begin{aligned} \square (a\wedge b)\le \square a\wedge \square b. \end{aligned}$$

On the other hand, \(\varphi \rightarrow (\psi \rightarrow (\varphi \wedge \psi ))\) is a propositional tautology and therefore denotes the top element, under any assignment. Thus, for all elements ab:

\(\square (a \rightarrow (b\rightarrow (a \wedge b)))\in TRUE \).

By condition (S3) along with ’Modus Ponens’:

\(\square (\square a\rightarrow \square (b\rightarrow (a\wedge b)))\in TRUE \), i.e. \(\square a\le \square (b \rightarrow (a\wedge b))\).

Then by (S3): \(\square (b\rightarrow (a\wedge b))\le \square (\square b\rightarrow \square (a \wedge b))\). Thus,

$$\begin{aligned} \begin{aligned}&\square a\le \square (\square b\rightarrow \square (a\wedge b))\le \square b\rightarrow \square (a\wedge b),\text { and hence}\\&\quad \square a\rightarrow (\square b\rightarrow \square (a \wedge b))=\top . \end{aligned} \end{aligned}$$

The term on the left hand side of the last equation is an interpretation of the formula \(x\rightarrow (y\rightarrow z)\) which is logically equivalent to \((x\wedge y)\rightarrow z\).

Hence, \((\square a\wedge \square b)\rightarrow \square (a\wedge b)=\top \), i.e.

$$\begin{aligned} \square a\wedge \square b\le \square (a\wedge b). \end{aligned}$$

Finally, \(\square a\wedge \square b = \square (a \wedge b)\).

In order to see that every \( S3 \)-model is an \( S1SP \)-model, it is enough to show that condition (3) of Definition 3.6 follows from the conditions of Definition 3.9:

\(((\varphi \rightarrow \psi )\wedge (\psi \rightarrow \chi ))\rightarrow (\varphi \rightarrow \chi )\) is a propositional tautology and is therefore interpreted by the top element of any model. Then by (1),

$$\begin{aligned} \square (((a\rightarrow b)\wedge (b\rightarrow c))\rightarrow (a\rightarrow c))\in TRUE . \end{aligned}$$

Applying (S3) and ‘Modus Ponens’, we get

$$\begin{aligned} \square (\square ((a\rightarrow b)\wedge (b\rightarrow c))\rightarrow \square (a\rightarrow c)) \in TRUE \end{aligned}$$

Since \(\square a\wedge \square b = \square (a \wedge b)\), as shown above, we obtain the following: \(\square ((\square (a\rightarrow b)\wedge \square (b\rightarrow c))\rightarrow \square (a\rightarrow c)) \in TRUE \). Applying condition (1) yields

$$\begin{aligned} (\square (a\rightarrow b)\wedge \square (b\rightarrow c))\rightarrow \square (a\rightarrow c)=\top , \end{aligned}$$

i.e. \(\square (a\rightarrow b)\wedge \square (b\rightarrow c)\le \square (a\rightarrow c)\), which is condition (3) of Definition 3.6. \(\square \)

Definition 3.11

We call a Boolean model \({\mathcal {M}}\) an \( S4 \)-model if the following conditions hold for all elements ab:

  1. (1)

    \(\square a\in TRUE \Leftrightarrow a=\top \)

  2. (2)

    \(\square a\le a\)

  3. (K)

    \(\square (a\rightarrow b)\le \square a \rightarrow \square b\)

  4. (S4)

    \(\square a\le \square \square a\)

Lemma 3.12

Every \( S4 \)-model is an \( S3 \)-model.

Proof

It is enough to show that condition (S3) holds in every \( S4 \)-model.

\(\square \top =\top \), by conditions (1) and (S4)

\(\square (\square (a\rightarrow b)\rightarrow (\square a\rightarrow \square b))=\top \), by (K)

\(\square \square (a\rightarrow b)\rightarrow \square (\square a\rightarrow \square b)=\top \), by (K)

\(\square \square (a\rightarrow b)\le \square (\square a\rightarrow \square b)\), by properties of Boolean algebras

\(\square (a\rightarrow b)\le \square (\square a\rightarrow \square b)\), by (S4). This is condition (S3). \(\square \)

In the literature, an \( S4 \)-algebra, also known as a topological Boolean algebra or an interior algebra, is defined as a Boolean algebra with an operator \(\square \) such that the following conditions (IA1)–(IA4) are satisfied by all elements ab:

  1. (IA1)

    \(\square a\le a\)

  2. (IA2)

    \(\square \square a=\square a\)

  3. (IA3)

    \(\square (a\wedge b) = \square a\wedge \square b\)

  4. (IA4)

    \(\square \top =\top \).

The operator \(\square \) then is called an interior operator in analogy to a corresponding situation in topology. The class of interior algebras is a subvariety of the variety of modal algebras.

Theorem 3.13

Every \( S4 \)-model is an \( S4 \)-algebra.

Proof

Suppose \({\mathcal {M}}\) is a \( S4 \)-model in the sense of Definition 3.11. Then (IA1) above holds trivially. (IA2) follows from (IA1) along with condition (S4). (IA3) is warranted by Lemmata 3.12 and 3.10. Finally, (IA4) follows from conditions (1) and (S4) of Definition 3.11. \(\square \)

The converse of Theorem 3.13 is not true. As a counter-example we consider any Boolean algebra with more than two elements and an interior operator \(\square \) given as the identity: \(a\mapsto \square a=a\). This yields an interior algebra, i.e. an \( S4 \)-algebra. Any ultrafilter U of that algebra contains some element \(a < \top \). Then condition (1) of Definition 3.11 cannot be satisfied by all elements. An interior algebra gives rise to an \( S4 \)-model in our sense if it has an ultrafilter \( TRUE \) such that for any element a of the algebra, \(a< \top \) implies \(\square a \notin TRUE \). Thus, the class of \( S4 \)-models is strictly contained in the class of all \( S4 \)-algebras. The variety of all \( S4 \)-algebras forms the standard algebraic semantics of modal system \( S4 \). Nevertheless, strong soundness and completeness of \( S4 \) can already be established w.r.t. the subclass of \( S4 \)-models, cf. Lewitzka (2016, 2017).

Definition 3.14

We call a Boolean model \({\mathcal {M}}\) an \( S5 \)-model if the following holds for all elements \(a\in M\):

$$\begin{aligned} \begin{aligned} \square a= {\left\{ \begin{array}{ll} &{}\top ,\text { if } a=\top \\ &{}\quad \bot ,\text { else.} \end{array}\right. } \end{aligned} \end{aligned}$$

Note that Definition 3.14 does not impose any condition on the designated ultrafilter \( TRUE \) of \({\mathcal {M}}\). This fact is reflected by the next result.

Lemma 3.15

Let \({\mathcal {M}}\) be a Boolean algebra with an operator \(\square \). The following conditions are equivalent:

  1. (i)

    \({\mathcal {M}}\) along with a particular ultrafilter is an \( S5 \)-model.

  2. (ii)

    \({\mathcal {M}}\) along with any arbitrary ultrafilter is an \( S5 \)-model.

  3. (iii)

    \({\mathcal {M}}\) along with any arbitrary ultrafilter is an \( S4 \)-model.

Proof

(i) implies (ii): It is clear that the condition of Definition 3.14 is independent from any particular ultrafilter.

(ii) implies (iii): If \({\mathcal {M}}\) (together with some ultrafilter) is an \( S5 \)-model, then there are exactly two possibilities for any \(a\in M\): \(\square a = \top \) or \(\square a = \bot \). Now one easily verifies that the conditions of Definition 3.11 are satisfied with respect to every ultrafilter of \({\mathcal {M}}\).

(iii) implies (i): Suppose (iii) is true. Then by conditions (1) and (S4) of Definition 3.11, we get \(\square \top =\top \). It remains to show that \(\square a=\bot \) whenever \(a<\top \). So let \(a <\top \). Suppose \(\square a >\bot \). Then there exists some ultrafilter \( TRUE \) such that \(\square a\in TRUE \). By hypothesis, \({\mathcal {M}}\) together with \( TRUE \) is an \( S4 \)-model. Since \(\square a\in TRUE \), condition (1) of an \( S4 \)-model then implies \(a =\top \), a contradiction to our assumption \(a <\top \). Thus, \(\square a =\bot \). \(\square \)

In particular, every \( S5 \)-model is an \( S4 \)-model and thus an interior algebra. \( S5 \)-models validate the equation \(\Diamond \square a=\square a\), where \(\Diamond a:= \lnot \square \lnot a\) is regarded a closure operator. If added to the equations (IA1)–(IA4) above, that equation defines a subvariety of interior algebras called \( S5 \)-algebras in the literature. Thus, \( S5 \)-models in the sense of Definition 3.14 are \( S5 \)-algebras (we believe that the converse is false).

Recall that the relation of satisfaction between \( S1SP \)-interpretations and formulas of \(Fm_\square \) is defined similarly as for \( SCI \) models and formulas of language \(Fm_\equiv \). Also the concept of logical consequence is defined analogously. Extending the proof of Theorem 3.8 in a straightforward way [see also Lewitzka (2017) for some details] and resuming this section, we then may conclude the following.

Theorem 3.16

Let \({\mathcal {L}}\in \{ S1SP , S3 , S4 , S5 \}\). Then logic \({\mathcal {L}}\) is strongly sound and complete w.r.t. the class of all \({\mathcal {L}}\)-models.

4 Equivalences Between \( SCI \)-Extensions and Lewis-Style Modal Logics

The goal of this section is to show that under certain assumptions, some Lewis-style modal logics are, in a precise sense, equivalent to certain axiomatic extensions of \( SCI \). The crucial conditions for these equivalences are the following:

  1. (I)

    ‘The \( SCI \) principles of propositional identity hold. In particular, SP is valid.’

  2. (II)

    ‘Propositional identity = strict equivalence’, i.e. \((\varphi \equiv \psi )\equiv \square (\varphi \leftrightarrow \psi )\) holds.

  3. (III)

    Necessity = identity with proposition \(\top \). In particular, there is exactly one necessary proposition: the proposition denoted by \(\top \)’, i.e. \(\square \varphi \equiv (\varphi \equiv \top )\) holds.

  4. (IV)

    ‘All classical tautologies are necessary: If \(\varphi \) is a classical tautology (i.e. an instance of a theorem of \( CPC \)), then \(\square \varphi \) is valid.’

From a semantic point of view, (III) and (IV) will ensure that the involved \( SCI \)-models are Boolean algebras (cf. Theorem 2.16 and the remark in the last paragraph of Sect. 2.)

We remark here that a similar type of equivalences between propositional logics with an identity connective and normal modal systems is established by Ishii (1998). His propositional calculus \( PCI \) is also defined in the language of \( SCI \) though the axioms (and rules) for the identity connective differ in some aspects from \( SCI \). Ishii shows equivalence between \( PCI \) and normal system \( K \), as well as a series of further equavalences between extensions of \( PCI \) and corresponding normal modal systems.

There are several notions of equivalence between logical systems introduced in the literature and there seems to be no standard definition of such a concept. However, these notions usually have the following in common: given two logics, there are two mappings (translations) between the respective languages which are, in a precise sense, inverse to each other and preserve the relation of derivability (or logical consequence). A typical example of such a notion of equivalence between deductive systems, defined in the context of abstract algebraic logics, can be found in Blok and Pigozzi (2001, Definition 4.1). We consider in the following a similar notion which, however, is restricted to two specific translations and is stronger in the sense that it involves propositional identity instead of interderivability and thus respects also contexts which are not only extensional but (hyper-) intensional. First, we define two specific translations: \( box \) from \(Fm_\equiv \) to \(Fm_\square \), and \( id \) from \(Fm_\square \) to \(Fm_\equiv \). Then we show that under certain assumptions these translations are inverse to each other (Theorem 4.2). This corresponds to the interderivability condition of Blok and Pigozzi (2001, Definition 4.1). Though, our condition is stronger since it is based on propositional identity instead of interderivability. In this context, we shall say that an axiomatic extension of \( SCI \) and a Lewis-style modal system are equivalent if the translations \( box \) and \( id \), which are inverse to each other, also preserve derivations (Definition 4.3). So equivalence in our specific sense then also implies the corresponding criteria of the usual notion of equivalence between deductive systems such as given in Blok and Pigozzi (2001, Definition 4.1).

Definition 4.1

The translation \( box :Fm_\equiv \rightarrow Fm_\square \) is inductively defined as follows:

$$\begin{aligned} \begin{aligned}&box (x):=x\\&\quad box (\bot ):=\bot \\&\quad box (\top ):=\top \\&\quad box (\lnot \varphi ):=\lnot box (\varphi )\\&\quad box (\varphi *\psi ):= ( box (\varphi )* box (\psi )),\text { for }*\in \{\wedge ,\vee ,\rightarrow \}\\&\quad box (\varphi \equiv \psi ):= \square ( box (\varphi )\leftrightarrow box (\psi )). \end{aligned} \end{aligned}$$

On the other hand, the translation \( id :Fm_\square \rightarrow Fm_\equiv \) is inductively defined as follows:

$$\begin{aligned} \begin{aligned}&id (x):=x\\&\quad id (\bot ):=\bot \\&\quad id (\top ):=\top \\&\quad id (\lnot \varphi ):=\lnot id (\varphi )\\&\quad id (\varphi *\psi ):= ( id (\varphi )* id (\psi )),\text { for }*\in \{\wedge ,\vee ,\rightarrow \}\\&\quad id (\square \varphi ):= (id(\varphi )\equiv \top ). \end{aligned} \end{aligned}$$

For \(\varPhi \subseteq Fm_\equiv \), we let \( box (\varPhi ):=\{ box (\psi )\mid \psi \in \varPhi \}\); and for \(\varPhi \subseteq Fm_\Box \), we let \( id (\varPhi )=\{id(\psi )\mid \psi \in \varPhi \}\).

Induction on formulas ensures that \( box (\varphi )\in Fm_\square \) for any \(\varphi \in Fm_\equiv \); and \( id (\varphi )\in Fm_\equiv \) for any \(\varphi \in Fm_\square \). If the underlying logics are strong enough, then the translations \( box \) and \( id \) are inverse to each other in the sense of the next result. Recall that we are working with the following abbreviations: In the language of modal logic \(Fm_\square \), we put \((\varphi \equiv \psi ):= \square (\varphi \leftrightarrow \psi )\) (cf. (3) at the beginning of Sect. 3), and in the language \({\mathcal {L}}_\equiv \) of \( SCI \), we put \(\square \varphi := (\varphi \equiv \top )\) (cf. (2) before Theorem 2.16).

Theorem 4.2

  • Let \({\mathcal {L}}\) be a modal logic in the language \(Fm_\square \) containing \( S1SP \). Then for any \(\varphi \in Fm_\square \)Footnote 10

    $$\begin{aligned} \vdash _{\mathcal {L}}\varphi \equiv box ( id (\varphi )). \end{aligned}$$
  • Let \({\mathcal {L}}_\equiv \) be an axiomatic extension of \( SCI \) in the language \(Fm_\equiv \) containing theorems of the form

    $$\begin{aligned} (\chi \equiv \psi )\equiv \square (\chi \leftrightarrow \psi ), \text {i.e. }(\chi \equiv \psi )\equiv ((\chi \leftrightarrow \psi )\equiv \top ). \end{aligned}$$

    Then for any \(\varphi \in Fm_\equiv \)Footnote 11

    $$\begin{aligned} \vdash _{{\mathcal {L}}_\equiv }\varphi \equiv id ( box (\varphi )). \end{aligned}$$

Proof

Under the assumptions of the first item, we show the assertion by induction on \(\varphi \in Fm_\square \). If \(\varphi \) is an atomic formula, we get \( box ( id (\varphi ))=\varphi \). Then the assertion holds because \(\square (\varphi \leftrightarrow \varphi )\) is a theorem of \({\mathcal {L}}\) (apply the rule AN to \(\varphi \leftrightarrow \varphi \)). Now suppose \(\varphi = \square \psi \) for some \(\psi \in Fm_\square \).

$$\begin{aligned} \begin{aligned} box ( id (\varphi ))&= box ( id (\square \psi ))\\&= box ( id (\psi )\equiv \top ),\text { by definition of } id \\&=\square ( box ( id (\psi )\leftrightarrow \top )),\text { by definition of } box \\&\equiv _{\mathcal {L}}\square (\psi \leftrightarrow \top ),\text { by induction hypothesis and SP}\\&=(\psi \equiv \top )\\&\equiv _{\mathcal {L}}\square \psi ,\text { recall that }\square \psi \equiv (\psi \equiv \top )\text { is a theorem of } S1SP \\&=\varphi \end{aligned} \end{aligned}$$

Hence, \(\varphi \equiv _{\mathcal {L}} box ( id (\varphi ))\), i.e. \(\vdash _{\mathcal {L}}\varphi \equiv box ( id (\varphi ))\). The remaining cases of the induction step follow straightforwardly. Now, we assume the hypotheses of the second item and show its assertion by induction on \(\varphi \in Fm_\equiv \). The induction base is clear; and in the induction step, only the case \(\varphi =(\psi \equiv \chi )\) requires some attention:

$$\begin{aligned} \begin{aligned} id ( box (\varphi ))&= id ( box (\psi \equiv \chi ))\\&= id (\square ( box (\psi )\leftrightarrow box (\chi ))),\text { by definition of } box \\&=( id ( box (\psi ))\leftrightarrow id ( box (\chi )))\equiv \top ,\text { by definition of } id \\&\equiv _{{\mathcal {L}}_\equiv } ( id ( box (\psi ))\equiv id ( box (\chi ))), \text { by assumptions on }{\mathcal {L}}_\equiv \\&\equiv _{{\mathcal {L}}_\equiv } (\psi \equiv \chi ),\text { by induction hypothesis and SP}\\&=\varphi \end{aligned} \end{aligned}$$

\(\square \)

If \({\mathcal {L}}\) is a modal logic and \({\mathcal {L}}_\equiv \) is an \( SCI \)-extension satisfying the hypotheses required in Theorem 4.2, then we are able to establish a condition (actually, two equivalent conditions) under which both logics have, in a precise sense, the same expressive power and are called equivalent:

Definition 4.3

Let \({\mathcal {L}}\) be a modal logic in the language \(Fm_\square \) containing \( S1SP \). Let \({\mathcal {L}}_\equiv \) be an extension of \( SCI \) in the language \(Fm_\equiv \) containing theorems of the form

$$\begin{aligned} (\chi \equiv \psi )\equiv \square (\chi \leftrightarrow \psi ). \end{aligned}$$

Furthermore, suppose one of the following two conditions is true:

  1. (i)

    For any \(\varPhi \cup \{\varphi \}\subseteq Fm_\equiv \): \(\varPhi \vdash _{\mathcal {L_\equiv }}\varphi \Longleftrightarrow box (\varPhi )\vdash _{{\mathcal {L}}} box (\varphi )\).

  2. (ii)

    For any \(\varPhi \cup \{\varphi \}\subseteq Fm_\square \): \(\varPhi \vdash _{{\mathcal {L}}}\varphi \Longleftrightarrow id (\varPhi )\vdash _{\mathcal {L_\equiv }} id (\varphi )\).

Then we say that the modal logic \({\mathcal {L}}\) and the \( SCI \)-extension \({\mathcal {L}}_\equiv \) are equivalent.

The next result justifies that in Defnition 4.3 it is enough to require only one of the conditions (i), (ii).

Lemma 4.4

Let \({\mathcal {L}}\) be a modal logic and let \({\mathcal {L}}_\equiv \) be an \( SCI \)-extension which is equivalent to \({\mathcal {L}}\) in the sense of Definition 4.3. Then both conditions (i) and (ii) of Definition 4.3 are satisfied.

Proof

Let \({\mathcal {L}}_\equiv \) be the \( SCI \)-extension equivalent to modal system \({\mathcal {L}}\) and suppose that fact is witnessed by condition (i) of Definition 4.3. We show that condition (ii) follows. Let \(\varPhi \cup \{\varphi \}\subseteq Fm_\square \) and suppose \(\varPhi \vdash _{\mathcal {L}}\varphi \). There are \(\varphi _1,\ldots ,\varphi _n\in \varPhi \) such that the following hold:

\(\vdash _{\mathcal {L}} (\varphi _1\wedge \cdots \wedge \varphi _n)\rightarrow \varphi \)

\(\vdash _{\mathcal {L}} box ( id ((\varphi _1\wedge \cdots \wedge \varphi _n)\rightarrow \varphi ))\), by Theorem 4.2

\(\vdash _{{\mathcal {L}}_\equiv } id ((\varphi _1\wedge \cdots \wedge \varphi _n)\rightarrow \varphi )\), by condition (i).

By definition of \( id \), we may conclude \( id (\varPhi )\vdash _{{\mathcal {L}}_\equiv } id (\varphi )\).

The implication from right-to-left of (ii) follows similarly. Analogously, one establishes condition (i) under the assumption that condition (ii) holds true. \(\square \)

Lemma 4.5

Let \({\mathcal {L}}\) be a modal logic and let \({\mathcal {L}}_\equiv \) be an \( SCI \)-extension equivalent to \({\mathcal {L}}\). Then the following hold:

  • For any \(\varphi \in Fm_\equiv \): \(\vdash _{\mathcal {L}} box (\square \varphi )\equiv \square box (\varphi )\), i.e. \( box (\square \varphi )\equiv _{{\mathcal {L}}}\square box (\varphi )\).

  • For any \(\varphi ,\psi \in Fm_\square \): \(\vdash _{{\mathcal {L}}_\equiv } id (\varphi \equiv \psi )\equiv ( id (\varphi )\equiv id (\psi ))\), which we also write as \( id (\varphi \equiv \psi )\equiv _{{\mathcal {L}}_\equiv } ( id (\varphi )\equiv id (\psi ))\).

Proof

Under the given assumptions, we have:

\( box (\square \varphi )= box (\varphi \equiv \top )=\square ( box (\varphi )\leftrightarrow \top )=( box (\varphi )\equiv \top )\equiv _{\mathcal {L}}\square box (\varphi )\). The last equation holds because \(\square \psi \equiv (\psi \equiv \top )\) is a theorem of \( S1SP \) and thus of \({\mathcal {L}}\).

On the other hand:

\( id (\varphi \equiv \psi )= id (\square (\varphi \leftrightarrow \psi ))=( id (\varphi )\leftrightarrow id (\psi ))\equiv \top )\equiv _{{\mathcal {L}}_\equiv } ( id (\varphi )\equiv id (\psi ))\).

The last equation holds because \((\chi \equiv \xi )\equiv ((\chi \leftrightarrow \xi )\equiv \top )\) is a theorem of \({\mathcal {L}}_\equiv \). \(\square \)

As expected, particular examples of Definition 4.3 are axiomatic extensions of \( SCI \) equivalent to the modal systems \( S1SP \), \( S3 \), \( S4 \) and \( S5 \), respectively, which we are going to define in the following.

Recall that the modal operator is defined as \(\square \varphi := (\varphi \equiv \top )\).

Definition 4.6

We consider the language \(Fm_\equiv \) of \( SCI \) and define deductive systems on the base of the following axiom schemes (CPC) + (1)–(5):

(CPC) any formula \(\varphi \) having the form of a classical tautology

  1. (1)

    \((\chi \equiv \psi )\leftrightarrow \square (\chi \leftrightarrow \psi )\)

  2. (2)

    \(\square \varphi \rightarrow \varphi \)

  3. (3’)

    \((\square (\varphi \rightarrow \psi )\wedge \square (\psi \rightarrow \chi ))\rightarrow \square (\varphi \rightarrow \chi )\)

  4. (3)

    \(\square (\varphi \rightarrow \psi )\rightarrow \square (\square \varphi \rightarrow \square \psi )\)

  5. (4)

    \(\square \varphi \rightarrow \square \square \varphi \)

  6. (5)

    \(\lnot \square \varphi \rightarrow \square \lnot \square \varphi \).

Then logic \( S1SP _\equiv \) is axiomatized by the axiom schemes (CPC), (1), (2), (3’) together with the scheme of theorems SP \((\varphi \equiv \psi )\rightarrow (\chi [x:=\varphi ]\equiv \chi [x:=\psi ])\). That is, \( S1SP _\equiv \) is given by the following deductive system. For \(\varPhi \cup \{\varphi \}\subseteq Fm_\equiv \), we write \(\varPhi \vdash _{ S1SP _\equiv }\varphi \) if there is a corresponding derivation, i.e. a sequence \(\varphi _1,\ldots ,\varphi _n=\varphi \), such that for every \(\varphi _i\), \(1\le i\le n\): \(\varphi _i\in \varPhi \) or \(\varphi _i\) is an instance of (CPC), (1)–(3’) or SP or \(\varphi _i\) is obtained by rule MP or \(\varphi _i\) is obtained by rule AN (i.e. there is some axiom \(\varphi _j\), \(1\le j<i\), given as an instance of (CPC) + (1)–(3’), such that \(\varphi _i=\square \varphi _j\)).

The deductive system \( S3 _\equiv \) is defined analogously but with axiom schemes (CPC), (1), (2), (3) (and without theorem scheme SP). Similarly, logic \( S4 _\equiv \) is given by the axioms (CPC) and (1)–(4). If additionally we consider axiom scheme (5), then we obtain system \( S5 _\equiv \) (of course, rule AN only applies to the given axioms of the respective underlying system).

Lemma 4.7

\((\chi \equiv \psi )\equiv \square (\chi \leftrightarrow \psi )\) is a theorem of \( S1SP _\equiv \).

Proof

We obtain the following sequence of theorems:

\(\square ((\chi \equiv \psi )\leftrightarrow \square (\chi \leftrightarrow \psi ))\) results from AN applied to (1).

\(((\chi \equiv \psi )\equiv \square (\chi \leftrightarrow \psi ))\leftrightarrow \square ((\chi \equiv \psi )\leftrightarrow \square (\chi \leftrightarrow \psi ))\) is an instance of (1).

Modus Ponens yields \((\chi \equiv \psi )\equiv \square (\chi \leftrightarrow \psi )\). \(\square \)

Theorem 4.8

\( SCI \subseteq SCI^+ \subseteq S1SP _\equiv \subseteq S3 _\equiv \subseteq S4 _\equiv \subseteq S5 _\equiv \).

Proof

The first inclusion is trivial by the definitions (cf. Definition 2.17).

Claim 1: \( SCI ^+\subseteq S1SP _\equiv \).

It is enough to show \( SCI \subseteq S1SP _\equiv \) since the additional axioms of \( SCI ^+\) are already contained in \( S1SP \) by definition. Recall that SP is equivalent to the identity axioms (id3)–(id7) (modulo the rest of \( SCI \)). So we only need to show that

  1. (id1)

    \(\varphi \equiv \varphi \) and

  2. (id2)

    \((\varphi \equiv \psi )\rightarrow (\varphi \rightarrow \psi )\) are theorems of \( S1SP _\equiv \).

  3. (id1)

    derives considering axiom \(\varphi \leftrightarrow \varphi \), rule AN and scheme (1). (id2) derives from (1)+(2). Thus Claim 1 is true.

Claim 2: \(\square (\varphi \wedge \psi )\leftrightarrow (\square \varphi \wedge \square \psi )\) is a theorem of \( S3 _\equiv \).

We may derive that theorem exactly as in normal modal system K using only classical propositional calculus, rule AN and modal principle K of distribution which, by schemes (3) and (2), is contained in \( S1SP _\equiv \) (with \(\square \varphi \) defined as \(\varphi \equiv \top \)). Such a derivation can be found, e.g., in Hughes and Cresswell (1996).

Claim 3: \( S1SP _\equiv \subseteq S3 _\equiv \).

It is enough to show that scheme (3) is stronger than (3’), and that scheme SP is derivable in \( S3 _\equiv \).

\((\varphi \rightarrow \psi )\rightarrow ((\psi \rightarrow \chi )\rightarrow (\varphi \rightarrow \chi ))\) is an axiom.

\(\square (\varphi \rightarrow \psi )\rightarrow (\square (\psi \rightarrow \chi )\rightarrow \square (\varphi \rightarrow \chi ))\) is obtained by applying rule AN, (3), (2) and Modus Ponens. Modulo \( CPC \), that is equivalent to (3’). Thus, (3) is stronger than (3’) (modulo the rest). Finally, in order to show that principle SP is derivable, we derive the identity axioms (id3)–(id7) of \( SCI \) which are equivalent to SP modulo the rest:

\((\varphi \leftrightarrow \psi )\rightarrow (\lnot \varphi \leftrightarrow \lnot \psi )\) is an axiom.

\(\square (\varphi \leftrightarrow \psi )\rightarrow \square (\lnot \varphi \leftrightarrow \lnot \psi )\) results from applications of AN, (3), (2) and MP.

\((\varphi \equiv \psi )\rightarrow (\lnot \varphi \equiv \lnot \psi )\), i.e. (id3), follows by scheme (1) and transitivity of implication.

\((\varphi \leftrightarrow \psi )\rightarrow ((\varphi '\leftrightarrow \psi ')\rightarrow ((\varphi \vee \varphi ')\leftrightarrow (\psi \vee \psi ')))\) is an axiom.

\(\square (\varphi \leftrightarrow \psi )\rightarrow (\square (\varphi '\leftrightarrow \psi ')\rightarrow \square ((\varphi \vee \varphi ')\leftrightarrow (\psi \vee \psi ')))\), by AN and appropriate axioms.

\((\varphi \equiv \psi )\rightarrow ((\varphi '\equiv \psi ')\rightarrow ((\varphi \vee \varphi ')\equiv (\psi \vee \psi ')))\) results from replacing formulas of the form \(\square (\chi _1\leftrightarrow \chi _2)\) by \(\chi _1\equiv \chi _2\), according to (1).

\(((\varphi \equiv \psi )\wedge (\varphi '\equiv \psi '))\rightarrow ((\varphi \vee \varphi ')\equiv (\psi \vee \psi '))\), i.e. (id4), follows by propositional calculus. Similarly, we derive (id5) and (id6). Finally, let us derive (id7).

\((\varphi \leftrightarrow \psi )\rightarrow ((\varphi '\leftrightarrow \psi ')\rightarrow ((\varphi \leftrightarrow \varphi ')\leftrightarrow (\psi \leftrightarrow \psi ')))\) is an axiom.

(*) \(\square (\varphi \leftrightarrow \psi )\rightarrow (\square (\varphi '\leftrightarrow \psi ')\rightarrow \square ((\varphi \leftrightarrow \varphi ')\leftrightarrow (\psi \leftrightarrow \psi ')))\), by AN and appropriate axioms.

\(\square ((\varphi \leftrightarrow \varphi ')\rightarrow (\psi \leftrightarrow \psi '))\rightarrow \square (\square (\varphi \leftrightarrow \varphi ')\rightarrow \square (\psi \leftrightarrow \psi '))\), instance of (3).

\(\square ((\psi \leftrightarrow \psi ')\rightarrow (\varphi \leftrightarrow \varphi '))\rightarrow \square (\square (\psi \leftrightarrow \psi ')\rightarrow \square (\varphi \leftrightarrow \varphi '))\), instance of (3).

\(\square ((\varphi \leftrightarrow \varphi ')\leftrightarrow (\psi \leftrightarrow \psi '))\rightarrow \square (\square (\varphi \leftrightarrow \varphi ')\leftrightarrow \square (\psi \leftrightarrow \psi '))\), apply Claim 2 to the last two theorems.

\(\square (\varphi \leftrightarrow \psi )\rightarrow (\square (\varphi '\leftrightarrow \psi ')\rightarrow \square (\square (\varphi \leftrightarrow \varphi ')\leftrightarrow \square (\psi \leftrightarrow \psi ')))\), by (*) and transitivity of implication.

Now, in the same way as before, we apply (1) and corresponding replacements to derive

(**) \((\varphi \equiv \psi )\rightarrow ((\varphi '\equiv \psi ')\rightarrow (\square (\varphi \leftrightarrow \varphi ')\equiv \square (\psi \leftrightarrow \psi ')))\). Note that the proof of Lemma 4.7 also works in \( S3 _\equiv \). By schemes (3’) and (1), the connective \(\equiv \) is transitive in \( S3 _\equiv \). Putting these observations together and considering the equations

\((\varphi \equiv \varphi ')\equiv \square (\varphi \leftrightarrow \varphi ')\equiv \square (\psi \leftrightarrow \psi ')\equiv (\psi \equiv \psi ')\)’,

we are able to derive

\((\square (\varphi \leftrightarrow \varphi ')\equiv \square (\psi \leftrightarrow \psi '))\rightarrow ((\varphi \equiv \varphi ')\equiv (\psi \equiv \psi '))\). This together with (**) and transitivity of implication yields

\((\varphi \equiv \psi )\rightarrow ((\varphi '\equiv \psi ')\rightarrow ((\varphi \equiv \varphi ')\equiv (\psi \equiv \psi ')))\) which is equivalent to (id7). Thus, Claim 3 is true. Finally, the inclusions \( S3 _\equiv \subseteq S4 _\equiv \subseteq S5 _\equiv \) are clear by Definition 4.6. \(\square \)

We are now able to establish the intended equivalences between some of our \( SCI \)-extensions and corresponding modal systems.

Theorem 4.9

The logics \( S1SP _\equiv \), \( S3 _\equiv \), \( S4 _\equiv \) and \( S5 _\equiv \) introduced in Definition 4.6 are \( SCI \)-extensions which are equivalent to the modal logics \( S1SP \), \( S3 \), \( S4 \) and \( S5 \), respectively.

Proof

We prove the equivalence between \( S3 \) and \( S3 _\equiv \). The remaining equivalences are shown in a similar way. First, let us check that the logics \({\mathcal {L}}:= S3 \) and \({\mathcal {L}}_\equiv := S3 _\equiv \) satisfy the conditions of Definition 4.3. On the one hand, we know that \( S3 \) is the weakest Lewis modal system containing principle SP (cf. Lewitzka (2015, 2016)) and thus contains \( S1SP \). On the other hand, by Theorem 4.8 and Lemma 4.7, we know that \({\mathcal {L}}_\equiv = S3 _\equiv \) contains \( SCI \) and theorems \((\chi \equiv \psi )\equiv \square (\chi \leftrightarrow \psi )\). It remains to check one of the equivalent conditions (i) or (ii) of Definition 4.3. We show that (i) holds. So let \(\varPhi \cup \{\varphi \}\subseteq Fm_\equiv \) and suppose \(\varPhi \vdash _{ S3 _\equiv }\varphi \). We show \( box (\varPhi )\vdash _{ S3 } box (\varphi )\) by induction on the length \(n\ge 1\) of derivations of \(\varphi \) from \(\varPhi \) in \( S3 _\equiv \). If \(n=1\), then we distinguish the following cases (a)–(e).

  1. (a)

    \(\varphi \in \varPhi \). Then trivially \( box (\varphi )\in box (\varPhi )\) and thus \( box (\varPhi )\vdash _{ S3 } box (\varphi )\).

  2. (b)

    \(\varphi \) has the form of a classical tautology. Since translation \( box \) preserves logical connectives, it follows that \( box (\varphi )\) is of the same form, i.e. has the form of a classical tautology, too, and as such is an axiom of \( S3 \).

  3. (c)

    \(\varphi \) is an instance of scheme (1), say \(\varphi = (\chi \equiv \psi )\leftrightarrow ((\chi \leftrightarrow \psi )\equiv \top )\). By definition of \( box \):

    $$\begin{aligned} box (\varphi )=\square ( box (\chi )\leftrightarrow box (\psi ))\leftrightarrow \square (( box (\chi )\leftrightarrow box (\psi ))\leftrightarrow \top ). \end{aligned}$$

    Considering the definition of the identity connective \((\varphi _1\equiv \varphi _2):=\square (\varphi _1\leftrightarrow \varphi _2)\) in \( S3 \), this yields

    $$\begin{aligned} box (\varphi )=( box (\chi )\equiv box (\psi ))\leftrightarrow (( box (\chi )\leftrightarrow box (\psi ))\equiv \top ). \end{aligned}$$

    By Lemma 3.4, \(\square ( box (\chi )\leftrightarrow box (\psi )) \equiv (( box (\chi )\leftrightarrow box (\psi ))\equiv \top )\) is a theorem of \( S3 \). Applying SP, we get

    $$\begin{aligned} \begin{aligned} box (\varphi )&\equiv _{ S3 }(( box (\chi )\equiv box (\psi ))\leftrightarrow \square ( box (\chi )\leftrightarrow box (\psi )))\\&=( box (\chi )\equiv box (\psi ))\leftrightarrow ( box (\chi )\equiv box (\psi )). \end{aligned} \end{aligned}$$

    Of course, any such trivial biconditional is a theorem of \( S3 \) and so is \( box (\varphi )\).

  4. (d)

    \(\varphi \) is an instance of scheme (2), say \(\varphi = (\square \psi \rightarrow \psi )\). By Lemma 4.5,

    $$\begin{aligned} box (\varphi )\equiv _{ S3 }\square box (\psi )\rightarrow box (\psi ). \end{aligned}$$

    The formula of the right hand side of that equation is an axiom of \( S3 \).

  5. (e)

    \(\varphi \) is an instance of scheme (3), say \(\varphi = \square (\psi \rightarrow \chi )\rightarrow \square (\square \psi \rightarrow \square \chi )\). As in (d), we apply Lemma 4.5 and get

    $$\begin{aligned} box (\varphi )\equiv _{ S3 }\square ( box (\psi )\rightarrow box (\chi ))\rightarrow \square (\square box (\psi )\rightarrow \square box (\chi )), \end{aligned}$$

which again results in an axiom of \( S3 \).Footnote 12

Examining the cases (b)–(e) above, we conclude in particular the following

Fact: For any axiom \(\chi \) of \( S3 _\equiv \), we have \( box (\chi )\equiv _ S3 \chi '\), where \(\chi '\) is an axiom of modal system \( S3 \).

Now, suppose \(\varphi \) is derived in \(n+1\) steps and the assertion is true for all derivations of length \(\le n\). We may assume that \(\varphi \) is obtained by an application of the rules MP or AN. In the former case, there are \(\psi \) and \(\psi \rightarrow \varphi \) derived in \(\le n\) steps, and the induction hypothesis yields \( box (\varPhi )\vdash _{ S3 } box (\varphi )\). In the latter case, \(\varphi =\square \chi \) for some axiom \(\chi \) of \( S3 _\equiv \) that occurs in the given derivation. By Lemma 4.5 and the Fact above, \( box (\varphi )\equiv _ S3 \square box (\chi )\) and \( box (\chi )\equiv _ S3 \chi '\), where \(\chi '\) is an axiom of modal system \( S3 \). Since SP holds in \( S3 \), we may replace \( box (\chi )\) by \(\chi '\) in every context. Then we get \( box (\varphi )\equiv _ S3 \square \chi '\). Since \(\chi '\) is an axiom of \( S3 \), formula \(\square \chi '\) is a theorem of \( S3 \) by the rule of Axiom Necessitation. Hence, \( box (\varphi )\) is a theorem of \( S3 \). We have finished the induction and thus the proof of the Theorem. \(\square \)

We have established equivalences between some particular \( SCI \)-extensions and corresponding Lewis-style modal logics by means of the respective deductive systems. How can these equivalences be described semantically? One easily recognizes that a given \( S1SP \)-model can be transformed into an \( SCI \)-model defining \((a\equiv b):=\square (a\leftrightarrow b)\). This corresponds to theorem \((\varphi \equiv \psi )\equiv \square (\varphi \leftrightarrow \psi )\) of \( S1SP \). The resulting \( SCI \)-model then will be a model of \( S1SP _\equiv \). The other way round, any given \( SCI \)-model which is a model of \( S1SP _\equiv \) can be transformed into an \( S1SP \)-model defining \(\square a:= (a\equiv \top )\). This corresponds to theorem \(\square \varphi \equiv (\varphi \equiv \top )\) of modal system \( S1SP \). We conclude that the \( SCI \)-extension \( S1SP _\equiv \) is sound and complete w.r.t. the class of exactly those \( SCI \)-models which can be obtained from \( S1SP \)-models by the above presented transformation. So from a semantic point of view, the equivalence between \( SCI \)-extension \( S1SP _\equiv \) and modal system \( S1SP \) is given by those respective classes of models (and the transformations in both directions). Analogously, we can describe the remaining equivalences semantically. Detailed proofs derive straightforwardly from the above results.

Our view on intensionality as a measure for the discernibility of propositions (‘the more propositions can be distinguished in models of the underlying logic the higher degree of intensionality’) is presented here in a rather informal and intuitive way. An interesting task for future work would be to give a precise formalization of that concept. The general framework of equivalences between \( SCI \)-extensions and certain modal logics established in this paper generalizes and extends earlier results (e.g. Bloom & Suszko, 1972; Lewitzka, 2016). There are further approaches to equivalences between modal systems and propositional logics with identity connective found in the literature (cf. Ishii, 1998) where, however, the axioms of the identity connective differ from those of logic \( SCI \). The question arises which further (hyper-) intensional logics can be modeled by appropriate \( SCI \)-extensions or similar logics with identity connective. Can any (hyper-) intensional logic be captured by an appropriate axiomatization of propositional identity? These and related questions remain to be further investigated.