Name
Abstract | ||
|---|---|---|
We enrich intuitionistic logic with a lax modal operator ○ and define a corresponding intensional enrichment of Kripke models M = (W, ⊑, V) by a function T giving an effort measure T(w, u) ∈
<img src="/fulltext-image.asp?format=htmlnonpaginated&src=G2U2V41G36643P37_html\11225_2004_Article_5117571_TeX2GIFIE1.gif" border="0" alt="
$${\mathbb{N}} \cup$$
" /> {∞} for each ⊑-related pair (w, u). We show that ○ embodies the abstraction involved in passing from “ϕ true up to bounded effort” to “ϕ true outright”. We then introduce a refined notion of intensional validityM |= p : ϕ and present a corresponding intensional calculus iLC-h which gives a natural extension by lax modality of the well-known G: odel/Dummett logic LC of (finite) linear Kripke models. Our main results are that for finite linear intensional models L the intensional theory iTh(L) = {p : ϕ | L |= p : ϕ} characterises L and that iLC-h generates complete information about iTh(L). |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1023/A:1022937306253 | Studia Logica |
Keywords | Field | DocType |
Intuitionistic logic,lax modality,abstraction,intensional models,Gödel-Dummett logic,propositions-as-types | Intuitionistic logic,Discrete mathematics,Gödel,Algorithm,Modal operator,Intensional logic,Kripke models,Completeness (statistics),Mathematics,Bounded function | Journal |
Volume | Issue | ISSN |
73 | 1 | 1572-8730 |
Citations | PageRank | References |
0 | 0.34 | 6 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Matt Fairtlough | 1 | 71 | 6.75 |
| Michael Mendler | 2 | 314 | 34.60 |