---
id: "2026-11-12-test-free-pdl-no-craig-interpolation-claude-fable"
url: "https://postcutoff.com/e/2026-11-12-test-free-pdl-no-craig-interpolation-claude-fable/"
as_of: "2026-11-13T13:49:00+01:00"
date: "2026-11-12"
date_precision: day
category: science
importance: 3
confidence: high
status: [Result confirmed]
verification: Lean-verified
sources: 3
editor: human editor
human_review: null
version: null
---

As of: 2026-11-13 13:49 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-11-12-test-free-pdl-no-craig-interpolation-claude-fable/

# Test-free PDL lacks interpolation; counterexample by Claude Fable in Lean

Full title: Test-free Propositional Dynamic Logic has no Craig interpolation: Claude Fable found the counterexample 'within a few minutes', with a Lean proof, after failing to repair the positive proof

arXiv 2611.16759 (12 Nov 2026), Malvin Gattinger (ILLC Amsterdam): a test-free PDL validity with one atomic program and Kleene star that has no test-free interpolant, so test-free PDL lacks Craig interpolation (full PDL has it, by Borzechowski et al. 2026). While adapting the Lean formalization of the positive result, Gattinger prompted Aristotle and Claude Fable; Claude Fable, asked to use the failed proof ideas "for the opposite goal", found a counterexample "within a few minutes, including a Lean formalization". Prompts and output summaries are on Zenodo; the Lean proof is public.

## Key facts
- Result: a valid test-free PDL implication with no test-free interpolant; it uses one atomic program and *, so it also re-proves Studer's (2009) result that K with reflexive transitive closure lacks interpolation
- Method (paper, §7, verbatim): 'We then prompted both Aristotle and Claude Fable to explore alternative constructions … This did not lead anywhere, so we eventually also prompted Claude Fable to use the failed proof ideas as inspiration for the opposite goal, namely to find a counterexample. It did so within a few minutes, including a Lean formalization of the result.'
- Human role: 'All text in this paper was written by its human author. The proof structure and lemma statements are strongly inspired by the Lean proof and its comments that were written by Claude.' The published example simplifies Claude's first one (fewer letters, smaller Kripke model)
- Timeline: obtained in September 2026; paper 12 Nov. Prompts and model summaries: doi:10.5281/zenodo.23987961; Lean: malv.in/2026/test-free-pdl-no-interpolation/
- Status: preprint with a Lean formalization of the counterexample

## What happened

Malvin Gattinger (University of Amsterdam), a co-author of the Lean formalization of interpolation for Propositional Dynamic Logic,
tried to adapt that proof to PDL without the test operator. One construction could not be repaired, and attempts with Harmonic's
Aristotle and Claude Fable to find a different one failed. He then asked Claude Fable to look for a counterexample instead; it found
one in minutes, with a Lean proof. The 12 Nov paper presents a simplified version, written by Gattinger, and links all prompts.

## Why it matters

It settles a question left open by the 2026 interpolation theorem for PDL, and documents a pattern seen elsewhere: a model asked to
turn failed proof attempts around finds the counterexample. The counterexample is formally checked.

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 196 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 135 days after its cutoff
- Gemini 4 Hydrogen (training cutoff March 2026): 226 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 165 days after its cutoff

## Sources

1. [arXiv 2611.16759: Propositional Dynamic Logic without tests does not have Craig Interpolation (Gattinger)](https://arxiv.org/abs/2611.16759) (arxiv.org, paper)
2. [Zenodo: prompts and LLM output summaries](https://doi.org/10.5281/zenodo.23987961) (doi.org, code)
3. [Lean formalization (malv.in)](https://malv.in/2026/test-free-pdl-no-interpolation/) (malv.in, code)

## Changes

- 2026-11-13 (filed): Created (science agent; arXiv PDF read)

## Related

- 2026-11-13: [AI-assisted results, 13 Nov](https://postcutoff.com/e/2026-11-13-ai-assisted-results-november-13-listing/index.md)