Medvedev logic is undecidable
Rodrigo Nicolau Almeida, Søren Brinck Knudstorp
math.LO
Sep 11, 2026 · v1
cs.LO
TL;DR
The central argument of the undecidability proof was formally verified in Lean by an LLM (Claude Opus 5).
Abstract
We show that Medvedev's logic of finite problems, a well-known superintuitionistic logic, is undecidable. The key method is a reduction from the periodic tiling problem to non-theoremhood in Medvedev's logic. This settles a longstanding open problem. Using similar techniques, but reducing instead to the ordinary tiling problem, we likewise obtain undecidability of Skvortsov's logic of infinite problems, and the fact that the two logics are distinct – in fact, they are separated by any aperiodic tiling of the plane. Due to the fact that Medvedev's logic figures in so many different areas, these results have implications for several fields – for example, the study of schematic fragments of logics such as propositional dependence logic, or the study of internal logics of toposes. The core idea and technical work of the undecidability proof were obtained using ChatGPT Sol 5.6, and formally verified in Lean by Claude Opus 5. A detailed methodology section outlines how such results were obtained.
Problem
Whether Medvedev's logic of finite problems (a superintuitionistic logic) is decidable/recursively axiomatizable was a longstanding open problem. The decidability status of Skvortsov's logic of infinite problems and the relationship between the two logics were likewise open.
Approach
Undecidability of Medvedev's logic is shown by reducing the periodic tiling problem to non-theoremhood, using Zakharyaschev's canonical formulas in their algebraic/dual reformulation to construct tiling posets and closed domains. A similar reduction from the ordinary tiling problem yields undecidability of Skvortsov's logic. The core idea was obtained with ChatGPT Sol 5.6, and the central argument was formally verified in Lean by Claude Opus 5.
Results
Both Medvedev's logic and Skvortsov's logic are shown to be undecidable, settling the open problem. The two logics are proven distinct, separated by any aperiodic tiling of the plane.
