Induction-induction

Last updated January 30, 2024

In intuitionistic type theory (ITT), some discipline within mathematical logic, induction-induction is for simultaneously declaring some inductive type and some inductive predicate over this type.

An inductive definition is given by rules for generating elements of some type. One can then define some predicate on that type by providing constructors for forming the elements of the predicate , such inductively on the way the elements of the type are generated. Induction-induction generalizes this situation since one can simultaneously define the type and the predicate, because the rules for generating elements of the type $A:{\mathsf {Type}}$ are allowed to refer to the predicate $B:A\to {\mathsf {Type}}$ .

Induction-induction can be used to define larger types including various universe constructions in type theory.^[1] and limit constructions in category/topos theory.

Example 1

Present the type $A$ as having the following constructors , note the early reference to the predicate $B$ :

$aa:A$
Failed to parse (Conversion error. Server ("https://wikimedia.org/api/rest_") reported: "Cannot get mml. upstream connect error or disconnect/reset before headers. reset reason: connection termination"): {\displaystyle \ell \ell :\sum _{x:A}B(x)\to A;}

and-simultaneously present the predicate $B$ as having the following constructors :

${\mathsf {Tru}}:B(aa)$
${\mathsf {Fal}}:B(aa)$
if $x:A$ and $y:B(x)$ then ${\mathsf {Zer}}:B(\ell \ell (x,y))$
if $x:A$ and $y:B(x)$ and $z:B(\ell \ell (x,y))$ then ${\mathsf {Suc}}(z):B(\ell \ell (x,y))$ .

Example 2

A simple common example is the Universe à la Tarski type former. It creates some inductive type $U:{\mathsf {Type}}$ and some inductive predicate $T:U\to {\mathsf {Type}}$ . For every type in the type theory (except $U$ itself!), there will be some element of $U$ which may be seen as some code for this corresponding type ; The predicate $T$ inductively encodes each possible type to the corresponding element of $U$ ; and constructing new codes in $U$ will require referring to the decoding-as-type of earlier codes , via the predicate $T$ .

Related Research Articles

In computability theory, a primitive recursive function is, roughly speaking, a function that can be computed by a computer program whose loops are all "for" loops. Primitive recursive functions form a strict subset of those general recursive functions that are also total functions.

In mathematical logic and computer science, a general recursive function, partial recursive function, or μ-recursive function is a partial function from natural numbers to natural numbers that is "computable" in an intuitive sense – as well as in a formal one. If the function is total, it is also called a total recursive function. In computability theory, it is shown that the μ-recursive functions are precisely the functions that can be computed by Turing machines. The μ-recursive functions are closely related to primitive recursive functions, and their inductive definition (below) builds upon that of the primitive recursive functions. However, not every total recursive function is a primitive recursive function—the most famous example is the Ackermann function.

In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems.

Intuitionistic type theory is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin-Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions. However, all versions keep the core design of constructive logic using dependent types.

In computability theory, the μ-operator, minimization operator, or unbounded search operator searches for the least natural number with a given property. Adding the μ-operator to the primitive recursive functions makes it possible to define all computable functions.

System F is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphism in programming languages, thus forming a theoretical basis for languages such as Haskell and ML. It was discovered independently by logician Jean-Yves Girard (1972) and computer scientist John C. Reynolds.

<span class="mw-page-title-main">Recursive definition</span> Defining elements of a set in terms of other elements in the set

In mathematics and computer science, a recursive definition, or inductive definition, is used to define the elements in a set in terms of other elements in the set. Some examples of recursively-definable objects include factorials, natural numbers, Fibonacci numbers, and the Cantor ternary set.

In computer programming languages, a recursive data type is a data type for values that may contain other values of the same type. Data of recursive types are usually viewed as directed graphs.

In set theory, $-induction$ , also called epsilon-induction or set-induction, is a principle that can be used to prove that all sets satisfy a given property. Considered as an axiomatic principle, it is called the axiom schema of set induction.

In mathematical logic, Heyting arithmetic $is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.$

Axiomatic constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with " $" and " " of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.$

Primitive recursive arithmetic (PRA) is a quantifier-free formalization of the natural numbers. It was first proposed by Norwegian mathematician Skolem (1923), as a formalization of his finitistic conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitistic. Many also believe that all of finitism is captured by PRA, but others believe finitism can be extended to forms of recursion beyond primitive recursion, up to ε₀, which is the proof-theoretic ordinal of Peano arithmetic. PRA's proof theoretic ordinal is ω^ω, where ω is the smallest transfinite ordinal. PRA is sometimes called Skolem arithmetic, although that has another meaning, see Skolem arithmetic.

The Grzegorczyk hierarchy, named after the Polish logician Andrzej Grzegorczyk, is a hierarchy of functions used in computability theory. Every function in the Grzegorczyk hierarchy is a primitive recursive function, and every primitive recursive function appears in the hierarchy at some level. The hierarchy deals with the rate at which the values of the functions grow; intuitively, functions in lower levels of the hierarchy grow slower than functions in the higher levels.

In constructive mathematics, Church's thesis $is the principle stating that all total functions are computable functions.$

In proof theory, ordinal analysis assigns ordinals to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory has a larger proof-theoretic ordinal than another it can often prove the consistency of the second theory.

In type theory, a system has inductive types if it has facilities for creating a new type from constants and functions that create terms of that type. The feature serves a role similar to data structures in a programming language and allows a type theory to add concepts like numbers, relations, and trees. As the name suggests, inductive types can be self-referential, but usually only in a way that permits structural recursion.

In intuitionistic type theory (ITT), a discipline within mathematical logic, induction-recursion is a feature for simultaneously declaring a type and function on that type. It allows the creation of larger types, such as universes, than inductive types. The types created still remain predicative inside ITT.

In mathematical logic, fixed-point logics are extensions of classical predicate logic that have been introduced to express recursion. Their development has been motivated by descriptive complexity theory and their relationship to database query languages, in particular to Datalog.

In set theory and logic, Buchholz's ID hierarchy is a hierarchy of subsystems of first-order arithmetic. The systems/theories $are referred to as "the formal theories of ν-times iterated inductive definitions". ID ν extends PA by ν iterated least fixed points of monotone operators.$

References

↑ Dybjer, Peter (June 2000). "A general formulation of simultaneous inductive-recursive definitions in type theory" (PDF). Journal of Symbolic Logic. 65 (2): 525–549. CiteSeerX 10.1.1.6.4575 . doi:10.2307/2586554. JSTOR 2586554. S2CID 18271311.

External links

A list of Peter Dybjer's publications on induction and induction-recursion

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[Dybjer-1] Dybjer, Peter (June 2000). "A general formulation of simultaneous inductive-recursive definitions in type theory" (PDF). Journal of Symbolic Logic. 65 (2): 525–549. CiteSeerX 10.1.1.6.4575 . doi:10.2307/2586554. JSTOR 2586554. S2CID 18271311.

[1]