Sciweavers

IANDC
2010

Functional interpretations of linear and intuitionistic logic

13 years 2 months ago
Functional interpretations of linear and intuitionistic logic
This article shows how different functional interpretations can be combined into what we term hybrid functional interpretations. These hybrid interpretations work on the setting of a multi-modal linear logic. Functional interpretations of intuitionistic logic can be combined via Girard’s embedding of intuitionistic logic into linear logic. We first show how to combine the usual Kreisel’s modified realizability, G¨odel’s Dialectica interpretation, and the Diller-Nahm interpretation into a basic hybrid interpretation. We then prove a monotone soundness theorem for the basic hybrid interpretation, in the style of Kohlenbach’s monotone interpretations. Finally, we present a hybrid bounded functional interpretation which, except for the additives, corresponds to a combination of the recently developed bounded functional interpretation and bounded modified realizability.
Paulo Oliva
Added 25 Jan 2011
Updated 25 Jan 2011
Type Journal
Year 2010
Where IANDC
Authors Paulo Oliva
Comments (0)