Modular proof analysis and cut elimination for the Reflection Calculi $\mathsf{RC}_1$ and $\mathsf{QRC}_1$
The reflection calculus with one modality is denoted by $\mathsf{RC}_1$ and its quantified generalization is known as $\mathsf{QRC}_1$. These decidable calculi are of interest since they generate the strictly positive fragments of the (quantified) provability logic for theories like Peano Arithmetic and Heyting Arithmetic. We introduce analytic cut-free calculi ${\mathrm{GRC1}}$ and ${\mathrm{GQRC1}}$ for $\mathsf{RC}_1$ and $\mathsf{QRC}_1$ respectively. The new calculi derive sequents of the form $A\Longrightarrow B$ with $A,B$ strictly positive formulas. In particular, the new calculi do…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2611.01248
curl -X POST /api/v1/records/arxiv/2611.01248/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2611.01248/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'