Skvortsov logic is the extension of propositional intuitionistic logic consisting of the formulas valid on every Kripke frame
 |
where 
is any nonempty set, 
denotes the power set, and a
world 
is accessible from 
exactly when 
is a subset of 
. Skvortsov (1979) introduced this logic of infinite problems.
In contrast, Medvedev logic restricts 
to finite sets. Consequently, every
theorem of Skvortsov logic is a theorem
of Medvedev logic. Skvortsov logic admits an effective
axiomatization, although this does not by itself provide an algorithm
deciding whether any given formula is a theorem.
Almeida and Knudstorp (2026) reported that Skvortsov logic is recursively undecidable and is a proper sublogic of Medvedev logic. Their argument uses the problem of deciding whether a finite set of Wang tiles can tile the entire plane. An aperiodic tiling gives a formula separating the two logics. The authors disclose central contributions from GPT-5.6 Sol and Claude Opus 5 to their project. As of Sep. 18, 2026, independent specialist verification and external peer review of the complete new argument had not been reported.
