Propositional Dynamic Logic without tests does not have Craig Interpolation
Malvin Gattinger
cs.LO
Nov 12, 2026 · v1
math.LO
TL;DR
The counterexample to interpolation for test-free PDL is formalized in Lean, using Mathlib semilinear sets; it was found by LLM agents (Claude, Aristotle) working on an existing Lean PDL formalization.
Abstract
It was shown recently by Borzechowski et al. (2026) that Propositional Dynamic Logic (PDL) has Craig Interpolation. Whether test-free PDL, i.e. PDL without the `?' operator, has interpolation remained open. Here we answer this question in the negative with a counterexample: a test-free PDL validity for which no test-free interpolant exists. The validity only uses one atomic program and the Kleene star, so it implies that the basic modal logic K extended with the reflexive transitive closure does not have interpolation, as previously shown by Studer (2009). The example was originally obtained using LLMs and Lean. We describe our methodology and provide links to all prompts, LLM output summaries as well as the Lean proof.
Problem
Full Propositional Dynamic Logic (PDL) is known to have Craig interpolation. Whether test-free PDL, i.e. PDL without the '?' operator, also has interpolation was an open question.
Approach
The authors give an explicit test-free PDL validity using one atomic program and the Kleene star. They build a Kripke countermodel in which two states satisfy the two sides of the implication while agreeing on all test-free {a,p}-formulas up to any given modal depth. A link to semilinear sets of execution lengths, a special case of Parikh's theorem, supports the argument. The counterexample was found by prompting Claude and Aristotle while adapting an existing Lean formalization of PDL interpolation, and the result is machine-checked in Lean.
Results
Test-free PDL does not have Craig interpolation. It follows that K extended with reflexive transitive closure also lacks interpolation. The Lean proof, prompts, and LLM output summaries are publicly released.
