Medvedev logic proven undecidable and extremely complex problem
Medvedev Logic is Not Decidable. It is π01 -complete. Who Would Have Guessed?
Logic in Computer Science
Summary
Medvedev logic is a type of logic used to understand finite computational problems. The authors found that this logic is undecidable, meaning no algorithm can fully determine its truths. They linked the logic’s complexity to a known hard mathematical tiling problem, showing it is deeply complex and cannot be simplified into a neat set of rules. This surprising discovery overturns previous hopes that Medvedev logic might be easier to decide using AI. The proof uses a new structure called a Wang-Medvedev pair to connect these concepts.
What this means in practice
- •For logic system designers: Determine that no algorithm can completely enumerate valid proofs in Medvedev logic, guiding proof system design away from this logic.
- •For complexity theorists: Use the undecidability and Pi-01-completeness result to better understand boundaries of decidability in computational logic and tiling problems.
A theory result. No direct application yet.
Authors
Pawel Pawlowski
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.