Infinitary provability logic
Gödel-Löb provability logic $\GL$ is a propositional modal system that on one hand enjoys completeness with respect to conversely well-founded Kripke frames and on the other hand captures all modal principles about $\PA$-provability that are provable in $\PA$ itself. In the present paper we carry out an initial investigation into the question of what the infinitary counterpart of $\GL$ is. We develop a non-well-founded deep inference proof system $\dgla$ for the modal language with at most countably infinite conjunctions and disjunctions. We show that the calculus is sound and complete for…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2609.24795
curl -X POST /api/v1/records/arxiv/2609.24795/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2609.24795/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'