Inducción-inducción

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

Una definición inductiva se da mediante reglas para generar elementos de algún tipo. Se puede entonces definir algún predicado sobre ese tipo proporcionando constructores para formar los elementos del predicado, de manera inductiva sobre 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 se permite que las reglas para generar elementos del tipo hagan referencia 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 como si tuviera los siguientes constructores, note la referencia temprana al predicado  : ${\estilo de visualización A}$${\estilo de visualización B}$

• ${\estilo de visualización aa:A}$
• ${\displaystyle \ell \ell :\suma _{x:A}B(x)\to A;}$

y simultáneamente presentar el predicado como si tuviera los siguientes constructores: ${\estilo de visualización B}$

• ${\displaystyle {\mathsf {Verdadero}}:B(aa)}$
• ${\displaystyle {\mathsf {Fal}}:B(aa)}$
• Si y entonces${\estilo de visualización x:A}$${\displaystyle y:B(x)}$${\displaystyle {\mathsf {Zer}}:B(\ell \ell (x,y))}$
• si y y entonces .${\estilo de visualización x:A}$${\displaystyle y:B(x)}$${\displaystyle z:B(\ell \ell (x,y))}$${\displaystyle {\mathsf {Suc}}(z):B(\ell \ell (x,y))}$

Un ejemplo común y sencillo 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 él mismo!), habrá algún elemento de que 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 en requerirá hacer referencia 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}$${\estilo de visualización T}$${\estilo de visualización U}$${\estilo de visualización U}$${\estilo de visualización T}$

• Inducción-recursión – para declarar simultáneamente algún tipo inductivo y alguna función recursiva sobre este tipo.

• Una lista de las publicaciones de Peter Dybjer sobre inducción e inducción-recursión