Forcing for an Optimal A-Translation

Kripke semantics for intuitionistic predicate logic IQC is often viewed as a forcing relation between posets and formulas. In this paper, we further introduce Cohen forcing into semantics. In particular, we use generic filters to interpret the double-negation translations from classical first-order logic to the intuitionistic version. It explains how our method interprets classical theories into constructive ones. In addition, our approach is generalized to Friedman’s A-translation. Consequently, we propose an optimal A-translation that extends the class of theorems that are conserved from a classical theory to its intuitionistic counterpart.