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 non­classical logics.

Filter by
Sorted by
Tagged with
3 votes
1 answer
47 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 ...
user avatar
1 vote
2 answers
42 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 ...
user avatar
2 votes
2 answers
54 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 ...
user avatar
  • 135
0 votes
1 answer
53 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 ...
user avatar
  • 199
4 votes
2 answers
160 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 ...
user avatar
-1 votes
1 answer
48 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!
user avatar
0 votes
2 answers
99 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 ...
user avatar
0 votes
0 answers
76 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 ...
user avatar
2 votes
1 answer
75 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 ...
user avatar
  • 612
1 vote
1 answer
34 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. ...
user avatar
  • 612
0 votes
0 answers
59 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′ ...
user avatar
1 vote
2 answers
122 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, ...
user avatar
1 vote
1 answer
52 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 ...
user avatar
  • 970
2 votes
0 answers
69 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 ...
user avatar
  • 564
1 vote
1 answer
73 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 ...
user avatar
  • 1,181
3 votes
0 answers
82 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 ...
user avatar
  • 4,397
2 votes
0 answers
39 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)?
user avatar
2 votes
1 answer
102 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 ...
user avatar
  • 5,978
2 votes
1 answer
354 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 ...
user avatar
  • 178
4 votes
1 answer
114 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 $\...
user avatar
2 votes
0 answers
132 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 $\...
user avatar
  • 2,740
1 vote
0 answers
167 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 ...
user avatar
  • 1,553
3 votes
1 answer
121 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 ...
user avatar
  • 1,553
0 votes
0 answers
68 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 ...
user avatar
0 votes
1 answer
278 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.
user avatar
0 votes
1 answer
531 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 ...
user avatar
1 vote
0 answers
38 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 ...
user avatar
0 votes
1 answer
175 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 ...
user avatar
  • 1,301
1 vote
1 answer
218 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 ...
user avatar
  • 164
0 votes
1 answer
639 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?
user avatar
  • 1
5 votes
1 answer
168 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\,\...
user avatar
  • 205
1 vote
0 answers
249 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\...
user avatar
  • 205
0 votes
1 answer
109 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 ...
user avatar
1 vote
1 answer
78 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 \...
user avatar
  • 133
1 vote
1 answer
270 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 ...
user avatar
1 vote
3 answers
495 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-...
user avatar
  • 863
2 votes
0 answers
161 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)$ ...
user avatar
  • 149
1 vote
2 answers
126 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$. ...
user avatar
  • 23
0 votes
1 answer
712 views

Properties of transitive modal frames

I am working through Fitting and Mendelsohn's First Order Modal Logic and have come across the following exercise: Prove that a frame $\langle \mathcal{G}, \mathcal{R} \rangle$ is transitive if and ...
user avatar
  • 65
2 votes
1 answer
70 views

Persistency on formulas in Kripke models

Let $ (W,R,f) $ a Kripke model. I have some trouble proving that the persistency property holds for formulas i.e if $ wRw' $ and $ w \Vdash \phi $ then $ w' \Vdash \phi $ , mainly due to the forcing ...
user avatar
2 votes
1 answer
102 views

Conditions for total orders in temporal logic

Let $(T,>)$ be a frame of minimal temporal logic, i.e. a frame as defined in Kripke semantics where the relation is a partial order relation $>$ defined on the set $T$ of worlds, called instants....
user avatar
5 votes
1 answer
321 views

Symmetric relations and $\varphi\rightarrow\square\diamond\varphi$

I read that the schema $$\varphi\rightarrow\square\diamond\varphi$$ corresponds to the symmetric property (D. Palladino, C. Palladino, Logiche non classiche, 'non-classical logics', 2007) of the ...
user avatar
2 votes
1 answer
664 views

Euclidean relations and $\diamond P\rightarrow\square\diamond P$

I read* that the formula $$\diamond \varphi\rightarrow\square\diamond\varphi$$is valid in a structure $(W,R)$, intended as in Kripke semantics, -i.e. that it is true for any interpretation $I$ and in ...
user avatar
2 votes
2 answers
486 views

Logical consequence in all structures in Kripke semantics

I read* the following definition of logical consequence in all structures within Kripke semantics:$$X\models A\iff\text{ for every } (W,R),\text{ if }(W,R)\models X,\text{ then }(W,R)\models A$$ $$\...
user avatar
0 votes
2 answers
364 views

what does the "fixed point" in fixpoint algorithms refer to?

I was reading the following powerpoint here to remember something I studied a long time ago. http://www.cs.cmu.edu/~emc/15-820A/reading/lecture_1.pdf the 12th slide is labeled fixpoint algorithms, ...
user avatar
1 vote
2 answers
184 views

Proving the non-derivability of formula using the of the kripke model

I try proving the non-derivability of $(p\to q) \to \lnot p \lor q$, using the of the kripke model. I tried using different combinations of $Wi$, but I get fail.
user avatar
  • 237
0 votes
1 answer
169 views

The definition of interpretation in a Kripke model collides with my intuition of what it should do

In Lindröm and Segerberg (2007) exposition of a Kripke model, with frame $F= \langle W,D,R,E,w_0\rangle$, they define an interpretation $I$ as a family of functions $I_w$, where $w$ ranges over $...
user avatar
  • 1
1 vote
1 answer
127 views

Propositional S5: is there a consistent set requiring continuously many worlds?

A recent question asked whether in systems of modal propositional logic having the "finite model property" there are consistent sets of sentences that were not satisfied by a finite model. @Carl ...
user avatar
  • 1,423
0 votes
1 answer
468 views

Propositional modal logic: infinite models required in systems with finite model property?

A system of propositional modal logic has the "finite model property" if any consistent sentence is satisfiable at a model with finitely many possible worlds. Some systems have this property and ...
user avatar
  • 1,423
1 vote
2 answers
115 views

Proving Gabbay rule for Modal Logic

I'm currently working on exercises of the book "Modal Logic" by A.Chagrov and M.Zakharyaschev (for pleasure, not homework). One exercise asks to prove this version of Gabbay rule (exercise $3.10$): A ...
user avatar
  • 340