Medvedev Logic is Not Decidable. It is π01 -complete. Who Would Have Guessed?
Pawel Pawlowski
cs.LO
Sep 10, 2026 · v1
math.LO
TL;DR
Results through Section 5 (Wang–Medvedev pairs, realizations, recognizing formula) were formalized in Lean with AI assistance; repository provided.
Abstract
This project began as an attempt to prove that Medvedev logic is decidable with the help of generative AI systems. The author (as well as the generative AI systems, or at least they claim to be since I have asked them) was surprised by its eventual conclusion. We prove that Medvedev logic ML, the intermediate logic of finite problems, is Pi-01-complete under computable many-one reductions. Consequently, ML is not recursively enumerable, a fortiori undecidable, and admits no recursively enumerable sound and complete proof calculus. The proof connects the periodic domino problem with intuitionistic formulas through a shared intermediate structure that we call a Wang-Medvedev pair. Such a pair consists of a finite partially ordered set of roles together with demands. Demands define the interaction between roles. A realization labels nonempty subsets of a finite set with these roles, respecting the order and satisfying the demands. We associate a pair with each finite Wang system and show that it has a realization iff the system tiles a finite torus. We then construct an intuitionistic formula that fails on some finite Medvedev frame iff the same pair is realizable. Realizability thus provides the link between periodic tilings and the countermodels.
Problem
Whether Medvedev logic ML, the intermediate logic of all finite Medvedev frames, is decidable or recursively axiomatizable had long been open.
Approach
The paper introduces Wang–Medvedev pairs: finite posets of roles with demands, realized by labeling nonempty subsets of a finite set. Each finite Wang system is assigned a pair that is realizable iff the system tiles a finite torus. An intuitionistic formula is then built that fails on some finite Medvedev frame iff the pair is realizable. Combining this with an effective periodic domino theorem gives a reduction from non-halting to ML membership. Generative AI assisted the proof search and produced a Lean formalization of the paper up to Section 6.
Results
ML is Π⁰₁-complete under computable many-one reductions. It is therefore not recursively enumerable, undecidable, and has no r.e. sound and complete proof calculus. The Lean formalization covers everything except the computability results of Section 6, which the author could not formalize against Mathlib's default machine model.
