We investigate basic forms of inference involving modal notions and quantifiers, called modal categorical inferences. We do so by extending Quarc, a novel logic that assigns a primary role to quantified phrases, with modalities from the hexagon of opposition. We show that there are two possible readings of de dicto modalities (called symmetric and asymmetric, respectively), as opposed to the unique reading of de re modalities. We focus on the asymmetric reading of de dicto modalities and explore the logical relations that obtain between them. These are proven in a natural deduction system, accompanied by an appropriate syntax and semantics, and graphically represented via a dodecagon of opposition. Moreover, we show that the asymmetric reading, in contrast to the symmetric one, preserves all properties of the hexagon for basic modal notions. Thus, it provides a particularly attractive basis on which to further investigate quantified modal reasoning.
Many arguments in everyday reasoning involve an
interaction of modal notions and quantification . Representing these
arguments in a formal setting is known to be challenging,
as witnessed by the existence of a plethora of rival accounts
of quantified modal logic [
We call a modal categorical statement if: • it makes reference to two categories of individuals (e.g. and ), one of which is used as a domain of quantification ; • it contains one modality from a given family; • it does not make reference to specific individuals. A modal categorical inference is an inference from a statement 1 to a statement 2 s.t. both 1 and 2 qualify as modal categorical statements. It can also be seen as a simple argument consisting of one premise (1) and a conclusion (2). Here is an example: (∗) It’s necessary that every data controller is authorized to process user data. Therefore, it isn’t contingent that some data controller is authorized to process user data.
In (∗), 1 is the first sentence and 2 the second; they are separated by the conclusion marker ‘therefore’. The two categories of individuals correspond to the properties ‘is a data controller’ and ‘is authorized to process user data’;1 the modalities involved are ‘necessity’ (in 1) and ‘contingency’ (in 2). Inferences of this kind are involved in more complex arguments, ranging from patterns of syllogism (with two premises) to tree-like argumentative structures. Thus, understanding how modal categorical inferences work is crucial to generally assess arguments including modalities and quantification.
We will be concerned with modalities from the hexagon of opposition in Fig. 1. Something will be said to be: • necessary if it holds in all cases; • possible if it holds in some cases; • impossible if it holds in no cases; • avoidable if it does not hold in some cases; • contingent if it holds in some cases and it does not hold in other cases; • absolute if either it holds in all cases or it holds in no cases.
For further analysis of the hexagon, see e.g. [
(∗∗) I know whether all user accounts are secure.
Statement (∗∗) is compatible with the three options below: • I know that all user accounts are secure; • I know that some user accounts are secure and some aren’t; • I know that no user account is secure.
This compatibility is explained by the diference between knowing absoluteness necessity impossibility possibility avoidability contingency
In this work we are interested in both the formal and the
visual representation of modal categorical inferences. As far
as the visual representation is concerned, it is well-known
that polygons of opposition, which originated in medieval
works on Aristotle’s logic, facilitate the comprehension of
logical relations and are therefore regarded as cognitively
eficient devices for deductive reasoning [
As far as the formal representation is concerned, we want to employ a mathematical language that is as simple as possible and closely adheres to the structure of natural languages (in particular, English); thus, a language that is useful to move back and forth between formal and informal reasoning. In this regard, we can observe that the syntax of the Predicate Calculus (hereafter, PC) does not keep track of the fact that quantified phrases are used as arguments of predication in modal categorical statements. For instance, when we formalize argument (∗) following PC’s syntax,3 we need to render the first sentence as a construction involving material implication (→), namely:
◻∀(DataController() → Authorized()) Yet, there is no natural language expression corresponding to → in (∗). Moreover, due to the use of → and of the individual variable , we lose information about the fact that the quantified phrase ‘every data controller’ plays the role of argument of predication in (∗).
By contrast, the formalism that we are going to employ,
the Quantified Argument Calculus (shortened ‘Quarc’) [
(∀DataController)Authorized
whether and knowing that. While knowing that can be interpreted
as a form of necessity/impossibility (hence, a modality in the square
of opposition), knowing whether should be interpreted as a form of
absoluteness (hence, a modality not in the square of opposition).
3We stress that our idea of reducing many-ary predicates to unary
predicates does not play any role in this argument.
to formalize ‘every data controller is authorized to process
user data’.4 As shown in [
When we combine a modal notion and a quantifier in a
sentence, we distinguish between de re and de dicto
combinations.6 In the former, the modalization applies to (categories
of) individuals, whereas in the latter it applies to an entire
sub-sentence. Consider the diference between ‘someone is
known to rob banks in this area’ (de re) and ‘it is known that
someone robs banks in this area’ (de dicto). Only the former
statement, when uttered, conveys the information that we
are aware of the identity of the robber. For a discussion of
de re and de dicto combinations in modal PC, see [
Quarc keeps track of the distinction between de dicto and de re modalities as follows, where ◻ denotes necessity:
◻(∀DataController)Authorized
(∀DataController) ◻ Authorized
Modal versions of Quarc are contained in various works,
including [
The analysis of modal categorical inferences in Quarc
was first put forward in [
Below is the reading of de dicto combinations ofered in
[
However, in the symmetric reading modalities involving
negation are decomposed. Take VU (Avoidable Universality),
rendered as ◇∀¬ . The quantified phrase ∀ occurs
between ◇ and ¬ and thus, in a sense, the modality at issue
is not purely de dicto (i.e. about the statement): while ◇
applies to a statement, ¬ applies to a category of
individuals (predicate). Moreover, as a consequence of this, some
fundamental properties of hexagon modalities fail. For
instance, one would expect that something is avoidable if it is
not necessary. Yet, this does not hold under the symmetric
reading. Consider again VU in the list above: assuming
the standard duality of ◻ and ◇, we can see that VU is not
equivalent to ¬NU, namely ¬ ◻ ∀ , under the symmetric
reading. Summing up, the symmetry between de re and de
dicto combinations proposed in [
The alternative reading of de dicto combinations that we will propose in this article avoids the aforementioned problems. The main idea behind this reading is anticipating the occurrence of negation in a formula so that it always appears (if at all) immediately after a modal operator. We will call it the asymmetric reading (with respect to de re combinations), since it gives rise to a dodecagon of opposition that is highly diferent from the one in Fig. 2. The new dodecagon is illustrated later in our article, in Fig. 3, once the analysis of the asymmetric reading is carried out in rigorous terms.
CU
CP BP
BU
Our contribution paves the way to a systematic taxonomy of modal categorical inferences, which have not received much attention in the literature so far, despite their relevance for everyday reasoning. We conjecture that this might be due to the fact that PC is the underlying framework used by many researchers working in the area of modal logic and NU PP
PU NP VP IU
IP VU 48–59 that the main ingredients of a modal categorical statement require a more complex representation in modal PC.
The article is organized as follows. In sections 2 and 3 we introduce the syntax and the semantics of modal Quarc, respectively. Section 4 contains a natural deduction calculus to build proofs. In section 5, we illustrate the modal categorical inferences associated with the new reading of de dicto combinations, together with the corresponding dodecagon of opposition. Finally, section 6 indicates directions for future research.
We follow the basic set-up for the language of Quarc found
in [
Definition 2.1 (Language). The language ℒ consists of the following symbols: (a) Denumerably many singular arguments 1, 2, 3, .... (b) Denumerably many predicate symbols of arity 1, 1, 2, 3, .... (c) Connectives: ∧, ∨, →, ¬. (d) Quantifiers: ∀, ∃. (e) One modal operator: ◻.
(f) Auxiliary symbols: brackets ((, )).
Remark 2.1. We shall use , , , , etc. to denote arbitrary predicate symbols, and , , , etc. to denote arbitrary singular arguments. The lower case letter q will be used to denote either of the quantifiers. The set of singular arguments of ℒ shall be denoted by , whereas the set of predicate symbols will be denoted by .
Remark 2.2. Although singular arguments are not involved in categorical reasoning, they are needed to provide truthconditions for quantified statements, as we will see below. The requirement for denumerably many singular arguments is not a necessity, but would enable more straightforward soundness and completeness proofs. While these aspects are not relevant to the present investigation, we decided to define languages in this way for the purpose of presenting a logic that is functional beyond its applications in this paper.
Before defining the set of formulas, one further notion needs to be introduced.
Definition 2.2 (Quantified Arguments) . Let ∈ . The expressions ∀ and ∃ are called universally and particularly quantified arguments , respectively.
Definition 2.3 (Formulas). The set of ℒ -formulas is defined recursively as follows: (a) Basic formulas: Let ∈ and ∈ be given. Then is a basic formula. (b) Predicate negation: Let and be as in (a). Then, ¬ is a formula.7 (c) Connectives: If and are formulas, then so are ( ∨ ), ( ∧ ) and ( → ). If is a formula, then so is ¬. 7It is possible to extend both the syntax and the semantics to allow for ifnite strings of ◻ and ¬ in this position, but these are irrelevant for our purposes. (d) Modals: If is a formula, then so is ◻. (e) Governed formulas: Let () be a formula containing an occurrence of some ∈ , and let be a quantified argument. If there is no quantified argugoverned by that occurrence of . ment to the left of in (), and there is no (proper) substring in () s.t. is a formula which contains , then ︀( ⇑⌋︀ is a formula. It is said to be (f) Nothing else is a formula.
The notion of governance provides an analogue to the usual
definitions of quantifier-scope and variable-binding in PC
(cf. [
Example 2.1. The expression (◻31 ∧ ∀58) is a formula of ℒ . However, it is not governed by ∀5. For a formula of the form (◻31 ∧ 8), for some ∈ , does not meet the requirements of 2.3 (e). Rather, it was generated via 2.3(c) by combining the formula ◻31 and the governed formula ∀58. The latter is governed, since it was generated from a formula of the form 8, satisfying the conditions of 2.3(e).
Remark 2.3. We shall usually omit the brackets in conjunctions, conditionals and disjunctions, as long as unique readability is preserved.
Remark 2.4. While it will not be crucial for the following
discussion, we wish to remark that has unique
parsing. The proof for an extended syntax can be found in
[
While Quarc has been interpreted with both model-theoretic
and truth-valuational semantics, we employ the former.
Originally introduced in [
(Frames). A frame is an ordered pair ︀∐ , ̃︀ of a non-empty set of possible worlds or indices and a binary relation ⊆ × . If ∈ stands in ℱ
We will primarily be working with serial frames, i.e.
where for each ∈ there is some ∈ s.t. .
Instead of providing a universal domain of quantification,
the model-theoretic semantics of Quarc employ only
interpretation functions. They specify for each predicate an
extension, which in turn functions as a ‘local’ domain of
quantification. Additionally, each singular argument is mapped
to some object under an interpretation – objects which
constitute the members of the various predicate-extensions (cf.
[
ifed for each ∈ : for all ∈ , there is an is called an expansion.
Remark 3.1. We shall sometimes talk about all that are order to denote the set { ∶ ∐︀ , ̃︀ ∈ ℐ ( )}. relative to a given ∈ , for some frame ︀∐ , ̃︀ and some interpretation ℐ . In that case, we shall write ⋃︀ ⋃︀ in
In order to assign the proper truth-conditions to formulas governed by a quantified argument , we need a way to extend an interpretation and the set so that we can name every object in ⋃︀ ⋃︀ , for each possible world . This ℒ Definition 3.3 (Expansions). Let ℐ be an interpretation of on a frame ℱ
= ∐︀ , ̃︀ . Let be a singular argument tion that satisfies the following conditions: ( (possibly already in ℒ , i.e. ) and let be an object. The → )-expansion of ℐ , denoted by ℐ →, is an interpreta1. Either ∈ , ℐ () = and ℐ →() = , or ∉ and ℐ →() = . 2. For all ′ ∈ s.t. ≠ ′, ℐ →(′) = ℐ (′).
3. For all ∈ , ℐ →( ) = ℐ ( ). ℐ () ≠ , there is no ( → )-expansion for ℐ .
Remark 3.2. Observe that in the case that ∈ and yet Definition 3.4 (Truth-Conditions). Let ℱ a frame and ℐ
an interpretation of ℒ conditions for formulas in on ℱ = ∐︀ , ̃︀ be on ℱ . The truthover ℐ are given by a function × → {0, 1}, which obeys the rules (i)-(vi) below. If a formula is assigned the value 1 in , conditions for a given are as follows: we write ℐ , ⊧ , and ℐ , ⊭ if it is assigned 0. The (iii) Connectives: ℐ , ⊧ ¬ if ℐ , ⊭
. (i) Basic formulas: Let be a basic formula. Then: ℐ , ⊧ if ∐︀ ℐ (),
︀̃ ∈ ℐ ( ).
tion. Then, ℐ , ⊧ ¬ if ℐ , ⊧ ¬ .9 (ii) Predicate Negation: Let ¬ be a predicate nega(ii) Sentential Negation: If is of the form ¬ , then 1. If is of the form if ℐ , ⊧
and ℐ , ⊧ . 2. If is of the form 3. If is of the form if ℐ , ⊧ or ℐ , ⊧ . ∧ ∨ , then ℐ , ⊧ ∧ , then ℐ , ⊧ ∨ → , then ℐ , ⊧
→ if ℐ , ⊭ or ℐ , ⊧ .
︀( ⇑∀ ⌋︀ . (v) Universal quantification: for every ∈ s.t. , ℐ , ⊧ . (iv) Modals: If is of the form ◻ , then ℐ , ⊧ ◻ if Let (∀ ) be governed by the universally quantified argument ℐ , ⊧ (∀ ) if for every ∈ ⋃︀ ⋃︀ , ℐ →, ⊧ ∀ . Then: 8In that sense, singular arguments are rigid designators. 9This clause only applies to formulas of the required form. As soon as quantification is involved, this equivalence no longer holds, as is easily verified. ︀( ⇑∃ ⌋︀ .
by the particularly quantified argument (vi) Particular quantification : Let (∃ ) be governed ∃ . Then: ℐ , ⊧ (∃ ) if for some ∈ ⋃︀ ⋃︀ , ℐ →, ⊧ Example 3.1. Consider the following interpretation ℐ on an equivalence frame with two worlds (reflexive arrows are suppressed): w , , , , v
with ≠ two random objects, and , and ∈ . Only the true basic formulas (for the symbols under consideration) are listed in the diagram. Since each predicate has at least one member for each world, 3.2(2.) is satisfied. In , ⋃︀ ⋃︀ = {}. Thus, in order to evaluate ∀ , we first pick some ∉ (for convenience) and check the truth of under the appropriate ( → )-expansion. Since there is only once case to check, and ∈ ⋃︀ ⋃︀ , the formula is true. • ℐ , ⊧ ∃ • ℐ , ⊭ ∀ • ℐ , ⊭ ∃ • ℐ , ⊭ ◻∀ • etc.
Having defined truth for formulas, we can now proceed to define validity and entailment over a class of frames in the usual way: Definition 3.5
(Entailment and Validity). We first define entailment, treating validity as a special case:
Γ ⊧ℱ . • Let ℱ
= ∐︀ , ̃︀ be a frame. A set of formulas Γ entails a formula on ℱ if for every interpretation ℐ and every world ∈ , if , ⊧ for every ∈ Γ , then , ⊧ . In such a case, we write • Let F be a class of frames. Then, a set of formulas Γ In this case, we write Γ ⊧F .
entails a formula on F if for every ℱ ∈ F, Γ ⊧ℱ . • A formula is a validity on a frame ℱ if if it is entailed by the empty set on ℱ . It is a validity on a class of frames F just in case the empty set entails it on F. In the latter case, we write ⊧F .
In this section, we introduce an unlabelled Gentzen-style
natural deduction system. It will be a Quarc-analogue of the
normal modal logic . We choose an unlabelled system in
order to once again remain closer to the linguistic form of
quantified modal reasoning in natural language. We follow
the basic set-up found in [
(Proofs). A proof is a rooted tree where
every vertex is labelled with an element of , and
each edge is labelled with one of the rules of definition 4.2.
The root is the conclusion of the proof, and its leaves are
assumptions that are either discharged or undischarged, as
specified by the rules. We say the conclusion
depends on
the undischarged assumptions. We explicitly allow empty
assumption classes (cf. [
With this standard graph-theoretic set-up, the logic ◻−
can be introduced, where − designates the simplified
version of Quarc we are employing. The rules for the ◻-free
fragment are taken from [
(◻− ). The logic ◻− is given by the 1. Connectives: We adopt the standard introduction following rules for ¬ are chosen: and elimination rules for ∧, ∨ and → .
Since the symbol is not part of the syntax, the [] ⋮ ¬ ¬ ¬ [] ⋮ ¬
PS
I ¬ ︀( ⌋︀
⋮ ︀( ⇑∀ ⌋︀ ︀( ∀ ⌋︀
∀I, ∗ 3. Quantification: Let ( ) be a formula governed by the quantified argument . Let (︀ ⇑ ⌋︀ be the formula where the governing occurrence of has been replaced by the singular argument .
The rules for universal quantification are as follows: [¬] ⋮ [¬] ⋮ ¬
¬E ¬ ¬
SP ︀( ∀ ⌋︀ ︀( ⇑∀ ⌋︀ ∀
E where the side condition ∗ requires to not occur in any undischarged assumption or in (∀ ).
Particular quantification has the following introduction rule:
︀( ⇑∃ ⌋︀ ︀( ∃ ⌋︀ ∃
I obey the following rule: Since no ∈ is ever empty, both quantifiers ︀( ⌋︀ ︀( ⌋︀ , ︀( ︀( ⇑ ⌋︀ ⋮
Imp, ∗ following introduction rule: where the side condition ∗ requires to not occur in any undischarged assumptions, or (∀ ). 4. Modality: For the modal operator ◻, we have the ◻ ◻I, ∗ where the condition ∗ says that if depended on the assumptions 1, ..., , then ◻ now depends on the assumptions ◻ 1, ..., ◻ .
Lastly, given our interest in working with serial frames, the following rules capture the modal logic : 10The authors are indebted to Elio La Rosa for suggesting such rules. I while having assumed , then, if bols: ◻ , we discharge the formula ◻ .
Remark 4.1. We allow multiple applications of ◻I, though this will never occur in the proofs in subsection 5.2. In any case, we keep track of the added ◻ s by putting ◻ into the superscript of an assumption . We add the following convention: if ◻ is a string of -many ◻s, then if we discharge Remark 4.2. Caution must be exercised when mixing the
I with others that use assumption classes. For exunderwent an application of ◻I on the left branch, but not on the right, we cannot derive ¬ ◻ via ¬I. For otherwise, the application of ¬I becomes incorrect, since does not have the prerequisite form on the right branch of the tree. Definition 4.3 (Syntactic Consequence). Let Γ be a set of formulas and a formula. Then, Γ proves , or is a syntactic consequence of Γ , just in case there are finitely many 1, ..., ∈ Γ = ∅, is a theorem and we write ⊢ . assumptions 1, ..., . In such a case, we write Γ ⊢ .11 If Γ s.t. there is a proof of with undischarged Remark 4.3. The preceding proof system has been stated in more generality than strictly required. For example, in ∀I, all (∀ ) will always be of the form ∀ or ∀ ¬, since the syntax only contains unary predicates. Nevertheless, we would like to stress that the rules for the quantifiers also work with respect to more complex syntaxes, such as those including Quarc’s other features, like anaphora, reordered predicates and -ary predicates. Likewise, the rules PS and SP are not used in subsection 5.2. However, they would be required to established the relations of the symmetric de dicto formalizations mentioned in sections 1 (cf. Fig. 2) and 5.4.
Since it is not the focus of the present investigation, we merely mention the following result, without proof: plete with respect to the class of all serial frames. Theorem 4.1. ◻− is both strongly sound as well as com
We shall rely on the soundness of ◻− in subsection 5.2.
A related result can be found in [
In this section, we establish the dodecagon of opposition for the asymmetric de dicto reading. We begin by detailing the latter reading of the twelve combinations of quantification and modality (subsection 5.1). After presenting these, we prove the resulting individual relations in ◻− (subsection 5.2) and provide example counter-models for some pairs that under consideration. 11Subscripts for ⊢ are suppressed, given that ◻− is the only logic 12It can be shown that the two semantics validate the same sequents, hence the result can be transferred. lack certain relations (subsection 5.3). Finally, we discuss these results by comparing them to the symmetric de dicto formalizations (5.4) of Fig. 2. 5.1. The Combinations and the Resulting
Dodecagon Before introducing the combinations themselves, further modal notions need to be introduced. The language introduced in 2.1 has only one primitive modal operator, viz. ◻ (necessity). We shall define the remaining modal notions in terms of ◻: Definition 5.1 (Further Modalities). Let ∈ be given. The following modal notions receive their own sym• Possibility: ◇ ∶≡ ¬ ◻ ¬. • Absoluteness: ∆ ∶≡ ◻ ∨ ◻¬.
• Contingency: ∇ ∶≡ ¬ ◻ ¬ ∧ ¬ ◻ .
avoidability and imposdirectly rendered as ¬ ◻ and ◻¬, respectively.13 sibility – do not receive a special symbol, but are instead
This definition yields the six modal notions introduced in section 1. We shall follow the terminology established there and denote the type of quantification with either U (universal) or P (particular)14, and use N, P, V, B, C and I for the six modal notions from section 1, respectively. This yields the same twelve names as in section 1, albeit with diferent logical profiles: tions are the following: Definition 5.2 (Asymmetric Reading). Let and be two predicates of ℒ . The twelve asymmetric de dicto combinaare not ’. ing formula.
Remark 5.2. In the following, if is a combination, we shall write ¬ for the negation of the whole correspond
Before presenting the main results, the Aristotelian
relations themselves must be introduced. Given the setting of
section 3, the relations are rendered as follows:
and are:
Definition 5.3 (Aristotelian Relations). Let ⊧ denote
entailment on the class of all serial frames (cf. 3.5). Then, a
formula is a subalternate of another formula if ⊧
and it is not the case that ⊧ . Furthermore, two formulas
• contraries if ⊧ ¬ ,
13This is a common choice in the literature, as witnessed by [
However, it should always be clear by context which role is intended. NU PP
PU NP VP IU
IP VU • subcontraries if ¬ ⊧ , • contradictories if they are both contaries and subcontaries, i.e. ⊧ ¬ and ¬ ⊧ . In such a case, we write â⊧ ¬ .
Given that there are twelve combinations, we must investigate a total of 66 pairs.15 In total, 16 pairs have no Aristotelian relation between them, with the remaining 50 instantiating one of the relations in definition 5.3. These ifndings are summarized in the following dodecagon: CU
CP BP
BU 5.2. Proofs of the Relations In this subsection, we prove all 50 relations, namely all modal categorical inferences resulting from our asymmetric reading of de dicto modalities. Instead of proving them classified by type, we will generally prove them in order of increasing proof complexity. This allows for a more compact and straightforward presentation of the proofs. As mentioned before, we rely on the soundness of ◻− throughout this section. The proofs themselves are categorized into two types: simple proofs, which only require propositional reasoning or straightforward modal reasoning, and complex proofs. We consider each in turn. 5.2.1. Simple Proofs Some of these relations hold purely by virtue of propositional reasoning. This holds for all contradictory pairs, in particular: Fact 5.1. The following hold: 15We disallow repetitions for reasons of triviality, and order does not matter with respect to forming the pairs, due to the properties of Aristotelian relations. 48–59 (i) â⊧ ¬ (ii) â⊧ ¬ (iii) â⊧ ¬ (iv) â⊧ ¬ (v) â⊧ ¬ (vi) â⊧ ¬ Proof. Given how the modalities are ultimately defined, proving all these claims becomes a matter of simple propositional reasoning: • (i) and (ii) are instances of the de Morgan rules.
For example, â⊧ ¬ becomes the claim ¬ ◻ ¬∃ ∧ ¬ ◻ ∃ â⊧ ¬(◻∃ ∨ ◻¬∃ ). • (iv) is an instance of double negation elimination/introduction: ◻∀ â⊧ ¬¬ ◻ ∀ . • (iii), (v) and (vi) are instances of the schema â⊧ .
For example, â⊧ ¬ is the claim that ¬ ◻ ¬∀ â⊧ ¬ ◻ ¬∀ .
Similarly, further relations are provable by applications of propositional reasoning. This applies to the following pairs: Fact 5.2. The following hold: (i) ⊧ (ii) ⊧ (iii) ⊧ (iv) ⊧ (v) ⊧ (vi) ⊧ (vii) ⊧ (viii) ⊧ (ix) ⊧ ¬ (x) ⊧ ¬ (xi) ⊧ ¬ (xii) ⊧ ¬ (xiii) ¬ ⊧ (xiv) ¬ ⊧ (xv) ¬ ⊧ (xvi) ¬ ⊧ Proof. We group the proofs by the type of relation they establish: • The subalternations (i)-(viii) are established either by a single application of ∨I or ∧E. For example, ⊧ is the claim that ◻¬∀ ⊧ ◻∀ ∨ ◻¬∀ , and ⊧ is the claim that ¬ ◻ ¬∃ ∧ ¬ ◻ ∃ ⊧ ¬ ◻ ∃ . • The contraries (ix)-(xii) are proven either by a singe application of ∧E – as in the case of (xi) – or a combination of ∧E and ¬I, as in the cases of (ix), (x) and (xii), since they are of the form ⊧ ¬( ∧ ¬) or ⊧ ¬(¬ ∧ ).16 • The remaining cases are subcontraries, and are proven by a combination of double negation elimination and ∨I – (xiii), (xv) and (xvi) – or by using the de Morgan rules and ∧E, as in (xiv). The latter is the claim that ¬(◻∃ ∨ ◻¬∃ ) ⊧ ¬ ◻ ∃ , and the former are of the form ¬¬ ⊧ ∨ .
A number of the relations depicted in theorem 5.1 are the result of an application of ◻¬, as well as double negation elimination: Fact 5.3. The following hold: 16Observe that the sequent in (xi) coincides with the one in (vi). Proof. Most of these pairs can be established with a single application of ◻¬ . This holds for (i)-(vi).17 We prove (iv): ◻¬∀ ︀( ◻∀ ⌋︀ 1
¬ ◻ ∀ This result, in turn, establishes (viii): ◻¬I1 ¬¬ ◻ ¬∀ DNE ◻¬∀ 5.3(iv) ¬ ◻ ∀ Lastly, (vii) has the same proof as (viii), except with particular quantification instead of universal one.
With these facts, thirty of the fifty relations have been established. We now turn to the more complex cases. 5.2.2. Complex Proofs We begin by noticing the following fact: Fact 5.4. ∀ ⊧ ∃ Proof.
∀
︀( ︀⌋ 1 ∃ ∃
In the following, we treat this proof as an admissible rule with the name Sub (‘subalternation’).18 As an immediate corollary, we gain the entailment ¬∃ ⊧ ¬∀ . The corresponding proof will also be treated as an admissible rule, named CSub (‘contrapositive subalternation’). With these basic building blocks, we can establish the following: Fact 5.5. The following hold: (i) ⊧ (ii) ⊧ (iii) ⊧ ¬ (iv) ⊧ Proof. We first prove (i): (v) ⊧ ¬ (vi) ⊧ (vii) ⊧ ¬ (viii) ¬ ⊧ ∀ ◻ Sub ◻∃∃ ◻I Recall that according to remark 4.1, we add ◻ as a superscript to all undischarged assumptions after applying ◻I. Thus, the conclusion ◻∃ now depends on the assumption ◻∀ . This proof can in turn be extended to yield (ii): ∀ ◻ ◻∃ ︀( ◻¬∃ ⌋︀ 2
¬ ◻ ¬∃ ◻¬I2 17Moreover, the sequents in (i) and (v), as well as (ii) and (vi), coincide. 18Essentially the same proof also establishes (∀ ) ⊧ (∃ ), irrespective of the complexity of and the underlying syntax, so long as the quantified arguments ∀ and ∃ are governing .
Additionally, (iii) is the same sequent as (ii). Certain propositional arguments further prove (iv)-(viii). First, (iv) is proven by applying ∨I to the conclusion of the proof in (i). Second, (v) is ultimately the same sequent as (vi): ¬ ◻ ∃ ⊧ ¬ ◻ ∀ , which is the contraposition of (i). Third, (vii) has the following proof: ∧E DNE ¬¬ ◻ ∀ ◻∀ ︀( ∀ ◻⌋︀ 2
◻∃ ◻∀ → ◻∃ ◻∃ 5.5(i)
I → 2 →E Observe that, given how ◻I works, ∀ ◻ must first be discharged, for we cannot reason with ◻∀ directly to ◻∃ .
From these proofs, we can further derive the following results: Fact 5.6. Fact 5.5 further entails the following: (i) ⊧ (ii) ¬ ⊧ (iii) ¬ ⊧ Proof. (i) follows directly from ∧E applied to ¬ ◻ ¬∃ ∧ ¬ ◻ ∃ and by proceeding as in 5.5(v)/(vi). (ii) follows from 5.5(viii) by applying ◻¬ : ¬¬ ◻ ∀ ◻∃ 5.5(viii) ¬ ◻ ¬∃ To prove (iii), we use the proof of 5.6(i) as a starting point and apply ∨ to its conclusion to yield ◻∃ ∨ ◻¬∃ .
We now turn to the amodal entailment ¬∃ ⊧ ¬∀ . It provides the basis for the remaining proofs: Fact 5.7. The following entailments obtain: ︀( ◻¬∃ ⌋︀ 2 ◻¬I2 (i) ⊧ (ii) ⊧ (iii) ⊧ (iv) ⊧ ¬ (v) ⊧ (vi) ¬ ⊧ (vii) ⊧ (viii) ⊧ ¬ (ix) ¬ ⊧
¬∃ ◻ CSub ◻¬¬∀∀ ◻I Via an application of ∨I, we immediately yield (ii). Via ◻¬ , we establish (iii): ¬∃ ◻ ◻¬∀ 5.7(i) ︀( ◻∀ ⌋︀ 1
◻¬I1 ¬ ◻ ∀ From (i) and double negation introduction, we can prove (iv). (v) is established in the following way, where CP refers to the transformation of a conditional into its contrapositive: ︀( ¬∃ ◻⌋︀ 1
5.7(i) ◻¬∀ I ◻¬∃ → ◻¬∀ → C1 P ¬ ◻ ¬∀ → ¬ ◻ ¬∃ ¬ ◻ ¬∀ →E ¬ ◻ ¬∃ Since (vi) is the same sequent as (v), we have therefore also established (vi). Furthermore, we can prove (vii) via applying ∧E to ¬◻¬∀ ∧¬◻∀ and then proceeding as in the proof of (v). (viii) is the same sequent as (vii), and (ix) is proven by first applying the de Morgan laws to ¬ to obtain (cf. 5.1(ii)), and then proceeding as in (vii).
With these results, theorem 5.1 has been established: Proof of theorem 5.1. Follows from facts 5.1, 5.2, 5.3, 5.5, 5.6 and 5.7. 5.3. Sample Counter-Models for the
Remaining Pairs The remaining sixteen pairs do not instantiate any Aristotelian relation. Proving this is mostly straightforward. We showcase one pair in detail, as well as two further failures of entailment that explain a large portion of the remaining cases. We will always exhibit 5-counter-models in order to avoid the suspicion that the relevant relations do not obtain due to the underlying accessibility relation. The reflexive arrows are suppressed throughout.
Example 5.1. Consider the pair / , i.e. ◻¬∀ and ¬ ◻ ∃ .
• ⊭ : w , , , , v where and are two distinct objects. We can see that for each world , ∈ {, }, ⋃︀ ︀⋃ ∩ ⋃︀ ⋃︀ ≠ ∅ and ︀⋃ ⋃︀ ⊈ ⋃︀ ⋃︀ . As such, ◻¬∀ and ◻∃ are both true in . • ⊭ : w , , v where and are once again dummy objects, distinct from each other. By construction: ⋃︀ ︀⋃ ∩⋃︀ ⋃︀ = ∅ and ⋃︀ ︀⋃ ⊆ ⋃︀ ⋃︀ . It follows that ¬ ◻ ¬∀ and ¬ ◻ ∃ are both true in . • ¬ ⊭ : We keep from the first and from the second counter-model. In that case, ◇∀ and ◻∃ are both true in . • : ⊭ ¬ is established with the following counter-model: w , , v 48–59 In this case, both ◻¬∀ and ¬ ◻ ∃ are true in , as is easily verified.
The fact that no relation obtains for this pair immediately explains why certain other entailments also fail to obtain. Thus, since IU does not entail VP, neither does ∆ ∀ entail ∇∃ , even if ◻∀ entails ◇∃ , as per 5.5(ii). In a similar vein, the following entailments also fail to hold: Example 5.2. ⊭ : w , , , v By construction, makes ◇∀ true, since ∀ is true in . In , is but not , making ∀ false at . Thus, ¬ ◻ ∀ is true at . As a consequence, makes ∇∀ true. However, ∃ is true in both worlds, hence makes ¬ ◻ ∃ false.
As a final example, we demonstrate that does not entail , since it entails neither disjunct: Example 5.3. ⊭ : Consider the following model: w , , , v In , ∃ is false and ¬∀ true. The latter formula is also true in , but so is ∃ . Thus, ◻∀ is true in , but neither ◻∃ nor ◻¬∃ .
With this last example, we also have a counter-model to verify that ◻¬∀ ⊭ ◻∃ (i.e. ⊭ ), or that ∆ ∀ ⊭ ∆ ∃ (i.e. ⊭ ). Lastly, as these countermodels demonstrate, it is straightforward to invalidate the purported entailments of the remaining pairs, thus we omit the remaining counter-models. 5.4. Comparison to the Symmetric De Dicto
Reading
We conclude this section by comparing the results of
theorem 5.1 with the symmetric de dicto reading from [
Thus, with the symmetric reading, we end up with six contradictories, twelve contraries and subcontraries, and 24 subalternations, for a total of 54 pairs instantiating an Aristotelian relation. Thus, at first glance, by going from the asymmetric reading to the symmetric one, we only seem to gain four additional relations. However, this superficial glance obscures the vast diferences between the two dodecagons.
In total, only 32 pairs do not change the relation they instantiate, whereas 34 do. The former do not include any contradictions, and the latter include two cases of subalternation where the direction of entailment is reversed. Ultimately, the 34 pairs that change their instantiated relation contain twelve cases of pairs whose relation merely shifts, and 22 where the pair only instantiates a relation in one of the two readings. Thus, there are vast diferences between the two dodecagons.
For clarity of reference, the 34 pairs that undergo change are detailed in table 1. In case a pair instantiates a subalternation, the arrow denotes the direction of entailment relative to the way the pair is listed in the left column. Subalternations are abbreviated with Subalt, contradictions with Contrad, contraries with Cont and subcontraries with SubC.
Instead of discussing all these pairs in detail, we would like to zero in on a few interesting facts. First, shifting the position of the negation can have the efect of a contraposition, as in the pairs ⇑ and ⇑ , where the direction of entailment reverses when transitioning from one setting to the other. Second, many of the relations in the symmetric setting obtain due to two underlying entailments: Fact 5.8. The following hold: 1. ¬(∀ ) ⊧ ∃¬ 2. ¬(∃ ) ⊧ ∀¬ Proof. The proof for 1. proceeds indirectly: ¬(∀ ) ︀( ¬∃¬ ⌋︀ 3 ∀ ∃¬ whereas 2. is established straightforwardly: ¬∃ ¬ ¬ ∀¬ ︀( ︀⌋ 2
∃ SP ∀I2 ︀( ︀⌋ 2
∃¬ ∀I2 ¬E3
Naturally, since predicate negation is completely absent in the asymmetric setting of definition 5.1, these entailments become irrelevant to establishing any of the relations in the latter context. As a consequence, many entailments are weakened or strengthened. Third, the shifting of negation and the resulting lack of predicate negation can also change the formula so much that entailments can be lost completely. For example, whereas ◇∀ ∧ ◇∀¬ ⊧ ◇∃ (i.e. ⊧ ) holds in the symmetric setting, the corresponding pair ◇∀ ∧ ◇¬∀ and ◇¬∃ from definition 5.1 do not instantiate any relation (cf. example 5.2). Fourth, the fact that most changes happen to pairs that are contrary or subcontrary (or both) in one of the settings is unsurprising. For given that many subalternations in either context hold purely due to simple propositional or modal reasoning, they are insensitive to the subtleties regarding the diference between predicate and sentence negation. Thus, we find that out of the 32 pairs that do not undergo change when switching settings, 17 are subalternations. Finally, and most importantly, whereas the dodecagon in Fig. 2 does not preserve the hexagon of opposition, the asymmetric reading generates one that does (cf. Fig. 3), as can be read of from the figures.
In this article we analyzed one of the basic building blocks
of modal quantified reasoning, namely modal categorical
inferences. We did this within Quarc, a formal framework that
significantly departs from Predicate Logic in representing
natural language sentences, especially due to the pivotal
role it assigns to quantified phrases . We focused on de dicto
combinations of modalities and quantifiers in modal
categorical statements and proposed a new reading for them, which
we called asymmetric, as opposed to the symmetric reading
presented in [
Clearly, our results can be transferred to other formal frameworks, thanks to the use of translation functions. For instance, consider definition 5.2. The following simple procedure indicates how one can move from a formula of modal Quarc that represents a modal categorical statement to an equivalent formula of modal PC (for reading disambiguation, we use quotation marks to delimit a string of symbols): • One must add the string of symbols ‘(’ immediately after the quantifier in , thus getting 1. • If 1 contains ∀, then one must add the string of symbols ‘ →’ immediately after (i.e. the predicate forming the quantified argument in ), otherwise 1 contains ∃ and one must add the string of symbols ‘∧’ immediately after . In any of these cases, one gets 2. • One must add the string of symbols ‘)’ at the end of 2, thus getting 3.
It is easy to verify that 3 is a formula of modal PC. Following this procedure, if our starting point is e.g. = ◇∀ (which represents PU), we get 3 = ◇∀( → ).
Looking into the future, a natural direction to follow is developing a theory of modal categorical syllogism. A syllogism of this kind consists of two premises and and a conclusion , all of which qualify as modal categorical statements. Here is an example: (∗ ∗ ∗) I don’t know whether all rooms on this floor have an access code. I know that all rooms with an access code are inaccessible to guests. Therefore, it’s possible that all rooms on this floor are inaccessible to guests.
A simple formalization of (∗ ∗ ∗) can be as follows, where stands for ‘is a room on this floor’, for ‘has an access code’ and for ‘is accessible to guests’:
{◇∀ ∧ ◇¬∀, ◻∀¬} ⊧ ◇∀¬ An important task is identifying all possible triples of (forms of) modal categorical statements that give rise to a valid syllogism. Moreover, one can look at the interaction between de re and de dicto combinations, or at the interaction between symmetric and asymmetric de dicto combinations, to identify other patterns of valid syllogism. The example provided above already illustrates some noteworthy interaction, since it has the following structure, where stands for ‘symmetric reading’ and for ‘asymmetric reading’: {CU(), IU()} ⊧ VU() Finally, one can analyse patterns of valid syllogism, where some categories of individuals are treated as -ary relations ( > 1) rather than properties (i.e. unary relations), generalizing the definition of a modal categorical statement used here.
As far as modalities are concerned, one can take into
account more complex statements formalized via at least two
modal operators (e.g. ‘it is necessarily possible that...’, ‘it is
known that it is unknown that...’) or a family of modalities
diferent from the one in the hexagon of opposition.
Extensive research has been done on generalizations of the modal
square of opposition, including works on solid figures such
as cubes of opposition, whose definition varies with authors
[
Simon D. Vonlanthen was supported by the German Federal Ministry of Education and Research, BMBF, through Kristina Liefke’s WISNA professorship. Matteo Pascucci was supported by the VEGA grant n. 2/0125/22 “Responsibility and Modal Logic”.