Questions tagged [modal-logic]
The modal-logic tag has no summary.
114 questions
10 votes
1 answer
491 views
Pure buttons in the modal logic of forcing
I've been trying to understand what it means for a button to be pure in the context of the modal logic of forcing, and it would help to have an example of a button which is not a pure button. Based on ...
- 345
3 votes
1 answer
219 views
Do independent collections of infinitely many buttons and infinitely many switches exist in models other than V=L?
The original paper by Hamkins and Löwe that the modal logic of forcing is exactly S4.2 uses the fact that there is consistently a model with an independent collection of infinitely many buttons and ...
- 345
1 vote
0 answers
79 views
Correspondence for distribution?
Take the distribution axiom, DA, of a modal logic to be: $\Box(A\to B)\to (\Box A \to \Box B).$ As there are distribution-free modal logics which do not have DA: What does DA correspond to in frames ...
- 4,122
4 votes
1 answer
217 views
Software for testing validity of propositional formulas in finite Kripke frames (modal SAT)
I have a formula $\varphi$ of propositional modal logic or propositional intuitionistic logic, a finite Kripke frame $W$, and I would like to test whether $\varphi$ is valid in $W$. This is an ...
- 38.1k
3 votes
1 answer
213 views
What corresponds to the necessitation rule in modal logics
In modal logics, the necessitation rule licences the inference from $\vdash p$ to $\vdash \Box p.$ Given a modal logic $\mathcal{L}$ with characteristic axioms in the set $\Sigma$, does the ...
- 4,122
3 votes
0 answers
69 views
Proving a proposition about the provability logic GL without using its completeness theorem
Let $GL$ be the provability logic containing the axioms $K := \Box (\varphi\to \psi)\to (\Box \varphi\to \Box \psi)$ and $L := \Box(\Box \varphi \to \varphi)\to \Box \varphi$, along with the ...
1 vote
0 answers
295 views
Christoph Benzmüller and Gödel's ontological proof?
Are there any notable mathematical or logical issues within Christoph Benzmüller and Bruno Woltzenlogel-Paleo formalized Gödel's ontological proof (pdf) that has been identified by the community?
2 votes
0 answers
70 views
Is the class of strongly Kripke complete normal modal logics closed under sums?
Given an arbitrary set of normal modal logics $\mathcal{L}$, one can define their sum $\bigoplus \mathcal{L}$ (or $\bigoplus_{L \in \mathcal{L}} L$ if you prefer) to be the least normal modal logic ...
- 21
6 votes
1 answer
472 views
Why is it not possible to define the necessity operator internally $\Box: \Omega \to \Omega$ in a topos?
I am looking for ways to internalize the modal operator of necessity $\Box$, ending up with a morphism $\Box: \Omega \to \Omega$ satisfying the necessitation rule (if $\phi$, then $\Box \phi$) and the ...
- 63
4 votes
1 answer
299 views
Are there atoms in the lattice of intermediate logics?
A few days ago I stumbled upon this question on MS. The question is: Does the lattice of intermediate logics have an atom, i.e. an element that is strictly stronger than IPC but not strictly stronger ...
- 173
2 votes
1 answer
198 views
Kripke frame, lattice and some intermediate logics
For a given finite and rooted intuitionistic Kripke frame $\mathcal{F}$, let $\log(\mathcal{F})=\{\phi : \mathcal{F}\vDash \phi\}$ and assume $S=\{\log(\mathcal{F}): \mathcal{F} \text{ is finite and ...
- 47
4 votes
0 answers
187 views
Do coproducts injections of Heyting algebras have left and right adjoints?
Given two Heyting algebras $A$ and $B$, let $A+B$ be their coproduct in the category of Heyting algebras. Is it true that the inclusion $A → A+B$ always has a left and a right adjoint ? (Actually, I ...
- 135
0 votes
0 answers
86 views
two different intermediate logics whose intersection is Int
Call a partial order $\mathcal{F}=(F, \leq)$ rooted if there is an element $a \in F$ such that for any $b \in F$, $a\leq b$. Let $\mathcal{F}_0$ and $\mathcal{F}_1$ be two different finite rooted ...
- 47
2 votes
0 answers
234 views
Reference request for a modification of Bi-Intuitionistic Logic
I’ve asked this same question on math.stackexchange.com, but haven’t received any answers. I ask this question in good faith, so I hope it meets this site’s standards. I have been spending the better ...
- 184
1 vote
1 answer
150 views
Normal modal Logic with finite proposition letters
Assume our modal language $L$ has only diamonds, and the set of proposition letters $Prop$ is finite. The deduction rules are the same as normal modal logic. Now consider $M$ is a finite model of this ...
- 11
2 votes
1 answer
254 views
An extension of the disjunction property in modal logic
A normal modal propositional logic $\Delta$ has the disjunction property if and only if For any formulas $A_1,\dotsc,A_n$, if $\Box A_1 \vee \dotsb\vee \Box A_n \in \Delta$ then $A_k\in \Delta$ for ...
- 357
2 votes
0 answers
123 views
Can this order relation, defined in terms of all topological spaces, be defined in terms of the reals alone?
Let $K$ be the operator monoid under composition of Kuratowski's $14$ set operators generated by topological closure $k$ and complement $c.$ Kuratowski's 1922 paper gives the poset diagram of the ...
- 902
2 votes
0 answers
94 views
A formula which is true in all possibilities for variables in IPL
Let $\mathcal{F}(n, 2^m)$ be an intuitionistic Kripke in Fig. 1, which is formed by the set $$ \left\{(i, j)\in \omega \times \omega \mid (0 \leq i \leq n-3, 0 \leq j \leq 1) \vee (i= n-2, 0 \leq j \...
- 53
3 votes
0 answers
155 views
A class of Kripke frames which preserves validity
The background of our discussion is intuitionistic logic, i.e. the following definitions are intuitionistic Kripke frame. For $1\leq s\leq n-2$, the frame $\mathcal{C}_n(s)$ denotes the frame which is ...
- 53
6 votes
1 answer
241 views
Preserve validity between the two Kripke frames
The background of our discussion is intuitionistic logic, i.e. the following definitions are intuitionistic Kripke frame. For $n \geq 1$, let $\mathcal{C}_n$ denote the frame which is shown in Fig.1. ...
- 53
1 vote
0 answers
86 views
Descriptive general frames without differentiation?
Descriptive general frames are usually defined as general frames that are tight, compact, and differentiated. On p.91 of this paper by Skvortsov and Shehtman 1993, the authors omit the third condition,...
4 votes
0 answers
267 views
Do the transitive models of ZFC form a canonical Kripke model for the Gödel-Löb axioms?
Let $\mathcal{C}$ be the class of all transitive models of ZFC, i.e., sets $S$ such that $S$ is downward closed ($x \in S \to x \subseteq S$) and $(S, \in)$ is a model of ZFC (where $\in$ is set ...
- 328
3 votes
1 answer
248 views
Existence of certain formulas in modal logic K
Does there exist a modal formula $φ$ with the following properties? for every finite Kripke frame $F$ there is some ground substitution $\sigma$ such that for every point $w \in F$ we have $F, w \...
- 137
7 votes
1 answer
282 views
How complicated are 3-player clopen determinacy facts?
Say that a clopen 3-player game is a well-founded tree $T\subseteq\omega^{<\omega}$; intuitively, starting with player $1$ and continuing cyclically, the players $1,2,3$ alternately play natural ...
- 19.5k
1 vote
0 answers
47 views
Finite axiomatisation of an extension of $T$ complete w.r.t. Neighbourhood Semantics and incomplete w.r.t. Kripke
A modal logic is normal if and only if $\Box (p \to q) \to (\Box p \to \Box q)$ is provable and the rules of modus ponens and necessitation holds. Let $T$ be a smallest normal modal logic in which $\...
- 804
8 votes
1 answer
417 views
Modal logic of "mostly-satisfiability"
For $n\in\omega+1$ let $\mathsf{ZFC}_n$ be $\mathsf{ZC}$ + $\{\Sigma_k$-$\mathsf{Rep}: k<n\}$. Let $\widehat{\mathsf{ZFC}}$ be the strongest consistent theory $\mathsf{ZFC}_n$ (so if $\mathsf{ZFC}$ ...
- 19.5k
3 votes
0 answers
114 views
Algebraic logical structure
Let $M=(W,R)$ be a Kripke frame, $A=(f_1,...,f_m)$ is a tuple of operations $f_i:W^{n_i}\to W$, and $\Phi=(\varphi_1,...,\varphi_m )$ is a tuple of first-order logic formulas in vocabulary $\sigma=\{=...
- 107
3 votes
0 answers
257 views
Self-referential Quinean proof of Löb's Theorem
Given its relevance for Open-source game theory, Dr. Andrew Critch asks the following about provability logic: We conjecture that Löb’s Theorem can be proven without the use of the modal fixed point $...
- 431
3 votes
0 answers
180 views
A modal logic with two diamonds, one is interpreted as the complement of the relation corresponding to the other one
Suppose our language has two diamond operators $\Diamond$ and $\overline{\Diamond}$ and, over a Kripke model whose relation is $R$, we have the following semantics: $w\models\Diamond\varphi$ if there ...
- 131
1 vote
0 answers
126 views
Doing reverse mathematics by regarding modal logic as weak first-order logic
Reverse mathematics seeks to find subsystems of second-order logic that are equivalent to certain mathematics theorems, say over $\mathsf{RCA}_0$. Modal logic can be regarded as a weak version of ...
- 49
5 votes
0 answers
294 views
How strong is this "modal definability principle"?
Throughout, we work in the class theory $\mathsf{MK}$ (although I'm open to tweaking this), "logic" means "set-sized logic whose semantics is definable over $V$," and "$\...
- 19.5k
7 votes
3 answers
1k views
Difference between provability and the existence of a proof?
In provability logic, $\square X \rightarrow X$ is not a theorem. In my head[1] this reads as "if X is provable you don't necessarily have a proof of X". This has lead to the question, what ...
- 209
1 vote
0 answers
180 views
Question regarding ultrafilter extension of $\tau$-model
Since I'm not native speaker, my writing is probably difficult to read. Hence please point out any mistakes. I'm reading page 96 and 97 of Modal Logic written by Patrick Blackburn. $\textbf{...
- 11
4 votes
1 answer
241 views
Predicativity and axiom $\mathbb{R}\flat$ in real cohesive homotopy type theory
In Mike Shulman's article Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, the fundamental axiom adopted for his real-cohesive homotopy type theory (axiom $\mathbb{R}\flat$), which ...
user483446
2 votes
1 answer
155 views
Initial reference on Gödel-Löb axiom in Kripke semantic of $GL$
It seems well known in modal logic society that $\Box(\Box p\to p) \to \Box p$ in Kripke semantics of $GL$ implies well-foundedness of the relation i.e. no infinite ascending chains are allowed. And ...
- 804
3 votes
0 answers
312 views
Does the following variant of common belief exist?
Let $A$ be a finite set of agents and $\mathtt{B}_a$ a modal operator where $\mathtt{B}_ap$ means agent $a$ believes proposition $p$. For now I don't assume any properties of $\mathtt{B}_a$, though ...
- 10.7k
1 vote
0 answers
96 views
Proof of the Local Deduction Theorem, for one of many logics
I'm looking for a proof of the Local Deduction Theorem for any one of many logics. That is, a proof of the statement: $\Sigma \cup \{\phi\} \models \psi$ iff for some positive $n,$ $\Sigma \models \...
- 431
2 votes
1 answer
115 views
An exercise in fuzzy logics built from a t-norm [closed]
Consider the following t-norm: $$ a * b = \begin{cases} 2ab, &\quad\text{if }a, b\le1/2\\ \min\{a, b\} &\quad\text{otherwise} \end{cases} $$ We build from it the $\...
- 431
6 votes
0 answers
247 views
Logics of proper class sized Kripke frames
The following can be stated as a sentence of Morse-Kelley set theory: If L is the logic of a proper class sized Kripke frame, then L is the logic of a set sized Kripke frame. It follows from a $\Pi^...
- 357
0 votes
0 answers
277 views
Inconsistency in a modal logic
I need a first order modal logic, where inconsistency between formulas in not binary: a pair of formulas may be more or less inconsistent. The modal operators express uncertainty. So the formulas ...
- 109
3 votes
0 answers
251 views
Bimodal determinacy logic for Borel games
This question is intended to be a first step towards answering this old question of mine. Let $K$ be the set of pairs $(\Sigma,\Pi)$ of quasistrategies, in the usual sense of games on $\omega$, for ...
- 19.5k
4 votes
2 answers
267 views
Modal logics which have an algebraic semantics but not a Kripke semantics
A colleague told me that there are modal logics which have an algebraic semantics of some kind but which do not have a Kripke semantics and in which both $\Box$ is not monotonic with respect to $\to$, ...
- 639
0 votes
1 answer
152 views
Counterexample equivalent in relevant logic DL
On page 7 in the article referred to below an axiom $D9$ is stated as follows: $$A\to B\to.\lnot(A \& \lnot B)~\\ (\text{equivalently: } (A\to\lnot A)\to\lnot A)$$ How may one prove the alleged ...
- 4,122
2 votes
0 answers
100 views
Deduction theorem for the modal mu-calculus
Does the modal mu-calculus have a deduction theorem? If yes, how is it stated? Does it have the 'classical' form (i.e. as in classical propositional logic) or is it more involved?
- 21
8 votes
1 answer
537 views
Interpretations of modal logic where $\Box$ means "valid"
Consider the propositional modal language in one propositional letter, $p$. Recall that a pointed Kripke frame is a Kripke frame $(W,R)$ with a designated world $w_0\in W$, and a sentence is valid in ...
- 357
7 votes
0 answers
227 views
The provability logic of $I\Delta_0+\Omega_1 $ and complexity theory
Almost 30 years ago, a number of folks in provability logic tried to show that GL (see for instance the excellent survey by Rineke Verbrugge here) is indeed the logic of $I\Delta_0+\Omega_1$ (in the ...
- 8,008
9 votes
0 answers
399 views
Sum and Product game
Two perfect logicians Steve and Pete, who have never met, before are imprisoned by an eccentric villain. "I have two positive integer numbers x and y" he says to them. "I will tell Steve the sum x+y, ...
- 2,871
0 votes
0 answers
129 views
Expressing a model transformation by using monads in the simply-typed lambda calculus
In https://link.springer.com/content/pdf/10.1007/s10670-019-00128-z.pdf , page 16, the following clause is given for a modal operator $\langle R_k \rangle$ (see definition 4.2 for the definition of a ...
- 639
18 votes
2 answers
1k views
Are buttons really enough to bound validities by S4.2?
Joel Hamkins recently claimed on twitter that buttons suffice to bound the validities of a potentialist system to the modal logic S4.2 (see here), and that switches are not necessary. We have been ...
- 183
4 votes
1 answer
190 views
In modal logic, is there a formula that could express the inverse of accessibility relation?
For example, in S4, is there a formula that corresponds to the proposition "p is true in every world from which u is accessible (but is not accessible from u)"?
- 41