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

Masahiro Hamano, Mitsuhiro Okada

Research output: Contribution to journalArticle

4 Citations (Scopus)

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

Original languageEnglish
Pages (from-to)67-89
Number of pages23
JournalArchive for Mathematical Logic
Volume37
Issue number2
Publication statusPublished - 1998 Mar

Fingerprint

Labeled Trees
Independence Results
Game
Inductive Definitions
Cut-elimination
Corollary
Independence

ASJC Scopus subject areas

  • Logic

Cite this

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

In: Archive for Mathematical Logic, Vol. 37, No. 2, 03.1998, p. 67-89.

Research output: Contribution to journalArticle

@article{1fa8f189ddd94ae18e7443b9182aff2f,
title = "A direct independence proof of Buchholz's Hydra Game on finite labeled trees",
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 (Π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.",
author = "Masahiro Hamano and Mitsuhiro Okada",
year = "1998",
month = "3",
language = "English",
volume = "37",
pages = "67--89",
journal = "Archive for Mathematical Logic",
issn = "0933-5846",
publisher = "Springer New York",
number = "2",

}

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 -