Skip to main content
10 votes
Accepted

Kripke Models - evaluating the meaning of $\Box\Box p$

This is an unfortunate use of the word “reachable”, in that Kripke structures are graphs but “reachable” in a Kripke structure is not the same thing as “reachable” ...
David Richerby's user avatar
8 votes
Accepted

How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"?

The $x$ in $\forall x . P(x)$ is not an argument. It is a bound variable indicating which variable the quantifer is ranging over. Let us compare the situation to the definite integral, for concretness ...
Andrej Bauer's user avatar
  • 30.9k
6 votes
Accepted

How to express modalities in lambda calculus - are some extensions required?

Are extensions required? Not really. You can take an axiomatic description of a modal logic and simply provide a "primitive" lambda term for each. The modal operators would become type constructors. ...
Derek Elkins left SE's user avatar
4 votes

Euclidean Models

Suppose $w$ is a world in an Euclidean frame, and $w\mathbin R v$, then by the Euclidean property $w$ reaches both of the "two" worlds $v$ and $v$ (indeed, the same world), and thus $v\mathbin R v$. ...
Vsotvep's user avatar
  • 141
3 votes
Accepted

Modal Logic - □ distribution over →

No. In the modal logic K, the formula □(p → q) implies □p → □q (by the distribution axiom) but it is not equivalent to it. A possible intuition is as follows. Read □(p → q) as: every time it rains, ...
chi's user avatar
  • 14.6k
3 votes

Meaning of the "why not" modality from linear type theory?

From a resource interpretation, If you receive a !T, you can extract as many copies of T as you need in your thread. However, ...
Rufflewind's user avatar
2 votes
Accepted

Meaning of the "why not" modality from linear type theory?

First off, one thing I'd recommend is reading Filinski's Linear Continuations for ideas on how to interpret linear connectives (note, the ? modality got typeset as Γ in that for some reason). In that ...
Dan Doel's user avatar
  • 2,707
2 votes
Accepted

Why we can't use deduction theorem on soundness to contravene second incompleteness with lob's theorem

We know from deduction theorem that $(\vdash q\rightarrow\vdash p)\iff (\vdash p\rightarrow q)$ This is false. If $\not\vdash q$ then the clause $(\vdash q)\rightarrow(\vdash p)$ (re-parenthesized ...
Noah Schweber's user avatar
2 votes
Accepted

CTL trouble translating text into formula

$\newcommand{AF}{\text{AF}\;}\newcommand{AG}{\text{AG}\;}$Try to decode this: For each path: In the future: p and In the future q and Always in the future not p You correctly concluded that the ...
Pål GD's user avatar
  • 16.7k
2 votes

Uses of of the one-variable fragment of first-order logic aka S5

Certainly there're meaningful research went to one-variable fragment of some specific first-order logics, though surprisingly in general they're undecidable even without any binary relations in this ...
cinch's user avatar
  • 235
1 vote

What is the Kripke semantic for a linear temporal logic?

tl;dr The accessibility relation needs to be the reflexive transitive closure of what you had in mind. Details: Let $P$ be a set of atomic proposition. Write $\Sigma$ for $P$'s powerset. Write $T$ for ...
Kai's user avatar
  • 917
1 vote

Euclidean Models

It's true actually. As a hint, the Euclidean property $$xRy \quad\&\quad xRz \implies yRz$$ does not require the $x,y,z$ to be distinct. So for instance it implies $$xRy \quad\&\quad xRy \...
Bjørn Kjos-Hanssen's user avatar
1 vote

How to represent software code for code generation / automatic programming? How to integrate procedural and declarative knowledge?

Use some form of metamodelling : The outputs are represented as abstract syntax trees (ASTs): and constructed by a decoder with a dynamically-determined modular structure paralleling the ...
Paul Sweatte's user avatar
1 vote
Accepted

Modal logic axiom S4, transitive and reflexive frame, tableaux solver

To find a descriptive answer to this post, please see my thesis which presents background information of various modal logics including S4. It also contains detailed implementations of the algorithms ...
marcincuber's user avatar

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