7

In topos theory there are modal operators known as the Lawvere-Tierney operators. Such an operator is a certain endomorphism $j : \Omega \to \Omega$ on the subobject classifier. The object $J$ of all such operators is definable in the internal language of the topos, and so we can quantify over all $j$'s. My topos-theoretic knowledge is too poor to know ...


5

There is a trivial sense in which the answer is yes. For any proposition $P$, there's a modality $O_P$ called the open modality determined by $P$, defined by $O_P(X) \equiv (P\to X)$. If you take $P$ to be the statement of the axiom of choice (relative to some universe), then for $M=O_P$ the type you showed is inhabited, since you get to use the axiom of ...


5

Modal logic does not capture any interesting complexity class. As it is invariant under bisimulation, it cannot even test whether the vertex $w$ has degree greater than $2$, which is a constant time property. We are interested in ML for a different reason: ML is the bisimulation invariant fragment of first-order logic (Theorem of van Benthem). In other words,...


5

Here is a sketch (massively simplifying for reasons of pedagogy): Setting the scence. You can think of logic as a tool, an API in computing parlance, to reason about things, where reasoning means deriving true statements from true assumptions. The things that we reason about using logic is called a model. What makes logic useful is that this API, in ...


4

The logic is EXP-complete. One way to prove the lower bound is to note that the logic KTB augmented with universal modality, or even just the global consequence relation of KTB, is EXP-complete (Chen and Lin [1]; note that they denote KTB as B). Note that a connected IK5-frame $(W,R,R^{-1})$ is either a single irreflexive point, or it consists of a ...


4

The key idea here is that for any conjunction of equations $F\equiv u_1=v_1\wedge\ldots\wedge u_k=v_k$, the set $S_F$ is convex in the geometric sense, i.e. for any two points $p,q\in S_F$, all points between $p$ and $q$ are also in $S_F$. Now suppose that $F\Rightarrow G$, where $G$ is a disjunction of equations $x_1=y_1\vee\ldots\vee x_n=y_n$ (note that ...


4

Perhaps relevant are term-modal logics. Term-modal logics are a family of qunatified modal logics in which the subscript of the modal operators are terms of a first-order language mkaing e.g. $\exists x K_x \varphi(x)$ a well-formed formula. You can find a recent review of the literature in this paper: https://arxiv.org/abs/1906.06047


3

For Q1, the answer is yes if we consider image-finite systems: for all node $t$ and label $a$, the number of $a$-successors of $t$ must be finite. In this case you don't even need fixpoints of the $\mu$-calculus, only the fragment called Hennessy-Milner Logic to distinguish non-bisimilar structures [HM85]. This is known as the Hennessy-Milner Theorem. ...


2

There's a lot to unpack here and I don't know about Goguen's institutions. But perhaps I can give a partial answer to your question. Let's start with "simple interpretations" of RDF, as defined by the spec, forgetting about richer languages like RDFS or OWL. If we ignore IRIs and literals, as in the first part of your question, then an RDF model is a simple ...


1

How about just a blanket statement with no assumptions: A and B may be the same part of C This would seem to be valid by the same reasoning! However it is only so if "may" ranges over all models of the language. If, as is usual, "may" only ranges over the possible worlds in a single model, it is not valid.


1

Not open source, but the AI engines of some successful computer games are based on modal logic, see e.g. "Using Exclusion Logic to Model Social Practices" and "Introducing Exclusion Logic as a Deontic Logic" by Richard Evans.


1

What semantics of the logical operators would you like to have? Two of the best studied semantics for degrees are (propositional) Łukasiewicz logic and Gödel-Dummet logic. The latter enforces the domain to be a linear order which would allow you to model them via the naturals. It is also axiomatizable, since it is equivalent to intuitionistic propositional ...


Only top voted, non community-wiki answers of a minimum length are eligible