8
$\begingroup$

What is the standard reference for the provability of the cut-elimination theorem in PRA?

Update: Rasmus Blanck has offered a reference for a system other than Gentzen's $\mathfrak L \mathfrak K$. The bounty is for a reference for the provability of the cut-elimination theorem for the sequent calculus $\mathfrak L \mathfrak K$ in PRA.

Improve this question
$\endgroup$
1
  • $\begingroup$ I don't have library resources where I am, so I can't verify the two suggestions by Not Mike and Rasmus before the bounty runs out. I am awarding a bounty to both answers. $\endgroup$
    – Andre Kornell
    Sep 24, 2017 at 20:53

2 Answers 2

Reset to default
11
+100
$\begingroup$

My suggestion is Theorem 5.17 in section V.5.(d) of Hájek and Pudlák's Metamathematics of First-Order Arithmetic, Springer-Verlag, 1993. There, cut-elimination is shown to be provable in the even weaker theory $I\Delta_0 + \text{superexp}$.

Improve this answer
$\endgroup$
2
  • 3
    $\begingroup$ Hájek and Pudlák appear to formulate the cut-elimination theorem for a system substantially different from Gentzen's $\mathfrak L \mathfrak K$, and adapting their result to derivations in $\mathfrak L \mathfrak K$ looks like a bit of a chore. Can you suggest another source for derivations in $\mathfrak L \mathfrak K$, or a definitive statement linking the two systems? $\endgroup$
    – Andre Kornell
    Sep 17, 2017 at 6:04
  • 2
    $\begingroup$ Perhaps chapter 1 of Handbook of Proof Theory (edited by Samuel Buss, Elsevier, 1998), might be what you are looking for. Cut-elimination is discussed in section 2.4. $\endgroup$
    – user103227
    Sep 23, 2017 at 19:10
2
+50
$\begingroup$

I think the chapter "Proof Theory: Some Applications of Cut-Elimination", by Helmut Schwichtenberg, from "Handbook of Mathematical Logic", might be what you are looking for.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.