We enrich intuitionistic logic with a lax modal operator O and define a corresponding intensional enrichment of Kripke models (W,<=,V) by a function T giving an effort measure for each <= related pair (w,u). We show that O embodies the abstraction involved in passing from "M true up to bounded effort" to "M true outright". We then introduce a refined notion of intensional validity and present a corresponding intensional calculus i-LC which gives a natural extension by lax modality of the well-known Goedel/Dummett logic LC of (finite) linear Kripke models. Our main results are that for finite linear intensional models L the intensional theory of L characterises L and that i-LC generates complete information about this intensional theory.
Our paper thus shows that the quantitative intensional information contained in the effort measure T can be abstracted away by the use of O and completely recovered by a suitable semantic interpretation of proofs.