Standpoint logics allow to represent multiple heterogeneous viewpoints in a unifying framework based on modal logic. We propose to combine standpoint modalities with the single modality of the non-monotonic modal logic S4F, thus defining standpoint S4F. The resulting language allows to express semantic commitments based on default reasoning. We define syntax and semantics of the logic, study the computational complexity of reasoning problems in the fragment of simple theories, and showcase standpoint S4F by exemplifying two concrete instantiations of the general language - standpoint default logic and standpoint argumentation frameworks.
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 [
“it is unequivocal [from the point of view s] that ”; • □ s, expressing: • ♢ 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 [
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 22nd International Workshop on Nonmonotonic Reasoning, November 2–4, 2024, Hanoi, Vietnam * Corresponding author. † These authors contributed equally. $ piotr.gorczyca@tu-dresden.de (P. Gorczyca); hannes.strass@tu-dresden.de (H. Strass) 0000-0002-6613-6061 (P. Gorczyca); 0000-0001-6180-6452 (H. Strass) © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). 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 [
Example 1. Cofee is consumed diferently in diferent
parts of the world – what is considered to be a “typical
cofee” varies among countries. Usually ( * ) it is consumed
hot, however in Vietnam ( ) iced cofee is a more common
choice. Apart from the temperature, in Italy ( ), one of
the most popular cofee drinks – espresso – is much higher
in cafeine than the typically filtered cofee 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 [
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.
All languages we henceforth consider build on propositional semantics is given by interpretations ⊆ logic, denoted ℒ, and built from a set of atoms according to ::= | ¬ | ∧ where ∈ . Its model-theoretic containing exactly the true atoms, and we denote satisfaction of a for ⊢ mula 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 ⊢ if |= ).
given by
Standpoint Logic was introduced by Gómez Álvarez and
Rudolph [
::= | ¬ | ∧ | □ 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 = (Π, , precisifications , : → ), where Π is a non-empty set of 2 Π assigns a set of precisifications to each standpoint name (with (* ) = Π fixed), and : Π → 2 assigns a propositional interpretation to each ) satisfies formula (at point ), is
, ⊩ , indicating that the precisification. The relation structure = (Π, , defined by induction: (, {s}s∈ precisifications , ), where the worlds are given by the
Π, the evaluation function is given by , and the reachability relation among worlds for a standpoint name (i.e., modality) s ∈ is simply s = Π × (s).
S4F is a propositional modal logic with a single modality
K, read as “knows”. It was studied in depth by
Segerberg [
::= | ¬ | ∧ | K formally, a modal default is built via with ∈ . For formulas
∈ ℒK without occurrences of K, we write
∈ ℒ and call them objective formulas.
Truszczyński [
. 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 semantics of S4F is given by S4F structures, tuples ℳ = (, , ) where and are disjoint sets of worlds with ̸= ∅, and : ∪ → 2 assigns to each world a propositional interpretation () ⊆ . The satisfaction relation ℳ, ⊩ for ∈ ∪ is defined by induction: ℳ, ⊩ ℳ, ⊩ ¬ :⇐⇒ ∈ () :⇐⇒
ℳ, ⊮ ℳ, ⊩ 1 ∧ 2 :⇐⇒ ℳ, ⊩ 1 and ℳ, ⊩ 2 ℳ, ⊩ K
:⇐⇒ ®ℳ, ⊩ for all ∈ ∪ , if ∈ , ℳ, ⊩ for all ∈ , otherwise. if
ℳ, ⊩ ; ℳ, is a model of a theory ⊆ ℒ K if ℳ, ⊩ for all ∈ . A formula ∈ ℒK is satisfiable if there exists an S4F structure = (, , ) and a world ∈ ∪ such that (, , ) , ⊩ theories ). An S4F structure (, , ) is a model of a (likewise for ℳ formula ∈ ℒK (theory ⊆ ℒ
K), written (, , ) ⊩ (ℳ ⊩ ) if for all ∈ ∪ , we have (, , ) , ⊩ (for each ∈ ). A formula ∈ ℒK is entailed by a theory , written |=S4F , if every model of is a model of .
S4F structures can also be seen as a restricted form of ordinary Kripke structures ( ∪ , , ) with reachability relation := ( × ) ∪ ( × ) ∪ ( × itively, an S4F structure consists of two clusters of fully inter ). Intuconnected worlds, the inner worlds and outer worlds . The outer worlds can reach all (inner and outer) worlds, while the inner worlds can only reach all inner worlds.
The entailment relation |=S4F has a proof-theoretic characterisation ⊢S4F based on necessitation and axiom schemata K, T, 4, and F,2 with being ( ∧ MK ) → M(K ∨ ), 2This also explains the name S4F, as S4 is characterised by K, T, and 4. , ⊩ 1 ∧ 2 :⇐⇒ , ⊩ 1 and , ⊩ 2 As usual, a standpoint structure (Π, , ) is a model for a formula if (Π, , ) ⊩ ; a formula if there exist (Π, , ) and ∈ Π with (Π, , ∈ ℒS is satisfiable ) , ⊩ .1
Standpoint structures can be regarded as a
restricted form of ordinary (multi-modal) Kripke structures
1Original standpoint logic [
u indicating that every precisification , ⊩ , ⊩ ¬
, ⊩ □ s :⇐⇒ ∈ ( ) :⇐⇒ , ⊮ :⇐⇒ , ′ ⊩ for all ′ 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 = ( ′, , ′) if ′ = ∅, ′ ⊇ ,3 and for some ∈ ℒ, we have ⊩ but ℳ ̸⊩ .
positional 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 .
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.
Schwarz and Truszczyński [
The above reasoning tasks were found to reside on the
second level of the polynomial hierarchy, with the first three
being ΣP2-complete and the last one ΠP2-complete. We
recall the proof idea by Schwarz and Truszczyński [
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 3We consider a function : → to be a relation ⊆ × that is functional, i.e., where for each ∈ there exists at most one ∈ with (, ) ∈ . Consequently, then ⊇ for functions and simply means that assigns just as does, while may have a strictly larger domain. 4Note that for a general S4F formula (including objective formulas), this task is not reducible to in-someS4F in a straightforward way by simply asking whether ¬ is satisfied in some minimal S4F model of , as non-satisfaction does not imply satisfaction of the negation. eficiently 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 [
Afterwards we check whether the introspection consistent pair (Φ, Ψ) corresponds to a minimal S4F model of [13, condition (2)], 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 [
The logic S4F is immensely useful for knowledge
representation purposes [
S4F [11, 1, . . . , , ∼ +1, . . . , ∼ + 0 ← K0. stable (K1 ∧ . . . ∧ K ∧ K¬K+1 ∧ . . . ∧ K¬K+) → The translation is faithful with respect to the model semantics.
(This
works similarly for
extended/disjunctive logic programs [
rule
becomes
2.5.3. Argumentation Frameworks
Last but not least, also argumentation frameworks [
K | ∈ } ∪ {K →
K¬ | (, ) ∈ }.
The stable extensions of and the minimal models of are in one-to-one correspondence.
Proof. Stable extension ⇝ minimal model of . 1. ℳ is a model of : a stable extension of . Define the S4F structure (∅, {} , ) with () = . We will show that ℳ is a minimal model: Let ⊆
be ℳ = ℳ ⊩ whence ℳ ̸⊩ • Consider = • Consider = K¬K¬ →
K ∈ . If ∈ , then K and ℳ ⊩ . If ∈/ , then ℳ ⊩ K¬, K¬K¬ and ℳ ⊩ .
K →
K¬ ∈ . Then (, ) ∈ ℳ ̸⊩ and ℳ ⊩ . and since is stable, ∈/ or ∈/ . If ∈/ , then K and ℳ ⊩ . If ∈/ , then ℳ ⊩ K¬ 2. ℳ is minimal: Consider the S4F structure (, {} , ′) to be strictly preferred to ℳ . Then there = exist ∈ and ∈
ℒ such that ℳ ⊩ , ⊮ . In particular, ′() ̸= ′() = (), say, and ′()() ̸= ()() for ∈ . • ∈ . Then () ⊩ and ′() ⊩ ¬ and , ⊮ On the other hand, , ⊩
K whence , ⊮
K.
K¬ and , ⊩
K¬K¬. Therefore, , ⊮
K¬K¬ → K → K¬ ∈ . It firstly holds that , ⊮ is stable, there exists a ∈ with (, ) ∈ . Thus K¬.
¬ and ′() ⊩ . Since
K and thus ⊮ . • ∈/ . Then () ⊩ – ′() ⊩ . Then , ⊩ whence ⊮ .
K and , ⊮
K → K¬, whence ∈/ ℳ.
as in the case for ∈ above. – ′() ⊩
¬. Then, since ∈ , ⊮ can be shown Minimal model ⇝
stable extension: Let ℳ = (∅, , ) be a minimal model of . Define ℳ = { ∈ | ℳ ⊩ K}. 1. ℳ is conflict-free: Consider ∈ ℳ with (, ) ∈ . By definition of ℳ we get ℳ ⊩ K. From ℳ ⊩ we get ℳ ⊩
K → K¬. Thus, ℳ ⊩
K¬, whence ℳ ̸⊩
K, 2. ℳ attacks ∖ ℳ: We first show a helpful intermediate result: ℳ ⊩
K.
Claim 1. For all ∈ , we have ℳ ⊩ K or ℳ ⊩
K¬.
Proof of the claim. Assume ℳ ̸⊩ ists a ∈ such that ℳ, ⊩ is an S5 structure, we get ℳ ⊩ K¬. Then there ex
¬K¬. Since ℳ K¬K¬. By definition, K¬K¬ →
K ∈ , thus by ℳ ⊩ we get Let ∈ ∖ ℳ. Then ℳ ̸⊩ K, which by the claim definition of
ℳ we get ℳ ̸⊩ means that ℳ ⊩
K¬. Assume to the contrary of what we want to show that for all ∈ with (, ) ∈ , we have ∈/ ℳ, and consider any such ∈ . Then, by K. We now construct = (, , ∪ ) with = {} (w.l.o.g. ∈/ ) and () = ℳ ∪ {}. is strictly preferred to ℳ because , ⊮ ¬ while ℳ ⊩
¬, therefore it remains to show ⊩ to obtain the desired contradiction. To show this, we only need consider formulas involving , for which there are three possibilities: a) ⊩
K¬K¬ →
K: We have , ⊩
K¬ for and , ⊮
K¬K¬ for all ∈ ∪ .
any ∈ , whence , ⊮ ¬K¬ for all ∈ b) ⊩
K →
K¬: For any ∈ ̸= ∅, due to
K; we thus also get , ⊩ , ⊮
K.
¬ we have , ⊮ c) ⊩
K →
K¬: For all ∈ , we have ℳ, ⊮ By ∈/ ℳ, we also get , ⊮ K by assumption above, whence , ⊮ K.
K directly.
□ ♢
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.
Standpoint S4F is the nesting of S4F into standpoint logic.
More technically, in the nomenclature of many-dimensional
modal logics [
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.6 6While it would pose no technical obstacles to allow the reverse nesting in syntax and semantics, we choose this restriction to clarify the intended use of SS4F.
Definition 1.
where ∈ ℒK is a modal default, that is, ::= | ¬ | ∧ | □ s ::= K | ¬ | ∧ | K with ∈ ℒ being a formula of propositional logic.
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. ∈ is of the form □ s or ♢ s for some ∈ ℒK.
Definition 2. standpoint names. A standpoint S4F structure is a tuple
S = (Π, Ω, , , ) where ♢ ♢ ♢ ♢ :⇐⇒ :⇐⇒
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 if S, , ⊩ , • S, is a model for , written S, ⊩ , if
) , , ⊩ for all ∈ ( ) ∪ ( ), • S is a model for , written
S ⊩ , if ) , ⊩ for all ∈ Π.
As usual, a standpoint S4F structure (Π, Ω, , , model for a theory , written (Π, Ω, , , ) ⊩ ) is a , if (Π, Ω, , , ) ⊩ for all
∈ . Likewise, a theory entails a formula , written |=SS4F , if every model of is a model of . We say that a formula ∈ ℒSK is satisfiable if there exists a standpoint S4F structure S = (Π, Ω, , , ), a precisification such that (Π, Ω, , ,
) , , ⊩ .
∈ Π, and a world ∈ ( ) ∪ ( )
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 ifrst 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 names, a standpoint assignment function : → 2Π, and a simple theory , we define the set of potentially relevant subformulas for a particular precisification ∈ Π as of standpoint the function resulting from restricting the domain of to . 7For a function : → and a subset ⊆ , we denote by | • Π is a non-empty set of precisifications , • Ω is a non-empty set of worlds,
Π assigns to each standpoint name a set • : → 2
of precisifications, • : Π → 2Ω × 2
Ω assigns to each precisification a evaluation. pair of disjoint sets of worlds, where we denote ( ) = ( ( ), ( )) and require ( ) ̸= ∅, • : Ω → 2 assigns to each world a propositional :⇐⇒ ∈ () :⇐⇒
S, , ⊮ () ⊆ 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.
Let S = (Π, Ω, , , ) be an SS4F strucpointed standpoint S4F structures is defined as follows: ∈ Π, and ∈ Ω. The satisfaction relation ⊩ for Definition 3. ture, S, , ⊩ S, , ⊩ ¬ S, , ⊩ 1 ∧ 2 :⇐⇒ S, , ⊩
K
S, , ⊩ 1 and S, , ⊩ 2 ®S, , ′ ⊩ for all ′ ∈ ( ) ∪ ( ), if ∈ ( ), S, , ′ ⊩ for all ′ ∈ ( ), Local (S4F) minimality then guarantees that in each precisification of the overall structure, there is no unjustiifed knowledge (w.r.t. the theory Ξ ). Accordingly, nonmonotonic entailment can then be defined as usual, that is, with respect to locally minimal models only. that is simple, we say that a formula ∈ ℒSK is: Definition 6.
1. sceptically entailed by , written |≈ scep , if
S ⊩ for all locally minimal models S of ; 2. credulously entailed by , written |≈ cred , if
S ⊩ for some locally minimal model S of . ♢ Other, intermediate, notions of non-monotonic entailment are possible to define, but not our main interest here.
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 [
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 in S, Π′ contains one precisification ∈ Sub( ) not satisfied ∈ Π, for which restricted to Π′, i.e., 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 • Ω′ = Ω ∩ ⋃︀ ′( ), ∈Π′ • ′(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 S, ⊩ when ∈ ⇐⇒
Sub( ): for every
Π′ it holds that S′, ⊩ . The only interesting case is
∈ = □ s ′. Assuming that S, ⊩ □ s ′, by the secause ′(s) ⊆ (s) and ′(s) ⊆ mantics we get that S, ′ ⊩ ′ for every ′ ∈ (s). BeΠ′ 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 ⊩ every ∈ Π. Naturally, since Π′ ⊆ we get S, ⊩ for Π also S, ′ ⊩ for every ′ ∈ Π′. Then by our intermediate result we get that S′, ′ ⊩ for every ′ ∈ Π′ and consequently S′ ⊩ . □ 4.1. Complexity of SS4F reasoning tasks We extend the reasoning tasks for S4F to the SS4F case in a straightforward manner, e.g. existenceSS4F 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 (Π, Ω, , , S5 if for every
∈ Π, we find ( ) = ∅ 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 ofer negative introspection.
) is pointwise . Obviously, by Lemma 3. Let S = (Π, Ω, , , that is pointwise S5. Then for all ∈ Π and all ∈ ℒSK: S, ⊩ or and Φ , Ψ ⊆ (Sub( ) ∩ ℒK) . (We guess |Π| such triples without any oracle calls in between.)
For each precisification , we check whether their respective Φ , Ψ are introspection consistent, i.e. the following (for brevity we use the abbreviation Θ = Ξ ∪ {¬K | ∈ Φ } ∪ {K | ∈ Ψ } ∪ Ψ ): (C1) Φ ∪ Ψ = (Sub( ) ∩ ℒK) K and Φ ∩ Ψ = ∅, (C2) Θ is propositionally consistent, (C3) for each ∈ Φ , we have Θ ̸⊢ (where ⊢ denotes the provability relation of propositional logic).
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 the initial SS4F theory (condition (1) of Definition 5). construction, namely (︁ Π, , (Φ, Ψ, Ξ) ∈Π︁) , is a model for 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 . T ⊪ +
□ s T ⊪ − □ s T ⊪ T ⊪ − T ⊪ T ⊪ − T ⊪ + K +
K ¬ ¬ :⇐⇒ :⇐⇒ :⇐⇒ :⇐⇒ :⇐⇒ :⇐⇒
T ′ ⊪
+ for every ′ T ′ ⊪ − for some ′ 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(Π, , (T ) ∈Π ings (T ) ∈Π as follows: ) = (Π, Ω, , ,
S) the SS4F structure ) based on the partition• Ω = ⋃︀ Ω where for every ∈ Π, we set
To this end we define the following relations ⊪ + and ⊪ − , where we abbreviate T := (Φ , Ψ , Ξ ) for brevity. ⃓ ⃓ ) ⃓ ⊆
+ 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 with the conditions (C1)–(C3) verified earlier exactly provides the desired correspondence between the “propositional” reading (via the propositional theory Θ ) and the “S4F” reading ∈ Π along (via the S5 structure Ω ) of S4F formulas: Claim 2. For every precisification relevant formula ∈ Sub( ) ∩ (ℒK ∪ ℒ): ∈ Π and potentially (∀ ∈ Ω : () ⊩ ) ⇐⇒
︁( ∀ ∈ Ω : 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, then, since Θ is propositionally consistent – condition (C2) –, we have Θ ̸| = ¬K. Thus ¬K ∈/ Θ and in particular, ∈/ Φ , whence by (C1) we get ∈ Ψ . Then also ∈ Θ and Θ |
= . turn means K ∈ Θ and Θ |= K.
On the other hand, if Θ |
= , then Θ ⊢ , whence by (C3) we obtain ∈/ Φ . Thus, by (C1), ∈ Ψ , which in We now obtain:
∀ ∈ Ω : () ⊩ K ⇐⇒ Θ |= K (†) ⇐⇒ Θ |= ⇐⇒ ∀ ∈ Ω : () ⊩ (IH) ⇐⇒ ∀ ∈ Ω : S(Π,, (T ) ∈Π),, ⊩ ⇐⇒ ∀ ∈ ( ) : S(Π,, (T ) ∈Π),, ⊩ ⇐⇒ ∀ ∈ ( ) : S(Π,, (T ) ∈Π),, ⊩ K ⇐⇒ ∀ ∈ Ω : S(Π,, (T ) ∈Π),, ⊩ K This concludes the proof of Claim 2.
To obtain the desired result, we will prove (making use of Claim 2 in the base case) that given the SS4F theory and the gvuereisfsyedmsotrdueclhtuoroed(︁ bΠy,c,he(cΦk,inΨg,⊪Ξ)+ ∈aΠnd ⊪ − , more formally, ︁) of partitions, we can for all precisifications ∈ Π and for all ∈ Sub(): T ⊪ + ⇐⇒ S(Π,, (T ) ∈Π), ⊩ T ⊪ − ⇐⇒ S(Π,, (T ) ∈Π), ⊩ ¬ ♢ (1) (2) The proof works by structural induction on . • = K . Then ∈ Sub() ∩ (ℒK ∪ ℒ), and regarding (1) we obtain:
T ⊪ + K ⇐⇒ Θ ⊢ ⇐⇒ Θ |= ⇐⇒ ∀ ∈ Ω : () ⊩ (C⇐lai⇒m2) ∀ ∈ Ω : S(Π,, (T ) ∈Π),, ⊩ ⇐⇒ ∀ ∈ ( ) : S(Π,, (T ) ∈Π),, ⊩ ⇐⇒ S(Π,, (T ) ∈Π), ⊩ K Regarding (2) we get:
T ⊪ − K ⇐⇒ Θ ̸⊢ ⇐⇒ Θ ̸|= ⇐⇒ ∃ ∈ Ω : () ⊮ (C⇐lai⇒m2) ∃ ∈ Ω : S(Π,, (T ) ∈Π),, ⊮ ⇐⇒ ∃ ∈ ( ) : S(Π,, (T ) ∈Π),, ⊮ ⇐⇒ ∃ ∈ ( ) : S(Π,, (T ) ∈Π),, ⊮ K (S5) ⇐⇒ ∀ ∈ ( ) : S(Π,, (T ) ∈Π),, ⊮ K ⇐⇒ ∀ ∈ ( ) : S(Π,, (T ) ∈Π),, ⊩ ¬K ⇐⇒ S(Π,, (T ) ∈Π), ⊩ ¬K • = ¬ . We have, with regard to (1),
T ⊪ + ¬ ⇐⇒ T ⊪ − Similarly, for (2),
T ⊪ − ¬ ⇐⇒ T ⊪ + ⇐(IH⇒) S(Π,, (T ) ∈Π), ⊩ ¬ • = ∧ . We have and (IH) ⇐⇒ S(Π,, (T ) ∈Π), ⊩ (Corollary4) S(Π,, (T ) ∈Π), ⊩ ¬¬
⇐⇒
T ⊪ + ∧ ⇐⇒ T ⊪ + and T ⊪ + ⇐(IH⇒) S(Π,, (T ) ∈Π), ⊩
and S(Π,, (T ) ∈Π), ⊩ ⇐⇒ S(Π,, (T ) ∈Π), ⊩ ∧
T ⊪ − ∧ ⇐⇒ T ⊪ − or T ⊪ − ⇐(IH⇒) S(Π,, (T ) ∈Π), ⊩ ¬
or S(Π,, (T ) ∈Π), ⊩ ¬ (Corollary4) S(Π,, (T ) ∈Π), ⊮ ⇐⇒
or S(Π,, (T ) ∈Π), ⊮ (Definition3) S(Π,, (T ) ∈Π), ⊮ ∧
⇐⇒ (Corollary4) S(Π,, (T ) ∈Π), ⊩ ¬( ∧ )
⇐⇒ • = □ s . Then
T ⊪ + □ s and likewise
T ⊪ − □ s ⇐⇒ T ′ ⊪ + for every ′ ∈ (s) ⇐(IH⇒) S(Π,, (T ) ∈Π), ′ ⊩ for every ′ ∈ (s) ⇐⇒ S(Π,, (T ) ∈Π), ⊩ □ s ⇐⇒ T ′ ⊪ − for some ′ ∈ (s) (IH) ⇐⇒ S(Π,, (T ) ∈Π), ′ ⊩ ¬ for some ′ ∈ (s) (Corollary4) S(Π,, (T ) ∈Π), ′ ⊮ for some ′ ∈ (s) ⇐⇒ ⇐⇒ S(Π,, (T ) ∈Π), ⊮ □ s (Corollary4) S(Π,, (T ) ∈Π), ⊩ ¬□ s
⇐⇒ Thus by verifying T ⊪ + for all ∈ and ∈ Π, we have checked that the structure (︁ Π,, (Φ,Ψ,Ξ) ∈Π︁) (which we do not explicitly construct) constitutes a model of . Together with the checks done earlier, this establishes that T constitutes a locally minimal model of . □ Example 2. Consider the following simple SS4F theory: = {□ sK, □ sK( → ),□ tK,□ tK¬} A witnessing model representing the locally minimal SS4F model of could be ({ 1, 2},, (T 1,T 2)) with (s) = { 1}, (t) = { 2} and:
T 1 =({¬} ,{, → ,} ,{K, K( → )}) T 2 =({, → } ,{,¬} ,{K,K¬}). ♢
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 . P Proposition 6. in-someSS4F and not-in-allSS4F are Σ2complete, in-allSS4F is ΠP2-complete.
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.
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 cofee, that an espresso cannot be low in cafeine 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 cofee is
usually consumed hot, unless served in Vietnam, where iced
variants are more common and that a typical cofee in Italy is
a highly-cafeinated espresso, contrary to the typical, filtered
cofee in the US.
=
We obtain the standpoint default theory = ∪ □ * .♢
Since extensions of a default theory can be characterised by
ifnite sets of defaults’ consequences [
2 : * ∪ {iced } 3 : * ∪ {hot , espresso}
4 : * ∪ {hot , low _caffeine} .
Therefore, we get the following conclusions: |≈ cred □ |≈ cred □ ︁[ Kespresso]︁
|≈ cred □ * Khot ︁[ 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 cofee is necessarily a hot, highly cafeinated drink: □ * K(coffee → (hot ∧ ¬low _caffeine)).
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: := ⋃︁ {□ i[K¬K¬ → K] | ∈ } ∪ =1
{□ i[K → K¬] | (, ) ∈ }
Example 4 presents individual frameworks in their usual graphical representation, i.e. with nodes denoting arguments and edges attacks between them. For such a representation being within the scope of a standpoint modality means that each node and attack is encoded for this standpoint using the formula above.
Example 4 ([
⎡ V1 ⎣⎢ ⎡ ⎡ V2 ⎣⎢ V3 ⎣⎢ ⎤ ⎤ ⎤ ⎥ ⎦ ⎥ ⎦ ⎥ ⎦ 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 □ V2 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 [
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 [
♢ * [K → K¬] → □ * [K′ → K¬′].
In particular, instantiating the schema for would efectively amount to supplying with:
⎡ ′
□ * ⎣⎢
′
′
′
′
′
′ ⎤
⎥
⎦
In a similar vein, also the majority (resp. the unanimity)
rule [
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 [
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 = {□ sK ∨ ¬□ sK} 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 [
We are indebted to Lucía Gómez Álvarez for helpful discussions on the subject matter.
We also acknowledge funding from BMBF within projects KIMEDS (grant no. GW0552B), MEDGE (grant no. 16ME0529), and SEMECO (grant no. 03ZU1210B).