Logics, Vol. 4, Pages 2: Forcing for an Optimal A-Translation

Logics doi: 10.3390/logics4010002

Authors:
Rui Li

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.

Source link

Rui Li www.mdpi.com