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 ...
- 31.2k
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. ...
- 12.1k
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$. ...
- 141
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, ...
- 163
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 ...
- 2,927
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 ...
- 2,989
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 ...
- 17.1k
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 ...
- 330
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 ...
- 923
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 ...
- 123
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 ...
- 137
Only top scored, non community-wiki answers of a minimum length are eligible