Classical propositional logic and decidability of variables in intuitionistic propositional logic

TL;DR

This paper investigates which specific excluded middle assumptions for propositional variables are sufficient to derive formulas in intuitionistic logic that are classically provable, enhancing understanding of the relationship between classical and intuitionistic logic.

Contribution

It provides a refined characterization of the minimal set of excluded middles needed for intuitionistic proofs of classically provable formulas.

Findings

Identifies minimal sets of excluded middles for propositional variables

Establishes conditions under which classical proofs translate to intuitionistic logic

Improves understanding of the logical strength needed for intuitionistic provability

Abstract

We improve the answer to the question: what set of excluded middles for propositional variables in a formula suffices to prove the formula in intuitionistic propositional logic whenever it is provable in classical propositional logic.