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.
