Intuitionism and computing with partial information

TL;DR

This paper explores how certain lattice structures model intuitionistic propositional calculus and their extensions, highlighting the construction of splitting classes and limitations of definable classes.

Contribution

It constructs splitting classes of enumeration degrees that model intuitionistic logic and analyzes the limitations of definable classes within these lattices.

Findings

Initial segments of the Dyment and Dyment-Muchnik lattices model intuitionistic propositional calculus.

Full lattices model intuitionistic logic plus the weak law of excluded middle.

Certain definable classes of enumeration degrees do not form splitting classes.

Abstract

There exist initial segments of both the Dyment lattice and the Dyment-Muchnik lattice that yield Brouwer algebras modeling exactly the intuitionistic propositional calculus. For the Dyment-Muchnik lattice, this result is obtained by constructing a splitting class of enumeration degrees. In contrast, the full Dyment lattice and the full Dyment-Muchnik lattice model the intuitionistic propositional calculus plus the weak law of excluded middle. We also observe that certain naturally definable classes of enumeration degrees, which are downwards closed under enumeration reducibility, fail to form splitting classes.