### 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 (Π^{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.

Original language | English |
---|---|

Pages (from-to) | 67-89 |

Number of pages | 23 |

Journal | Archive for Mathematical Logic |

Volume | 37 |

Issue number | 2 |

Publication status | Published - 1998 Mar |

### Fingerprint

### ASJC Scopus subject areas

- Logic

### Cite this

*Archive for Mathematical Logic*,

*37*(2), 67-89.

**A direct independence proof of Buchholz's Hydra Game on finite labeled trees.** / Hamano, Masahiro; Okada, Mitsuhiro.

Research output: Contribution to journal › Article

*Archive for Mathematical Logic*, vol. 37, no. 2, pp. 67-89.

}

TY - JOUR

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

AU - Hamano, Masahiro

AU - Okada, Mitsuhiro

PY - 1998/3

Y1 - 1998/3

N2 - 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 (Π11 - 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.

AB - 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 (Π11 - 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.

UR - http://www.scopus.com/inward/record.url?scp=0032033989&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0032033989&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0032033989

VL - 37

SP - 67

EP - 89

JO - Archive for Mathematical Logic

JF - Archive for Mathematical Logic

SN - 0933-5846

IS - 2

ER -