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) ∈ \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $${\mathbb{N}} \cup$$ \end{document} {∞} 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).Our paper thus shows that the quantitative intensional information contained in the effort measure T can be abstracted away by the use of ○ and completely recovered by a suitable semantic interpretation of proofs.