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 ⊇. The frame is that poset with its top element (the singleton-generated maximum) removed. 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 open: Finite axiomatizability — Medvedev's problem, open since 1962. Decidability — also open. These are the two questions the logic is known for.

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.

Symbol	Unicode	Name	Meaning
ML	—	Medvedev logic	The logic of finite problems
℘(A)	—	Power set	Source of the frame
⊇	U+2287	Superset	The frame order
KC	—	Weak excluded middle	¬p ∨ ¬¬p; validated
KP	—	Kreisel–Putnam	Validated
IPC / CL	—	Intuitionistic / classical	The bounds

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. It is one of the few natural intermediate logics whose axiomatizability is open, and the negative results — it is not finitely axiomatizable over any of the standard candidates that have been tried — accumulate without a proof. 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 two questions it exists for — finite axiomatizability and decidability — are both open, 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.