Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [kripke-models]

The tag has no usage guidance.

2
votes
1answer
257 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 ...
2
votes
1answer
47 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 $\...
1
vote
0answers
192 views

What does the category of RDF models look like in Institution Theory? [closed]

This question has been represented on cstheory.stackexchange.com where it is getting answers. The Question in short Here is the question in its pure form. Details of my reasoning can be found below. ...
1
vote
0answers
89 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 $\...
1
vote
0answers
96 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 ...
2
votes
1answer
91 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 ...
0
votes
0answers
51 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
1answer
117 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.
0
votes
1answer
225 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 ...
1
vote
0answers
31 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 ...
0
votes
1answer
125 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 ...
0
votes
1answer
120 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 ...
0
votes
1answer
370 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?
5
votes
1answer
118 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\,\...
1
vote
0answers
162 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\...
0
votes
1answer
90 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 ...
1
vote
1answer
62 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 \...
1
vote
1answer
183 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 ...
0
votes
3answers
323 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-...
2
votes
0answers
143 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)$ ...
1
vote
2answers
107 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$. ...
0
votes
1answer
482 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 ...
2
votes
1answer
56 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 ...
2
votes
1answer
76 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....
5
votes
1answer
212 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 ...
2
votes
1answer
444 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 ...
2
votes
2answers
291 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$$ $$\...
0
votes
2answers
123 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, ...
1
vote
2answers
173 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.
0
votes
1answer
143 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 $...
1
vote
1answer
103 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 ...
0
votes
1answer
312 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 ...
1
vote
2answers
99 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 ...
0
votes
1answer
50 views

Explanation of states, worlds and models?

Can someone explain to me how the concepts of states, models and worlds work together in Kripke semantics? I've been trying to piece together how the parts work are linked together but cannot figure ...
0
votes
1answer
114 views

Question concerning satisfiability in a certain Kripke model

My question concerns the exercise on p.77 of Boolos, Logic of Provability: True or false: if $A$ is satisfiable in some finite transitive and irreflexive [FIT] model and contains at most one ...
2
votes
1answer
308 views

What is the difference between First-Order Structures and Kripke Structures?

In the SEP article on Model Theory by Wilfrid Hodges (here), he writes: Particular kinds of model theory use particular kinds of structure; for example mathematical model theory tends to use so-...
0
votes
1answer
175 views

A question on intuitionistc propositional logic

Prove that: Two finite rooted frames are isomorphic iff they validate the same formulas. (This is an exercise in the book "Modal Logic" by A.Chagrov and M.Zakharyaschev)