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 does not validate weak excluded middle: ¬p ∨ ¬¬p fails on the frame over a two-element set, 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.

Symbol	Unicode	Name	Meaning
ML	—	Medvedev logic	The logic of finite problems
℘	U+2118	Script capital P / Power set	℘(A) is the source of the frame
⊇	U+2287	Superset of or equal to	The frame order
\	U+005C	Reverse solidus / Set difference	℘(A) \ {∅}: the top is removed
∅	U+2205	Empty set	Deleted from the powerset to make the frame topless
⊊	U+228A	Subset of with not equal to	Proper inclusion, as in IPC ⊊ ML ⊊ CL
⊆	U+2286	Subset of or equal to	Inclusion, as in KP ⊆ ML
¬	U+00AC	Not sign / Negation	Occurs in both validated axioms
∨	U+2228	Logical or / Disjunction	The connective of weak excluded middle
→	U+2192	Rightwards arrow / Implication	The connective the KP axiom distributes
KC	—	Jankov's logic	Axiomatized by weak excluded middle ¬p ∨ ¬¬p; not contained in ML
KP	—	Kreisel–Putnam logic	Validated by ML
IPC	—	Intuitionistic propositional calculus	The lower bound
CL	—	Classical logic	The upper bound
InqB	—	Basic inquisitive logic	Shares the downward-closed structure
A	—	Finite set	The parameter of a Medvedev frame
p, q, r	—	Propositional variables	The letters of the validated axioms

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.