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

Masahiro Hamano; Mitsuhiro Okada

doi:10.1007/s001530050084

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

Masahiro Hamano, Mitsuhiro Okada

Department of Philosophy

Research output: Contribution to journal › Article › peer-review

5 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 (Π¹₁ - 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
DOIs	https://doi.org/10.1007/s001530050084
Publication status	Published - 1998 Mar

ASJC Scopus subject areas

Philosophy
Logic

Access to Document

10.1007/s001530050084

Cite this

@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 = mar,

doi = "10.1007/s001530050084",

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

U2 - 10.1007/s001530050084

DO - 10.1007/s001530050084

M3 - Article

AN - SCOPUS:0032033989

SN - 0933-5846

VL - 37

SP - 67

EP - 89

JO - Archive for Mathematical Logic

JF - Archive for Mathematical Logic

IS - 2

ER -

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

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this