Inducción-inducción

---

En la teoría de tipo intuicionista (ITT), alguna disciplina dentro de la lógica matemática , la inducción-inducción es para declarar simultáneamente algún tipo inductivo y algún predicado inductivo sobre este tipo.

Una definición inductiva viene dada por reglas para generar elementos de algún tipo. Luego, uno puede definir algún predicado en ese tipo al proporcionar constructores para formar los elementos del predicado, de manera inductiva en la forma en que se generan los elementos del tipo. La inducción-inducción generaliza esta situación ya que se puede definir simultáneamente el tipo y el predicado, porque las reglas para generar elementos del tipo pueden referirse al predicado .${\displaystyle A:{\mathsf {Tipo}}}$ ${\displaystyle B:A\to {\mathsf {Tipo}}}$

La inducción-inducción se puede utilizar para definir tipos más grandes, incluidas varias construcciones de universos en la teoría de tipos. ^[1] y construcciones de límites en la teoría de categorías/topos.

Presente el tipo con los siguientes constructores, tenga en cuenta la primera referencia al predicado  :${\ estilo de visualización A}$${\ estilo de visualización B}$

y simultáneamente presenta el predicado con los siguientes constructores:${\ estilo de visualización B}$

Un ejemplo común simple es el formador de tipos Universe à la Tarski. Crea algún tipo inductivo y algún predicado inductivo . Para cada tipo en la teoría de tipos (¡excepto para sí misma!), habrá algún elemento del cual puede verse como algún código para este tipo correspondiente; El predicado codifica inductivamente cada tipo posible al elemento correspondiente de  ; y la construcción de nuevos códigos requerirá referirse a la decodificación como tipo de códigos anteriores, a través del predicado .${\displaystyle U:{\mathsf {Tipo}}}$${\displaystyle T:U\to {\mathsf {Tipo}}}$${\ estilo de visualización U}$${\ estilo de visualización U}$${\displaystyle T}$${\displaystyle U}$${\displaystyle U}$${\displaystyle T}$

---