On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains

TL;DR

This paper provides a computational interpretation of the intuitionistic logic of constant domains extended with the forall-shift axiom, using natural deduction and Curry-Howard correspondence, revealing its constructive nature despite classical implications.

Contribution

It introduces a natural deduction framework and Curry-Howard interpretation for the logic of constant domains with the forall-shift axiom, demonstrating its constructiveness.

Findings

The logic is constructive despite classical implications.

A simple computational interpretation is established.

Natural deduction methods are effectively applied.

Abstract

The logic of constant domains is intuitionistic logic extended with the so-called forall-shift axiom, a classically valid statement which implies the excluded middle over decidable formulas. Surprisingly, this logic is constructive and so far this has been proved by cut-elimination for ad-hoc sequent calculi. Here we use the methods of natural deduction and Curry-Howard correspondence to provide a simple computational interpretation of the logic.