Infinite Games and Transfinite Recursion of Multiple Inductive Definitions

2012 ◽  
pp. 374-383 ◽  
Author(s):  
Keisuke Yoshii ◽  
Kazuyuki Tanaka
Keyword(s):  
Infinite Games ◽  
Inductive Definitions ◽  
Transfinite Recursion

scholarly journals Functional interpretation and inductive definitions

2009 ◽  
Vol 74 (4) ◽  
pp. 1100-1120 ◽  
Author(s):  
Jeremy Avigad ◽  
Henry Towsner
Keyword(s):  
Finite Type ◽  
Functional Interpretation ◽  
Inductive Definitions ◽  
Transfinite Recursion

AbstractExtending Gödel's Dialectica interpretation, we provide a functional interpretation of classical theories of positive arithmetic inductive definitions, reducing them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.

scholarly journals Equivalents of the finitary non-deterministic inductive definitions

2019 ◽  
Vol 170 (10) ◽  
pp. 1256-1272 ◽  
Author(s):  
Ayana Hirata ◽  
Hajime Ishihara ◽  
Tatsuji Kawai ◽  
Takako Nemoto
Keyword(s):  
Inductive Definitions

Determinacy of Banach games

1985 ◽  
Vol 50 (1) ◽  
pp. 110-122
Author(s):  
Howard Becker
Keyword(s):  
Winning Strategy ◽  
Similar Type ◽  
Infinite Games ◽  
Real Numbers ◽  
Positive Real ◽  
Infinite Game ◽  
First Time

For any A ⊂ R, the Banach game B(A) is the following infinite game on reals: Players I and II alternately play positive real numbers a1; a2, a3, a4,… such that for n > 1, an < an−1. Player I wins iff ai exists and is in A.This type of game was introduced by Banach in 1935 in the Scottish Book [15], Problem 43. The (rather vague) problem which Banach posed was to characterize those sets A for which I (II) has a winning strategy in B(A). (There are three parts to Problem 43. In the first, Mazur defined a game G**(A) for every set A ⊂ R and conjectured that II has a winning strategy in G**(A) iff A is meager and I has a winning strategy in G**(A) iff A is comeager in some neighborhood; this conjecture was proved by Banach. Presumably Banach had this result in mind when he asked the question about B(A), and hoped for a similar type of characterization.) Incidentally, Problem 43 of the Scottish Book appears to be the first time infinite games of any sort were studied by mathematicians.This paper will not provide the reader with any answer to Banach's question. I know of no nontrivial way to characterize when player I (or II) wins, and I suspect there is none. This paper is concerned with a different (also rather vague) question: For which sets A is the Banach game B(A) determined? To say that B(A) is determined means, of course, that one of the players has a winning strategy for B(A).

μ-definable sets of integers

1993 ◽  
Vol 58 (1) ◽  
pp. 291-313 ◽  
Author(s):  
Robert S. Lubarsky
Keyword(s):  
Fixed Point ◽  
Free Variable ◽  
Order Logic ◽  
First Order Logic ◽  
Inductive Definition ◽  
Natural Class ◽  
First Order ◽  
Inductive Definitions ◽  
Definable Sets ◽  
The Universe

Inductive definability has been studied for some time already. Nonetheless, there are some simple questions that seem to have been overlooked. In particular, there is the problem of the expressibility of the μ-calculus.The μ-calculus originated with Scott and DeBakker [SD] and was developed by Hitchcock and Park [HP], Park [Pa], Kozen [K], and others. It is a language for including inductive definitions with first-order logic. One can think of a formula in first-order logic (with one free variable) as defining a subset of the universe, the set of elements that make it true. Then “and” corresponds to intersection, “or” to union, and “not” to complementation. Viewing the standard connectives as operations on sets, there is no reason not to include one more: least fixed point.There are certain features of the μ-calculus coming from its being a language that make it interesting. A natural class of inductive definitions are those that are monotone: if X ⊃ Y then Γ (X) ⊃ Γ (Y) (where Γ (X) is the result of one application of the operator Γ to the set X). When studying monotonic operations in the context of a language, one would need a syntactic guarantor of monotonicity. This is provided by the notion of positivity. An occurrence of a set variable S is positive if that occurrence is in the scopes of exactly an even number of negations (the antecedent of a conditional counting as a negation). S is positive in a formula ϕ if each occurrence of S is positive. Intuitively, the formula can ask whether x ∊ S, but not whether x ∉ S. Such a ϕ can be considered an inductive definition: Γ (X) = {x ∣ ϕ(x), where the variable S is interpreted as X}. Moreover, this induction is monotone: as X gets bigger, ϕ can become only more true, by the positivity of S in ϕ. So in the μ-calculus, a formula is well formed by definition only if all of its inductive definitions are positive, in order to guarantee that all inductive definitions are monotone.

A TYPE-FREE THEORY OF HALF-MONOTONE INDUCTIVE DEFINITIONS

1995 ◽  
Vol 06 (03) ◽  
pp. 203-234 ◽  
Author(s):  
YUKIYOSHI KAMEYAMA
Keyword(s):  
Type Theory ◽  
Characteristic Point ◽  
Logical Theory ◽  
Inductive Definition ◽  
Program Extraction ◽  
First Order ◽  
Inductive Definitions ◽  
Free Theory ◽  
Program Proof ◽  
Definition Of

This paper studies an extension of inductive definitions in the context of a type-free theory. It is a kind of simultaneous inductive definition of two predicates where the defining formulas are monotone with respect to the first predicate, but not monotone with respect to the second predicate. We call this inductive definition half-monotone in analogy of Allen’s term half-positive. We can regard this definition as a variant of monotone inductive definitions by introducing a refined order between tuples of predicates. We give a general theory for half-monotone inductive definitions in a type-free first-order logic. We then give a realizability interpretation to our theory, and prove its soundness by extending Tatsuta’s technique. The mechanism of half-monotone inductive definitions is shown to be useful in interpreting many theories, including the Logical Theory of Constructions, and Martin-Löf’s Type Theory. We can also formalize the provability relation “a term p is a proof of a proposition P” naturally. As an application of this formalization, several techniques of program/proof-improvement can be formalized in our theory, and we can make use of this fact to develop programs in the paradigm of Constructive Programming. A characteristic point of our approach is that we can extract an optimization program since our theory enjoys the program extraction theorem.

Sign in / Sign up

Export Citation Format

Share Document