# Tag Info

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” ...
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 ...
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. ...

### 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$. ...
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, ...

### complexity of modal logic axioms

You might find interesting some of the results in On the Complexity of Fragments of Modal Logics by Linh Anh Nguyen (in Advances in Modal Logic, 2004: 249-268). A version of the paper is available in ...

### 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, ...
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 ...
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 ...
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 ...

### 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 ...
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 ...
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 \...
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 ...
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 ...

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