Dialectica for constructible falsity

We can instantiate the Dialectica construction to the category of Heyting algebras, as the category of Heyting algebras has all finite products and pullbacks. Then we get not only a model of classical linear logic, as it happens for other categories with finite limits, but we also get a model of a different logic, related to Nelson’s ‘Constructible Falsity’. The Chu/Dialectica construction considered over Heyting algebras provides us with a bridge to ‘strong negation’ based logics. We discuss how, while the original idea was basically described in Patterson’s 1998 doctoral thesis, much work on Nelson’s systems was and still is required to make good on the claim that the categories can be considered models for these different logics. We also discuss briefly why this is important.