Medvedev Logic

Medvedev logic is the extension of propositional intuitionistic logic consisting of the formulas valid on every finite Kripke frame

where , denotes the power set, and a world is accessible from exactly when is a subset of . Its interpretation as a logic of finite problems originates with Medvedev (1962). For , the worlds are , , and , with the first world accessing both singleton worlds. Validity requires truth at every world for every interpretation of the propositional variables allowed by Kripke frame semantics.

Almeida and Knudstorp (2026) reported that the set of valid formulas is recursively undecidable and is not a recursively enumerable set. Their reduction relates invalidity to the existence of periodic tilings by Wang tiles. Independently, Pawłowski (2026) reported that the complement is a recursively enumerable set with the following completeness property. After encoding formulas by Gödel numbers, for any recursively enumerable set there is a computable function defined on every natural number such that iff encodes an invalid formula. These results would answer the longstanding question of whether Medvedev logic admits an effective enumeration of its theorems in the negative.

Almeida and Knudstorp (2026) disclose that GPT-5.6 Sol and Claude Opus 5 supplied central arguments and Lean formalization. The Lean development checks the central reduction. As of Sep. 18, 2026, an independent rebuild and specialist review of the complete argument had not been reported. Their paper also reports that the related Skvortsov logic is recursively undecidable and is a proper sublogic of Medvedev logic.