A direct independence proof of Buchholz's Hydra Game on finite labeled trees |
| |
Authors: | Masahiro Hamano Mitsuhiro Okada |
| |
Institution: | (1) Department of Philosophy, Keio University, Tokyo, Japan e-mail: hamano@abelard.flet.keio.ac.jp; mitsu@abelard.flet.keio.ac.jp , JP |
| |
Abstract: | 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 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.
Received: August 23, 1994 / Revised: July 24, 1995 and May 9, 1996 |
| |
Keywords: | Mathematics Subject Classification: 03F03 03F05 03F35 |
本文献已被 SpringerLink 等数据库收录! |