Introduction

Standpoint logic is a modal logic-based formalism for representing multiple diverse (and potentially conflicting) viewpoints within a single framework. Its main appeal derives from its conceptual simplicity and its attractive properties:

In the presence of conflicting information, standpoint logic sacrifices neither consistency nor logical conclusions about the shared understanding of common vocabulary [1]. The underlying idea is to start from a base logic (originally propositional logic [1]) and to enhance it with two modalities pertaining to what holds according to certain standpoints. There, a standpoint is a specific point of view that an agent or other entity may have, and that may have a bearing on how the entity understands and employs a given logical vocabulary (that may at the same time be used by other entities with a potentially different understanding). The two modalities are, respectively:

• □s𝜑, expressing: "it is unequivocal [from the point of view s] that 𝜑";

• ♢ s 𝜑, expressing: "it is conceivable [from the point of view s] that 𝜑".

Standpoint logic escapes global inconsistency by keeping conflicting pieces of knowledge separate, yet avoids duplication of vocabulary and in this way conveniently keeps portions of common understanding readily available. It has its history and roots within the philosophical theory of supervaluationism [2], stating that semantic variability "can be explained by the fact that natural language can be interpreted in many different yet equally acceptable ways, commonly referred to as precisifications" [1].

In our work, such semantic commitments can be made, as is often done, on the basis of incomplete knowledge using a form of default reasoning. Consequently, in our work each precisification embodies a consistent (but possibly partial) viewpoint on what can be known, potentially using nonmonotonic reasoning (NMR) to arrive there. This entails that the overall formalism becomes non-monotonic with respect to its logical conclusions.

Several non-monotonic formalisms that could be employed for default reasoning within standpoints come to mind, and obvious criteria for selection among the candidates are not immediate. We choose to employ the nonmonotonic modal logic S4F [3,4], which is a very general formalism that subsumes several other NMR languages, decidedly allowing the possibility for later specialisation via restricting to proper fragments. The usefulness of nonmonotonic S4F for knowledge representation and especially non-monotonic reasoning has been aptly demonstrated by Schwarz and Truszczyński [4] (among others), but seems to be underappreciated in the literature to this day. In our case, employing S4F as base language for standpoint logic entails, as easy corollary, for example standpoint default logic, a standpoint variant of Reiter's default logic [5], where defaults and definite knowledge can be annotated with standpoint modalities. In Example 1, the annotated defaults are of the standard form, namely 𝜙 : 𝜓1, . . . , 𝜓𝑛/𝜓, where (as usual) if the prerequisite 𝜙 is believed to be true and the justifications 𝜓1, . . . , 𝜓𝑛 are consistent with one's current beliefs, the consequence 𝜓 can be concluded.

Example 1. Coffee is consumed differently in different parts of the world -what is considered to be a "typical coffee" varies among countries. Usually (*) it is consumed hot, however in Vietnam ( ) iced coffee is a more common choice. Apart from the temperature, in Italy ( ), one of the most popular coffee drinks -espresso -is much higher in caffeine than the typically filtered coffee popular in the US ( ). The above considerations could be formalised using standpoint defaults as follows:

□* [︁ coffee : hot/hot ]︁ , □ [︁ coffee : iced /iced ]︁ , □ [︁ coffee : espresso/espresso ]︁ , □ [︁ coffee : low _caffeine/low _caffeine ]︁ ♢

Several monotonic logics have been "standpointified" so far: Apart from propositional logic in the original work of Gómez Álvarez and Rudolph [1], also first-order logic and various fragments thereof [6] as well as the description logics 𝒮ℛ𝒪ℐ𝒬 [6], ℰℒ+ [7,8], and 𝒮ℋℐ𝒬 [9], and the temporal logic LTL [10]. We add the first non-monotonic logic to the realm of standpoint logics, that is, the first standpoint logic where the points of view embodied by standpoints can be obtained by reasoning in a non-monotonic fashion.

More specifically, in this paper, we introduce the syntax and semantics of standpoint S4F. We analyse the computational complexity of its associated reasoning problems and show that reasoning does not become harder (than in the base logic) through the addition of standpoint modalities. Finally, we demonstrate some of the more concrete standpoint formalisms we obtain as corollaries, more specifically standpoint default logic and standpoint argumentation frameworks. We conclude with a discussion of future work.

Background

All languages we henceforth consider build on propositional logic, denoted ℒ, and built from a set 𝒜 of atoms according to 𝜙 ::= 𝑝 | ¬𝜙 | 𝜙 ∧ 𝜙 where 𝑝 ∈ 𝒜. Its model-theoretic semantics is given by interpretations 𝐼 ⊆ 𝒜 containing exactly the true atoms, and we denote satisfaction of a formula 𝜙 by an interpretation 𝐼 by 𝐼 ⊩ 𝜙, and entailment of a formula 𝜙 by a set 𝑇 of formulas by 𝑇 |= 𝜙. The provability relation for propositional logic is denoted by ⊢ (where 𝑇 ⊢ 𝜙 means that from 𝑇 , we can derive 𝜙) and assumed to be given by some standard proof system that is sound and complete (that is, where 𝑇 ⊢ 𝜙 iff 𝑇 |= 𝜙).

Standpoint Logic

Standpoint Logic was introduced by Gómez Álvarez and Rudolph [1] as a modal logic-based formalism for representing multiple (potentially contradictory) perspectives in a single framework. Building upon propositional logic, in addition to a set 𝒜 of propositional atoms, it uses a set 𝒮 of standpoint names, where a standpoint represents a point of view an agent or other entity can take, and * ∈ 𝒮 is a designated special standpoint, the universal standpoint. Formally, the syntax of propositional standpoint logic ℒ S is given by

𝜙 ::= 𝑝 | ¬𝜙 | 𝜙 ∧ 𝜙 | □s𝜙

where 𝑝 ∈ 𝒜, and s ∈ 𝒮 is a standpoint name. We allow the notational shorthands 𝜙 ∨ 𝜓, 𝜙 → 𝜓, and ♢ s 𝜙 := ¬□ s ¬𝜙.

The semantics of standpoint logic is given by standpoint structures 𝒩 = (Π, 𝜎, 𝛾), where Π is a non-empty set of precisifications, 𝜎 : 𝒮 → 2 Π assigns a set of precisifications to each standpoint name (with 𝜎(*) = Π fixed), and 𝛾 : Π → 2 𝒜 assigns a propositional interpretation to each precisification. The relation 𝒩 , 𝜋 ⊩ 𝜙, indicating that the structure 𝒩 = (Π, 𝜎, 𝛾) satisfies formula 𝜙 (at point 𝜋), is defined by induction:

𝒩 , 𝜋 ⊩ 𝑝 :⇐⇒ 𝑝 ∈ 𝛾(𝜋) 𝒩 , 𝜋 ⊩ ¬𝜙 :⇐⇒ 𝒩 , 𝜋 ̸ ⊩ 𝜙 𝒩 , 𝜋 ⊩ 𝜙1 ∧ 𝜙2 :⇐⇒ 𝒩 , 𝜋 ⊩ 𝜙1 and 𝒩 , 𝜋 ⊩ 𝜙2 𝒩 , 𝜋 ⊩ □s𝜙 :⇐⇒ 𝒩 , 𝜋 ′ ⊩ 𝜙 for all 𝜋 ′ ∈ 𝜎(s)

As usual, a standpoint structure (Π, 𝜎, 𝛾) is a model for a formula 𝜙 iff (Π, 𝜎, 𝛾) ⊩ 𝜙; a formula 𝜙 ∈ ℒ S is satisfiable iff there exist (Π, 𝜎, 𝛾) and 𝜋 ∈ Π with (Π, 𝜎, 𝛾) , 𝜋 ⊩ 𝜙. 1Standpoint structures can be regarded as a restricted form of ordinary (multi-modal) Kripke structures pressions of the form s ⪯ u indicating that every precisification subscribing to s must also subscribe to u as realised by their formal semantics 𝜎(s) ⊆ 𝜎(u). We disregard sharpening statements in this work for clarity of exposition; they could be added without difficulty.

(𝑊, {𝑅s} s∈𝒮 , 𝑣), where the worlds 𝑊 are given by the precisifications Π, the evaluation function 𝑣 is given by 𝛾, and the reachability relation among worlds for a standpoint name (i.e., modality) s ∈ 𝒮 is simply 𝑅s = Π × 𝜎(s).

Modal Logic S4F

S4F is a propositional modal logic with a single modality K, read as "knows". It was studied in depth by Segerberg [3]; we base our study on the works of Schwarz and Truszczyński [11,12,13,4]. We again start from a propositional vocabulary 𝒜.

The syntax of the modal logic S4F ℒ K is given by

𝜙 ::= 𝑝 | ¬𝜙 | 𝜙 ∧ 𝜙 | K𝜙

with 𝑝 ∈ 𝒜. For formulas 𝜙 ∈ ℒ K without occurrences of K, we write 𝜙 ∈ ℒ and call them objective formulas.

Truszczyński [14] introduced a useful fragment of S4F, so-called modal defaults. There, the base case of formula induction is not a propositional atom as above, but of the form K𝜓 for 𝜓 ∈ ℒ a formula of propositional logic. More formally, a modal default is built via

𝜙 ::= K𝜓 | ¬𝜙 | 𝜙 ∧ 𝜙 | K𝜙

with 𝜓 ∈ ℒ. The fragment of modal defaults is still expressive enough for our desired applications in knowledge representation and reasoning, so we will mostly restrict our attention to modal defaults later on.

The

Non-Monotonic S4F

A non-monotonic logic can be obtained by restricting attention to models where what is known is minimal. As defined by Schwarz and Truszczyński [4, Definitions 3.2 and 3.3], an S4F structure ℳ = (𝑉, 𝑊, 𝜉) is said to be strictly preferred over another S4F structure 𝒦 = (𝑉 ′ , 𝑊, 𝜉 ′ ) iff 𝑉 ′ = ∅, 𝜉 ′ ⊇ 𝜉, 3 and for some 𝜓 ∈ ℒ, we have 𝒦 ⊩ 𝜓 but ℳ ̸ ⊩ 𝜓. We say that 𝒦 is a minimal model of a theory 𝑇 ⊆ ℒ K iff (1) 𝒦 is a model of 𝑇 , and (2) there is no model ℳ of 𝑇 that is strictly preferred over 𝒦.

So if ℳ is strictly preferred over 𝒦, then there is a propositional formula 𝜓 ∈ ℒ such that (1) 𝒦, 𝑤 ⊩ 𝜓 for all 𝑤 ∈ 𝑊 , and (2) there is a 𝑤 ′ ∈ 𝑉 such that ℳ, 𝑤 ′ ̸ ⊩ 𝜓. For a minimal model of a theory 𝑇 , all strictly preferred structures violate some formula of 𝑇 .

Intuitively, 𝒦 having a strictly preferred alternative means that the knowledge of 𝒦 is not minimal. We note that a minimal model (𝑉, 𝑊, 𝜉) has 𝑉 = ∅ by definition, and thus is an S5 structure, that is, a set of worlds with a universal accessibility relation.

Complexity of Non-Monotonic S4F

Schwarz and Truszczyński [13] provide complexity results for decision problems associated with non-monotonic S4F. The problems are defined w.r.t. a finite S4F theory 𝐴 ⊆ ℒ K and a formula 𝜙 ∈ ℒ K and can be summarized as follows:

• existenceS4F: Does 𝐴 have a minimal model?

• in-someS4F: Is there a minimal model ℳ of 𝐴, such that ℳ ⊩ 𝜙?

• not-in-allS4F: 4 Is there a minimal model ℳ of 𝐴, such that ℳ ̸ ⊩ 𝜙?

• in-allS4F: Does ℳ ⊩ 𝜙 hold for every minimal model ℳ of 𝐴?

The above reasoning tasks were found to reside on the second level of the polynomial hierarchy, with the first three being Σ P 2 -complete and the last one Π P 2 -complete. We recall the proof idea by Schwarz and Truszczyński [13] of existenceS4F given an S4F theory 𝐴 ⊆ ℒ K below.

Let 𝐴 K = {𝜙 | K𝜙 ∈ Sub(𝐴)}, where Sub(𝐴) denotes the set of all subformulas of formulas in 𝐴. Note that given any minimal S4F model ℳ of 𝐴, which necessarily is an S5 structure, and a formula 𝜙 ∈ ℒ K , due to the universal accessibility relation it is the case that either ℳ ⊩ K𝜙 or ℳ ⊩ ¬K𝜙. Then, there has to be a subset Ψ ⊆ 𝐴 K , such that ℳ ⊩ K𝜓 and ℳ ⊩ 𝜓 for all 𝜓 ∈ Ψ. For the remaining elements of 𝐴 K , namely 𝜑 ∈ Φ := 𝐴 ∖ Ψ then it has to hold that ℳ ⊩ ¬K𝜑. The minimal models of a theory 𝐴 can therefore be compactly represented by partitionings (Φ, Ψ) of 𝐴 K . Such a sparse representation of a minimal model is necessary, as the actual minimal model cannot be efficiently constructed due to potentially containing exponentially many worlds (w.r.t. the input theory). Towards minimisation of knowledge, note that the set Φ needs to be maximal, so that the set of known formulas Ψ is restricted to only what is absolutely necessary.

The procedure for existenceS4F work as follows: Given a theory 𝐴 ⊆ ℒ K , we guess a partitioning of 𝐴 K into (Φ, Ψ). Based on this pair, we define the set

Θ = 𝐴 ∪ {¬K𝜙 | 𝜙 ∈ Φ} ∪ {K𝜓 | 𝜓 ∈ Ψ} ∪ Ψ which is interpreted as a theory of propositional logic over an extended signature 𝒜 ∪ {︁ K𝜑 ⃓ ⃓ 𝜑 ∈ 𝐴 K }︁

, that is, where subformulas of the form K𝜑 are treated as propositional atoms. Then, we verify whether the guessed pair is introspection consistent [13], that is, whether:

(C1) Φ ∪ Ψ = 𝐴 K and Φ ∩ Ψ = ∅; (C2) Θ is propositionally consistent;

(C3) for each 𝜑 ∈ Φ, we have Θ ̸ ⊢ 𝜑 (where ⊢ denotes the provability relation of propositional logic).

Afterwards we check whether the introspection consistent pair (Φ, Ψ) corresponds to a minimal S4F model of 𝐴 [13, condition

], by checking if for every 𝜓 ∈ Ψ, we have

𝐴 ∪ {¬K𝜑 | 𝜑 ∈ Φ} ⊢S4F 𝜓.

The containment proof relies on the fact that S4F provability (Is a formula 𝜙 S4F-provable from a given finite set of premises 𝐴 ⊆ ℒ K ?) is in NP [13]. Since the number of calls to an NP-oracle is polynomial, existenceS4F is in Σ P 2 . A matching lower bound follows from the faithful embedding of default logic [5] into S4F, which will be covered in the next subsection.

S4F in Knowledge Representation

The logic S4F is immensely useful for knowledge representation purposes [13,4], as it allows to naturally embed several non-monotonic logics. Among others, it subsumes the (bimodal) logic of GK by Lin and Shoham [15] as well as the (bimodal) logic of MKNF by Lifschitz [16], all while being unimodal and thus arguably having a simpler semantics. In the following subsections, we briefly sketch how several well-known knowledge representation formalisms can be recovered in S4F, and note especially that all of them stay within the fragment of modal defaults.

Default Logic

Most importantly, the default logic of Reiter [5] can be faithfully and modularly embedded into S4F [11]: For a default 𝜙 : 𝜓1, . . . , 𝜓𝑛/𝜓, the corresponding S4F formula is given by (K𝜙∧K¬K¬𝜓1 ∧. . .∧K¬K¬𝜓𝑛) → K𝜓. Modularly here means that a default theory can be translated default by default, without looking at the whole theory, something that is not possible [17] when translating default logic into autoepistemic logic [18]. 5 Faithfully means that the extensions of the default theory are in one-to-one correspondence with the minimal models of the resulting S4F translation. (A similar translation exists for disjunctive default logic [21].) Deciding whether a propositional default theory has an extension is Σ P 2 -complete [22], thus providing the matching lower bound to S4F minimal model existence.

Logic Programs

In a similar vein, normal logic programs can be translated modularly into S4F [11,4]:

A rule 𝑝0 ← 𝑝1, . . . , 𝑝𝑚, ∼𝑝𝑚+1, . . . , ∼𝑝𝑚+𝑛 becomes (K𝑝1 ∧ . . . ∧ K𝑝𝑚 ∧ K¬K𝑝𝑚+1 ∧ . . . ∧ K¬K𝑝𝑚+𝑛) → K𝑝0. The translation is faithful with respect to the stable model semantics.

(This works similarly for extended/disjunctive logic programs [23,4].)

Argumentation Frameworks

Last but not least, also argumentation frameworks [24] (under stable semantics) can be modularly and faithfully translated into S4F. Given that argumentation frameworks (AFs) can be modularly translated into normal logic programs (over an extended vocabulary) using Dung's translation [24, Section 5; 25], we have the following straightforward result: Proposition 1. Given a (finite) argumentation framework 𝐹 = (𝐴, 𝑅), we define the following S4F theory:

𝑇𝐹 := {K¬K¬𝑎 → K𝑎 | 𝑎 ∈ 𝐴} ∪ {K𝑎 → K¬𝑏 | (𝑎, 𝑏) ∈ 𝑅}.

The stable extensions of 𝐹 and the minimal models of 𝑇𝐹 are in one-to-one correspondence.

Proof. Stable extension ⇝ minimal model: Let 𝑆 ⊆ 𝐴 be a stable extension of 𝐹 . Define the S4F structure ℳ𝑆 = (∅, {𝑤} , 𝜉) with 𝜉(𝑤) = 𝑆. We will show that ℳ𝑆 is a minimal model of 𝑇𝐹 .

1. ℳ𝑆 is a model of 𝑇𝐹 : Intuitively, the first part of the theory asserts that arguments are accepted unless they are defeated, and the second part expresses that an argument is defeated whenever one of its attackers is accepted.

• Consider 𝜑 = K¬K¬𝑎 → K𝑎 ∈ 𝑇𝐹 . If 𝑎 ∈ 𝑆,

Standpoint S4F

Standpoint S4F is the nesting of S4F into standpoint logic. More technically, in the nomenclature of many-dimensional modal logics [26], it is the product of the two logics above. This means that in each precisification, we have an "ordinary" S4F structure with two sets of worlds, which altogether come from a common pool of globally "available" possible worlds.

Syntax

As before, we start out from a set 𝒮 of standpoint names and a set 𝒜 of propositional atoms. We intend the language to be used to express what is known according to certain standpoints. This entails that nothing is known about the standpoints, but that they are an outer layer that is intuitively not accessible to the K modality. Accordingly, we restrict the ways the modalities can be nested already in the syntax: while S4F modality K can be used in the scope of a standpoint modality □s, we disallow the reverse. 6Definition 1. The language ℒ SK of SS4F is built via:

𝜙 ::= 𝜓 | ¬𝜙 | 𝜙 ∧ 𝜙 | □s𝜙 where 𝜓 ∈ ℒ K is a modal default, that is, 𝜓 ::= K𝜑 | ¬𝜓 | 𝜓 ∧ 𝜓 | K𝜓

with 𝜑 ∈ ℒ being a formula of propositional logic. ♢

We sometimes call formulas from ℒ K ∖ℒ subjective (because they depend on what is known), and those from ℒ objective formulas. For Boolean combinations, we allow the usual abbreviations 𝜑∨𝜓 := ¬(¬𝜑∧¬𝜓) and 𝜑 → 𝜓 := ¬𝜑∨𝜓, and for the (standpoint and S4F) modalities we sometimes use their duals M𝜑 := ¬K¬𝜑 and ♢ s 𝜑 := ¬□ s ¬𝜑.

Given an SS4F formula 𝜙 ∈ ℒ SK , as before (for S4F) we denote the set of its subformulas by Sub(𝜙). The size of a formula 𝜙 is defined as the number of its subformulas, that is, ‖𝜙‖ := |Sub(𝜙)|. Both notions generalise in a straightforward way to theories 𝑇 ⊆ ℒ SK .

An SS4F theory 𝑇 ⊆ ℒ SK is simple iff every formula 𝜙 ∈ 𝑇 is of the form □s𝜓 or ♢ s 𝜓 for some 𝜓 ∈ ℒ K .

Semantics

Definition 2. Consider a set 𝒜 of atoms and a set 𝒮 of standpoint names. A standpoint S4F structure is a tuple S = (Π, Ω, 𝜎, 𝜁, 𝛾) where • Π is a non-empty set of precisifications,

• Ω is a non-empty set of worlds,

• 𝜎 : 𝒮 → 2 Π assigns to each standpoint name a set of precisifications,

• 𝜁 : Π → 2 Ω × 2 Ω assigns to each precisification a pair of disjoint sets of worlds, where we denote 𝜁(𝜋) = (𝜁𝑜(𝜋), 𝜁𝑖(𝜋)) and require 𝜁𝑖(𝜋) ̸ = ∅,

• 𝛾 : Ω → 2 𝒜 assigns to each world a propositional evaluation. ♢

The set Π of precisifications is as before in standpoint logic, in that each precisification represents one possible point of view an entity could have, and where each precisification can belong to one or more standpoints (via 𝜎). The function 𝜁 assigns an S4F structure (𝜁𝑜(𝜋), 𝜁𝑖(𝜋), 𝛾) to each precisification, with outer worlds 𝜁𝑜(𝜋) and inner worlds 𝜁𝑖(𝜋), where worlds 𝑤 ∈ Ω can (but need not) be reused across precisifications. As usual, by a propositional evaluation 𝛾(𝑤) ⊆ 𝒜 we mean that all and only the elements of 𝛾(𝑤) are those atoms that are evaluated as true.

As is generally the case for Kripke structures, the evaluation of a formula in a structure might depend on the "point" in the structure at which we evaluate the formula. Since we now have a two-dimensional modal logic with S4F structures nested into standpoint structures, we use doubly pointed structures to clarify where in the nested structure we evaluate formulas. Definition 3. Let S = (Π, Ω, 𝜎, 𝜁, 𝛾) be an SS4F structure, 𝜋 ∈ Π, and 𝑤 ∈ Ω. The satisfaction relation ⊩ for pointed standpoint S4F structures is defined as follows: and

𝑤 ′ ∈ 𝜁𝑜(𝜋 ′ ) ∪ 𝜁𝑖(𝜋 ′ ) ♢

So while objective formulas (those without any modalities) are evaluated in the world, subjective formulas are evaluated with respect to a specific precisification, where standpoint modalities are evaluated with respect to a set of precisifications according to the used standpoint symbol.

We say that:

• S, 𝜋, 𝑤 is a model for 𝜙 iff S, 𝜋, 𝑤 ⊩ 𝜙,

• S, 𝜋 is a model for 𝜙, written S, 𝜋 ⊩ 𝜙, iff (Π, Ω, 𝜎, 𝜁, 𝛾) , 𝜋, 𝑤 ⊩ 𝜙 for all 𝑤 ∈ 𝜁𝑜(𝜋) ∪ 𝜁𝑖(𝜋),

• S is a model for 𝜙, written S ⊩ 𝜙, iff (Π, Ω, 𝜎, 𝜁, 𝛾) , 𝜋 ⊩ 𝜙 for all 𝜋 ∈ Π.

As usual, a standpoint S4F structure (Π, Ω, 𝜎, 𝜁, 𝛾) is a model for a theory 𝑇 , written (Π, Ω, 𝜎, 𝜁, 𝛾) ⊩ 𝑇 , iff (Π, Ω, 𝜎, 𝜁, 𝛾) ⊩ 𝜙 for all 𝜙 ∈ 𝑇 . Likewise, a theory 𝑇 entails a formula 𝜙, written 𝑇 |= SS4F 𝜙, iff every model of 𝑇 is a model of 𝜙. We say that a formula 𝜙 ∈ ℒ SK is satisfiable iff there exists a standpoint S4F structure S = (Π, Ω, 𝜎, 𝜁, 𝛾), a precisification 𝜋 ∈ Π, and a world 𝑤 ∈ 𝜁𝑜(𝜋) ∪ 𝜁𝑖(𝜋) such that (Π, Ω, 𝜎, 𝜁, 𝛾) , 𝜋, 𝑤 ⊩ 𝜙.

Non-Monotonic Semantics

As usual, a non-monotonic semantics can be obtained by restricting attention to models that are in some sense minimal.

Here, we require what we call local minimality, where knowledge has to be minimal in each precisification (according to the requirements of minimal S4F models), but the overall structure of precisifications and extents of standpoint names is allowed to freely vary. Before the minimisation of knowledge at each precisification can be carried out, one first has to determine which of the (sub)formulas of the original theory are relevant at that precisification. The formal definitions follow.

Definition 4 (Potentially relevant subformulas).

Given a set Π of precisifications, a set 𝒮 of standpoint names, a standpoint assignment function 𝜎 : 𝒮 → 2 Π , and a simple theory 𝑇 , we define the set of potentially relevant subformulas for a particular precisification 𝜋 ∈ Π as

𝑇 □ 𝜋 = {𝜙 ∈ Sub(𝑇 ) | ∃s ∈ 𝒮 : 𝜋 ∈ 𝜎(s) and (□ s 𝜙 ∈ 𝑇 or ♢ s 𝜙 ∈ 𝑇 )} ♢

The potentially relevant formulas will then be used for determining the non-monotonic semantics of simple theories, in that they provide an upper bound on what can possibly be known in a precisification.

Definition 5 (Locally minimal model).

For a simple standpoint S4F theory 𝑇 , we say that S = (Π, Ω, 𝜎, 𝜁, 𝛾) is a locally minimal model of 𝑇 iff (1) S ⊩ 𝑇 and (2) for each 𝜋 ∈ Π there exists an S4F theory Ξ𝜋 ⊆ 𝑇 □ 𝜋 such that (︁ 𝜁𝑜(𝜋), 𝜁𝑖(𝜋), 𝛾| 𝜁(𝜋) )︁ is a minimal S4F model for Ξ𝜋. 7 ♢ Intuitively, for a precisification 𝜋 ∈ Π, the theory Ξ𝜋 contains all standpoint-free formulas that are relevant at 𝜋. Local (S4F) minimality then guarantees that in each precisification of the overall structure, there is no unjustified knowledge (w.r.t. the theory Ξ𝜋). Accordingly, nonmonotonic entailment can then be defined as usual, that is, with respect to locally minimal models only. Definition 6. Given a standpoint S4F theory 𝑇 ⊆ ℒ SK that is simple, we say that a formula 𝜙 ∈ ℒ SK is:

Complexity

In this section we will show that the SS4F reasoning tasks we defined are not harder than their S4F counterparts. We start out with showing that standpoint S4F possesses, much like other standpoint logics [6], the small model property, where satisfiable theories are guaranteed to have models of linear size.

Lemma 2 (Small model property). An SS4F formula 𝜙 is satisfiable if and only if 𝜙 has a model with at most |Sub(𝜙) ∩ ℒ SK | ≤ ‖𝜙‖ precisifications.

Proof. The "if" direction holds trivially. For the "only if" direction, consider an arbitrary SS4F structure S = (Π, Ω, 𝜎, 𝜁, 𝛾) such that S ⊩ 𝜙. We will show that it can be "pruned" to obtain a small model

S ′ = (Π ′ , Ω ′ , 𝜎 ′ , 𝜁 ′ , 𝛾 ′ ) with |Π ′ | ≤ |Sub(𝜙) ∩ ℒ SK |.

We will consider a set of precisifications that will serve as witnesses for the satisfaction of subformulas preceded by a diamond modality (i.e. some □s in negative polarity.)

To this end, let Π ′ be a subset of Π with the following property: for each subformula □s𝜓 ∈ Sub(𝜙) not satisfied in S, Π ′ contains one precisification 𝜋 𝜓 ∈ Π, for which S, 𝜋 𝜓 ̸ ⊩ 𝜓 holds (note that the existence of such a 𝜋 𝜓 follows directly from the definition of ⊩.) Otherwise, assuming all □s𝜓 are satisfied in S, we set Π ′ = {𝜋} for an arbitrary 𝜋 ∈ Π. The definition of the remaining components of S ′ is restricted to Π ′ , i.e.,

• Ω ′ = Ω ∩ ⋃︀ 𝜋∈Π ′ 𝜁 ′ (𝜋),

• 𝜎 ′ (s) = 𝜎(s) ∩ Π ′ for each s ∈ 𝒮,

• 𝜁 ′ = 𝜁| Π ′ and 𝛾 ′ = 𝛾| Ω ′ .

To show that S ′ ⊩ 𝜙, we fill first prove an intermediate result by induction on the structure of each subformula 𝜓 ∈ Sub(𝜙): for every 𝜋 ∈ Π ′ it holds that S, 𝜋 ⊩ 𝜓 ⇐⇒ S ′ , 𝜋 ⊩ 𝜓. The only interesting case is when 𝜓 = □s𝜓 ′ . Assuming that S, 𝜋 ⊩ □s𝜓 ′ , by the semantics we get that S, 𝜋 ′ ⊩ 𝜓 ′ for every 𝜋 ′ ∈ 𝜎(s). Because 𝜎 ′ (s) ⊆ 𝜎(s) and 𝜎 ′ (s) ⊆ Π ′ by induction hypothesis we get that S ′ , 𝜋 ′′ ⊩ 𝜓 ′ for every 𝜋 ′′ ∈ 𝜎 ′ (s) and consequently (by semantics) S ′ ⊩ □s𝜓 ′ . Conversely, assume that S, 𝜋 ̸ ⊩ □s𝜓 ′ . Then there is 𝜋 ′ ∈ Π such that 𝜋 ′ ∈ 𝜎(s)

and S, 𝜋 ′ ̸ ⊩ 𝜓 ′ . Since by construction of S ′ we required that for each formula of the form □u𝛼 not satisfied in S a "witness" precisification 𝜋𝛼 ∈ 𝜎(u) such that S, 𝜋𝛼 ̸ ⊩ 𝛼 is contained in Π ′ , w.l.o.g. we can assume that 𝜋 ′ = 𝜋𝛼 and therefore 𝜋 ′ ∈ Π ′ . Then also 𝜋 ′ ∈ 𝜎 ′ (s) and by induction hypothesis we have that S ′ , 𝜋 ′ ̸ ⊩ 𝜓 ′ and consequently S ′ ̸ ⊩ □s𝜓 ′ , which concludes the proof of the intermediate result.

Since 𝜙 ∈ Sub(𝜙) and S ⊩ 𝜙 we get S, 𝜋 ⊩ 𝜙 for every 𝜋 ∈ Π. Naturally, since Π ′ ⊆ Π also S, 𝜋 ′ ⊩ 𝜙 for every 𝜋 ′ ∈ Π ′ . Then by our intermediate result we get that S ′ , 𝜋 ′ ⊩ 𝜙 for every 𝜋 ′ ∈ Π ′ and consequently S ′ ⊩ 𝜙. □

Complexity of SS4F reasoning tasks

We extend the reasoning tasks for S4F to the SS4F case in a straightforward manner, e.g. existence SS4F decides whether a simple theory 𝑇 ⊆ ℒ SK has a locally minimal SS4F model. (Since locally minimal models are only defined for simple theories, all subsequent results are necessarily restricted to this fragment; we will not always explicitly state the requirement that theories be strict.) In what follows we show that for locally minimal models, the complexities of SS4F reasoning tasks match those of S4F.

We say that an SS4F structure (Π, Ω, 𝜎, 𝜁, 𝛾) is pointwise S5 iff for every 𝜋 ∈ Π, we find 𝜁𝑜(𝜋) = ∅. Obviously, by definition of S4F minimal models, every locally minimal model (of some simple theory 𝑇 ) is pointwise S5.

We start out with some preparatory observations on SS4F structures. The first result looks trivial, it however is not, and crucially hinges on the fact that (1) modal defaults allow atoms only within the scope of K;8 and ( 2) that we restrict attention to structures that are pointwise S5, and thus offer negative introspection. Afterwards, we check whether an introspection consistent pair (Φ𝜋, Ψ𝜋) corresponds to a minimal S4F model of Ξ𝜋,by checking if for every 𝜓 ∈ Ψ𝜋,

Ξ𝜋 ∪ {¬K𝜑 | 𝜑 ∈ Φ𝜋} ⊢S4F 𝜓

The above requires at most polynomially many calls to an NP oracle (the number of calls is polynomially bounded by the cardinality of the set Ψ𝜋; the oracle decides ⊢ and ⊢S4F). At this step, it is proven that at each precisification 𝜋, the pair (Φ𝜋, Ψ𝜋) represents a minimal S4F model for the relevant theory Ξ𝜋. What remains to be proven is whether the entire construction, namely

(︁ Π, 𝜎, (Φ, Ψ, Ξ) 𝜋∈Π )︁

, is a model for the initial SS4F theory 𝑇 (condition (1) of Definition 5).

It is clear that for all 𝜋 ∈ Π, we have Sub(Ξ𝜋) ⊆ Sub(𝑇 ) and the local theory Ξ𝜋 is satisfied at 𝜋; what remains to be detected is whether there is a modal default 𝜙 ∈ 𝑇 □ 𝜋 ∖ Ξ𝜋 that has wrongly been excluded from being relevant at 𝜋. This can be checked locally using the NP oracle again, making use of Θ𝜋 at each precisification 𝜋. The procedure will be given inductively on the structure of an SS4F formula 𝜙.

To this end we define the following relations ⊪ + and ⊪ − , where we abbreviate T𝜋 := (Φ𝜋, Ψ𝜋, Ξ𝜋) for brevity.

T𝜋 ⊪ + □s𝜑 :⇐⇒ T 𝜋 ′ ⊪ + 𝜑 for every 𝜋 ′ ∈ 𝜎(s) T𝜋 ⊪ − □s𝜑 :⇐⇒ T 𝜋 ′ ⊪ − 𝜑 for some 𝜋 ′ ∈ 𝜎(s) T𝜋 ⊪ + K𝜑 :⇐⇒ Θ𝜋 ⊢ 𝜑 T𝜋 ⊪ − K𝜑 :⇐⇒ Θ𝜋 ̸ ⊢ 𝜑 T𝜋 ⊪ + ¬𝜑 :⇐⇒ T𝜋 ⊪ − 𝜑 T𝜋 ⊪ − ¬𝜑 :⇐⇒ T𝜋 ⊪ + 𝜑 T𝜋 ⊪ + 𝜑 ∧ 𝜓 :⇐⇒ T𝜋 ⊪ + 𝜑 and T𝜋 ⊪ + 𝜓 T𝜋 ⊪ − 𝜑 ∧ 𝜓 :⇐⇒ T𝜋 ⊪ − 𝜑 or T𝜋 ⊪ − 𝜓

Our approach then is to verify that T𝜋 ⊪ + 𝜙 for all 𝜙 ∈ 𝑇 and 𝜋 ∈ Π (which can be done in deterministic polynomial time with an NP oracle for deciding ⊢ in the cases with K𝜑), and we claim that this establishes overall modelhood of the guessed structure for 𝑇 . To show this correspondence, we define (slightly abusing notation S) the SS4F structure S(Π, 𝜎, (T𝜋) 𝜋∈Π ) = (Π, Ω, 𝜎, 𝜁, 𝛾) based on the partitionings (T𝜋) 𝜋∈Π as follows:

• Ω = ⋃︀ 𝜋∈Π Ω𝜋 where for every 𝜋 ∈ Π, we set

Ω𝜋 = ¶ (𝜋, 𝜈) ⃓ ⃓ ⃓ 𝜈 ⊆ 𝒜 + with 𝜈 ⊩ Θ𝜋 © denoting 𝒜 + = 𝒜 ∪ {K𝜑 | K𝜑 ∈ Sub(𝑇 )};

• 𝜁𝑜(𝜋) = ∅ and 𝜁𝑖(𝜋) = Ω𝜋 for every 𝜋 ∈ Π;

• 𝛾((𝜋, 𝜈)) = 𝜈 for every (𝜋, 𝜈) ∈ Ω𝜋.

Note that we allow all formulas K𝜑 ∈ Sub(𝑇 ) to be evaluated as "virtual atoms" in every world in every precisification. This leads us to our first technical observation: The definition of the S5 structures at each precisification 𝜋 ∈ Π along with the conditions (C1)-(C3) verified earlier exactly provides the desired correspondence between the "propositional" reading (via the propositional theory Θ𝜋) and the "S4F" reading (via the S5 structure Ω𝜋) of S4F formulas: Claim 2. For every precisification 𝜋 ∈ Π and potentially relevant formula 𝜓 ∈ Sub(𝑇 ) ∩ (ℒ K ∪ ℒ):

(∀𝑤 ∈ Ω𝜋 : 𝛾(𝑤) ⊩ 𝜓) ⇐⇒ (︁ ∀𝑤 ∈ Ω𝜋 : S(Π, 𝜎, (T𝜋) 𝜋∈Π ), 𝜋, 𝑤 ⊩ 𝜓 )︁

Proof of the claim. We use induction on the structure of 𝜓; since we also cover ℒ, the base case is for 𝜓 = 𝑝 ∈ 𝒜. Most of the cases are trivial, the only interesting case is for 𝜓 = K𝜑, which in turn covers all 𝜑 ∈ ℒ K ∪ ℒ. We first use 𝜑 ∈ (Sub(𝑇 ) ∩ ℒ K ) K = Ψ𝜋 ∪ Φ𝜋 to show: ♢

Θ𝜋 |= K𝜑 ⇐⇒ Θ𝜋 |= 𝜑 ( †) If Θ𝜋 |= K𝜑,

To obtain the desired result, we will prove (making use of Claim 2 in the base case) that given the SS4F theory 𝑇 and the guessed structure (︁ Π, 𝜎, (Φ, Ψ, Ξ) 𝜋∈Π )︁ of partitions, we can verify modelhood by checking ⊪ + and ⊪ − , more formally, for all precisifications 𝜋 ∈ Π and for all 𝜙 ∈ Sub(𝑇 ):

T𝜋 ⊪ + 𝜙 ⇐⇒ S(Π, 𝜎, (T𝜋) 𝜋∈Π ), 𝜋 ⊩ 𝜙 (1) T𝜋 ⊪ − 𝜙 ⇐⇒ S(Π, 𝜎, (T𝜋) 𝜋∈Π ), 𝜋 ⊩ ¬𝜙 (2)

The proof works by structural induction on 𝜙.

• 𝜙 = K𝜓. Then 𝜓 ∈ Sub(𝑇 ) ∩ (ℒ K ∪ ℒ), and regarding (1) we obtain: The construction of a witnessing model can also be used for credulous reasoning, where we additionally verify that (Φ𝜋, Ψ𝜋, Ξ𝜋) ⊪ + 𝜙 for all 𝜋 ∈ Π to demonstrate that 𝑇 | ≈ cred 𝜙. In a similar vein, for sceptical reasoning, we guess a locally minimal model for 𝑇 and verify that (Φ𝜋, Ψ𝜋, Ξ𝜋) ⊪ − 𝜙 for some 𝜋 ∈ Π to show that 𝑇 | ̸ ≈ scep 𝜙.

T𝜋 ⊪ + K𝜓 ⇐⇒ Θ𝜋 ⊢ 𝜓 ⇐⇒ Θ𝜋

Proposition 6. in-some SS4F and not-in-all SS4F are Σ P 2complete, in-all SS4F is Π P 2 -complete.

Instantiations

Intuitively, each precisification of a locally minimal SS4F model encodes an S4F minimal model for the locallyrelevant S4F theory. Given that S4F theories are capable of encoding multiple non-monotonic reasoning formalisms (as described in Section 2.5), we find that SS4F provides standpoint-enhanced variants of those formalisms. As such, each precisification of a locally minimal model encodes an extension of a default theory in case of standpoint default logic, stable extension in case of standpoint argumentation framework or an answer set in case of standpoint logic program. Below we provide examples of the first two SS4F instantiations.

Standpoint Default Logic

Utilising the S4F encoding of defaults we obtain standpoint defaults of the form

□s[(K𝜙 ∧ K¬K¬𝜓1 ∧ . . . ∧ K¬K¬𝜓𝑛) → K𝜓]

which we conveniently denote as □s[𝜙 : 𝜓1, . . . , 𝜓𝑛/𝜓]. Below we assume the standpoint default theory 𝑇 to be a set of standpoint defaults. To facilitate the reading of background knowledge, by formulas □sK𝜙 we denote modal defaults of the form □s[⊤ : /𝜙] (i.e. where 𝑛 = 0).

Example 3 (Example 1 continued).

The following S4F formulas of a theory 𝑇* express common knowledge, such as that we are indeed dealing with a coffee, that an espresso cannot be low in caffeine and that a drink cannot be hot and iced at the same time, i.e.

𝑇* = {Kcoffee, K¬(iced ∧ hot), K¬(espresso ∧ low _caffeine)}

We use 𝑇 □* to denote the set 𝑇 □* = {□ * 𝜙 | 𝜙 ∈ 𝑇*}. Additionally, we provide the set of standpoint defaults 𝑇𝐷 presented in the introduction, expressing that coffee is usually consumed hot, unless served in Vietnam, where iced variants are more common and that a typical coffee in Italy is a highly-caffeinated espresso, contrary to the typical, filtered coffee in the US. Therefore, we get the following conclusions:

𝑇𝐷 = ß □* [︁ coffee : hot/hot ]︁ , □ [︁ coffee : iced /iced ]︁ , □ [︁ coffee : espresso/espresso ]︁ , □[𝑇 | ≈ cred □ [︁ Kespresso ]︁ 𝑇 | ≈ cred □*Khot 𝑇 | ≈ cred □ [︁ Klow _caffeine ]︁ 𝑇 | ≈ cred □ [︁ Kiced ]︁

To emphasise the non-monotonic nature of our framework, we note that the two bottom conclusions would be retracted if we added additional background knowledge to 𝑇 stating e.g. that coffee is necessarily a hot, highly caffeinated drink:

□*K(coffee → (hot ∧ ¬low _caffeine)).

Standpoint (Abstract) Argumentation

Similarly, employing the S4F encodings of abstract argumentation frameworks with standpoint modalities gives rise to standpoint argumentation frameworks. A profile 𝒫 = (𝐹1, . . . , 𝐹𝑛) of 𝑛 argumentation frameworks (with 𝐹𝑖 = (𝐴𝑖, 𝑅𝑖) for all 1 ≤ 𝑖 ≤ 𝑛) can be encoded as a single SS4F theory 𝑇𝐹 over 𝒮 = {1, . . . , n, *} as follows: 1.]. Generally, in each view arguments draw from a common pool of arguments, whereas attacks between them are up for individual judgement of a respective agent. Here, the entire theory 𝑇𝐹 is defined as:

𝑇𝐹 := 𝑛 ⋃︁ 𝑖=1 {□ i [K¬K¬𝑎 → K𝑎] | 𝑎 ∈ 𝐴𝑖} ∪ {□ i [K𝑎 → K¬𝑏] | (𝑎, 𝑏) ∈ 𝑅𝑖}□V 1 ⎡ ⎢ ⎣ 𝑏 𝑔 𝑑 𝑐 𝑓 𝑒 ⎤ ⎥ ⎦ □V 2 ⎡ ⎢ ⎣ 𝑏 𝑔 𝑑 𝑐 𝑒 𝑎 ⎤ ⎥ ⎦ □V 3 ⎡ ⎢ ⎣ 𝑏 𝑔 𝑑 𝑐 𝑓 𝑒 𝑎 ⎤ ⎥ ⎦

where standpoint argumentation frameworks are used to express each of the distinct viewpoints, 𝑉1, 𝑉2 and 𝑉3. ♢

Viewpoints from Example 4 have the following stable extensions -𝑉1: {𝑐, 𝑒, 𝑔}, 𝑉2: {𝑎, 𝑐, 𝑒, 𝑔}, 𝑉3: {𝑎, 𝑐, 𝑒, 𝑔} and {𝑎, 𝑑, 𝑓 }. Since in a locally minimal SS4F model of 𝑇𝐹 each precisification must encode precisely one stable extension of a related framework, we find e.g. 𝑇𝐹 | ≈ cred □V 2 K𝑎 or 𝑇𝐹 | ≈ cred □*K𝑐, but 𝑇𝐹 | ̸ ≈ scep □*K𝑐. We consider how standpoint argumentation relates to approaches for collective acceptability in abstract argumentation discussed in the literature [28,27]. In the so-called argument-wise approaches, acceptability of the individual views (frameworks) is determined using standard methods (argumentation semantics) followed by semantic aggregation, where arguments deemed acceptable individually are aggregated into a single set of jointly accepted arguments. Other techniques, referred to as framework-wise, first aggregate individual views into a collective representation, e.g. single argumentation framework and then employ standard (or dedicated) methods to obtain the joint set of accepted arguments from that representation.

Semantics of standpoint argumentation, in which precisifications encode single stable extensions and where moreover standpoint modalities are employed to aggregate the extensions, follows the argument-wise approach. Interestingly, general (i.e. non-simple) SS4F theories are capable of capturing the framework-wise techniques e.g. the nomination rule [27], in which an attack between a pair of arguments in the resulting framework is established if it occurs in at least one of the input frameworks. For a set of all arguments of a profile 𝒫, defined as 𝐴𝒫 = 𝐴1 ∪ . . . ∪ 𝐴𝑛, necessitation can be obtained by instantiating the below schema for every pair of arguments 𝑎, 𝑏 ∈ 𝐴𝒫 :

♢ * [K𝑎 → K¬𝑏] → □*[K𝑎 ′ → K¬𝑏 ′ ].

In particular, instantiating the schema for 𝑇𝐹 would effectively amount to supplying 𝑇𝐹 with:

□* ⎡ ⎢ ⎣ 𝑏 ′ 𝑔 ′ 𝑑 ′ 𝑐 ′ 𝑓 ′ 𝑒 ′ 𝑎 ′ ⎤ ⎥ ⎦

In a similar vein, also the majority (resp. the unanimity) rule [27] -adding the attack if it is present in the majority (resp. all) of the individual frameworks -could be captured in SS4F. However, as mentioned above, enabling frameworkwise aggregation techniques requires non-simple SS4F theories, which is beyond the scope of this paper and is considered as future work.

Conclusion

In this paper we introduced standpoint S4F, a twodimensional modal logic for describing heterogeneous viewpoints that can incorporate default reasoning to make semantic commitments. We defined syntax and semantics and analysed the complexity of the most pertinent reasoning problems associated to our logic. The pleasant result was that incorporating standpoint modalities comes at no additional computational cost, as the complexity of the underlying logic, non-monotonic S4F, is preserved. We exemplified the new formalism by showcasing two instantiations with concrete NMR formalisms, namely Reiter's default logic [5] and Dung's argumentation frameworks [24]. A drawback of our current preliminary results is that we restricted our attention to simple theories, where standpoint modalities are essentially used only in an atomic form. The reason is that the definition of the set 𝑇 □ 𝜋 is hard to generalise without enabling to potentially guess unjustified knowledge into the locally relevant theory. For example, with 𝑇 = {□ s K𝑝 ∨ ¬□ s K𝑝} we expect, as the theory is tautological, a unique minimal model where nothing is known; alas, guessing Ξ𝜋 = {K𝑝} is not straightforward to avoid and leads to knowing 𝑝 without justification.

A potential fix via considering globally minimal models that do not require syntax-based guessing is the objective of current and future work. Furthermore, while we have mostly ignored sharpening statements s ⪯ u herein, they could be easily added, but would increase the amount of constructs to treat in checks and proofs.

In further future work, we intend to come up with a (disjunctive) ASP encoding for relevant fragments of SS4F with the intent of providing a prototypical implementation. We also want to study strong equivalence for SS4F; the case of plain S4F has been studied by Truszczyński [14]. Finally, it is also worthwhile to develop a proof system for our new logic. S4F has a proof system via the axioms (K), (T), (4), and (F); propositional standpoint logic has proof systems as well [1,29]. It will be challenging to combine these proof systems to obtain one for SS4F.