A direct independence proof of Buchholz's Hydra Game on finite labeled trees

Archive for Mathematical Logic 37 (2):67-89 (1998)
  Copy   BIBTEX


We shall give a direct proof of the independence result of a Buchholz style-Hydra Game on labeled finite trees. We shall show that Takeuti-Arai's cut-elimination procedure of $(\Pi^{1}_{1}-CA) + BI$ and of the iterated inductive definition systems can be directly expressed by the reduction rules of Buchholz's Hydra Game. As a direct corollary the independence result of the Hydra Game follows.



    Upload a copy of this work     Papers currently archived: 93,745

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

60 (#92,080)

6 months
16 (#899,032)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

References found in this work

No references found.

Add more references