The Modal Logic of Aristotelian Diagrams — TEI-tagged view

Stef FrijterspersName, Lorenz DemeypersName (2023date). “The Modal Logic of Aristotelian Diagrams.” Axiomstitle·j.

Object of study — Aristotelian diagramsterm - squares and hexagons of opposition - and the logical relations of opposition holding among their formulas

Research question — whether a modal language can describe Aristotelian diagramsterm themselves, reversing the usual direction in which Aristotelian diagramsterm are used to visualise modal logic

Contribution — AD-logicterm, a hybrid modal logic interpreted on 'AD-framesterm', with a sound and strongly complete axiomatizationterm, a bijection between finite Aristotelian diagramsterm and finite AD-framesterm, and modal formulas that generically characterise Aristotelian familiesterm

Full text — tagged

The reference list is not part of the text we hold for this paper. Our copy was extracted from the publisher's page and the bibliography did not survive that extraction, so the article below ends before its references. Nothing has been removed by us.

The Modal Logic of Aristotelian Diagramsterm Abstract Abstract In this paper, we introduce and study AD-logicterm, i.e., a system of (hybrid) modal logic that can be used to reason about Aristotelian diagramsterm. The language of AD-logicterm, 𝐿 AD , is interpreted on a kind of birelational Kripke framesterm, which we call “AD-framesterm”. We establish a sound and strongly complete axiomatizationterm for AD-logicterm, and prove that there exists a bijection between finite Aristotelian diagramsterm (up to Aristotelian isomorphismterm) and finite AD-framesterm (up to modal isomorphism). We then show how AD-logicterm can express several major insights about Aristotelian diagramsterm; for example, for every well-known Aristotelian family A, we exhibit a formula 𝜒 𝐴 ∈ 𝐿 AD and show that an Aristotelian diagramterm D belongs to the family A iff 𝜒 𝐴 is validated by D (when the latter is viewed as an AD-frameterm). Finally, we show that AD-logicterm itself gives rise to new and interesting Aristotelian diagramsterm, and we reflect on their profoundly peculiar status. Keywords: square of oppositionterm; Aristotelian diagramterm; modal logic; hybrid logicterm; logical geometryterm MSC: 03B45; 03A05; 03G05 1. Introduction The interaction between modal logic and Aristotelian diagramsterm has a rich and well-documented history. The oldest kind of Aristotelian diagramterm is the square of oppositionterm for syllogistics, which dates back to the second century CE [1]. However, from the twelfth century onwards, philosophers started to make use of these diagrams to explicate their theorizing on modalities as well [2,3,4,5]. Furthermore, historical scholarship has shown that Aristotelian diagramsterm for modal logic can be reconstructed from the works of many earlier authors, such as Theophrastus [6,7], Chrysippus [8,9], and Avicenna [10,11]. Today, Aristotelian diagramsterm not only appear in well-known textbooks on modal logic [12,13], but they are also used in applications of modal logic to a variety of philosophical and logical topics, such as paraconsistency [14,15], logic-sensitivity [16,17,18], and theories of truth [19,20]. It should be emphasized that all of these applications manifest a wide diversity of Aristotelian diagramsterm: next to the “ordinary” squares of oppositions, we also find several types of hexagons, octagons, and even more complex diagrams [21].

In all of this work, Aristotelian diagramsterm are used to visualize the logical relations holding among a number of modal statements. In this paper, however, we take a completely different approach, as we will be using a modal language to describe Aristotelian diagramsterm. This boils down to “reversing the directionality” of the interaction between modal logic and Aristotelian diagramsterm. Whereas the aforementioned work was mainly concerned with Aristotelian diagramsterm for modal logic, in this paper, we rather study the modal logic of Aristotelian diagramsterm.

More concretely, we start from the basic observation that Aristotelian diagramsterm are graphs, i.e., relational structures consisting of vertices (viz., formulas) and edges (viz., Aristotelian relationsterm) between them. Consequently, we can view these diagrams as Kripke framesterm, which allows us to interpret, i.e., to provide a relational semantics for, a modal language. (For reasons of expressivity, we will actually interpret a language of hybrid logicterm, rather than one of “basic” modal logic.) We can then express formulas in this modal language that correspond exactly with properties of Aristotelian diagramsterm that we are interested in. For example, we will exhibit a modal formula 𝜒 classical that precisely captures the property of being a classical squareterm of opposition: an Aristotelian diagramterm is a classical squareterm if and only if 𝜒 classical is valid on that diagram (considered as a Kripke frameterm). Similarly, the modal formulas 𝜒 degenerate and 𝜒 square capture the properties of being a degenerate squareterm and being a square of oppositionterm “in general”, respectively. (Precise definitions of classical squaresterm, degenerate squaresterm, and squares in general are provided later in the paper.) We can take this idea of viewing Aristotelian diagramsterm as Kripke framesterm one step further, which gives rise to the modal consequence relationterm ⊨ AD . Many results from logical geometryterm (i.e., the systematic study of Aristotelian diagramsterm) can now be formally expressed as AD-valid arguments. Consider, for example, the well-known fact that every square of oppositionterm is either a classical squareterm or a degenerate squareterm: this is formally captured by the argument 𝜒 square ⊨ AD 𝜒 classical ∨ 𝜒 degenerate . (It should be noted that this approach was partially inspired by the work of Grossi [22,23]: he proposed to view argumentation frameworks as Kripke framesterm, which then allowed him to study abstract argumentation theory using modal logic).

There are several complementary reasons for studying the modal logic of Aristotelian diagramsterm from the perspective of logical geometryterm as well as from that of modal logic itself. First of all, it nicely illustrates the expressive power of modal—and in particular, hybrid—languages to describe relational structures. Secondly, even though this is not the main concern of this paper, we will show how a sound and strongly complete axiomatizationterm of ⊨ AD can be obtained almost immediately from general results about hybrid logicterm. Thirdly, based on the intuitive idea of “viewing an Aristotelian diagramterm as a Kripke frameterm”, we formally define the notion of an AD-frameterm. We will prove that this definition completely captures the structural properties of Aristotelian diagramsterm, thus shedding new light on the very nature of these diagrams. Fourthly, and perhaps most importantly, the modal language developed here can be used to formulate generic descriptions of families of Aristotelian diagramsterm. For example, in order to define the family of all classical squaresterm of opposition, we usually refer to an arbitrary logical system (or in more algebraically oriented parts of logical geometryterm, to an arbitrary Boolean algebra). Such a definition is indeed general (because it works for all logical systems), but it is not generic (because it still refers to some logical system—regardless of whether that system was chosen arbitrarily or not). For most purposes, such a general definition is appropriate, but there also exist certain theoretical contexts where we really want to work with generic descriptions of Aristotelian familiesterm (that do not refer to any logical system at all) [24]. Using the modal language developed in this paper, we can define the family of classical squaresterm of opposition as consisting of precisely those diagrams which (when viewed as Kripke framesterm) validate the formula 𝜒 classical . Since this characterization does not refer to any logical system at all, the modal formula 𝜒 classical provides a fully generic description of the family of classical squaresterm of opposition.

The paper is organized as follows. Section 2 provides some basic background information on Aristotelian diagramsterm in order to keep this paper self-contained. Section 3 introduces all the key components of AD-logicterm, including the modal language 𝐿 AD , the AD-framesterm that this language will be interpreted on, and the consequence relationterm ⊨ AD . In Section 4, we prove that there exists a bijection between finite Aristotelian diagramsterm and finite AD-framesterm (up to isomorphism), which shows that AD-framesterm completely capture the structural properties of Aristotelian diagramsterm. Section 5 shows how AD-logicterm allows us to express several key results from logical geometryterm (in particular, characterizations of and relations between various families of Aristotelian diagramsterm). In Section 6, we demonstrate how AD-logicterm can be used to construct interesting new Aristotelian diagramsterm, which simultaneously contain certain formulas (when viewed as Aristotelian diagramsterm) and validate those same formulas (when viewed as AD-framesterm). Finally, Section 7 wraps things up, and mentions some avenues for further research.

2. The Basic Building Blocks of Logical Geometryterm Aristotelian diagramsterm can be defined in several ways [25]. The most general definition is in terms of Boolean algebras, but for the purposes of this paper, it suffices to focus on Aristotelian diagramsterm relative to logical systems. We first introduce the Aristotelian relationsterm in Definition 1 and then move on to the diagrams themselves in Definition 2.

(Aristotelian relationsterm). Let 𝑆 be a logical system, which is assumed to have Boolean operators and a model–theoretic semantics ⊨ 𝑆 . The formulas 𝛼 , 𝛽 ∈ 𝐿 𝑆 are said to be 𝑆 -contradictory iff ⊨ 𝑆 ¬ ( 𝛼 ∧ 𝛽 ) and ⊨ 𝑆 𝛼 ∨ 𝛽 , 𝑆 -contrary iff ⊨ 𝑆 ¬ ( 𝛼 ∧ 𝛽 ) and ⊭ 𝑆 𝛼 ∨ 𝛽 , 𝑆 -subcontrary iff ⊭ 𝑆 ( 𝛼 ∧ 𝛽 ) and ⊨ 𝑆 𝛼 ∨ 𝛽 , in 𝑆 -subalternation iff ⊨ 𝑆 𝛼 → 𝛽 and ⊭ 𝑆 𝛽 → 𝛼 . These relations are abbreviated as CD 𝑆 , 𝐶 𝑆 , SC 𝑆 , and SA 𝑆 .

(Aristotelian diagramterm). Let 𝑆 be a logical system, as shown in Definition 1, and let 𝐹 ⊆ 𝐿 𝑆 be a non-empty fragment of formulas. An Aristotelian diagramterm for ( 𝐹 , 𝑆 ) is a vertex- and edge-labeled graph: its vertices are labeled by the formulas from 𝐹 , while its edges are labeled by the Aristotelian relationsterm holding between those formulas (relative to 𝑆 ). Furthermore, the fragment 𝐹 is required to satisfy the following conditions: 1. for every 𝛼 ∈ 𝐹 , there is a 𝛽 ∈ 𝐹 \ { 𝛼 } such that ⊨ 𝑆 𝛽 ↔ ¬ 𝛼 , 2. for every 𝛼 ∈ 𝐹 , there is no 𝛾 ∈ 𝐹 \ { 𝛼 } such that ⊨ 𝑆 𝛼 ↔ 𝛾 , 3. there is no 𝛿 ∈ 𝐹 such that ⊨ 𝑆 𝛿 or ⊨ 𝑆 ¬ 𝛿 .

Figure 1 shows two basic examples of Aristotelian diagramsterm, viz., classical squaresterm of opposition for ( { 𝑝 ∧ 𝑞 , 𝑝 ∨ 𝑞 , ¬ 𝑝 ∧ ¬ 𝑞 , ¬ 𝑝 ∨ ¬ 𝑞 } , CPL ) and for ( { □ 𝑝 , ⋄ 𝑝 , □ ¬ 𝑝 , ⋄ ¬ 𝑝 } , KD ) , where CPL is the system of classical propositional logic, and KD is the system of modal logic that is interpreted on Kripke framesterm with a serial accessibility relation [13].

Definition 2’s three conditions on 𝐹 are motivated by various theoretical and cognitive considerations [26]. The vast majority of diagrams that are found in the extant literature indeed satisfy these conditions. In recent theoretical work on Aristotelian diagramsterm [27], these conditions are sometimes dropped. However, for the purposes of this paper, we stick to the more traditional approach, and do include these conditions in our definition. Finally, note that because of conditions 1 and 2, we can always write the elements of a finite Aristotelian diagramterm for ( 𝐹 , 𝑆 ) (up to 𝑆 -equivalence) as 𝐹 = { 𝛼 1 , ¬ 𝛼 1 , 𝛼 2 , ¬ 𝛼 2 , … , 𝛼 𝑛 , ¬ 𝛼 𝑛 } , which shows that | 𝐹 | = 2 𝑛 is an even number.

The notion of Aristotelian isomorphismterm, which was first introduced in [24,28], is of crucial importance in logical geometryterm, because it allows us to start studying Aristotelian diagramsterm as objects of independent interest. More concretely, Aristotelian isomorphismsterm enable us to make abstraction of the specific formulas and logical system that define a given Aristotelian diagramterm, and thus, to say that two diagrams are “essentially the same”, despite being built from completely different fragments and logical systems.

(Aristotelian isomorphismterm). Consider Aristotelian diagramsterm D for ( 𝐹 , 𝑆 ) and 𝐷 ′ for ( 𝐹 ′ , 𝑆 ′ ) . An Aristotelian isomorphismterm from D to 𝐷 ′ is a bijection 𝑓 : 𝐹 → 𝐹 ′ such that, for all 𝛼 , 𝛽 ∈ 𝐹 and all Aristotelian relationsterm 𝑅 𝑆 ∈ { CD 𝑆 , 𝐶 𝑆 , SC 𝑆 , SA 𝑆 } , it holds that 𝑅 𝑆 ( 𝛼 , 𝛽 ) iff 𝑅 𝑆 ′ ( 𝑓 ( 𝛼 ) , 𝑓 ( 𝛽 ) ) .

Upon visual inspection, it is immediately clear that function f, defined by 𝑓 ( 𝑝 ∧ 𝑞 ) : = □ 𝑝 , 𝑓 ( 𝑝 ∨ 𝑞 ) : = ⋄ 𝑝 , 𝑓 ( ¬ 𝑝 ∧ ¬ 𝑞 ) : = □ ¬ 𝑝 and 𝑓 ( ¬ 𝑝 ∨ ¬ 𝑞 ) : = ⋄ ¬ 𝑝 , is an Aristotelian isomorphismterm between the two Aristotelian diagramsterm shown in Figure 1. For example, we have SA CPL ( 𝑝 ∧ 𝑞 , 𝑝 ∨ 𝑞 ) and SA KD ( 𝑓 ( 𝑝 ∧ 𝑞 ) , 𝑓 ( 𝑝 ∨ 𝑞 ) ) , i.e., SA KD ( □ 𝑝 , ⋄ 𝑝 ) .

3. AD-Logicterm: The Modal Logic of Aristotelian Diagramsterm In this section, we introduce the modal logic of Aristotelian diagramsterm, or AD-logicterm for short. We first introduce the language 𝐿 AD , and then define its semantics in terms of AD-framesterm. Finally, we provide a sound and strongly complete axiomatizationterm of AD-logicterm.

3.1. The Syntax of AD-Logicterm We begin by defining the language 𝐿 AD of AD-logicterm (Definition 4). This language is highly expressive: next to the “ordinary” modalities [ CD ] and [ 𝐶 ] , we introduce the global modalityterm □ and, especially, some key ingredients from hybrid logicterm: nominalsterm, the @-operator, and the ↓-binder. (Note that although all details are provided below, we do presuppose that the reader has a basic level of familiarity with hybrid logicterm [29,30,31,32].) (Language). Let 𝐼 = { 𝑖 1 , 𝑖 2 , … } be a countably infinite set of nominalsterm and 𝑉 = { 𝑥 1 , 𝑥 2 , 𝑥 3 … } be a countably infinite set of state variables. We use s as a metavariable ranging over 𝐼 ∪ 𝑉 . The language 𝐿 AD is defined by the following BNF: 𝜑 : : = 𝑠 ∣ ¬ 𝜑 ∣ 𝜑 ∨ 𝜑 ∣ [ CD ] 𝜑 ∣ [ 𝐶 ] 𝜑 ∣ □ 𝜑 ∣ @ 𝑠 𝜑 ∣ ↓ 𝑥 ( 𝜑 ) The definitions of free and bound (state) variables are as in first-order logic, with ↓ being the only binding operator.

We now make a number of comments about this language, ranging from technical to more philosophical in nature. We begin by discussing the primitive and defined operators of 𝐿 AD . Given negation and disjunction, the other Boolean connectives are defined as usual. Given the modal operators [ CD ] , [ 𝐶 ] and □, their duals 〈 CD 〉 , 〈 𝐶 〉 and ⋄ are defined as usual. For our purposes later in this paper, it is useful to define two more operators: 〈 SC 〉 𝜑 : = 〈 CD 〉 〈 𝐶 〉 〈 CD 〉 𝜑 and 〈 SA 〉 𝜑 : = 〈 𝐶 〉 〈 CD 〉 𝜑 ; note that these definitions are directly inspired by Lemmas 2 and 3 of [26]. Finally, given the presence of the global modalityterm in 𝐿 AD , the @-operator can actually be defined as @ 𝑠 𝜑 : = □ ( 𝑠 → 𝜑 ) , or alternatively (using an equivalent formula) as @ 𝑠 𝜑 : = ⋄ ( 𝑠 ∧ 𝜑 ) (see [31], p. 284). However, later in this paper, we will point out that we often do not have to rely on the global modalityterm at all, and therefore, we follow the more traditional approach and add @ as a primitive operator to our language.

A somewhat peculiar feature of 𝐿 AD is that it only contains nominalsterm and state variables (which are true in a unique world), and there are no “ordinary” atomic propositions (which are typically true in multiple worlds). Using standard terminology from hybrid logicterm [29,30,31,32], this means that all formulas of 𝐿 AD are, by definition, pure. Technically speaking, there is nothing that prevents us from taking such atomic propositions into account as well. However, since they are not needed for the specific purposes of this paper, and some definitions and results can be formulated more elegantly in their absence, we decided not to add “ordinary” atomic propositions to 𝐿 AD .

In order to avoid a potentially dire confusion, one should keep in mind which purposes the language 𝐿 AD (and, more generally, the system of AD-logicterm) is meant to serve and which ones it is not. More concretely, recall that Aristotelian diagramsterm were defined in Section 2 for pairs ( 𝐹 , 𝑆 ) , and thus exist relative to some “underlying” logical system 𝑆 (for example, CPL or KD ; see Figure 1). Furthermore, formulas from the language 𝐿 𝑆 of this underlying logic occur in the diagram for ( 𝐹 , 𝑆 ). By contrast, AD-logicterm does not serve as such an “underlying” logic of one particular diagram, but is rather meant to describe the behavior of Aristotelian diagramsterm in general. Similarly, formulas from 𝐿 AD do not occur in Aristotelian diagramsterm, but are rather interpreted on them. As a notational reminder of this important distinction, throughout this paper we will systematically use (i) letters from the beginning of the Greek alphabet ( 𝛼 , 𝛽 , 𝛾 , etc.) as metavariables over the language 𝐿 𝑆 of the underlying logic of some Aristotelian diagramterm ( 𝐹 , 𝑆 ) and (ii) letters from the end of the Greek alphabet ( 𝜑 , 𝜒 , 𝜓 , etc.) as metavariables over the language 𝐿 AD of AD-logicterm.

3.2. The Semantics of AD-Logicterm We now introduce the semantics of AD-logicterm. Ultimately, the idea is that 𝐿 AD -formulas can be interpreted on Aristotelian diagramsterm, but for now, we focus on AD-framesterm (Definition 5) and AD-modelsterm (Definition 6), which are a specific kind of birelational Kripke framesterm and models. The connection with actual Aristotelian diagramsterm will be discussed in detail in Section 4.

(AD-frameterm). An AD-frameterm is a tuple 𝐹 = 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 such that 1. W is a non-empty set, the elements of which are called “worlds” or “states”, 2. 𝑅 𝐶 𝐷 ⊆ 𝑊 × 𝑊 is a relation such that (a) for all 𝑤 , 𝑤 ′ ∈ 𝑊 , if 〈 𝑤 , 𝑤 ′ 〉 ∈ 𝑅 𝐶 𝐷 , then 〈 𝑤 ′ , 𝑤 〉 ∈ 𝑅 𝐶 𝐷 , i.e., 𝑅 𝐶 𝐷 is symmetric, (b) for all 𝑤 ∈ 𝑊 , 〈 𝑤 , 𝑤 〉 ∉ 𝑅 𝐶 𝐷 , i.e., 𝑅 𝐶 𝐷 is irreflexive, (c) for all 𝑤 ∈ 𝑊 there is a 𝑤 ′ ∈ 𝑊 such that 〈 𝑤 , 𝑤 ′ 〉 ∈ 𝑅 𝐶 𝐷 , i.e., 𝑅 𝐶 𝐷 is serial, (d) for all 𝑤 , 𝑤 ′ , 𝑤 ′ ′ ∈ 𝑊 , if 〈 𝑤 , 𝑤 ′ 〉 , 〈 𝑤 , 𝑤 ′ ′ 〉 ∈ 𝑅 𝐶 𝐷 , then 𝑤 ′ = 𝑤 ′ ′ , i.e., 𝑅 𝐶 𝐷 is a partial function, 3. 𝑅 𝐶 ⊆ 𝑊 × 𝑊 is a relation such that (a) for all 𝑤 , 𝑤 ′ ∈ 𝑊 , if 〈 𝑤 , 𝑤 ′ 〉 ∈ 𝑅 𝐶 then 〈 𝑤 ′ , 𝑤 〉 ∈ 𝑅 𝐶 , i.e., 𝑅 𝐶 is symmetric, (b) for all 𝑤 ∈ 𝑊 , 〈 𝑤 , 𝑤 〉 ∉ 𝑅 𝐶 , i.e., 𝑅 𝐶 is irreflexive, 4. (a) 𝑅 𝐶 𝐷 ∩ 𝑅 𝐶 = ∅ , i.e., 𝑅 𝐶 𝐷 and 𝑅 𝐶 are mutually exclusive, (b) if 〈 𝑤 , 𝑤 ′ 〉 , 〈 𝑤 ′ ′ , 𝑤 ′ ′ ′ 〉 ∈ 𝑅 𝐶 𝐷 and 〈 𝑤 , 𝑤 ′ ′ 〉 ∈ 𝑅 𝐶 , then 〈 𝑤 , 𝑤 ′ ′ ′ 〉 ∉ 𝑅 𝐶 and 〈 𝑤 ′ , 𝑤 ′ ′ ′ 〉 ∉ 𝑅 𝐶 , (c) if 〈 𝑤 , 𝑤 ′ ′ 〉 , 〈 𝑤 ′ , 𝑤 ′ ′ ′ 〉 ∈ 𝑅 𝐶 and 〈 𝑤 ′ ′ , 𝑤 ′ ′ ′ 〉 ∈ 𝑅 𝐶 𝐷 , then 〈 𝑤 , 𝑤 ′ 〉 ∈ 𝑅 𝐶 .

(AD-modelterm). An AD-modelterm is a tuple 𝑀 = 〈 𝐹 , 𝑉 〉 such that F is an AD-frameterm and 𝑉 : 𝐼 → 𝑊 is a valuation function that maps each nominalterm 𝑠 ∈ 𝐼 onto a state 𝑉 ( 𝑠 ) ∈ 𝑊 .

Conditions 2(c–d) of Definition 5 state that the relation 𝑅 𝐶 𝐷 can be viewed as a total function 𝑅 𝐶 𝐷 : 𝑊 → 𝑊 , so instead of 𝑅 𝐶 𝐷 ( 𝑤 , 𝑤 ′ ) , we can also write 𝑅 𝐶 𝐷 ( 𝑤 ) = 𝑤 ′ . Next, conditions 2(a–b) entail that this function is an involution without any fixed points, i.e., 𝑅 𝐶 𝐷 ( 𝑅 𝐶 𝐷 ( 𝑤 ) ) = 𝑤 ≠ 𝑅 𝐶 𝐷 ( 𝑤 ) for all 𝑤 ∈ 𝑊 . Consequently, we can always list the elements of a finite AD-frameterm as 𝑊 = { 𝑤 1 , 𝑅 𝐶 𝐷 ( 𝑤 1 ) , 𝑤 2 , 𝑅 𝐶 𝐷 ( 𝑤 2 ) , … , 𝑤 𝑛 , 𝑅 𝐶 𝐷 ( 𝑤 𝑛 ) } , which shows that | 𝑊 | = 2 𝑛 is an even number. Needless to say, the fact that finite AD-framesterm have an even number of worlds corresponds exactly to the fact that finite Aristotelian diagramsterm have an even number of formulas (see Section 2). More generally, conditions 2(a)–4(c) are all motivated by the definition of Aristotelian diagramsterm, as will become more clear in Section 4. Finally, with respect to Definition 6, it should be noted that the valuation V only needs to interpret nominalsterm (since there are no “ordinary” atomic propositions in 𝐿 AD ), and hence, we can simply take its codomain to be W. (Otherwise, we would have to take the codomain of V to be ℘ ( 𝑊 ) , while imposing the requirement that | 𝑉 ( 𝑠 ) | = 1 for nominalsterm 𝑠 ∈ 𝐼 , as is usually done in hybrid logicterm [29,30,31]).

We are now in a position to define the semantics of AD-logicterm. We introduce two more auxiliary notions (which are entirely standard from hybrid logicterm) in Definitions 7 and 8, and then formulate the semantic clauses for 𝐿 AD in Definition 9.

(Assignment). An assignment g on an AD-modelterm 𝑀 = 〈 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 , 𝑉 〉 is a function 𝑔 : 𝑉 → 𝑊 that maps each state variable 𝑠 ∈ 𝑉 onto a state 𝑔 ( 𝑠 ) ∈ 𝑊 .

(x-variant). Consider an assignment g on an AD-modelterm 𝑀 = 〈 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 , 𝑉 〉 , a state variable 𝑥 ∈ 𝑉 , and a world 𝑤 ∈ 𝑊 . The x-variant of g that maps x to w, denoted 𝑔 𝑤 𝑥 : 𝑉 → 𝑊 , is the assignment defined by 𝑔 𝑤 𝑥 ( 𝑥 ) = 𝑤 and 𝑔 𝑤 𝑥 ( 𝑠 ) = 𝑔 ( 𝑠 ) for all state variables 𝑠 ∈ 𝑉 \ { 𝑥 } .

(Semantic clauses). Let 𝑀 = 〈 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 , 𝑉 〉 be an AD-modelterm, let g be an assignment on M, and let [ 𝑠 ] 𝑀 , 𝑔 be 𝑉 ( 𝑠 ) if 𝑠 ∈ 𝐼 and 𝑔 ( 𝑠 ) if 𝑠 ∈ 𝑉 . Then we define 𝑀 , 𝑔 , 𝑤 ⊨ 𝑠 iff [ 𝑠 ] 𝑀 , 𝑔 = 𝑤 , 𝑀 , 𝑔 , 𝑤 ⊨ ¬ 𝜑 iff not 𝑀 , 𝑔 , 𝑤 ⊨ 𝜑 , 𝑀 , 𝑔 , 𝑤 ⊨ 𝜑 ∨ 𝜓 iff 𝑀 , 𝑔 , 𝑤 ⊨ 𝜑 or 𝑀 , 𝑔 , 𝑤 ⊨ 𝜓 , 𝑀 , 𝑔 , 𝑤 ⊨ [ CD ] 𝜑 iff for all v such that 〈 𝑤 , 𝑣 〉 ∈ 𝑅 𝐶 𝐷 : 𝑀 , 𝑔 , 𝑣 ⊨ 𝜑 , 𝑀 , 𝑔 , 𝑤 ⊨ [ 𝐶 ] 𝜑 iff for all v such that 〈 𝑤 , 𝑣 〉 ∈ 𝑅 𝐶 : 𝑀 , 𝑔 , 𝑣 ⊨ 𝜑 , 𝑀 , 𝑔 , 𝑤 ⊨ □ 𝜑 iff for all 𝑣 ∈ 𝑊 : 𝑀 , 𝑔 , 𝑣 ⊨ 𝜑 , 𝑀 , 𝑔 , 𝑤 ⊨ @ 𝑠 𝜑 iff 𝑀 , 𝑔 , [ 𝑠 ] 𝑀 , 𝑔 ⊨ 𝜑 , 𝑀 , 𝑔 , 𝑤 ⊨ ↓ 𝑥 ( 𝜑 ) iff 𝑀 , 𝑔 𝑤 𝑥 , 𝑤 ⊨ 𝜑 .

It is now entirely standard to define the notions of AD-frameterm validity (Definition 10), AD-validityterm·def (Definition 11) and AD-consequenceterm·def (Definition 12). Upon unpacking the definitions, it is easy to see that AD-validityterm·def is a special case of AD-consequenceterm·def if we take the premise set to be empty (formally: ⊨ AD 𝜑 iff ∅ ⊨ AD 𝜑 ). Nevertheless, we choose to define these two notions in two separate definitions, because they will be important later in this paper for distinct reasons.

(Validity on an AD-frameterm). The formula 𝜑 ∈ 𝐿 AD is said to be valid on the AD-frameterm 𝐹 = 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 , written as 𝐹 ⊨ 𝜑 , iff for every valuation 𝑉 : 𝐼 → 𝑊 on F, every assignment 𝑔 : 𝑉 → 𝑊 on 〈 𝐹 , 𝑉 〉 and every world 𝑤 ∈ 𝑊 , it holds that 〈 𝐹 , 𝑉 〉 , 𝑔 , 𝑤 ⊨ 𝜑 .

(AD-validityterm·def). The formula 𝜑 ∈ 𝐿 AD is said to be AD-valid, written as ⊨ AD 𝜑 , iff for every AD-frameterm F, it holds that 𝐹 ⊨ 𝜑 .

(AD-consequenceterm·def). Given formulas Ψ ∪ { 𝜑 } ⊆ 𝐿 AD , we say that φ is an AD-consequenceterm·def of Ψ, written as Ψ ⊨ AD 𝜑 , iff for every AD-modelterm M, every assignment g on M and every world w in M, it holds that if 𝑀 , 𝑔 , 𝑤 ⊨ 𝜓 for every 𝜓 ∈ Ψ , then 𝑀 , 𝑔 , 𝑤 ⊨ 𝜑 .

3.3. Frame Correspondenceterm and Completeness Since this paper is strongly semantically driven, we will not spend much time on proof theory. However, we will show how a sound and strongly complete axiomatizationterm of AD-logicterm can be obtained directly from general results about hybrid logicterm. We start by stating frame correspondencesterm for all the defining properties of AD-framesterm. In Lemma 1 below, expressions such as “2(a)” and “4(c)” refer to the conditions mentioned in Definition 5.

Let 𝐹 = 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 be an arbitrary birelational Kripke frameterm.

F satisfies condition 2(a) (i.e., symmetry of 𝑅 𝐶 𝐷 ) iff 𝐹 ⊨ @ 𝑖 〈 CD 〉 𝑗 → @ 𝑗 〈 CD 〉 𝑖 , F satisfies condition 2(b) (i.e., irreflexivity of 𝑅 𝐶 𝐷 ) iff 𝐹 ⊨ @ 𝑖 ¬ 〈 CD 〉 𝑖 , F satisfies condition 2(c) (i.e., seriality of 𝑅 𝐶 𝐷 ) iff 𝐹 ⊨ 〈 CD 〉 ⊤ , F satisfies condition 2(d) (i.e., partial functionality of 𝑅 𝐶 𝐷 ) iff 𝐹 ⊨ ( 〈 CD 〉 𝑖 ∧ 〈 CD 〉 𝑗 ) → @ 𝑖 𝑗 , F satisfies condition 3(a) (i.e., symmetry of 𝑅 𝐶 ) iff 𝐹 ⊨ @ 𝑖 〈 𝐶 〉 𝑗 → @ 𝑗 〈 𝐶 〉 𝑖 , F satisfies condition 3(b) (i.e., irreflexivity of 𝑅 𝐶 ) iff 𝐹 ⊨ @ 𝑖 ¬ 〈 𝐶 〉 𝑖 , F satisfies condition 4(a) iff 𝐹 ⊨ @ 𝑖 〈 CD 〉 𝑗 → @ 𝑖 ¬ 〈 𝐶 〉 𝑗 , F satisfies condition 4(b) iff 𝐹 ⊨ ( @ 𝑖 〈 CD 〉 𝑗 ∧ @ 𝑘 〈 CD 〉 ℓ ∧ @ 𝑖 〈 𝐶 〉 𝑘 ) → ( ¬ @ 𝑖 〈 𝐶 〉 ℓ ∧ ¬ @ 𝑗 〈 𝐶 〉 ℓ ) , F satisfies condition 4(c) iff 𝐹 ⊨ ( @ 𝑖 〈 𝐶 〉 𝑗 ∧ @ 𝑘 〈 𝐶 〉 ℓ ∧ @ 𝑗 〈 CD 〉 ℓ ) → @ 𝑖 〈 𝐶 〉 𝑘 .

All items are easy to check; many of them are standard frame correspondenceterm results from hybrid logicterm. □ Let Ψ AD be the set consisting of all nine 𝐿 AD -formulas that are mentioned in Lemma 1. Together with the formula ⋄ 𝑖 (which fully captures the behavior of the global modalityterm ⋄ ; see [31], p. 284), this yields a sound and strongly complete axiomatizationterm of AD-logicterm.

A birelational Kripke frameterm F is an AD-frameterm iff for every 𝜓 ∈ Ψ AD , 𝐹 ⊨ 𝜓 .

This follows immediately from Lemma 1 and Definition 5. □ Let 𝐾 𝐻 ( @ , ↓ ) be the standard axiomatizationterm of hybrid logicterm with @ and ↓-binder (see [30], p. 833 and [31], p. 304). Then, 𝐾 𝐻 ( @ , ↓ ) + Ψ AD ∪ { ⋄ 𝑖 } is sound and strongly complete for the class of AD-framesterm.

Soundness is straightforward. Strong completeness follows from Theorem 5 of [30], p. 833 (also see Theorem 5 of [31], p. 304), since all formulas in Ψ AD ∪ { ⋄ 𝑖 } are pure, ⋄ 𝑖 is the sole axiom governing the global modalityterm (see [31], p. 284), and Ψ AD defines the class of AD-framesterm (see Lemma 2). □ We finish this section with a more general, methodological reflection. At first sight, it might look like the system of AD-logicterm is quite ad hoc, being a combination of ingredients that have been haphazardly put together with the sole purpose of capturing the intuitive idea of “viewing Aristotelian diagramsterm as Kripke framesterm”. However, we hope that throughout this section, it has become clear that AD-logicterm is firmly rooted in the vast tradition of modal logic research. This includes, most importantly, the notions of nominalsterm, the @-operator and the ↓-binder from hybrid logicterm [29,30,31,32], but also the study of global modalities [33,34] and functional accessibility relations [35,36]. Furthermore, in relational semantics for relevance logic, one of the accessibility relations is an involutive function (usually called the “Routley star” [37,38,39]), just like 𝑅 𝐶 𝐷 is an involutive function in AD-framesterm.

4. The Relation between AD-Logicterm and Aristotelian Diagramsterm At this point, there might seem to be a subtle mismatch between the informal motivation for this paper, as laid out in Section 1, and the technical development of AD-logicterm in Section 3. After all, the formulas of 𝐿 AD are interpreted on AD-framesterm and AD-modelsterm (see Definitions 9–12), whereas the fundamental intuition was that we wanted to interpret such formulas on the Aristotelian diagramsterm themselves. The distinction is a subtle one, as AD-framesterm and Aristotelian diagramsterm are clearly related to each other; for example, the notations 𝑅 𝐶 𝐷 and 𝑅 𝐶 for the relations in an AD-frameterm are highly suggestive, and the same holds for the parallel observations regarding even numbers of worlds/formulas in finite AD-framesterm/Aristotelian diagramsterm. In this section, we will close this gap altogether. We first introduce the notion of an AD-frameterm being “based on” a given Aristotelian diagramterm, and then show that there exists a bijection between finite Aristotelian diagramsterm (up to Aristotelian isomorphismterm) and finite AD-framesterm (up to modal isomorphism). (The restriction to finite diagrams/AD-framesterm is needed for technical reasons; however, this restriction is not very significant, since all Aristotelian diagramsterm and AD-framesterm that we will be working with later in the paper are finite anyway).

4.1. AD-Framesterm Based on Aristotelian Diagramsterm We start by introducing the idea of an AD-frameterm being based on an Aristotelian diagramterm. We first formulate this in terms of arbitrary birelational Kripke framesterm, and then prove that all such frames are indeed AD-framesterm (see Lemma 3).

(Birelational Kripke frameterm based on an Aristotelian diagramterm). Consider an Aristotelian diagramterm D for ( 𝐹 , 𝑆 ) . A birelational Kripke frameterm 𝐹 = 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 is said to be based on D iff there exists a bijection ℎ : 𝑊 → 𝐹 such that for all 𝑤 , 𝑤 ′ ∈ 𝑊 : 1. 〈 𝑤 , 𝑤 ′ 〉 ∈ 𝑅 𝐶 𝐷 iff CD 𝑆 ( ℎ ( 𝑤 ) , ℎ ( 𝑤 ′ ) ) , 2. 〈 𝑤 , 𝑤 ′ 〉 ∈ 𝑅 𝐶 iff 𝐶 𝑆 ( ℎ ( 𝑤 ) , ℎ ( 𝑤 ′ ) ) .

Note that all components of the Kripke frameterm F and the Aristotelian diagramterm D play key roles in Definition 13: the sets W and 𝐹 are the domain and codomain of the bijection h, while conditions 1 and 2 specify a correspondence between the relations 𝑅 𝐶 𝐷 and 𝑅 𝐶 of the Kripke frameterm F and the actual Aristotelian relationsterm that hold among the formulas of D, relative to the logical system 𝑆 (see Definition 1). Additionally, note that because of its bijective nature and the presence of conditions 1 and 2, the function h from Definition 13 looks very much like an Aristotelian isomorphismterm (see Definition 3); the only difference is that h connects an AD-frameterm with an Aristotelian diagramterm, whereas an Aristotelian isomorphismterm is defined between two Aristotelian diagramsterm. (One point of difference is that h is concerned with just two relations, 𝑅 𝐶 𝐷 and 𝑅 𝐶 , whereas an Aristotelian isomorphismterm is concerned with all four Aristotelian relationsterm. However, this difference is very minor, since SC 𝑆 and SA 𝑆 can be defined in terms of CD 𝑆 and 𝐶 𝑆 ; see Lemmas 2 and 3 of [26]).

We now prove that if a birelational Kripke frameterm is based on an Aristotelian diagramterm, then it is an AD-frameterm. This is exactly as it should be, and justifies our terminological choice for the word “AD-frameterm”.

Let 𝐹 = 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 be a birelational Kripke frameterm that is based on an Aristotelian diagramterm D for ( 𝐹 , 𝑆 ) . Then F is an AD-frameterm.

Since F is based on D, there exists a bijection ℎ : 𝑊 → 𝐹 that satisfies the two conditions mentioned in Definition 13. In order to show that F is an AD-frameterm, it suffices to check that it satisfies all the conditions of Definition 5. All these conditions follow, via the bijection h, from Definitions 1 and 2. For example, 𝑅 𝐶 is symmetric because the Aristotelian relationterm of 𝑆 -contrariety is symmetric; in detail: for all 𝑤 , 𝑤 ′ ∈ 𝑊 , we have 〈 𝑤 , 𝑤 ′ 〉 ∈ 𝑅 𝐶 iff 𝐶 𝑆 ( ℎ ( 𝑤 ) , ℎ ( 𝑤 ′ ) ) iff [ ⊨ 𝑆 ¬ ( ℎ ( 𝑤 ) ∧ ℎ ( 𝑤 ′ ) ) and ⊭ 𝑆 ℎ ( 𝑤 ) ∨ ℎ ( 𝑤 ′ ) ] iff [ ⊨ 𝑆 ¬ ( ℎ ( 𝑤 ′ ) ∧ ℎ ( 𝑤 ) ) and ¬ ⊨ 𝑆 ℎ ( 𝑤 ′ ) ∨ ℎ ( 𝑤 ) ] iff 𝐶 𝑆 ( ℎ ( 𝑤 ′ ) , ℎ ( 𝑤 ) ) iff 〈 𝑤 ′ , 𝑤 〉 ∈ 𝑅 𝐶 .

For a more elaborate example, we check that condition 4(c) of Definition 5 holds. Consider arbitrary worlds 𝑤 , 𝑤 ′ , 𝑤 ″ , 𝑤 ‴ ∈ 𝑊 and suppose that 〈 𝑤 , 𝑤 ″ 〉 , 〈 𝑤 ′ , 𝑤 ‴ 〉 ∈ 𝑅 𝐶 and 〈 𝑤 ″ , 𝑤 ‴ 〉 ∈ 𝑅 𝐶 𝐷 . It follows that 𝐶 𝑆 ( ℎ ( 𝑤 ) , ℎ ( 𝑤 ″ ) ) and 𝐶 𝑆 ( ℎ ( 𝑤 ′ ) , ℎ ( 𝑤 ‴ ) ) and CD 𝑆 ( ℎ ( 𝑤 ″ ) , ℎ ( 𝑤 ‴ ) ) . By the definition of CD 𝑆 and 𝐶 𝑆 , it follows that ⊨ 𝑆 ℎ ( 𝑤 ) → ¬ ℎ ( 𝑤 ″ ) and ⊨ 𝑆 ¬ ℎ ( 𝑤 ″ ) → ℎ ( 𝑤 ‴ ) and ⊨ 𝑆 ℎ ( 𝑤 ‴ ) → ¬ ℎ ( 𝑤 ′ ) , and hence, by transitivity, ⊨ 𝑆 ℎ ( 𝑤 ) → ¬ ℎ ( 𝑤 ′ ) , i.e., ⊨ 𝑆 ¬ ( ℎ ( 𝑤 ) ∧ ℎ ( 𝑤 ′ ) ) (†). Furthermore, it follows from 𝐶 𝑆 ( ℎ ( 𝑤 ) , ℎ ( 𝑤 ″ ) ) that ⊭ 𝑆 ℎ ( 𝑤 ) ∨ ℎ ( 𝑤 ″ ) and, hence, there exists an 𝑆 -model M such that 𝑀 ⊭ ℎ ( 𝑤 ) and 𝑀 ⊭ ℎ ( 𝑤 ″ ) , i.e., 𝑀 ⊨ ¬ ℎ ( 𝑤 ″ ) . From 𝐶 𝐷 ( ℎ ( 𝑤 ″ ) , ℎ ( 𝑤 ‴ ) ) and 𝐶 ( ℎ ( 𝑤 ′ ) , ℎ ( 𝑤 ‴ ) ) , it follows that ⊨ 𝑆 ¬ ℎ ( 𝑤 ″ ) → ℎ ( 𝑤 ‴ ) and ⊨ 𝑆 ℎ ( 𝑤 ‴ ) → ¬ ℎ ( 𝑤 ′ ) and, hence, by transitivity, ⊨ 𝑆 ¬ ℎ ( 𝑤 ″ ) → ¬ ℎ ( 𝑤 ′ ) . Since 𝑀 ⊨ ¬ ℎ ( 𝑤 ″ ) , it follows that 𝑀 ⊨ ¬ ℎ ( 𝑤 ′ ) , i.e., 𝑀 ⊭ ℎ ( 𝑤 ′ ) . Since 𝑀 ⊭ ℎ ( 𝑤 ) and 𝑀 ⊭ ℎ ( 𝑤 ′ ) , it follows that 𝑀 ⊭ ℎ ( 𝑤 ) ∨ ℎ ( 𝑤 ′ ) and, hence, ⊭ 𝑆 ℎ ( 𝑤 ) ∨ ℎ ( 𝑤 ′ ) ( ‡ ) . From (†) and (‡), it follows that 𝐶 𝑆 ( ℎ ( 𝑤 ) , ℎ ( 𝑤 ′ ) ) and, hence, 〈 𝑤 , 𝑤 ′ 〉 ∈ 𝑅 𝐶 , as required. □ We are now ready to entirely close the gap between Aristotelian diagramsterm and AD-framesterm. In particular, validity on an Aristotelian diagramterm D can straightforwardly be defined in terms of validity on all AD-framesterm that are based on D (see Definition 10).

(Validity on an Aristotelian diagramterm). The formula 𝜑 ∈ 𝐿 AD is said to be valid on an Aristotelian diagramterm D, written as ⊨ 𝐷 𝜑 , iff for every AD-frameterm F that is based on D, it holds that 𝐹 ⊨ 𝜑 .

This notion of “diagrammatic validity” will play a crucial role in Section 5 and Section 6 later in the paper. However, in the remainder of the current section, we will first investigate the relationship between Aristotelian diagramsterm and AD-framesterm in more detail.

4.2. From Aristotelian Diagramsterm to AD-Framesterm We have just introduced the notion of a birelational Kripke frameterm being based on a given Aristotelian diagramterm, and shown that such frames are always AD-framesterm. However, there are two questions that have not been answered thus far. First of all, given an Aristotelian diagramterm D, we can ask whether there always exists an AD-frameterm based on D. Secondly, we can ask to what extent the AD-framesterm based on a given Aristotelian diagramterm are unique. In order to provide an affirmative answer to the first question, we define the canonical frame 𝐹 𝐷 for a given Aristotelian diagramterm D.

Consider an Aristotelian diagramterm D for ( 𝐹 , 𝑆 ) . The canonical frame for D is the birelational Kripke frameterm 𝐹 𝐷 = 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 , where 𝑊 : = 𝐹 , 𝑅 𝐶 𝐷 : = CD 𝑆 ∩ ( 𝐹 × 𝐹 ) and 𝑅 𝐶 : = 𝐶 𝑆 ∩ ( 𝐹 × 𝐹 ) .

Consider an Aristotelian diagramterm D for ( 𝐹 , 𝑆 ) . Then the canonical frame 𝐹 𝐷 is based on D, and is thus an AD-frameterm.

To see that 𝐹 𝐷 is based on D, it suffices to note that the identity function id 𝐹 has all the required properties to fulfill the role of h in Definition 13. By Lemma 3, it immediately follows that 𝐹 𝐷 is an AD-frameterm. □ Since an Aristotelian diagramterm D for ( 𝐹 , 𝑆 ) yields an AD-frameterm 𝐹 𝐷 “via” the identity function id 𝐹 , there is a potentially confusing situation that needs our careful consideration. After all, given a formula 𝛼 ∈ 𝐹 and a formula 𝜑 of AD-logicterm, it now makes sense to ask whether (for any valuation V on 𝐹 𝐷 and any assignment g on 〈 𝐹 𝐷 , 𝑉 〉 ) we have 〈 𝐹 𝐷 , 𝑉 〉 , 𝑔 , 𝛼 ⊨ 𝜑 , or, using a common abbreviation, whether 𝛼 ⊨ 𝜑 . However, this latter expression does not mean that we are dealing with a valid argument with a single premise 𝛼 and conclusion 𝜑 , but rather, that the formula 𝜑 ∈ 𝐿 AD is true at the “formula-viewed-as-a-world” 𝛼 ∈ 𝐿 𝑆 (recall our notational convention regarding metavariables for 𝐿 𝑆 and 𝐿 AD ). For example, given the classical squareterm of opposition for ( { □ 𝑝 , ⋄ 𝑝 , □ ¬ 𝑝 , ⋄ ¬ 𝑝 } , KD ) that was already shown in Figure 1b, we can say that □ 𝑝 ⊨ 〈 𝐶 〉 〈 CD 〉 ⊤ , since 𝐶 KD ( □ 𝑝 , □ ¬ 𝑝 ) and CD KD ( □ ¬ 𝑝 , ⋄ 𝑝 ) and ⋄ 𝑝 ⊨ ⊤ . Furthermore, note that □ 𝑝 ⊨ 〈 𝐶 〉 〈 CD 〉 ⊤ does not mean that the formula □ 𝑝 is contrary to the formula 〈 CD 〉 ⊤ : this would involve a category mistake, since □ 𝑝 belongs to the basic modal language 𝐿 □ , whereas 〈 CD 〉 ⊤ belongs to 𝐿 AD . (Formally speaking, there is no overarching logic that □ 𝑝 and 〈 CD 〉 ⊤ both belong to, and with respect to which they could be said to be contrary to each other.) We now turn to the second question about AD-framesterm based on a given Aristotelian diagramterm. It is easy to see that two distinct AD-framesterm can be based on the same Aristotelian diagramterm. For example, the three frames (i) 〈 { 𝑤 , 𝑤 ′ } , { 〈 𝑤 , 𝑤 ′ 〉 , 〈 𝑤 ′ , 𝑤 〉 } , ∅ 〉 , (ii) 〈 { 𝑤 , 𝑣 } , { 〈 𝑤 , 𝑣 〉 , 〈 𝑣 , 𝑤 〉 } , ∅ 〉 and (iii) 〈 { 𝑝 , ¬ 𝑝 } , { 〈 𝑝 , ¬ 𝑝 〉 , 〈 ¬ 𝑝 , 𝑝 〉 } , ∅ 〉 are all nominally distinct from each other, yet all three are based on the diagram for ( { 𝑝 , ¬ 𝑝 } , CPL ) (recall that CPL is short for classical propositional logic). We thus cannot hope for there to be a unique AD-frameterm based on a given Aristotelian diagramterm; however, as the example above already suggests, we can show that AD-framesterm based on a given Aristotelian diagramterm are unique up to modal isomorphism. In order to formulate this correctly, we first recall the notion of modal isomorphism (which is entirely standard from modal logic; see [40], p. 58) in Definition 16. Furthermore, we will actually prove a slightly stronger result: if 𝐷 1 and 𝐷 2 are two Aristotelian diagramsterm that are Aristotelian isomorphic to each other, and 𝐹 1 and 𝐹 2 are AD-framesterm that are based on resp. 𝐷 1 and 𝐷 2 , then 𝐹 1 and 𝐹 2 are modally isomorphic to each other.

Consider AD-framesterm 𝐹 1 = 〈 𝑊 1 , 𝑅 1 CD , 𝑅 1 𝐶 〉 and 𝐹 2 = 〈 𝑊 2 , 𝑅 2 CD , 𝑅 2 𝐶 〉 . A modal isomorphism between these two frames is a bijection 𝑔 : 𝑊 1 → 𝑊 2 such that for all 𝑤 , 𝑤 ′ ∈ 𝑊 , it holds that 〈 𝑤 , 𝑤 ′ 〉 ∈ 𝑅 1 CD iff 〈 𝑔 ( 𝑤 ) , 𝑔 ( 𝑤 ′ ) 〉 ∈ 𝑅 2 CD and 〈 𝑤 , 𝑤 ′ 〉 ∈ 𝑅 1 𝐶 iff 〈 𝑔 ( 𝑤 ) , 𝑔 ( 𝑤 ′ ) 〉 ∈ 𝑅 2 𝐶 .

Consider Aristotelian diagramsterm 𝐷 1 for ( 𝐹 1 , 𝑆 1 ) and 𝐷 2 for ( 𝐹 2 , 𝑆 2 ) , and consider an AD-frameterm 𝐹 1 = 〈 𝑊 1 , 𝑅 1 CD , 𝑅 1 𝐶 〉 based on 𝐷 1 and an AD-frameterm 𝐹 2 = 〈 𝑊 2 , 𝑅 2 CD , 𝑅 2 𝐶 〉 based on 𝐷 2 . If 𝐷 1 and 𝐷 2 are Aristotelian isomorphic, then 𝐹 1 and 𝐹 2 are modally isomorphic.

For 𝑖 = 1 , 2 , since 𝐹 𝑖 is based on 𝐷 𝑖 , there exists a bijection ℎ 𝑖 : 𝑊 𝑖 → 𝐹 𝑖 that satisfies the requirements of Definition 13. Furthermore, since 𝐷 1 and 𝐷 2 are Aristotelian isomorphic to each other, there exists a bijection 𝑓 : 𝐹 1 → 𝐹 2 that satisfies the requirements of Definition 3. We now show that ℎ 2 − 1 ∘ 𝑓 ∘ ℎ 1 : 𝑊 1 → 𝑊 2 is a modal isomorphism.

First of all, note that since ℎ 2 : 𝑊 2 → 𝐹 2 is a bijection, the function ℎ 2 − 1 : 𝐹 2 → 𝑊 2 exists and is a bijection as well. Furthermore, instead of saying that for all 𝑤 , 𝑤 ′ ∈ 𝑊 2 , 〈 𝑤 , 𝑤 ′ 〉 ∈ 𝑅 2 CD iff CD 𝑆 2 ( ℎ 2 ( 𝑤 ) , ℎ 2 ( 𝑤 ′ ) ) (see Definition 13), we can equivalently say that for all 𝛼 , 𝛼 ′ ∈ 𝐹 2 , 〈 ℎ 2 − 1 ( 𝛼 ) , ℎ 2 − 1 ( 𝛼 ′ ) 〉 ∈ 𝑅 2 CD iff CD 𝑆 2 ( 𝛼 , 𝛼 ′ ) . (Exactly the same remark applies to 𝑅 2 𝐶 and 𝐶 𝑆 2 .) The function ℎ 2 − 1 ∘ 𝑓 ∘ ℎ 1 : 𝑊 1 → 𝑊 2 is a composition of three bijections and is itself thus also a bijection. Furthermore, for all 𝑤 , 𝑤 ′ ∈ 𝑊 1 , we have the following chain of equivalences: 〈 ( ℎ 2 − 1 ∘ 𝑓 ∘ ℎ 1 ) ( 𝑤 ) , ( ℎ 2 − 1 ∘ 𝑓 ∘ ℎ 1 ) ( 𝑤 ′ ) 〉 ∈ 𝑅 2 CD iff 〈 ℎ 2 − 1 ( 𝑓 ( ℎ 1 ( 𝑤 ) ) ) , ℎ 2 − 1 ( 𝑓 ( ℎ 1 ( 𝑤 ′ ) ) ) 〉 ∈ 𝑅 2 CD (def. of functional composition) iff CD 𝑆 2 ( 𝑓 ( ℎ 1 ( 𝑤 ) ) , 𝑓 ( ℎ 1 ( 𝑤 ′ ) ) ) (by the remark about ℎ 2 − 1 above) iff CD 𝑆 1 ( ℎ 1 ( 𝑤 ) , ℎ 1 ( 𝑤 ′ ) ) (since f is an Arist. isomorphism) iff 〈 𝑤 , 𝑤 ′ 〉 ∈ 𝑅 1 CD (by the properties of ℎ 1 ). In exactly the same way, we can show that 〈 ( ℎ 2 − 1 ∘ 𝑓 ∘ ℎ 1 ) ( 𝑤 ) , ( ℎ 2 − 1 ∘ 𝑓 ∘ ℎ 1 ) ( 𝑤 ′ ) 〉 ∈ 𝑅 2 𝐶 iff 〈 𝑤 , 𝑤 ′ 〉 ∈ 𝑅 1 𝐶 . This shows that ℎ 2 − 1 ∘ 𝑓 ∘ ℎ 1 : 𝑊 1 → 𝑊 2 is a modal isomorphism. □ We are now in a position to define a function 𝜆 from finite Aristotelian diagramsterm (up to Aristotelian isomorphismterm) to finite AD-framesterm (up to modal isomorphism). We introduce some auxiliary notions in Definition 17, and the actual function 𝜆 in Definition 18. It is quite easy to show that 𝜆 is injective, which we do in Lemma 6.

For each Aristotelian diagramterm D and AD-frameterm F, we define [ 𝐷 ] AI : = { 𝐷 ′ ∣ 𝐷 ′ is an Aristotelian diagramterm that is Aristotelian isomorphic to 𝐷 } , [ 𝐹 ] MI : = { 𝐹 ′ ∣ 𝐹 ′ is an AD - frame that is modally isomorphic to 𝐹 } .

Furthermore, we define 𝐷 : = { [ 𝐷 ] AI ∣ 𝐷 is a finite Aristotelian diagramterm } , 𝐹 : = { [ 𝐹 ] MI ∣ 𝐹 is a finite AD - frame } .

The function 𝜆 : 𝐷 → 𝐹 is defined by putting 𝜆 ( [ 𝐷 ] AI ) : = [ 𝐹 𝐷 ] MI , for every [ 𝐷 ] AI ∈ 𝐷 . Note that this is a well-defined function because of Lemmas 4 and 5: if 𝐷 1 and 𝐷 2 are Aristotelian isomorphic, then 𝐹 𝐷 1 and 𝐹 𝐷 2 are modally isomorphic.

The function λ is injective.

Consider arbitrary Aristotelian diagramsterm 𝐷 1 for ( 𝐹 1 , 𝑆 1 ) and 𝐷 2 for ( 𝐹 2 , 𝑆 2 ) and suppose that [ 𝐹 𝐷 1 ] MI = 𝜆 ( [ 𝐷 1 ] AI ) = 𝜆 ( [ 𝐷 2 ] AI ) = [ 𝐹 𝐷 2 ] MI , i.e., 𝐹 𝐷 1 and 𝐹 𝐷 2 are modally isomorphic. We show that [ 𝐷 1 ] AI = [ 𝐷 2 ] AI , i.e., 𝐷 1 and 𝐷 2 are Aristotelian isomorphic. Since 𝐹 𝐷 1 and 𝐹 𝐷 2 are modally isomorphic, there exists a modal isomorphism 𝑓 : 𝐹 1 → 𝐹 2 . For all 𝛼 , 𝛽 ∈ 𝐹 1 , we have CD 𝑆 1 ( 𝛼 , 𝛽 ) iff 〈 𝛼 , 𝛽 〉 ∈ 𝑅 1 CD (by Definition 15) iff 〈 𝑓 ( 𝛼 ) , 𝑓 ( 𝛽 ) 〉 ∈ 𝑅 2 CD (by Definition 16) iff CD 𝑆 2 ( 𝑓 ( 𝛼 ) , 𝑓 ( 𝛽 ) ) (by Definition 15). Similarly, we can show that 𝐶 𝑆 1 ( 𝛼 , 𝛽 ) iff 𝐶 𝑆 2 ( 𝑓 ( 𝛼 ) , 𝑓 ( 𝛽 ) ) . Furthermore, since subcontrariety and subalternationterm can be defined in terms of contradiction and contrariety (recall Lemmas 2 and 3 from [26]), we also get SC 𝑆 1 ( 𝛼 , 𝛽 ) iff SC 𝑆 2 ( 𝑓 ( 𝛼 ) , 𝑓 ( 𝛽 ) ) and SA 𝑆 1 ( 𝛼 , 𝛽 ) iff SA 𝑆 2 ( 𝑓 ( 𝛼 ) , 𝑓 ( 𝛽 ) ) . This shows that f is an Aristotelian isomorphismterm between 𝐷 1 and 𝐷 2 , as desired. □ Note that the proof of Lemma 6 does not rely on the fact that 𝐷 and 𝐹 contain only finite Aristotelian diagramsterm and AD-framesterm. This stands in sharp contrast with the proof of Lemma 8 below, which deals with the surjectivity of 𝜆 .

4.3. From AD-Framesterm to Aristotelian Diagramsterm In this subsection, we finish our investigation of the relation between AD-framesterm and Aristotelian diagramsterm, by showing that the function 𝜆 defined above is not only injective, but also surjective. This proof will be a bit more involved, so we first introduce the auxiliary notion of (maximal) F-consistency in Definition 19 and prove Lemma 7. The latter is a Lindenbaum-type lemma, which states that every F-consistent set can be extended to a maximally F-consistent set. Finally, it bears emphasizing that the proof of Lemma 8 is closely related to the algorithm described in Section 4 of [24].

Let 𝐹 = 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 be an AD-frameterm. A set 𝑋 ⊆ 𝑊 is said to be F-consistent iff there are no 𝑤 , 𝑣 ∈ 𝑋 such that 〈 𝑤 , 𝑣 〉 ∈ 𝑅 𝐶 𝐷 or 〈 𝑤 , 𝑣 〉 ∈ 𝑅 𝐶 . Furthermore, X is said to be maximally F-consistent iff (i) X is F-consistent and (ii) for all 𝑤 ∈ 𝑊 \ 𝑋 , the set 𝑋 ∪ { 𝑤 } is not F-consistent. Finally, Π ( 𝐹 ) is defined to be the set of all maximally F-consistent subsets of W.

Let 𝐹 = 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 be an AD-frameterm. For every F-consistent set 𝑋 ⊆ 𝑊 , there exists a maximally F-consistent set 𝐴 ∈ Π ( 𝐹 ) such that 𝑋 ⊆ 𝐴 .

Let 𝑃 be the collection of all sets 𝑆 ⊆ 𝑊 such that 𝑋 ⊆ 𝑆 and S is F-consistent. Note that 𝑃 is non-empty (since 𝑋 ∈ 𝑃 ) and that 𝑃 is partially ordered by ⊆. We now prove that every non-empty chain in the poset 𝑃 has an upper bound in 𝑃 . Consider an arbitrary chain 𝐶 in 𝑃 . Clearly, ⋃ 𝐶 is an upper bound for 𝐶 , so it suffices to show that ⋃ 𝐶 ∈ 𝑃 , i.e., (i) 𝑋 ⊆ ⋃ 𝐶 and (ii) ⋃ 𝐶 is F-consistent. Regarding (i), since 𝐶 is non-empty, there exists an 𝑆 ∈ 𝐶 ⊆ 𝑃 , and hence 𝑋 ⊆ 𝑆 ⊆ ⋃ 𝐶 . Regarding (ii), suppose, toward a reductio, that ⋃ 𝐶 is not F-consistent. Hence, there exist 𝑥 , 𝑦 ∈ ⋃ 𝐶 such that 〈 𝑥 , 𝑦 〉 ∈ 𝑅 𝐶 𝐷 or 〈 𝑥 , 𝑦 〉 ∈ 𝑅 𝐶 . Since 𝑥 , 𝑦 ∈ ⋃ 𝐶 , there exist 𝐶 𝑥 , 𝐶 𝑦 ∈ 𝐶 such that 𝑥 ∈ 𝐶 𝑥 and 𝑦 ∈ 𝐶 𝑦 . Since 𝐶 is a chain, we have 𝐶 𝑥 ⊆ 𝐶 𝑦 or 𝐶 𝑦 ⊆ 𝐶 𝑥 . Consider the case 𝐶 𝑥 ⊆ 𝐶 𝑦 (the case 𝐶 𝑦 ⊆ 𝐶 𝑥 is analogous). It then follows that 𝑥 , 𝑦 ∈ 𝐶 𝑦 , and thus 𝐶 𝑦 is not F-consistent, which contradicts 𝐶 𝑦 ∈ 𝐶 ⊆ 𝑃 .

We have now checked that every non-empty chain in the poset 𝑃 has an upper bound in 𝑃 . By Zorn’s lemma, it follows that 𝑃 has at least one maximal element, A. Since 𝐴 ∈ 𝑃 , we have, by definition of 𝑃 , that 𝑋 ⊆ 𝐴 and that A is F-consistent. To show that 𝐴 ∈ Π ( 𝐹 ) , it thus suffices to check that A is maximal. Toward a reductio, assume that there exists some 𝑤 ∈ 𝑊 \ 𝐴 such that 𝐴 ∪ { 𝑤 } is F-consistent. Since 𝑋 ⊆ 𝐴 ⊆ 𝐴 ∪ { 𝑤 } and 𝐴 ∪ { 𝑤 } is F-consistent, we have 𝐴 ∪ { 𝑤 } ∈ 𝑃 . However, since 𝐴 𝐴 ∪ { 𝑤 } , this contradicts the fact that A is a maximal element of 𝑃 . □ The function 𝜆 : 𝐷 → 𝐹 is surjective.

Consider an arbitrary finite AD-frameterm 𝐹 = 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 . We will show that there exists an Aristotelian diagramterm D such that [ 𝐹 ] MI = 𝜆 ( [ 𝐷 ] AI ) = [ 𝐹 𝐷 ] MI , i.e., such that F is modally isomorphic to 𝐹 𝐷 . In order to specify D, we have to specify a logical system 𝑆 and a fragment 𝐹 ⊆ 𝐿 𝑆 . For our logical system, we take classical propositional logic, CPL , while for 𝐹 , we take the image of W under the function f, which is defined below.

First of all, note that | Π ( 𝐹 ) | ≤ 2 | 𝑊 | , so since F is finite, it follows that Π ( 𝐹 ) is finite as well. Now fix an ordering on the elements of Π ( 𝐹 ) : 𝐴 1 , 𝐴 2 , ⋯ , 𝐴 | Π ( 𝐹 ) | . Secondly, we consider a partition Π CPL of CPL consisting of | Π ( 𝐹 ) | formulas: Π CPL : = { 𝛼 1 , 𝛼 2 , ⋯ , 𝛼 | Π ( 𝐹 ) | } . The set Π CPL is called a “partition of CPL ”, because its elements are mutually exclusive (i.e., ⊨ CPL ¬ ( 𝛼 𝑖 ∧ 𝛼 𝑗 ) for distinct 𝛼 𝑖 , 𝛼 𝑗 ∈ Π CPL ) and jointly exhaustive (i.e., ⊨ CPL ⋁ Π CPL ). It is easy to see that such a partition Π CPL always exists; see below for a concrete example and see the proof of Theorem 4 in [28] for a general construction method. For each 𝑤 ∈ 𝑊 , we define 𝑓 ( 𝑤 ) : = ⋁ { 𝛼 𝑖 ∈ Π CPL ∣ 𝑤 ∈ 𝐴 𝑖 } . Now let 𝑓 [ 𝑊 ] : = { 𝑓 ( 𝑤 ) ∣ 𝑤 ∈ 𝑊 } , and consider the Aristotelian diagramterm D for ( 𝑓 [ 𝑊 ] , CPL ) . (This can also be formulated using the well-known representation format of bitstrings [24,28,41]: define 𝛽 ( 𝑤 ) ∈ { 0 , 1 } | Π ( 𝐹 ) | to be the bitstring that has a 1 in its i th bit position iff 𝑤 ∈ 𝐴 𝑖 .) We will show that f is a modal isomorphism from F to 𝐹 𝐷 .

We first check that f is bijective. Surjectivity follows immediately from the definition of f. For injectivity, consider arbitrary 𝑤 , 𝑣 ∈ 𝑊 and suppose that 𝑤 ≠ 𝑣 . We will show that ⋁ { 𝛼 𝑖 ∈ Π CPL ∣ 𝑤 ∈ 𝐴 𝑖 } = 𝑓 ( 𝑤 ) ≠ 𝑓 ( 𝑣 ) = ⋁ { 𝛼 𝑖 ∈ Π CPL ∣ 𝑣 ∈ 𝐴 𝑖 } , by showing that there exists an 𝐴 𝑖 ∈ Π ( 𝐹 ) such that 𝑤 ∈ 𝐴 𝑖 iff 𝑣 ∉ 𝐴 𝑖 . By the seriality of 𝑅 𝐶 𝐷 , there exist 𝑤 ′ , 𝑣 ′ ∈ 𝑊 such that 〈 𝑤 , 𝑤 ′ 〉 , 〈 𝑣 , 𝑣 ′ 〉 ∈ 𝑅 𝐶 𝐷 . Now consider the following case distinction: The set { 𝑤 , 𝑣 ′ } ⊆ 𝑊 is F-consistent. By Lemma 7, there exists some 𝐴 𝑖 ∈ Π ( 𝐹 ) such that { 𝑤 , 𝑣 ′ } ⊆ 𝐴 𝑖 . We have 𝑤 ∈ 𝐴 𝑖 but 𝑣 ∉ 𝐴 𝑖 (because 𝐴 𝑖 is F-consistent, 𝑣 ′ ∈ 𝐴 𝑖 and 〈 𝑣 , 𝑣 ′ 〉 ∈ 𝑅 𝐶 𝐷 ), as desired. The set { 𝑤 ′ , 𝑣 } ⊆ 𝑊 is F-consistent. Analogously to the previous case, we can now show that there exists some 𝐴 𝑖 ∈ Π ( 𝐹 ) such that 𝑤 ∉ 𝐴 𝑖 but 𝑣 ∈ 𝐴 𝑖 , as desired. Neither { 𝑤 , 𝑣 ′ } nor { 𝑤 ′ , 𝑣 } is F-consistent. We will show that this case cannot occur. Since { 𝑤 , 𝑣 ′ } is not F-consistent, we have 〈 𝑤 , 𝑣 ′ 〉 ∈ 𝑅 𝐶 𝐷 or 〈 𝑤 , 𝑣 ′ 〉 ∈ 𝑅 𝐶 . If 〈 𝑤 , 𝑣 ′ 〉 ∈ 𝑅 𝐶 𝐷 , then it would follow by the symmetry and functionality of 𝑅 𝐶 𝐷 that 𝑤 = 𝑣 , which contradicts our assumption that 𝑤 ≠ 𝑣 . Hence, 〈 𝑤 , 𝑣 ′ 〉 ∈ 𝑅 𝐶 . Similarly, since { 𝑤 ′ , 𝑣 } is not F-consistent, it follows that 〈 𝑤 ′ , 𝑣 〉 ∈ 𝑅 𝐶 . However, from 〈 𝑤 , 𝑤 ′ 〉 , 〈 𝑣 , 𝑣 ′ 〉 ∈ 𝑅 𝐶 𝐷 and 〈 𝑤 , 𝑣 ′ 〉 ∈ 𝑅 𝐶 , it follows by condition 4(b) of Definition 5 that 〈 𝑤 ′ , 𝑣 〉 ∉ 𝑅 𝐶 .

We now check that for all 𝑤 , 𝑣 ∈ 𝑊 , we have 〈 𝑤 , 𝑣 〉 ∈ 𝑅 𝐶 𝐷 iff CD CPL ( 𝑓 ( 𝑤 ) , 𝑓 ( 𝑣 ) ) . For the left to right direction, suppose that 〈 𝑤 , 𝑣 〉 ∈ 𝑅 𝐶 𝐷 . By the definition of CD CPL , it suffices to prove the following two claims: ⊨ CPL ¬ ( 𝑓 ( 𝑤 ) ∧ 𝑓 ( 𝑣 ) ) . Consider an arbitrary CPL -model M and suppose, toward a contradiction, that 𝑀 ⊨ 𝑓 ( 𝑤 ) ∧ 𝑓 ( 𝑣 ) . Since 𝑀 ⊨ 𝑓 ( 𝑤 ) = ⋁ { 𝛼 𝑖 ∈ Π CPL ∣ 𝑤 ∈ 𝐴 𝑖 } , there exists 1 ≤ 𝑖 ≤ | Π ( 𝐹 ) | such that 𝑀 ⊨ 𝛼 𝑖 and 𝑤 ∈ 𝐴 𝑖 . Similarly, since 𝑀 ⊨ 𝑓 ( 𝑣 ) = ⋁ { 𝛼 𝑗 ∈ Π CPL ∣ 𝑣 ∈ 𝐴 𝑗 } , there exists 1 ≤ 𝑗 ≤ | Π ( 𝐹 ) | such that 𝑀 ⊨ 𝛼 𝑗 and 𝑣 ∈ 𝐴 𝑗 . Since 𝛼 𝑖 and 𝛼 𝑗 are members of a partition of CPL , it follows from 𝑀 ⊨ 𝛼 𝑖 and 𝑀 ⊨ 𝛼 𝑗 that 𝑖 = 𝑗 . Hence, we have 𝑤 ∈ 𝐴 𝑖 and 𝑣 ∈ 𝐴 𝑗 = 𝐴 𝑖 , which, together with 〈 𝑤 , 𝑣 〉 ∈ 𝑅 𝐶 𝐷 , contradicts the F-consistency of 𝐴 𝑖 . ⊨ CPL 𝑓 ( 𝑤 ) ∨ 𝑓 ( 𝑣 ) . We have to show that ⊨ CPL ⋁ { 𝛼 𝑖 ∈ Π CPL ∣ 𝑤 ∈ 𝐴 𝑖 } ∨ ⋁ { 𝛼 𝑖 ∈ Π CPL ∣ 𝑣 ∈ 𝐴 𝑖 } , i.e., that ⊨ CPL ⋁ { 𝛼 𝑖 ∈ Π CPL ∣ 𝑤 ∈ 𝐴 𝑖 or 𝑣 ∈ 𝐴 𝑖 } . Since ⊨ CPL ⋁ Π CPL , it suffices to show that for each 𝐴 𝑖 ∈ Π ( 𝐹 ) , we have 𝑤 ∈ 𝐴 𝑖 or 𝑣 ∈ 𝐴 𝑖 . Consider some 𝐴 𝑖 ∈ Π ( 𝐹 ) and suppose that 𝑤 ∉ 𝐴 𝑖 . We will show that 𝑣 ∈ 𝐴 𝑖 . Since 𝐴 𝑖 is maximal, it follows from 𝑤 ∉ 𝐴 𝑖 that 𝐴 𝑖 ∪ { 𝑤 } is not F-consistent, i.e., there exist 𝑥 , 𝑦 ∈ 𝐴 𝑖 ∪ { 𝑤 } such that 〈 𝑥 , 𝑦 〉 ∈ 𝑅 𝐶 𝐷 or 〈 𝑥 , 𝑦 〉 ∈ 𝑅 𝐶 . Now, if x and y both come from 𝐴 𝑖 , then 𝐴 𝑖 itself would be F-inconsistent. Furthermore, if x and y both come from { 𝑤 } , then 𝑥 = 𝑤 = 𝑦 , which contradicts the irreflexivity of 𝑅 𝐶 𝐷 and 𝑅 𝐶 . So without loss of generality, we assume that 𝑥 ∈ 𝐴 𝑖 and 𝑦 = 𝑤 , and thus we have 〈 𝑥 , 𝑤 〉 ∈ 𝑅 𝐶 𝐷 or 〈 𝑥 , 𝑤 〉 ∈ 𝑅 𝐶 . In the first case, i.e., 〈 𝑥 , 𝑤 〉 ∈ 𝑅 𝐶 𝐷 , it follows by the symmetry and functionality of 𝑅 𝐶 𝐷 that 𝑥 = 𝑣 . Since 𝑥 ∈ 𝐴 𝑖 , we thus have 𝑣 ∈ 𝐴 𝑖 , as desired. We now turn to the second case: 〈 𝑥 , 𝑤 〉 ∈ 𝑅 𝐶 . Toward a contradiction, assume 𝑣 ∉ 𝐴 𝑖 . Since 𝐴 𝑖 is maximal, it follows that 𝐴 𝑖 ∪ { 𝑣 } is not F-consistent, i.e., there exist 𝑦 , 𝑧 ∈ 𝐴 𝑖 ∪ { 𝑣 } such that 〈 𝑦 , 𝑧 〉 ∈ 𝑅 𝐶 𝐷 or 〈 𝑦 , 𝑧 〉 ∈ 𝑅 𝐶 . Reasoning as before, we again assume, without loss of generality, that 𝑦 ∈ 𝐴 𝑖 and 𝑧 = 𝑣 , and thus we have 〈 𝑦 , 𝑣 〉 ∈ 𝑅 𝐶 𝐷 or 〈 𝑦 , 𝑣 〉 ∈ 𝑅 𝐶 . In the first subcase, i.e., 〈 𝑦 , 𝑣 〉 ∈ 𝑅 𝐶 𝐷 , it follows by the symmetry and functionality of 𝑅 𝐶 𝐷 that 𝑦 = 𝑤 . Since 𝑦 ∈ 𝐴 𝑖 , we thus have 𝑤 ∈ 𝐴 𝑖 , which contradicts our assumption that 𝑤 ∉ 𝐴 𝑖 . In the second subcase, i.e., 〈 𝑦 , 𝑣 〉 ∈ 𝑅 𝐶 , it follows by condition 4(c) from Definition 5 that 〈 𝑥 , 𝑦 〉 ∈ 𝑅 𝐶 . However, since 𝑥 , 𝑦 ∈ 𝐴 𝑖 , this contradicts the F-consistency of 𝐴 𝑖 .

For the right to left direction, suppose that CD CPL ( 𝑓 ( 𝑤 ) , 𝑓 ( 𝑣 ) ) and, toward a contradiction, that 〈 𝑤 , 𝑣 〉 ∉ 𝑅 𝐶 𝐷 . We make the following case distinction: 〈 𝑤 , 𝑣 〉 ∉ 𝑅 𝐶 . Then the set { 𝑤 , 𝑣 } ⊆ 𝑊 is F-consistent, so by Lemma 7, there exists some 𝐴 * ∈ Π ( 𝐹 ) such that { 𝑤 , 𝑣 } ⊆ 𝐴 * . It follows from CD CPL ( 𝑓 ( 𝑤 ) , 𝑓 ( 𝑣 ) ) that ⋁ { 𝛼 𝑖 ∈ Π CPL ∣ 𝑤 ∈ 𝐴 𝑖 } = 𝑓 ( 𝑤 ) ⊨ CPL ¬ 𝑓 ( 𝑣 ) = ¬ ⋁ { 𝛼 𝑖 ∈ Π CPL ∣ 𝑤 ∈ 𝐴 𝑖 } . Hence, for all 𝐴 𝑖 ∈ Π ( 𝐹 ) , if 𝑤 ∈ 𝐴 𝑖 then 𝑣 ∉ 𝐴 𝑖 . This is in contradiction with the fact that 𝑤 , 𝑣 ∈ 𝐴 * . 〈 𝑤 , 𝑣 〉 ∈ 𝑅 𝐶 . By the seriality of 𝑅 𝐶 𝐷 , there exist 𝑤 ′ , 𝑣 ′ ∈ 𝑊 such that 〈 𝑤 , 𝑤 ′ 〉 , 〈 𝑣 , 𝑣 ′ 〉 ∈ 𝑅 𝐶 𝐷 . Now, if 〈 𝑤 ′ , 𝑣 ′ 〉 ∈ 𝑅 𝐶 𝐷 , then by the symmetry and functionality of 𝑅 𝐶 𝐷 it would follow that 𝑤 = 𝑣 ′ and 𝑣 = 𝑤 ′ , so 〈 𝑤 ′ , 𝑣 ′ 〉 ∈ 𝑅 𝐶 𝐷 would mean that 〈 𝑣 , 𝑤 〉 ∈ 𝑅 𝐶 𝐷 , and thus (by the symmetry of 𝑅 𝐶 𝐷 ) that 〈 𝑤 , 𝑣 〉 ∈ 𝑅 𝐶 𝐷 , which contradicts 𝑅 𝐶 𝐷 ∩ 𝑅 𝐶 = ∅ . This shows that 〈 𝑤 ′ , 𝑣 ′ 〉 ∉ 𝑅 𝐶 𝐷 . Furthermore, it cannot happen that 〈 𝑤 ′ , 𝑣 ′ 〉 ∈ 𝑅 𝐶 either, since together with 〈 𝑤 , 𝑣 〉 ∈ 𝑅 𝐶 and the symmetry of 𝑅 𝐶 , that would contradict condition 4(b) of Definition 5. Since 〈 𝑤 ′ , 𝑣 ′ 〉 ∉ 𝑅 𝐶 𝐷 and 〈 𝑤 ′ , 𝑣 ′ 〉 ∉ 𝑅 𝐶 , it follows that the set { 𝑤 ′ , 𝑣 ′ } ⊆ 𝑊 is F-consistent, and hence, by Lemma 7, there exists some 𝐴 * ∈ Π ( 𝐹 ) such that { 𝑤 ′ , 𝑣 ′ } ⊆ 𝐴 * . Note that 𝑤 ∉ 𝐴 * , since together with 𝑤 ′ ∈ 𝐴 * and 〈 𝑤 , 𝑤 ′ 〉 ∈ 𝑅 𝐶 𝐷 , this would violate the F-consistency of 𝐴 * . Analogously, we show that 𝑣 ∉ 𝐴 * . It follows from CD CPL ( 𝑓 ( 𝑤 ) , 𝑓 ( 𝑣 ) ) that ⊨ CPL 𝑓 ( 𝑤 ) ∨ 𝑓 ( 𝑣 ) , i.e., ⊨ CPL ⋁ { 𝛼 𝑖 ∈ Π CPL ∣ 𝑤 ∈ 𝐴 𝑖 } ∨ ⋁ { 𝛼 𝑖 ∈ Π CPL ∣ 𝑣 ∈ 𝐴 𝑖 } . Hence, for all 𝐴 𝑖 ∈ Π ( 𝐹 ) , it holds that 𝑤 ∈ 𝐴 𝑖 or 𝑣 ∈ 𝐴 𝑖 . This contradicts the fact that 𝑤 , 𝑣 ∉ 𝐴 * .

In an analogous fashion, we can check that for all 𝑤 , 𝑣 ∈ 𝑊 , we have 〈 𝑤 , 𝑣 〉 ∈ 𝑅 𝐶 iff 𝐶 CPL ( 𝑓 ( 𝑤 ) , 𝑓 ( 𝑣 ) ) . To summarize: f is a modal isomorphism from 𝐹 = 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 to the AD-frameterm 𝐹 𝐷 that is based on the Aristotelian diagramterm D for ( 𝑓 [ 𝑊 ] , CPL ) . □ In order to better grasp the proof of Lemma 8, it may be useful to work through a concrete example. Consider the AD-frameterm 𝐹 = 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 shown in Figure 2a. An easy calculation yields Π ( 𝐹 ) = { 𝐴 1 : = { 𝑤 , 𝑢 } , 𝐴 2 : = { 𝑢 , 𝑠 } , 𝐴 3 : = { 𝑣 , 𝑠 } } . Since | Π ( 𝐹 ) | = 3 , we need to consider a partition Π CPL that consists of three formulas, for example Π CPL : = { 𝛼 1 : = 𝑝 , 𝛼 2 : = ¬ 𝑝 ∧ 𝑞 , 𝛼 3 : = ¬ 𝑝 ∧ ¬ 𝑞 } . Since w only belongs to 𝐴 1 , we define 𝑓 ( 𝑤 ) : = 𝛼 1 = 𝑝 . Since v only belongs to 𝐴 3 , we define 𝑓 ( 𝑣 ) : = 𝛼 3 = ¬ 𝑝 ∧ ¬ 𝑞 . Since u belongs to 𝐴 1 and 𝐴 2 , we define 𝑓 ( 𝑢 ) : = 𝛼 1 ∨ 𝛼 2 = 𝑝 ∨ ( ¬ 𝑝 ∧ 𝑞 ) ≡ CPL 𝑝 ∨ 𝑞 . Finally, since s belongs to 𝐴 2 and 𝐴 3 , we define 𝑓 ( 𝑠 ) : = 𝛼 2 ∨ 𝛼 3 = ( ¬ 𝑝 ∧ 𝑞 ) ∨ ( ¬ 𝑝 ∧ ¬ 𝑞 ) ≡ CPL ¬ 𝑝 . In this way, we obtain the Aristotelian diagramterm D for ( 𝑓 [ 𝑊 ] , CPL ) that is shown in Figure 2b. Upon visual inspection of the left- and right-hand sides of Figure 2, it should be immediately clear that F is modally isomorphic to 𝐹 𝐷 .

We can now put everything together in Theorem 2. The importance of this theorem, and in particular, of Lemma 8, should not be underestimated. These results tell us that Definition 5 completely captures the structural properties of Aristotelian diagramsterm. More concretely, the various conditions stated in Definition 5 are sufficient to exhaustively describe the behavior of Aristotelian relationsterm (consider how each of these properties played a role in the proof of Lemma 8!). Until now, there was a long list of various properties of Aristotelian relationsterm (e.g., we know that subalternationterm is transitive), but it was unknown whether this list was exhaustive. In other words, it was conceptually possible that some complex property of the Aristotelian relationsterm might exist that we did not yet know about, and that does not follow from the properties that are already known. Theorem 2 tells us definitively that no such properties exist.

The function 𝜆 : 𝐷 → 𝐹 is bijective.

This follows immediately from Lemmas 6 and 8. □ To conclude this section, it is worth mentioning that the proof of Theorem 2 immediately yields another interesting result as well: every Aristotelian diagramterm for some finite fragment 𝐹 ⊆ 𝐿 𝑆 and some logical system 𝑆 is Aristotelian isomorphic to a diagram for a finite fragment 𝐹 CPL ⊆ 𝐿 CPL and the logic CPL (Lemma 9). This means that when we are studying Aristotelian diagramsterm, we can essentially restrict ourselves to diagrams for (fragments from) classical propositional logic.

Consider an Aristotelian diagramterm 𝐷 1 for ( 𝐹 , 𝑆 ) , where 𝐹 is finite. There exist a finite fragment 𝐹 CPL ⊆ 𝐿 CPL and a diagram 𝐷 2 for ( 𝐹 CPL , CPL ) such that 𝐷 1 is Aristotelian isomorphic to 𝐷 2 .

Consider the canonical frame 𝐹 𝐷 1 that is based on 𝐷 1 . In the proof of Lemma 8, we constructed a finite fragment 𝐹 CPL ⊆ 𝐿 CPL (namely, 𝐹 CPL : = 𝑓 [ 𝐹 ] ) and an Aristotelian diagramterm 𝐷 2 for ( 𝐹 CPL , CPL ) such that 𝐹 𝐷 1 is modally isomorphic to 𝐹 𝐷 2 . By the proof of Lemma 6, it follows that the Aristotelian diagramsterm 𝐷 1 and 𝐷 2 themselves are Aristotelian isomorphic. □ 5. Characterizing Aristotelian Familiesterm in AD-Logicterm In this section, we really start putting AD-logicterm to use, in order to capture some important insights from logical geometryterm. In particular, one of the main ongoing research efforts in logical geometryterm is to develop a systematic typology of Aristotelian familiesterm (i.e., maximal classes of Aristotelian diagramsterm that are closed under Aristotelian isomorphismterm) [24,28,42]. We will now prove frame correspondenceterm results for several of the most important families of Aristotelian diagramsterm: for each such family A, we exhibit a formula 𝜒 𝐴 ∈ 𝐿 AD , and show that ⊨ 𝐷 𝜒 𝐴 iff D belongs to the Aristotelian family A, for all diagrams D. These frame correspondencesterm do not refer to any underlying logical system, and thus provide fully generic descriptions of the Aristotelian familiesterm [24] (recall the distinction between general and generic characterizations of Aristotelian familiesterm from Section 1).

5.1. Expressing Frame Cardinalities We start by mentioning an auxiliary result. Because our language 𝐿 AD is so expressive, it can be used to count the number of worlds in a (finite) AD-frameterm. We write “ ) 𝑛 ” to denote a sequence of n closing brackets.

Consider an AD-frameterm 𝐹 = 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 . Then we have: | 𝑊 | = 2 iff 𝐹 ⊨ ↓ 𝑥 1 ( ⋄ ( ¬ 𝑥 1 ∧ ↓ 𝑥 2 ( □ ( 𝑥 1 ∨ 𝑥 2 ) ) ) ) , | 𝑊 | = 4 iff 𝐹 ⊨ ↓ 𝑥 1 ( ⋄ ( ¬ 𝑥 1 ∧ ↓ 𝑥 2 ( ⋄ ( ¬ 𝑥 1 ∧ ¬ 𝑥 2 ∧ ↓ 𝑥 3 ( ⋄ ( ¬ 𝑥 1 ∧ ¬ 𝑥 2 ∧ ¬ 𝑥 3 ∧ ↓ 𝑥 4 ( □ ( 𝑥 1 ∨ 𝑥 2 ∨ 𝑥 3 ∨ 𝑥 4 ) 8 , and in general, for any even number n: | 𝑊 | = 𝑛 iff 𝐹 ⊨ ↓ 𝑥 1 ( ⋄ ( ¬ 𝑥 1 ∧ ↓ 𝑥 2 ( ⋄ ( ¬ 𝑥 1 ∧ ¬ 𝑥 2 ∧ ↓ 𝑥 3 ( ⋄ ( ¬ 𝑥 1 ∧ ¬ 𝑥 2 ∧ ¬ 𝑥 3 ∧ ⋮ ↓ 𝑥 𝑛 − 1 ( ⋄ ( ¬ 𝑥 1 ∧ ⋯ ∧ ¬ 𝑥 𝑛 − 1 ∧ ↓ 𝑥 𝑛 ( □ ( 𝑥 1 ∨ ⋯ ∨ 𝑥 𝑛 ) 2 𝑛 . The aforementioned 𝐿 AD -formula is henceforth abbreviated as 𝜒 𝑛 , so | 𝑊 | = 𝑛 iff 𝐹 ⊨ 𝜒 𝑛 .

This is an easy exercise in frame correspondenceterm theory for hybrid logicterm. The structure of the formula 𝜒 𝑛 is clear: each variable 𝑥 𝑖 gets bound to a world 𝑤 𝑖 ∈ 𝑊 ; for all 1 ≤ 𝑖 < 𝑗 ≤ 𝑛 we have a formula of the form ¬ 𝑥 𝑖 ∧ ⋯ ∧ ↓ 𝑥 𝑗 ( 𝜑 ) inside 𝜒 𝑛 , which shows that 𝑤 𝑖 ≠ 𝑤 𝑗 ; finally, the subformula □ ( 𝑥 1 ∨ ⋯ ∨ 𝑥 𝑛 ) of 𝜒 𝑛 means that 𝑤 1 , ⋯ , 𝑤 𝑛 are all the worlds in W, and thus | 𝑊 | = 𝑛 . □ Note that the formula 𝜒 𝑛 contains only the binder and the global modalityterm, and hence, there is nothing specifically “(Aristotelian) diagrammatical” about 𝜒 𝑛 (in particular, it does not contain 〈 CD 〉 or 〈 𝐶 〉 ). This is exactly as it should be, since 𝜒 𝑛 merely describes the cardinality of the AD-frameterm F, which is (nearly) independent of F’s status as (based on) an Aristotelian diagramterm. (But do note that we define 𝜒 𝑛 only for even numbers n, since finite Aristotelian diagramsterm/AD-framesterm have, by definition, an even number of formulas/worlds; see Definitions 2 and 5).

5.2. Characterizing the Aristotelian Family of Pairs of Contradictories Within the typology of Aristotelian diagramsterm, there exists a unique smallest type of Aristotelian diagramterm, viz., the pair of contradictories (PCD) (see Figure 3). For a diagram for ( 𝐹 , 𝑆 ) to be a PCD, it suffices to require that 𝐹 contains exactly two formulas; from the general Definition 2 of an Aristotelian diagramterm, it then follows that these two formulas are 𝑆 -contradictory to each other (hence the term “pair of contradictories”). Consequently, it is also straightforward to characterize PCDs in AD-logicterm.

An Aristotelian diagramterm for ( 𝐹 , 𝑆 ) is a pair of contradictories iff | 𝐹 | = 2 .

Define 𝜒 PCD : = 𝜒 2 . An Aristotelian diagramterm D for ( 𝐹 , 𝑆 ) is a PCD iff ⊨ 𝐷 𝜒 PCD .

For the left to right direction, suppose that D is a PCD and consider an arbitrary AD-frameterm 𝐹 = 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 that is based on D. By Definitions 13 and 20, it follows that | 𝑊 | = 2 , so by Lemma 10, we get 𝐹 ⊨ 𝜒 2 , i.e., 𝐹 ⊨ 𝜒 PCD .

For the right to left direction, suppose that ⊨ 𝐷 𝜒 PCD , and consider the canonical AD-frameterm 𝐹 𝐷 . By Lemma 4, it follows that 𝐹 𝐷 ⊨ 𝜒 PCD , i.e., 𝐹 𝐷 ⊨ 𝜒 2 , so by Lemma 10, we find that | 𝐹 | = 2 , which means that D is a PCD. □ Let us have another look at Definition 20 and Theorem 3. At first sight, it might look like the right-hand side of Definition 20 does not refer to any underlying logical system 𝑆 (and is thus fully generic in nature). However, recall that by Definition 2, it follows from the requirement that | 𝐹 | = 2 that there are 𝛼 , 𝛽 ∈ 𝐹 such that CD 𝑆 ( 𝛼 , 𝛽 ) , which does involve a reference to 𝑆 . Definition 20 is thus general but not generic in nature, because its right-hand side still (implicitly) refers to some underlying logical system 𝑆 (even though that system can be chosen arbitrarily). By contrast, the right-hand side of Theorem 3 does not refer to any underlying logical system 𝑆 whatsoever, and thus offers a fully generic characterization of the Aristotelian family of PCDs. (This contrast between official definitions and 𝐿 AD -characterizations will become even clearer when we are dealing with Aristotelian familiesterm of squares, hexagons, and octagons, because their official definitions refer much more explicitly to the underlying logical system 𝑆 ).

5.3. Characterizing the Two Aristotelian Familiesterm of Squares of Opposition Within the typology of Aristotelian diagramsterm, there exist exactly two families of squares of opposition: the classical squareterm and the degenerate squareterm; see Figure 4 [24,28,42]. The classical squareterm is by far the oldest and most well-known kind of Aristotelian diagramterm. In comparison to a classical squareterm, a degenerate squareterm has lost all Aristotelian relationsterm, except for the two relations of contradiction (which are required to be present by the very definition of Aristotelian diagramterm). Both families of squares are straightforwardly characterized in AD-logicterm.

Consider an Aristotelian diagramterm D for ( 𝐹 , 𝑆 ) . Then: 1. D is a square of oppositionterm iff | 𝐹 | = 4 , 2. D is a classical squareterm of opposition iff | 𝐹 | = 4 and there exist 𝛼 , 𝛽 ∈ 𝐹 such that 𝐶 𝑆 ( 𝛼 , 𝛽 ) , 3. D is a degenerate squareterm of opposition iff | 𝐹 | = 4 and there do not exist 𝛼 , 𝛽 ∈ 𝐹 such that 𝐶 𝑆 ( 𝛼 , 𝛽 ) .

Define the 𝐿 AD -formulas 𝜒 square : = 𝜒 4 , 𝜒 classical : = 𝜒 4 ∧ ⋄ 〈 𝐶 〉 ⊤ and 𝜒 degenerate : = 𝜒 4 ∧ ¬ ⋄ 〈 𝐶 〉 ⊤ . Then for any Aristotelian diagramterm D for ( 𝐹 , 𝑆 ) , we have: 1. D is a square of oppositionterm iff ⊨ 𝐷 𝜒 square , 2. D is a classical squareterm of opposition iff ⊨ 𝐷 𝜒 classical , 3. D is a degenerate squareterm of opposition iff ⊨ 𝐷 𝜒 degenerate .

Analogous to the proof of Theorem 3. For purposes of illustration, we prove the second item. For the left to right direction, suppose that D is a classical squareterm of opposition, and consider an arbitrary AD-frameterm 𝐹 = 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 that is based on D. By Definitions 13 and 21, it follows that | 𝑊 | = 4 and that there exist 𝑤 , 𝑣 ∈ 𝑊 such that 〈 𝑤 , 𝑣 〉 ∈ 𝑅 𝐶 . From | 𝑊 | = 4 , it follows by Lemma 10 that 𝐹 ⊨ 𝜒 4 . From 〈 𝑤 , 𝑣 〉 ∈ 𝑅 𝐶 , it follows that 𝐹 ⊨ ⋄ 〈 𝐶 〉 ⊤ . Hence, 𝐹 ⊨ 𝜒 4 ∧ ⋄ 〈 𝐶 〉 ⊤ , i.e., 𝐹 ⊨ 𝜒 classical .

For the right to left direction, suppose that ⊨ 𝐷 𝜒 classical and consider the canonical AD-frameterm 𝐹 𝐷 . By Lemma 4, it follows that 𝐹 𝐷 ⊨ 𝜒 classical , i.e., 𝐹 𝐷 ⊨ 𝜒 4 ∧ ⋄ 〈 𝐶 〉 ⊤ . From 𝐹 𝐷 ⊨ 𝜒 4 , it follows by Lemma 10 that | 𝐹 | = 4 . From 𝐹 𝐷 ⊨ ⋄ 〈 𝐶 〉 ⊤ , it follows that there exist 𝛼 , 𝛽 ∈ 𝐹 such that 𝐶 𝑆 ( 𝛼 , 𝛽 ) . By Definition 21, this means that D is a classical squareterm of opposition. □ Just like with the PCDs, let us have another look at Definition 21 and Theorem 4. Note that items 2 and 3 of Definition 21 are general but not generic in nature, because their right-hand sides still refer to some underlying logical system 𝑆 (even though that system can be chosen arbitrarily). By contrast, the right-hand sides of items 2 and 3 of Theorem 4 do not refer to any underlying logical system 𝑆 whatsoever, and thus offer fully generic characterizations of the Aristotelian familiesterm of classical and degenerate squaresterm. Entirely analogous remarks apply to the characterizations of Aristotelian familiesterm of hexagons and octagons in the remainder of this section (compare Definitions 22 and 23 with Theorems 5 and 6, respectively).

Next to characterizing the classical and degenerate squaresterm, we can also easily express in AD-logicterm that these two types of diagrams jointly constitute an exhaustive classification of the squares of opposition. To illustrate the versatility of AD-logicterm, we prove the two parts of Lemma 11 in different fashions: the first item is proved directly “within” AD-logicterm, while the second is proved by reducing it to the corresponding result in logical geometryterm. (If we had only considered the proof’s difficulty and length, it would have been more straightforward to prove both items directly within AD-logicterm).

The following hold: 1. 𝜒 square ≡ AD 𝜒 classical ∨ 𝜒 𝑑 𝑒 𝑔 𝑒 𝑛 𝑒 𝑟 𝑎 𝑡 𝑒 , i.e., 𝜒 square ⊨ AD 𝜒 classical ∨ 𝜒 𝑑 𝑒 𝑔 𝑒 𝑛 𝑒 𝑟 𝑎 𝑡 𝑒 and 𝜒 classical ∨ 𝜒 𝑑 𝑒 𝑔 𝑒 𝑛 𝑒 𝑟 𝑎 𝑡 𝑒 ⊨ AD 𝜒 square , 2. ⊨ AD ¬ ( 𝜒 classical ∧ 𝜒 𝑑 𝑒 𝑔 𝑒 𝑛 𝑒 𝑟 𝑎 𝑡 𝑒 ) .

For item 1, propositional reasoning yields 𝜒 classical ∨ 𝜒 𝑑 𝑒 𝑔 𝑒 𝑛 𝑒 𝑟 𝑎 𝑡 𝑒 = ( 𝜒 4 ∧ ⋄ 〈 𝐶 〉 ⊤ ) ∨ ( 𝜒 4 ∧ ¬ ⋄ 〈 𝐶 〉 ⊤ ) ≡ AD 𝜒 4 ∧ ( ⋄ 〈 𝐶 〉 ⊤ ∨ ¬ ⋄ 〈 𝐶 〉 ⊤ ) ≡ AD 𝜒 4 ∧ ⊤ ≡ AD 𝜒 4 = 𝜒 square .

For item 2, consider an arbitrary AD-frameterm F and suppose, toward a contradiction, that 𝐹 ⊨ 𝜒 classical ∧ 𝜒 𝑑 𝑒 𝑔 𝑒 𝑛 𝑒 𝑟 𝑎 𝑡 𝑒 . It follows that 𝐹 ⊨ 𝜒 4 , so by Lemma 10, F is finite, and by Lemma 8, there exists an Aristotelian diagramterm D such that F is modally isomorphic to 𝐹 𝐷 . Since modal isomorphisms preserve frame validity, it follows from 𝐹 ⊨ 𝜒 classical that 𝐹 𝐷 ⊨ 𝜒 classical , and, by Lemma 5, that 𝐹 ′ ⊨ 𝜒 classical for every AD-frameterm 𝐹 ′ that is based on D. By Definition 14, this means that ⊨ 𝐷 𝜒 classical , so by Theorem 4, it follows that D is a classical squareterm of opposition. In exactly the same way, it follows from 𝐹 ⊨ 𝜒 degenerate that D is a degenerate squareterm of opposition. However, this is impossible, since by Definition 21, a diagram cannot simultaneously be a classical and a degenerate squareterm of opposition. □ Note that the formula 𝜒 classical contains the global modalityterm, ⋄, both in its left conjunct 𝜒 4 and in its right conjuct ⋄ 〈 𝐶 〉 ⊤ . However, if one prefers to work without the global modalityterm (e.g., because one adheres to the credo that modal logic should be local; see [40], p. ix) and is prepared to put the cardinality condition in the metalanguage instead of in 𝐿 AD , then we can characterize classical squaresterm of opposition without the global modalityterm altogether. In particular, we have to replace ⋄ 〈 𝐶 〉 ⊤ with the disjunction 〈 𝐶 〉 ⊤ ∨ 〈 SC 〉 ⊤ . (Entirely analogous remarks apply to 𝜒 degenerate ).

Consider an Aristotelian diagramterm D for ( 𝐹 , 𝑆 ) and suppose that | 𝐹 | = 4 . Then D is a classical squareterm of opposition iff ⊨ 𝐷 〈 𝐶 〉 ⊤ ∨ 〈 SC 〉 ⊤ .

For the left to right direction, suppose that D is a classical squareterm of opposition, and consider an arbitrary AD-frameterm 𝐹 = ( 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 ) that is based on D. By Definitions 13 and 21, it follows that | 𝑊 | = 4 and that there exist 𝑤 , 𝑣 ∈ 𝑊 such that 〈 𝑤 , 𝑣 〉 ∈ 𝑅 𝐶 (and thus also 〈 𝑣 , 𝑤 〉 ∈ 𝑅 𝐶 , by the symmetry of 𝑅 𝐶 ). By the seriality and functionality of 𝑅 𝐶 𝐷 , there exist unique 𝑤 ′ , 𝑣 ′ ∈ 𝑊 such that 〈 𝑤 , 𝑤 ′ 〉 , 〈 𝑣 , 𝑣 ′ 〉 ∈ 𝑅 𝐶 𝐷 . By the irreflexivity of 𝑅 𝐶 𝐷 and 𝑅 𝐶 , it follows that 𝑥 ≠ 𝑦 for all 𝑥 , 𝑦 ∈ { 𝑤 , 𝑣 , 𝑤 ′ , 𝑣 ′ } , so since | 𝑊 | = 4 , it follows that 𝑊 = { 𝑤 , 𝑣 , 𝑤 ′ , 𝑣 ′ } . Consider an arbitrary valuation V on F and assignment g on 〈 𝐹 , 𝑉 〉 . Since 〈 𝑤 , 𝑣 〉 , 〈 𝑣 , 𝑤 〉 ∈ 𝑅 𝐶 , we have 〈 𝐹 , 𝑉 〉 , 𝑔 , 𝑥 ⊨ 〈 𝐶 〉 ⊤ for 𝑥 ∈ { 𝑤 , 𝑣 } , and 〈 𝐹 , 𝑉 〉 , 𝑔 , 𝑥 ⊨ 〈 SC 〉 ⊤ for 𝑥 ∈ { 𝑤 ′ , 𝑣 ′ } . Since 𝑊 = { 𝑤 , 𝑣 , 𝑤 ′ , 𝑣 ′ } , it follows that 𝐹 ⊨ 〈 𝐶 〉 ⊤ ∨ 〈 SC 〉 ⊤ , as desired.

For the right to left direction, suppose that ⊨ 𝐷 〈 𝐶 〉 ⊤ ∨ 〈 SC 〉 ⊤ , and consider the canonical AD-frameterm 𝐹 𝐷 . By Lemma 4, it follows that 𝐹 𝐷 ⊨ 〈 𝐶 〉 ⊤ ∨ 〈 SC 〉 ⊤ . Consider an arbitrary valuation V on 𝐹 𝐷 and assignment g on 〈 𝐹 𝐷 , 𝑉 〉 , and a world 𝛼 ∈ 𝐹 . We thus have 〈 𝐹 𝐷 , 𝑉 〉 , 𝑔 , 𝛼 ⊨ 〈 𝐶 〉 ⊤ ∨ 〈 SC 〉 ⊤ . On the one hand, if 〈 𝐹 𝐷 , 𝑉 〉 , 𝑔 , 𝛼 ⊨ 〈 𝐶 〉 ⊤ , then there exists 𝛽 ∈ 𝐹 such that 𝐶 𝑆 ( 𝛼 , 𝛽 ) . On the other hand, if 〈 𝐹 𝐷 , 𝑉 〉 , 𝑔 , 𝛼 ⊨ 〈 SC 〉 ⊤ , then there exists 𝛽 ∈ 𝐹 such that SC 𝑆 ( 𝛼 , 𝛽 ) . By Definitions 1 and 2, there exist 𝛾 , 𝛿 ∈ 𝐹 such that 𝛾 ≡ 𝑆 ¬ 𝛼 , 𝛿 ≡ 𝑆 ¬ 𝛽 and 𝐶 𝑆 ( 𝛾 , 𝛿 ) . In both cases, we find, by Definition 21, that D is a classical squareterm of opposition. □ 5.4. Characterizing the Five Aristotelian Familiesterm of the Hexagons of Opposition One can show that there are exactly five families of hexagons of opposition: the Jacoby–Sesmat–Blanché (JSB) hexagon, the Sherwood–Czeżowski (SC) hexagon, and the unconnected-n (U-n) hexagon for 𝑛 ∈ { 4 , 8 , 12 } (see Figure 5 and Figure 6) [42]. The JSB hexagons are named after Jacoby [43], Sesmat [44], and Blanché [45], and the SC hexagons after William of Sherwood [46] and Czeżowski [47]. The U4, U8, and U12 hexagons are less well-known, and are named after the number of pairs of unconnected formulas that they contain. (Recall that two formulas are said to be unconnected iff they do not stand in any Aristotelian relationterm to each other.) Once again, all families of hexagons are straightforwardly characterized in AD-logicterm.

Consider an Aristotelian diagramterm D for ( 𝐹 , 𝑆 ) . Then: 1. D is a hexagon of opposition iff | 𝐹 | = 6 , 2. D is a JSB hexagon iff | 𝐹 | = 6 and there exist 𝛼 , 𝛽 , 𝛾 ∈ 𝐹 such that 𝐶 𝑆 ( 𝛼 , 𝛽 ) , 𝐶 𝑆 ( 𝛼 , 𝛾 ) and 𝐶 𝑆 ( 𝛽 , 𝛾 ) , 3. D is an SC hexagon iff | 𝐹 | = 6 and there exist 𝛼 , 𝛽 , 𝛾 , 𝛾 ′ ∈ 𝐹 such that 𝐶 𝑆 ( 𝛼 , 𝛽 ) , 𝐶 𝑆 ( 𝛼 , 𝛾 ′ ) , 𝐶 𝑆 ( 𝛽 , 𝛾 ) and CD 𝑆 ( 𝛾 , 𝛾 ′ ) , 4. D is a U4 hexagon iff | 𝐹 | = 6 and there exist 𝛼 , 𝛽 , 𝛾 ∈ 𝐹 such that 𝐶 𝑆 ( 𝛼 , 𝛾 ) and 𝐶 𝑆 ( 𝛽 , 𝛾 ) , and for all 𝛿 , 𝜀 ∈ 𝐹 , if 𝐶 𝑆 ( 𝛿 , 𝜀 ) , then { 𝛿 , 𝜀 } ∈ { { 𝛼 , 𝛾 } , { 𝛽 , 𝛾 } } , 5. D is a U8 hexagon iff | 𝐹 | = 6 and there exist 𝛼 , 𝛽 ∈ 𝐹 such that 𝐶 𝑆 ( 𝛼 , 𝛽 ) , and for all 𝛿 , 𝜀 ∈ 𝐹 , if 𝐶 𝑆 ( 𝛿 , 𝜀 ) , then { 𝛿 , 𝜀 } = { 𝛼 , 𝛽 } , 6. D is a U12 hexagon iff | 𝐹 | = 6 and there do not exist 𝛼 , 𝛽 ∈ 𝐹 such that 𝐶 𝑆 ( 𝛼 , 𝛽 ) .

Define the following 𝐿 AD -formulas: 1. 𝜒 hexagon : = 𝜒 6 , 2. 𝜒 JSB : = 𝜒 6 ∧ ⋄ ↓ 𝑥 ( 〈 𝐶 〉 〈 𝐶 〉 〈 𝐶 〉 𝑥 ) , 3. 𝜒 SC : = 𝜒 6 ∧ ⋄ ↓ 𝑥 ( 〈 𝐶 〉 ↓ 𝑦 ( [ 𝐶 ] ( 𝑥 ∧ 〈 𝐶 〉 ( ¬ 𝑦 ∧ ↓ 𝑧 ( 〈 𝐶 〉 ( 〈 CD 〉 𝑦 ∧ [ 𝐶 ] 𝑧 ) ) ) ) ) ) , 4. 𝜒 𝑈 4 : = 𝜒 6 ∧ ⋄ ↓ 𝑥 ( 〈 𝐶 〉 ↓ 𝑦 ( [ 𝐶 ] ( 𝑥 ∧ 〈 𝐶 〉 ( ¬ 𝑦 ∧ [ 𝐶 ] 𝑥 ) ) ) ) , 5. 𝜒 𝑈 8 : = 𝜒 6 ∧ ⋄ ↓ 𝑥 ( 〈 𝐶 〉 ↓ 𝑦 ( [ 𝐶 ] ( 𝑥 ∧ [ 𝐶 ] 𝑦 ) ) ) , 6. 𝜒 𝑈 12 : = 𝜒 6 ∧ ¬ ⋄ 〈 𝐶 〉 ⊤ .

Then for any Aristotelian diagramterm D for ( 𝐹 , 𝑆 ) , we have: 1. D is a hexagon of opposition iff ⊨ 𝐷 𝜒 hexagon , 2. D is a JSB hexagon iff ⊨ 𝐷 𝜒 JSB , 3. D is an SC hexagon iff ⊨ 𝐷 𝜒 SC , 4. D is a U4 hexagon iff ⊨ 𝐷 𝜒 𝑈 4 , 5. D is a U8 hexagon iff ⊨ 𝐷 𝜒 𝑈 8 , 6. D is a U12 hexagon iff ⊨ 𝐷 𝜒 𝑈 12 .

This is analogous to the proofs of Theorems 3 and 4. For purposes of illustration, we prove the third item. For the left to right direction, suppose that D is an SC hexagon, and consider an arbitrary AD-frameterm 𝐹 = 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 that is based on D. By Definitions 13 and 22, it follows that | 𝑊 | = 6 and that there exist 𝑤 , 𝑣 , 𝑢 , 𝑢 ′ ∈ 𝑊 such that 〈 𝑤 , 𝑣 〉 , 〈 𝑤 , 𝑢 ′ 〉 , 〈 𝑣 , 𝑢 〉 ∈ 𝑅 𝐶 and 〈 𝑢 , 𝑢 ′ 〉 ∈ 𝑅 𝐶 𝐷 . If we let the state variables x, y and z get bound to the worlds w, 𝑢 ′ , and v, respectively, then it is easy to check that 𝐹 ⊨ ⋄ ↓ 𝑥 ( 〈 𝐶 〉 ↓ 𝑦 ( [ 𝐶 ] ( 𝑥 ∧ 〈 𝐶 〉 ( ¬ 𝑦 ∧ ↓ 𝑧 ( 〈 𝐶 〉 ( 〈 CD 〉 𝑦 ∧ [ 𝐶 ] 𝑧 ) ) ) ) ) ) . (Note that the world u does not get bound to any state variable; u is the world (i) that is 𝑅 𝐶 -reachable from (the world bound to) z, and (ii) at which 〈 CD 〉 𝑦 ∧ [ 𝐶 ] 𝑧 holds.) Furthermore, from | 𝑊 | = 6 it follows by Lemma 10 that 𝐹 ⊨ 𝜒 6 . In sum, we find that 𝐹 ⊨ 𝜒 SC .

For the right to left direction, suppose that ⊨ 𝐷 𝜒 SC , and consider the canonical AD-frameterm 𝐹 𝐷 . By Lemma 4, it follows that 𝐹 𝐷 ⊨ 𝜒 SC , i.e., 𝐹 𝐷 ⊨ 𝜒 6 ∧ ⋄ ↓ 𝑥 ( 〈 𝐶 〉 ↓ 𝑦 ( [ 𝐶 ] ( 𝑥 ∧ 〈 𝐶 〉 ( ¬ 𝑦 ∧ ↓ 𝑧 ( 〈 𝐶 〉 ( 〈 CD 〉 𝑦 ∧ [ 𝐶 ] 𝑧 ) ) ) ) ) ) . From 𝐹 𝐷 ⊨ 𝜒 6 , it follows by Lemma 10 that | 𝐹 | = 6 . From 𝐹 𝐷 ⊨ ⋄ ↓ 𝑥 ( 〈 𝐶 〉 ↓ 𝑦 ( [ 𝐶 ] ( 𝑥 ∧ 〈 𝐶 〉 ( ¬ 𝑦 ∧ ↓ 𝑧 ( 〈 𝐶 〉 ( 〈 CD 〉 𝑦 ∧ [ 𝐶 ] 𝑧 ) ) ) ) ) ) , it follows that there exist 𝛼 , 𝛽 , 𝛾 , 𝛾 ′ ∈ 𝐹 such that 𝐶 𝑆 ( 𝛼 , 𝛽 ) , 𝐶 𝑆 ( 𝛼 , 𝛾 ′ ) , 𝐶 𝑆 ( 𝛽 , 𝛾 ) , and CD 𝑆 ( 𝛾 , 𝛾 ′ ) . (Namely, 𝛼 , 𝛾 ′ and 𝛽 are the worlds that get bound to the state variables x, y, and z, respectively; 𝛾 does not get bound to any state variable, but is the world (i) that is 𝐶 𝑆 -reachable from (the world bound to) z and (ii) at which 〈 CD 〉 𝑦 ∧ [ 𝐶 ] 𝑧 holds.) By Definition 22, this means that D is an SC hexagon. □ Just as before, for some of these characterizing formulas, we can get rid of the global modalityterm, ⋄, if we are prepared to put the cardinality condition in the metalanguage instead of in 𝐿 AD . For example, in 𝜒 JSB , we have to replace ⋄ ↓ 𝑥 ( 〈 𝐶 〉 〈 𝐶 〉 〈 𝐶 〉 𝑥 ) with the disjunctive formula ↓ 𝑥 ( 〈 𝐶 〉 〈 𝐶 〉 〈 𝐶 〉 𝑥 ∨ 〈 SC 〉 〈 SC 〉 〈 SC 〉 𝑥 ) .

Consider an Aristotelian diagramterm D for ( 𝐹 , 𝑆 ) and suppose that | 𝐹 | = 6 . Then D is a JSB hexagon iff ⊨ 𝐷 ↓ 𝑥 ( 〈 𝐶 〉 〈 𝐶 〉 〈 𝐶 〉 𝑥 ∨ 〈 SC 〉 〈 SC 〉 〈 SC 〉 𝑥 ) .

This is analogous to the proof of Lemma 12. □ 5.5. Characterizing Some Aristotelian Familiesterm of Octagons of Opposition In the project of setting up a systematic typology of Aristotelian diagramsterm, it has been shown that there are exactly 18 families of octagons of opposition [42]. In this paper, we will not deal with all these families, but rather focus on some of the most well-known ones: the Moretti–Pellissier octagons [48,49], the Lenzen octagons [50,51,52], the Buridan octagons [53,54,55], the Beziau octagons [56,57], and the Keynes–Johnson octagons [58,59] (see Figure 7 and Figure 8). Once again, these families of octagons (and also the other ones, wintroduced the notion of an Aristotelian diagramhich we do not deal with in this paper) can straightforwardly be characterized in AD-logicterm.

Consider an Aristotelian diagramterm D for ( 𝐹 , 𝑆 ) . Then: 1. D is an octagon of opposition iff | 𝐹 | = 8 , 2. D is a Moretti–Pellissier octagon iff | 𝐹 | = 8 and there exist 𝛼 , 𝛽 , 𝛾 , 𝛿 ∈ 𝐹 such that 𝐶 𝑆 ( 𝛼 , 𝛽 ) , 𝐶 𝑆 ( 𝛼 , 𝛾 ) , 𝐶 𝑆 ( 𝛼 , 𝛿 ) , 𝐶 𝑆 ( 𝛽 , 𝛾 ) , 𝐶 𝑆 ( 𝛽 , 𝛿 ) and 𝐶 𝑆 ( 𝛾 , 𝛿 ) , 3. D is a Lenzen octagon iff | 𝐹 | = 8 and there exist 𝛼 , 𝛽 , 𝛾 , 𝛾 ′ , 𝛿 , 𝛿 ′ ∈ 𝐹 such that 𝐶 𝑆 ( 𝛼 , 𝛽 ) , 𝐶 𝑆 ( 𝛼 , 𝛾 ′ ) , 𝐶 𝑆 ( 𝛼 , 𝛿 ) , 𝐶 𝑆 ( 𝛽 , 𝛾 ) , 𝐶 𝑆 ( 𝛽 , 𝛿 ′ ) , 𝐶 𝑆 ( 𝛾 , 𝛿 ) , CD 𝑆 ( 𝛾 , 𝛾 ′ ) , and CD 𝑆 ( 𝛿 , 𝛿 ′ ) , 4. D is a Buridan octagon iff | 𝐹 | = 8 and there exist 𝛼 , 𝛽 , 𝛾 , 𝛾 ′ , 𝛿 , 𝛿 ′ ∈ 𝐹 such that 𝐶 𝑆 ( 𝛼 , 𝛽 ) , 𝐶 𝑆 ( 𝛼 , 𝛾 ′ ) , 𝐶 𝑆 ( 𝛼 , 𝛿 ) , 𝐶 𝑆 ( 𝛽 , 𝛾 ) , 𝐶 𝑆 ( 𝛽 , 𝛿 ′ ) , CD 𝑆 ( 𝛾 , 𝛾 ′ ) and CD 𝑆 ( 𝛿 , 𝛿 ′ ) , and for all 𝜀 , 𝜁 ∈ 𝐹 , if 𝐶 𝑆 ( 𝜀 , 𝜁 ) then { 𝜀 , 𝜁 } ∈ { { 𝛼 , 𝛽 } , { 𝛼 , 𝛾 ′ } , { 𝛼 , 𝛿 } , { 𝛽 , 𝛾 } , { 𝛽 , 𝛿 ′ } } , 5. D is a Beziau octagon iff | 𝐹 | = 8 and there exist 𝛼 , 𝛽 , 𝛾 , 𝛿 , 𝛿 ′ ∈ 𝐹 such that 𝐶 𝑆 ( 𝛼 , 𝛽 ) , 𝐶 𝑆 ( 𝛼 , 𝛾 ) , 𝐶 𝑆 ( 𝛼 , 𝛿 ) , 𝐶 𝑆 ( 𝛽 , 𝛾 ) , 𝐶 𝑆 ( 𝛽 , 𝛿 ′ ) and CD 𝑆 ( 𝛿 , 𝛿 ′ ) , and for all 𝜀 , 𝜁 ∈ 𝐹 , if 𝐶 𝑆 ( 𝜀 , 𝜁 ) then { 𝜀 , 𝜁 } ∈ { { 𝛼 , 𝛽 } , { 𝛼 , 𝛾 } , { 𝛼 , 𝛿 } , { 𝛽 , 𝛾 } , { 𝛽 , 𝛿 ′ } } , 6. D is a Keynes–Johnson octagon iff | 𝐹 | = 8 and there exist 𝛼 , 𝛽 , 𝛾 , 𝛿 ∈ 𝐹 such that 𝐶 𝑆 ( 𝛼 , 𝛽 ) , 𝐶 𝑆 ( 𝛼 , 𝛿 ) , 𝐶 𝑆 ( 𝛽 , 𝛾 ) and 𝐶 𝑆 ( 𝛾 , 𝛿 ) , and for all 𝜀 , 𝜁 ∈ 𝐹 , if 𝐶 𝑆 ( 𝜀 , 𝜁 ) , then { 𝜀 , 𝜁 } ∈ { { 𝛼 , 𝛽 } , { 𝛼 , 𝛿 } , { 𝛽 , 𝛾 } , { 𝛾 , 𝛿 } } .

Define the following 𝐿 AD -formulas: 1. 𝜒 octagon : = 𝜒 8 , 2. 𝜒 MorPel : = 𝜒 8 ∧ ⋄ ↓ 𝑥 ( 〈 𝐶 〉 ↓ 𝑦 ( 〈 𝐶 〉 ( ¬ 𝑥 ∧ 〈 𝐶 〉 𝑥 ∧ 〈 𝐶 〉 ( ¬ 𝑥 ∧ ¬ 𝑦 ∧ 〈 𝐶 〉 𝑥 ∧ 〈 𝐶 〉 𝑦 ) ) ) ) , 3. 𝜒 Lenzen : = 𝜒 8 ∧ ⋄ ↓ 𝑥 ( 〈 𝐶 〉 [ 𝐶 ] 𝑥 ∧ 〈 𝐶 〉 ↓ 𝑦 ( 〈 𝐶 〉 [ 𝐶 ] 𝑦 ∧ 〈 𝐶 〉 ( ¬ 𝑥 ∧ [ 𝐶 ] ¬ 𝑥 ∧ 〈 𝐶 〉 ( ¬ 𝑥 ∧ ¬ 𝑦 ∧ [ 𝐶 ] ¬ 𝑦 ∧ 〈 𝐶 〉 𝑥 ) ) ) ) , 4. 𝜒 Buridan : = 𝜒 8 ∧ ⋄ ↓ 𝑥 ( 〈 𝐶 〉 ↓ 𝑦 ( [ 𝐶 ] ( 𝑥 ∧ 〈 𝐶 〉 ( ¬ 𝑦 ∧ ↓ 𝑧 ( [ 𝐶 ] ( 𝑥 ∧ 〈 𝐶 〉 ↓ 𝑥 2 ( 〈 𝐶 〉 ( 〈 CD 〉 𝑧 ∧ [ 𝐶 ] ( 𝑥 2 ∧ 〈 𝐶 〉 ( 〈 CD 〉 𝑦 ∧ [ 𝐶 ] 𝑥 2 ) ) ) ) ) ) ) ) ) ) , 5. 𝜒 Beziau : = 𝜒 8 ∧ ⋄ ↓ 𝑥 ( 〈 𝐶 〉 ↓ 𝑦 ( [ 𝐶 ] ( 𝑥 ∧ 〈 𝐶 〉 ↓ 𝑧 ( 〈 𝐶 〉 〈 𝐶 〉 𝑥 ∧ 〈 𝐶 〉 ( 〈 CD 〉 𝑦 ∧ [ 𝐶 ] 𝑧 ) ) ) ) ) , 6. 𝜒 KeyJo : = 𝜒 8 ∧ ⋄ ↓ 𝑥 ( 〈 𝐶 〉 ↓ 𝑦 ( 〈 𝐶 〉 ( ¬ 𝑥 ∧ [ 𝐶 ] ¬ 𝑥 ∧ 〈 𝐶 〉 ( ¬ 𝑥 ∧ ¬ 𝑦 ∧ [ 𝐶 ] ¬ 𝑦 ∧ 〈 𝐶 〉 𝑥 ) ) ) ) .

Then for any Aristotelian diagramterm D for ( 𝐹 , 𝑆 ) , we have: 1. D is an octagon of opposition iff ⊨ 𝐷 𝜒 octagon , 2. D is a Moretti–Pellissier octagon iff ⊨ 𝐷 𝜒 MorPel , 3. D is a Lenzen octagon iff ⊨ 𝐷 𝜒 Lenzen , 4. D is a Buridan octagon iff ⊨ 𝐷 𝜒 Buridan , 5. D is a Beziau octagon iff ⊨ 𝐷 𝜒 Beziau , 6. D is a Keynes–Johnson octagon iff ⊨ 𝐷 𝜒 KeyJo .

This is analogous to the proofs of Theorems 3–5. For purposes of illustration, we prove the fifth item. For the left to right direction, suppose that D is a Beziau octagon, and consider an arbitrary AD-frameterm 𝐹 = 〈 𝑊 , 𝑅 𝐶 𝐷 , 𝑅 𝐶 〉 that is based on D. By Definitions 13 and 23, it follows that | 𝑊 | = 8 and that there exist 𝑤 , 𝑣 , 𝑢 , 𝑠 , 𝑠 ′ ∈ 𝑊 such that 〈 𝑤 , 𝑣 〉 , 〈 𝑤 , 𝑢 〉 , 〈 𝑤 , 𝑠 〉 , 〈 𝑣 , 𝑢 〉 , 〈 𝑣 , 𝑠 ′ 〉 ∈ 𝑅 𝐶 and 〈 𝑠 , 𝑠 ′ 〉 ∈ 𝑅 𝐶 𝐷 , and for all 𝑟 , 𝑡 ∈ 𝑊 , if 〈 𝑟 , 𝑡 〉 ∈ 𝑅 𝐶 , then { 𝑟 , 𝑡 } ∈ { { 𝑤 , 𝑣 } , { 𝑤 , 𝑢 } , { 𝑤 , 𝑠 } , { 𝑣 , 𝑢 } , { 𝑣 , 𝑠 ′ } } . If we let the state variables x, y and z get bound to the worlds w, s and v, respectively, then it is easy to check that 𝐹 ⊨ ⋄ ↓ 𝑥 ( 〈 𝐶 〉 ↓ 𝑦 ( [ 𝐶 ] ( 𝑥 ∧ 〈 𝐶 〉 ↓ 𝑧 ( 〈 𝐶 〉 〈 𝐶 〉 𝑥 ∧ 〈 𝐶 〉 ( 〈 CD 〉 𝑦 ∧ [ 𝐶 ] 𝑧 ) ) ) ) ) . (Note that the worlds u and 𝑠 ′ do not get bound to any state variables; these two worlds are 𝑅 𝐶 -reachable from (the world bound to) z. At u, it holds that 〈 𝐶 〉 𝑥 , and at 𝑠 ′ , it holds that 〈 CD 〉 𝑦 ∧ [ 𝐶 ] 𝑧 .) Furthermore, from | 𝑊 | = 8 , it follows by Lemma 10 that 𝐹 ⊨ 𝜒 8 . In sum, we find that 𝐹 ⊨ 𝜒 Beziau .

For the right to left direction, suppose that ⊨ 𝐷 𝜒 Beziau , and consider the canonical AD-frameterm 𝐹 𝐷 . By Lemma 4, it follows that 𝐹 𝐷 ⊨ 𝜒 Beziau , i.e., 𝐹 𝐷 ⊨ 𝜒 8 ∧ ⋄ ↓ 𝑥 ( 〈 𝐶 〉 ↓ 𝑦 ( [ 𝐶 ] ( 𝑥 ∧ 〈 𝐶 〉 ↓ 𝑧 ( 〈 𝐶 〉 〈 𝐶 〉 𝑥 ∧ 〈 𝐶 〉 ( 〈 CD 〉 𝑦 ∧ [ 𝐶 ] 𝑧 ) ) ) ) ) . From 𝐹 𝐷 ⊨ 𝜒 8 , it follows by Lemma 10 that | 𝐹 | = 8 . From 𝐹 𝐷 ⊨ ⋄ ↓ 𝑥 ( 〈 𝐶 〉 ↓ 𝑦 ( [ 𝐶 ] ( 𝑥 ∧ 〈 𝐶 〉 ↓ 𝑧 ( 〈 𝐶 〉 〈 𝐶 〉 𝑥 ∧ 〈 𝐶 〉 ( 〈 CD 〉 𝑦 ∧ [ 𝐶 ] 𝑧 ) ) ) ) ) , it follows that there exist 𝛼 , 𝛽 , 𝛾 , 𝛿 , 𝛿 ′ ∈ 𝐹 such that 𝐶 𝑆 ( 𝛼 , 𝛽 ) , 𝐶 𝑆 ( 𝛼 , 𝛾 ) , 𝐶 𝑆 ( 𝛼 , 𝛿 ) , 𝐶 𝑆 ( 𝛽 , 𝛾 ) , 𝐶 𝑆 ( 𝛽 , 𝛿 ′ ) and CD 𝑆 ( 𝛿 , 𝛿 ′ ) , and that there are no other pairs of 𝑆 -contrary formulas in 𝐹 , apart from the aforementioned ones. (Namely, 𝛼 , 𝛿 and 𝛽 are the worlds that get bound to the state variables x, y, and z, respectively. The worlds 𝛾 and 𝛿 ′ do not get bound to any state variables: these two worlds are 𝐶 𝑆 -reachable from (the world bound to) z. At 𝛾 , it holds that 〈 𝐶 〉 𝑥 , and at 𝛿 ′ , it holds that 〈 CD 〉 𝑦 ∧ [ 𝐶 ] 𝑧 .) By Definition 23, this means that D is a Beziau hexagon. □ 6. Aristotelian Diagramsterm for AD-Logicterm In Section 2, we introduced the notion of an Aristotelian diagramterm for a fragment of formulas 𝐹 ⊆ 𝐿 𝑆 , relative to some logical system 𝑆 . For example, we can take 𝑆 to be some system of modal logic, and thus study Aristotelian diagramsterm for modal logic; for example, recall the classical squareterm of opposition for KD in Figure 1b. Next, in Section 3, Section 4 and Section 5, we presented the system of AD-logicterm. This gives rise to a modal consequence relationterm ⊨ AD , and can thus be viewed as the modal logic of Aristotelian diagramsterm.

Already in the opening paragraphs of this paper, we drew a sharp distinction between these two approaches. More concretely, we distinguished the system of AD-logicterm from the underlying logic 𝑆 of some Aristotelian diagramterm; recall the notational convention introduced at the end of Section 3.1: 𝛼 , 𝛽 , 𝛾 ⋯ as metavariables over 𝐿 𝑆 versus 𝜑 , 𝜒 , 𝜓 ⋯ as metavariables over 𝐿 AD . This distinction was, and still remains, important in order to avoid significant confusions. However, on a strictly technical level, there is no reason why we cannot take the underlying logic 𝑆 of our Aristotelian diagramsterm to be the system of AD-logicterm itself. In light of the results of Section 5, this might even be a very fruitful idea. In this way, we thus end up studying Aristotelian diagramsterm for AD-logicterm, or, putting together the two aforementioned italicized expressions: Aristotelian diagramsterm for the modal logic of Aristotelian diagramsterm.

In this section, we briefly illustrate the viability and fruitfulness of this idea by means of a concrete example. Recall the formulas 𝜒 square , 𝜒 classical , 𝜒 degenerate ∈ 𝐿 AD that were introduced and studied in Section 5. Since the language 𝐿 AD is closed under negation, we also have ¬ 𝜒 square , ¬ 𝜒 classical , ¬ 𝜒 degenerate ∈ 𝐿 AD . Hence, we can define the following fragment of 𝐿 AD -formulas: 𝐹 AD : = { 𝜒 square , 𝜒 classical , 𝜒 degenerate , ¬ 𝜒 square , ¬ 𝜒 classical , ¬ 𝜒 degenerate } ⊆ 𝐿 AD .

We clearly have all the ingredients at our disposal for defining an Aristotelian diagramterm (see Definition 2). First of all, note that AD-logicterm is a logical system with Boolean operators and a model–theoretic semantics ⊨ AD . Secondly, the fragment 𝐹 AD ⊆ 𝐿 AD is non-empty, and moreover: The fragment 𝐹 AD satisfies the following properties: 1. for every 𝜒 ∈ 𝐹 AD , there is a 𝜒 ′ ∈ 𝐹 \ { 𝜒 } such that ⊨ AD 𝜒 ′ ↔ ¬ 𝜒 , 2. for every 𝜒 ∈ 𝐹 AD , there is no 𝜒 ′ ∈ 𝐹 \ { 𝜒 } such that ⊨ AD 𝜒 ′ ↔ 𝜒 , 3. there is no 𝜒 ∈ 𝐹 AD such that ⊨ AD 𝜒 or ⊨ AD ¬ 𝜒 .

Item 1 follows trivially from the definition of 𝐹 AD . For item 2, we show that 𝜒 square and 𝜒 classical are not AD-equivalent to each other (all other cases are analogous). Consider some degenerate squareterm of opposition D. By Definition 21, D is a square of oppositionterm but not a classical squareterm. By Theorem 4, it follows that ⊨ 𝐷 𝜒 square and ⊭ 𝐷 𝜒 classical . Hence, there exists an AD-frameterm F that is based on D such that 𝐹 ⊭ 𝜒 classical and 𝐹 ⊨ 𝜒 square .

For item 3, we show that 𝜒 classical is AD-contingent, i.e., ⊭ AD 𝜒 classical and ⊭ AD ¬ 𝜒 classical (all other cases are analogous). Consider some degenerate squareterm D and some classical squareterm 𝐷 ′ . By Definition 21 and Theorem 4, it follows that ⊭ 𝐷 𝜒 classical and ⊨ 𝐷 ′ 𝜒 classical . From ⊭ 𝐷 𝜒 classical , it follows that there exists an AD-frameterm F that is based on D such that 𝐹 ⊭ 𝜒 classical (and thus ⊭ AD 𝜒 classical ). From ⊨ 𝐷 ′ 𝜒 classical , it follows that 𝐹 𝐷 ′ ⊨ 𝜒 classical (and thus ⊭ AD ¬ 𝜒 classical ). □ It remains to be determined what the Aristotelian diagramterm for ( 𝐹 AD , ⊨ AD ) looks like exactly, i.e., which Aristotelian family it belongs to. This is straightforward to check: The following hold: 1. ⊨ AD ¬ ( 𝜒 classical ∧ 𝜒 𝑑 𝑒 𝑔 𝑒 𝑛 𝑒 𝑟 𝑎 𝑡 𝑒 ) , 2. ⊭ AD 𝜒 classical ∨ 𝜒 degenerate , 3. ⊨ AD ¬ ( 𝜒 classical ∧ ¬ 𝜒 𝑠 𝑞 𝑢 𝑎 𝑟 𝑒 ) , 4. ⊭ AD 𝜒 classical ∨ ¬ 𝜒 square , 5. ⊨ AD ¬ ( 𝜒 degenerate ∧ ¬ 𝜒 𝑠 𝑞 𝑢 𝑎 𝑟 𝑒 ) , 6. ⊭ AD 𝜒 degenerate ∨ ¬ 𝜒 square .

These are all easy exercises in reasoning about AD-framesterm. Note that item 1 has already been proved above, as item 2 of Lemma 11. □ Items 1–2 of Lemma 15 state that 𝜒 classical and 𝜒 degenerate are contrary to each other in AD-logicterm (see Definition 1), which we abbreviate as 𝐶 AD ( 𝜒 classical , 𝜒 degenerate ) . Completely analogously, items 3–4 state that 𝐶 AD ( 𝜒 classical , ¬ 𝜒 square ) , and items 5–6 state that 𝐶 AD ( 𝜒 degenerate , ¬ 𝜒 square ) . Since | 𝐹 AD | = 6 , it follows by Definition 22 that the Aristotelian diagramterm for ( 𝐹 AD , ⊨ AD ) is a JSB hexagon, as shown in Figure 9.

We finish this section by making three comments about this JSB hexagon for AD-logicterm, in increasing order of conceptual importance. First of all, recall that it is common in logical geometryterm to distinguish two subtypes of JSB hexagons, viz., strong and weak [28]. In general, given a JSB hexagon H for ( 𝐹 , 𝑆 ) with 𝐶 𝑆 ( 𝛼 , 𝛽 ) , 𝐶 𝑆 ( 𝛼 , 𝛾 ) and 𝐶 𝑆 ( 𝛽 , 𝛾 ) , we say that H is a strong JSB hexagon iff ⊨ 𝑆 𝛼 ∨ 𝛽 ∨ 𝛾 and that H is a weak JSB hexagon iff ⊭ 𝑆 𝛼 ∨ 𝛽 ∨ 𝛾 . With this definition in mind, it is easy to check that the hexagon for ( 𝐹 AD , ⊨ AD ) , as shown in Figure 9, is a strong JSB hexagon, since it follows from Lemma 11 that ⊨ AD 𝜒 classical ∨ 𝜒 degenerate ∨ ¬ 𝜒 square .

Secondly, next to the standard research on Aristotelian diagramsterm for (formulas coming from) the object language 𝐿 𝑆 of some logical system 𝑆 , there is also a flourishing tradition of studying Aristotelian diagramsterm for metalogical notions [25,60,61,62,63,64,65]. For example, given a logic 𝑆 , we can say that the Aristotelian relationsterm of 𝑆 -contrariety and 𝑆 -subcontrariety are themselves contrary to each other (since two 𝐿 𝑆 -formulas cannot simultaneously be 𝑆 -contraries and 𝑆 -subcontraries, while they can be neither 𝑆 -contraries nor 𝑆 -subcontraries, e.g., when they are 𝑆 -contradictories). From this perspective, the JSB hexagon for ( 𝐹 AD , ⊨ AD ) , as shown in Figure 9, is simultaneously an object-level and a meta-level Aristotelian diagramterm. On the one hand, this hexagon is situated at the object level, because it is concerned with formulas such as 𝜒 classical and 𝜒 degenerate , which come from the object language 𝐿 AD of AD-logicterm. On the other hand, this hexagon is, at the same time, situated at the meta-level as well, because of the correspondence results established in Section 5. For example, 𝐶 AD ( 𝜒 classical , 𝜒 degenerate ) means that the Aristotelian familiesterm of classical and degenerate squaresterm are contrary to each other (since an Aristotelian diagramterm cannot simultaneously be a classical and a degenerate squareterm, while it can be neither a classical nor a degenerate squareterm, e.g., when it is a PCD).

Finally, and perhaps most subtly, note that because of their specific setup, Aristotelian diagramsterm for AD-logicterm can simultaneously contain and validate a given formula. Concretely, let us write D to refer to the JSB hexagon in Figure 9, and consider the formula ¬ 𝜒 square . On the one hand, we have ¬ 𝜒 square ∈ 𝐹 AD and, thus, the formula ¬ 𝜒 square occurs insideD when D is viewed as an Aristotelian diagramterm for ( 𝐹 AD , ⊨ AD ) . On the other hand, D is a JSB hexagon, and thus not a square, which means that ⊨ 𝐷 ¬ 𝜒 square , i.e., the formula ¬ 𝜒 square is validated byD, when D is viewed as an AD-frameterm. It bears emphasizing that there is nothing paradoxical or inconsistent about this situation. Nevertheless, we do acknowledge that this can quickly get very confusing, and that is precisely the reason why we postponed discussing Aristotelian diagramsterm for AD-logicterm until this section, at the very end of the paper.

7. Conclusions In this paper, we developed the system of AD-logicterm, i.e., the (hybrid) modal logic of Aristotelian diagramsterm. We established a sound and strongly complete axiomatizationterm for AD-logicterm, and proved that there exists a bijection between finite Aristotelian diagramsterm (up to Aristotelian isomorphismterm) and finite AD-framesterm (up to modal isomorphism). This means that the properties of AD-framesterm are sufficient to derive all structural properties of Aristotelian diagramsterm. We then showed how AD-logicterm can capture several major results from logical geometryterm; for example, for every well-known Aristotelian family A, we exhibited a formula 𝜒 𝐴 ∈ 𝐿 AD and showed that an Aristotelian diagramterm D belongs to the family A iff 𝜒 𝐴 is validated by D (when the latter is viewed as an AD-frameterm). These correspondence results do not refer to any underlying logical system, and thus offer fully generic characterizations of the Aristotelian familiesterm. Finally, we showed that AD-logicterm gives rise to interesting new Aristotelian diagramsterm, and we reflected on their profoundly peculiar status.

There are many avenues for future research. For example, continuing along the lines of Section 6, we can investigate further Aristotelian diagramsterm for AD-logicterm. In the context of Section 5, we can continue to formalize significant portions of logical geometryterm in AD-logicterm. For example, we can define characterizing formulas 𝜒 𝐴 ∈ 𝐿 AD for less well-known Aristotelian familiesterm A. More fundamentally, in logical geometryterm, we not only consider Aristotelian (families of) diagrams in isolation of each other, but also study how they are related to each other. For example, there is work on the notions of subdiagrams (e.g., in each JSB hexagon, three classical squaresterm of opposition can be embedded as subdiagrams) and complementarity (e.g., a JSB hexagon is complementary to a Buridan octagon, relative to an Aristotelian rhombic dodecahedron) [66,67,68]. Is AD-logicterm sufficiently expressive to formalize such relational claims as well?

Finally, we also need to consider what cannot be expressed in AD-logicterm. In particular, in the development of a systematic typology of Aristotelian diagramsterm, it has become clear that many (though not all) Aristotelian familiesterm can be divided into Boolean subfamilies; for example, there are two Boolean subfamilies of JSB hexagons (usually called “strong” and “weak”; we briefly encountered these in Section 6), there are three Boolean subfamilies of Buridan octagons, etc. These Boolean subfamilies cannot be expressed in AD-logicterm; for example, there do not exist any formulas 𝜒 strongJSB , 𝜒 weakJSB ∈ 𝐿 AD such that D is a strong JSB hexagon iff ⊨ 𝐷 𝜒 strongJSB and D is a weak JSB hexagon iff ⊨ 𝐷 𝜒 weakJSB . At first sight, this might appear to be a disadvantage or a limitation of AD-logicterm. However, one could also argue that this is exactly what we want, in order to keep AD-logicterm fully generic, i.e., independent of any underlying logic 𝑆 . For example, whether a JSB hexagon for ( 𝐹 , 𝑆 ) is strong or weak fundamentally depends on the underlying logic 𝑆 ; from the perspective of AD-logicterm, we do not (want to) have “access” to the entire logic 𝑆 , but only to the Aristotelian relationsterm CD 𝑆 and 𝐶 𝑆 that it gives rise to (via the abstract relations 𝑅 𝐶 𝐷 and 𝑅 𝐶 in the AD-framesterm). It is clear that more thorough reflection is needed regarding this subtle issue.