Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM
Pitts' proof-theoretic technique for uniform interpolation, which generates uniform interpolants from terminating sequent calculi, has only been applied to logics on an intuitionistic basis through single-succedent sequent calculi. We adapt the technique to the intuitionistic multi-succedent setting by focusing on the intuitionistic modal logic KM. To do this, we design a novel multi-succedent sequent calculus for this logic which terminates, eliminates cut, and provides a decidability argument for KM. Then, we adapt Pitts' technique to our calculus to construct uniform interpolants for KM,…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2602.16445
curl -X POST /api/v1/records/arxiv/2602.16445/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2602.16445/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'