Questions tagged [kripke-models]
This tag is for questions relating to "Kripke’s models" for modal logic (or variants thereof) are the basis for many modern approaches to reasoning about knowledge and belief. For philosophers, by far the most important examples are ‘Kripke models’, which have been adopted as the standard type of models for modal and related nonclassical logics.
66
questions
0
votes
1
answer
72
views
How to prove that a formula is intuitionistically valid using Kripke semantics?
I want to know how to use Kripke semantics so that I can prove that a formula is intuitionistically valid.
I think that all others cases will clear out if I understand the case of implication.
Let's ...
2
votes
1
answer
67
views
Intuitionistic proof of $((p\rightarrow q)\rightarrow p)\rightarrow\neg \neg p$
I need to prove that the $\psi=((p\rightarrow q)\rightarrow p)\rightarrow\neg \neg p$ is intuitionistically valid. I tried using the topology of open sets of $\mathbb{R}$ and an arbitrary valuation, ...
1
vote
0
answers
23
views
Related work for a 'compatibility' modality in modal logic meaning ◊(𝜙∧𝜙′)
Fix some set of propositional atoms $\mathsf{Atoms}$ and consider a (very simple) propositional logic with a binary compatibility modality $\mathsf{C}$ as follows:
$$
\phi,\phi' ::= A,B,C\in\mathsf{...
- 446
0
votes
1
answer
78
views
Linear temporal logic question
I am curious about what if we have this Kripke model
and I am trying determine the set of worlds where $\Box\Box p$ is satisfied
This is the part I am confused about when we have $\Box$ I am ...
- 313
1
vote
1
answer
82
views
Is there a simpler Kripke counter-model for this formula?
$\forall x \neg \neg \phi(x) \to \neg \neg \forall x \phi(x)$ is not intuititionistically valid. I can come up with a complicated Kripke counter-model as follows:
Let there be a countably infinite ...
- 993
2
votes
1
answer
77
views
Constructing a Kripke model where $p \rightarrow \Box \Diamond q$ is false.
I have constructed the following Kripke model for this problem:
My idea is the following: Implication is false iff we have $ \top \implies \bot$.
For world $0$, we have that $p$ is true. Now we need ...
- 623
0
votes
1
answer
69
views
Apparent counterexamples to claims of tautologies in modal logic
I'm reading the paper "A fixpoint semantics and an SLD-resolution calculus for modal logic programs" by L.A.Nguyen, and in the paper he asserts that certain tautologies hold, but it seems ...
- 1,631
3
votes
1
answer
50
views
If you have a tableau proof for $\Box A$, show that there is also a tableau proof for A.
If you have a tableau proof for $\Box A$, Show that there is also a tableau proof for A.
Here is my attempt but I'm not sure if it's correct:
If we have a tableau proof for $\Box A$, it means that all ...
- 41
1
vote
1
answer
48
views
Tableau Calculus for Reflexive Frames
How would you create a tableau calculus for modal logics that have reflexive frames? What rules would need to be added to the existing system K?
My attempt is to refer to the axiom scheme for ...
- 53
0
votes
0
answers
66
views
The semantics of until operator in linear temporal logic
According to the definition of until operator from Wiki:
$w \models \varphi~\text{U}~\psi$ if there exists $i \geq 0$ such that $w^i \models \psi$ and for all $0 \leq k < i, w^k \models \varphi$.
...
- 377
0
votes
0
answers
24
views
Requirement of the Second part of PDL Filtration Lemma
I was reading this filtration lemma of PDL in David Harel's book Dynamic Logic.
The Filtration Lemma:
Let $\kappa = \langle W, \mathcal{R}, V\rangle$ be a Kripke model of PDL and let $u, v\in W$:
(i) ...
1
vote
2
answers
210
views
Intuitionistic logic, tree-like Kripke model
There is a tree-like Kripke model in which the set of worlds $\mathfrak{W}$ is ordered as a tree:
(a) there is a smallest world $W_0$
(b) for any $W_i \ne W_0$ there is a unique preceding world $W_k: ...
- 11
3
votes
1
answer
90
views
Rooted Kripke frames connection to $K$
I was reading the Modal logic book from Chagrov and Zakharyaschev.
I read the following theorem (generation theorem 3.11):
If $N$ is a generated submodel of $M$, then for every point x and every ...
- 686
1
vote
2
answers
45
views
For every intuitionistic kripke frame $F = (W, R)$ and every formula $\phi$ and points $x,y \in W$ if $x \models \phi$ and $x R y$ then $y\models\phi$
I need to show that:
For every intuitionistic kripke frame $F = (W, R)$ and every formula $\phi$ and every points $x,y \in W$ if $x \models \phi$ and $x R y$ then $y \models \phi$
I know it's done by ...
- 686
2
votes
2
answers
90
views
About interpretation of accessibility relations in Kripke like structure
A Kripke like structure is something like tuple $(S, R, V)$ in which $S$ is a set of states, $R$ is the relationship between states and $V$ is an evaluation function that maps propositions to some ...
- 157
0
votes
1
answer
147
views
Find and prove a necessary and sufficient condition for a Kripke Frame
I am studying Kripke frames in modal logic and I am trying to understand how to solve the task below (the task comes from a workbook and this particular question lacks a conclusion).
I know that ...
- 391
4
votes
3
answers
263
views
Why is Normality an axiom in Modal Logic?
Why are we having $\square(A → B) → (\square A → \square B)$ as an axiom when we can prove* that if we have $\square(A → B)$ then we will have $(\square A → \square B)$?
*$B$ is true in every world by ...
user332328
-1
votes
1
answer
61
views
Exact definition of SAT problem in S4 [closed]
I kind of know what SAT problem is and I need the exact formal description of this problem for S4 logic.
I am trying to prove this problem is PSPACE-Complete!
Any help would be very much appreciated!
- 33
0
votes
2
answers
278
views
Why S4 logic should have kripke models with reflexive and transitive relations?
From here and here you can see that in S4 modal logic we should have Kripke models (S,R,V) which have a relationship R on their set of states S so that R is reflexive and transitive on S!
I know that ...
- 33
0
votes
0
answers
127
views
Necessity and sufficiency on dead end worlds in Kripke's model
Suppose we are evaluating $\square p$, $\diamondsuit$p, $\square\square$p, $\diamondsuit\diamondsuit$p, $\square$$\diamondsuit$p, $\diamondsuit$$\square$p on a dead end world (the world that can't ...
- 13
2
votes
1
answer
104
views
Semantic explanation for converting intuitionistic logic into classical logic by adding LEM as an axiom
I have a question about converting intuitionistic logic (IL) into classical logic (CL) by adding LEM as an axiom. IL is usually understood as a logic without LEM.
$$\textrm{LEM}:=A\vee\neg A.$$
In ...
- 642
1
vote
1
answer
63
views
Accessibility relation in non-classical logics: hereditary or not?
Recently, I am reading course materials on intuitionistic and modal logics. I have two questions about the notion of accessibility relation in Kripke semantics for intuitionistic and modal logics. ...
- 642
0
votes
0
answers
81
views
Proofing transitivity of simulation relation in Kripke structures
I would like to proof transitivity of simulation in Kripke Structures.
Proof Sketch:
Let A, B, C be Kripke Structures, with
A=(Sa,S0a,Ra,AP,La)
B=(Sb,S0b,Rb,AP,Lb)
C=(Sc,S0c,Rc,AP,Lc)
H ⊆ S × S′ ...
1
vote
2
answers
166
views
Why is $\lozenge (p\to p)$ not valid in system $K$ of modal logic?
Why is $\lozenge (p\to p)$ not valid in system $K$ of modal logic?
How could this formula be false in any accessibility relation or setting of values in worlds? Even if it was a dead end world, ...
- 11
1
vote
1
answer
62
views
Is the statement $(\exists x\psi(x)\rightarrow\forall x\theta(x))\vdash \forall x(\psi(x)\rightarrow\theta(x))$ true in intuitionistic/minimal logic?
I know that this sequent is true for classical logic. But is it true in minimal or intuitionistic logic?
What would be a Kripke model that doesn't satisfy the property?
I would appreciate some (as ...
- 979
2
votes
0
answers
85
views
How does the problem of quantified modal logic relate to Kripke's model
Throughout multiple papers and reviews, Kripke's models are viewed as a countertheory to the work of Quine on the three grades of modal involvement. I understand how the modal is set up: I consider a ...
- 584
2
votes
1
answer
123
views
Is Kripke/relational/possible world semantics the special case of the the set semantics or first order logic?
I am reading https://www.springer.com/gp/book/9783319225562 about expression of modal operators as the predicates in the first order (and possibly higher order) logic. My question is - is the modal ...
- 1,265
3
votes
0
answers
92
views
On provability in modal logic
Consider the classical modal logic $\mathsf K$, given by the following axioms and rules over a language containing the standard propositional connectives and $\Box$:
A complete set of axiom schemes ...
- 4,774
2
votes
0
answers
56
views
characterization of non-reflexive Kripke frames
Can the class of non-reflexive (that is not being reflexive of course) be characterized with a set of modal formulae?
What about irreflexive (having only non-reflexive points)?
- 21
2
votes
1
answer
190
views
Counterexample of Goldblatt-Thomason theorem
The Goldblatt-Thomason theorem states that a class of first-order definable Kripke frames is modally definable if it
is closed under disjoint unions,
is closed under generated subframes,
is closed ...
- 6,083
2
votes
1
answer
374
views
How to prove in K $ \vdash_{p \rightarrow \lozenge \square p} (\square p \rightarrow \lozenge p)$?
Let us denote $C$ the modal system obtained by adding the axiom $ \alpha \rightarrow \lozenge \square \alpha$ to the axiom $K$ and all the propositional tautologies.
As said in the title, I'm looking ...
- 188
4
votes
1
answer
151
views
$\mathcal{M} \models \Box \phi \rightarrow \Box \Box \phi$ for all $\phi$ if and only if $\mathcal{M}$ is transitive
Exercise 1.8.2 in Fitting and Mendelson's "First Order Logic" asks to show that $\mathcal{M} \models \Box \phi \rightarrow \Box \Box \phi$ for all $\phi$ if and only if the accessibility relation of $\...
- 355
2
votes
0
answers
137
views
Understanding The First Axiom Of Gödel's Ontological Proof
On Wikipedia, the first Axiom of Gödel's ontological proof is $$(P(\phi)\land\square\forall x(\phi(x)\Rightarrow\psi(x)))\Rightarrow P(\psi),$$ I assume there are implicit quantifiers present for $\...
- 3,522
1
vote
0
answers
259
views
Proving the Glivenko theorem via Kripke models
We'll prove it in just one direction, since the other one is obvious. So, assume $\psi$ is a theorem of classical propositional logic. Prove that $\lnot \lnot \psi$ is a theorem of intuitionistic ...
- 1,771
3
votes
1
answer
140
views
Proving $\lnot \lnot (\psi \lor \lnot \psi)$ is a theorem of intuitionistic propositional logic
Here, $\psi$ is some arbitrary formula.
The proof I've come up with is as follows.
Assume $\lnot \lnot (\psi \lor \lnot \psi)$ is not a theorem of IPL, which means there exists some Kripke model ...
- 1,771
0
votes
0
answers
81
views
What is the Upper-Bound for a Kripke Model in Normal Modal Logics?
I am currently looking for a paper for a proof about the upper-bound on the size of a Kripke model in modal logic, no matter the axiom considered.
I am considering only the propositional modal logic ...
0
votes
1
answer
387
views
Determine a modal logic formula which a connective that is not valid but is true
I'm trying to understand how a formula can not be valid but also true in the above question.
- 185
0
votes
1
answer
684
views
Counter examples in modal logic
As I'm new to modal logic, I wanted to check whether my counter examples for the given formula is right.
$$
\Box A \rightarrow \Diamond B \Rightarrow \Box(\Box A \rightarrow \Diamond B)
$$
First I ...
- 15
1
vote
0
answers
39
views
How to show that someone beleive someone don't beleive $\phi$ with Kripke models?
I want to model a logic of beliefs with two agents where :
$$M,w^*⊨\phi\wedge Ba\phi\wedge Bb\neg\phi\wedge BaBb\neg\phi$$
I think I'm using Kripke semantics.
I think that i.e. it describe a world ...
- 1,473
0
votes
1
answer
195
views
Minimal Modal Logic and the Class of all Kripke Models
It's well known that minimal modal logic (i.e. propositional tautologies and axiom $K$ together with modus ponens and necessitation rule) captures the validities of the semantic class of all Kripke ...
- 1,351
1
vote
1
answer
320
views
Church-Rosser property and normal modal logic
I am trying to prove soundness and completeness for S4.2 and I am considering Kripke frames which are reflexive, transitive and have the Church-Rosser property. Now, there is one thing that really ...
- 358
0
votes
1
answer
790
views
Modal logic Box and diamond T
I didn't understand what is mean Box T, diamond T in this example:
what is mean box True exist in world v?
- 1
5
votes
1
answer
198
views
Are there any invalid $S5$-formulas $\psi$ such that $\diamond\psi$ is valid?
I cannot find an example for an invalid $S5$ formula $\psi$ (i.e. $\nvDash\psi$), such that $\diamond\psi$ is valid (i.e. $\vDash\diamond\psi$).
If there is none, then $\vDash\diamond\psi\Rightarrow\,\...
- 206
1
vote
0
answers
270
views
I am looking for a soundness, completeness and consistency proof for this particular $S5$ calculus.
I know that it suffices to add the axioms
$(T)~\square\psi\rightarrow\psi$
$(K)~\square(\psi\rightarrow\varphi)\rightarrow(\square\psi\rightarrow\square\varphi)$
$(5)~\diamond\psi\rightarrow\square\...
- 206
0
votes
1
answer
122
views
Proove that all finite non-standard Kripke frames are standard
In Harel's book on PDL (Propositional Dynamic Logic) I've learnt that Kripke frames are pairs such as:
K = (K; $m_k$)
Where $K$ is a set called states and $m_k$ is a meaning function assigning ...
- 728
1
vote
1
answer
114
views
Helping me to prove H axiom in S4.3
We have frame $\mathcal{F} = (W,R)$ that $R$ is reflexive and transitive and
$\forall x,y,z (xRy \wedge xRz \wedge y\ne z \rightarrow yRz \vee zRy)$
,prove
$\mathcal{F} \models \square(\square p \...
- 133
1
vote
1
answer
442
views
Show that (using Kripke models) formula $\phi:p\vee (p\to q)$ is not tautology in intuitionistic logic
Show that (using Kripke models) formula $\phi:p\vee (p\to q)$ is not tautology in
intuitionistic logic.
My proof*
Above, you can see my trial. Check it please and try to help me defeat my ...
user343207
1
vote
3
answers
679
views
Proof of the disjunction property
I am trying to prove the disjunction property "if $\,\vdash\phi\lor\psi$ then $\,\vdash\phi$ or $\,\vdash\psi$" for intuitionistic propositional logic.
So far I thought about choosing two non-...
- 893
2
votes
0
answers
183
views
Different ways to define Kripke structure
The Wikipedia page https://en.wikipedia.org/wiki/Kripke_structure_(model_checking)#Example has an example of a Kripke structure $M = (S,R,L)$; however, others define Kripke structures as $M = (S,R,V)$ ...
- 149
1
vote
2
answers
164
views
Validity of $ F \supset \Box F$
I started to study propositional modal logic and Kripke semantics. I learned that for any Kripke interpration $\mathcal{M}$, we have that, if $\mathcal{M} \models A$ then $\mathcal{M} \models \Box A$. ...
- 23