In Hamano and Okada's "A relationship among Gentzen's proof-reduction, Kirby-Paris' hydra game, and Buchholz's hydra game", they briefly introduce a proof calculus for Peano arithmetic, but it isn't clear what sequents they allow as initial sequents (i.e. sequents at leaves of the proof tree.) What do they use, if this system does relate to sequent calculi in the literature?

As a start, they cite Takeuti's Proof Theory, 2nd edition for the development of this proof system for PA. But the initial sequents appearing in derivations in the Hamano-Okada paper don't match the system $\mathbf{PA}$ from Proof Theory in at least two ways:

  • On p.76 of Proof Theory there is a list of six initial sequents added to system LK to obtain a sequent calculus named $\mathbf{PA}$. But on p.72 of Hamano-Okada's paper it seems like "$m=n\Rightarrow$" is used as an initial sequent, which is not part of Takeuti's six. Superficially this initial sequent reminds me of those in $\mathbf{LK}_e$ (appearing on p.37 of Proof Theory and on p.177 of the Open Logic Project's "Sets, Logic, Computation".) But $\mathbf{LK}_e$ looks like it's designed for first-order logic with only a single relation symbol $=$, not for Peano arithmetic.
  • Also, Takeuti's six sequents closely resemble the axioms of PA, for example the initial sequent $s'=t'\Rightarrow s=t$ resembles $\forall s\forall t(s'=t'\rightarrow s=t)$. (It also seems like this "axioms as initial sequents" approach is common, cf. the ten "elementary axioms" appearing on p.183 of "Provably computable functions and the fast-growing hierarchy" by Buchholz and Wainer.) But I can't find these sequent versions of the PA axioms in Hamano-Okada.
  • $\begingroup$ I'm not familiar with the paper you are referring to, but (Takeuti, page 76) the axiom $s'=0 \to$ is an example of sequent $m=n \to$. $\endgroup$ Jul 5, 2022 at 10:26
  • $\begingroup$ At the end of the proof of page 72, there is a ref to axioms $\to m=n$ that IMO covers other PA axioms in sequent form. $\endgroup$ Jul 5, 2022 at 10:32
  • $\begingroup$ Thanks! The reference to axioms $\rightarrow m=n$ is offhand, but I suppose in both cases since Hamano-Okada says "let $m$ and $n$ denote numerals", we don't get to set $m=a'$ and $n=a+0'$ for example. Instead we'd need concrete numerals in the sequent such as "$0'''=0'''\rightarrow$". $\endgroup$
    – C7X
    Jul 6, 2022 at 20:47
  • $\begingroup$ I don't know why they didn't let terms appear in these axioms and instead only used numerals, this seems like it makes it more difficult to inductively prove $\Pi_1^0$-statements as we can't refer to the arbitrary case of $m'=n'\rightarrow m=n$. Also Buchholz-Wainer seem to allow terms in their initial sequents $\endgroup$
    – C7X
    Jul 6, 2022 at 21:15


You must log in to answer this question.

Browse other questions tagged .