Medvedev Logic

Origin. Yuri Medvedev, "Finite problems" (1962) and "Interpretation of logical formulas by means of finite problems" (1966). An intermediate logic arising from a semantics of problems rather than of proofs: the logic of finite problems, ML. Studied since by Maksimova, Shehtman, Skvortsov, and connected to inquisitive semantics by Ciardelli and Roelofsen.

Models. Brouwer's meaning explanation reads a formula as a problem and a proof as a solution. Medvedev takes the problems to be finite and the solutions to be reductions between them, and asks which formulas are solvable for every finite problem. The answer is an intermediate logic that no one has been able to axiomatize.

Formalism.

Medvedev frames: For a finite non-empty set A, take ℘(A) \ {∅}, ordered by ⊇. Under ⊇ the empty set would be the top, so this is the powerset frame with its top removed — a "topless" finite Boolean lattice. Medvedev's logic ML = the intermediate logic of the class of all such frames.

Position in the lattice: IPC ⊊ ML ⊊ CL ML validates weak excluded middle: ¬p ∨ ¬¬p (so KC ⊆ ML) ML validates the Kreisel–Putnam axiom: (¬p → q ∨ r) → ((¬p → q) ∨ (¬p → r)) so KP ⊆ ML, and ML has the disjunction property.

What is settled: Not finitely axiomatizable (Maksimova, Skvortsov, Shehtman 1979) — in fact not axiomatizable in finitely many propositional variables. Shehtman (1990) extended this to the modal counterparts.

What is open: Recursive axiomatizability — equivalently, decidability. Medvedev's problem, open since 1962. The equivalence holds because the Medvedev frames form a recursive class of finite frames, so ML is co-r.e.; a recursive axiomatization would make it r.e. as well, hence decidable.

What is known: Kripke complete (defined by the Medvedev frames). Has the disjunction property. Not the logic of any finite frame; every Medvedev frame is finite but the class is infinite. Structurally complete (Prucnal).

Connection to inquisitive semantics: InqB's negative-variable fragment coincides with ML on the relevant formulas. The Medvedev frames and inquisitive information states carry the same downward-closed structure — which is why the two literatures keep rediscovering each other.

Symbols.

Metatheory. Medvedev's problem is the reason the logic is remembered: an intermediate logic given by a simple, finite, entirely explicit class of frames, for which no axiom set has been found in sixty years. The negative half is a theorem — Maksimova, Skvortsov, and Shehtman proved in 1979 that ML is not finitely axiomatizable, and not even axiomatizable in finitely many variables — but whether it is recursively axiomatizable at all, equivalently whether it is decidable, is still open. It is one of the few natural intermediate logics in that position. The disjunction property and structural completeness make it well-behaved in every respect except the one that matters.

Applies to. The lattice of intermediate logics. The problem interpretation of intuitionistic logic and its finite restriction. Inquisitive semantics, where the same downward-closed structure appears from a different motivation.

Limitations. The question it exists for — decidability, equivalently recursive axiomatizability — is still open, and the axiomatizability question was answered only negatively, so the entry records a definition and a gap rather than a theory. The restriction to finite problems is a stipulation Medvedev made to get a definite object, not a consequence of the problem interpretation, and the infinite analogue (Muchnik's logic) is a different and equally intractable system.

© 2026 Lingenic LLC