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.
