Inducción de bar

Dados dos predicados${\displaystyle R}$y${\displaystyle A}$sobre secuencias finitas de números naturales tales que se cumplen todas las siguientes condiciones:

• Cada secuencia de elección contiene al menos un segmento inicial que satisface${\displaystyle R}$en algún momento (esto se expresa diciendo que${\displaystyle R}$es un bar );
• ${\displaystyle R}$es decidible (es decir, nuestro bar es decidible );
• toda secuencia finita que satisface${\displaystyle R}$también satisface${\displaystyle A}$(entonces${\displaystyle A}$se cumple para cada secuencia de elección que comienza con la secuencia finita mencionada anteriormente);
• si todas las extensiones de una secuencia finita por un elemento satisfacen${\displaystyle A}$, entonces esa secuencia finita también satisface${\displaystyle A}$(a esto a veces se le denomina${\displaystyle A}$siendo hereditario ascendente );

Entonces podemos concluir que${\displaystyle A}$se cumple para la secuencia vacía (es decir, A se cumple para todas las secuencias de elección que comienzan con la secuencia vacía).

Este principio de inducción de barras es favorecido en las obras de AS Troelstra , SC Kleene y Albert Dragalin.

Dados dos predicados${\displaystyle R}$y${\displaystyle A}$sobre secuencias finitas de números naturales tales que se cumplen todas las siguientes condiciones:

• Cada secuencia de elección contiene un segmento inicial único que satisface${\displaystyle R}$en algún momento (es decir, nuestra barra es delgada );
• toda secuencia finita que satisface${\displaystyle R}$también satisface${\displaystyle A}$;
• si todas las extensiones de una secuencia finita por un elemento satisfacen${\displaystyle A}$, entonces esa secuencia finita también satisface${\displaystyle A}$;

Entonces podemos concluir que${\displaystyle A}$se cumple para la secuencia vacía.

Este principio de inducción de barras es el preferido en los trabajos de Joan Moschovakis y es (intuicionistamente) demostrablemente equivalente a la inducción de barras decidible.

Dados dos predicados${\displaystyle R}$y${\displaystyle A}$sobre secuencias finitas de números naturales tales que se cumplen todas las siguientes condiciones:

• Cada secuencia de elección contiene al menos un segmento inicial que satisface${\displaystyle R}$en algún momento;
• una vez que una secuencia finita satisface${\displaystyle R}$, entonces toda extensión posible de esa secuencia finita también satisface${\displaystyle R}$(es decir, nuestra barra es monótona );
• toda secuencia finita que satisface${\displaystyle R}$también satisface${\displaystyle A}$;
• si todas las extensiones de una secuencia finita por un elemento satisfacen${\displaystyle A}$, entonces esa secuencia finita también satisface${\displaystyle A}$;

Entonces podemos concluir que${\displaystyle A}$se cumple para la secuencia vacía.

Este principio de inducción de barras se utiliza en las obras de AS Troelstra , SC Kleene , Dragalin y Joan Moschovakis .

Los siguientes resultados sobre estos esquemas pueden demostrarse intuicionistamente :

${\displaystyle {\begin{aligned}BI_{M}&\vdash BI_{D}\\[3pt]BI_{D}&\vdash BI_{T}\\[3pt]BI_{T}&\vdash BI_{D}\end{aligned}}}$

(El símbolo "${\displaystyle \,\vdash \,}$" es un " torniquete ".)

Un esquema adicional de inducción de barras fue dado originalmente como un teorema por Brouwer (1975) que no contenía ninguna restricción "extra" sobre${\displaystyle R}$bajo el nombre de Teorema de la Barra . Sin embargo, la demostración de este teorema fue errónea, y la inducción de barra sin restricciones no se considera válida desde el punto de vista intuicionista (véase Dummett 1977, págs. 94-104, para un resumen de por qué). El esquema de la inducción de barra sin restricciones se presenta a continuación para mayor claridad.

Dados dos predicados${\displaystyle R}$y${\displaystyle A}$sobre secuencias finitas de números naturales tales que se cumplen todas las siguientes condiciones:

• Cada secuencia de elección contiene al menos un segmento inicial que satisface${\displaystyle R}$en algún momento;
• toda secuencia finita que satisface${\displaystyle R}$también satisface${\displaystyle A}$;
• si todas las extensiones de una secuencia finita por un elemento satisfacen${\displaystyle A}$, entonces esa secuencia finita también satisface${\displaystyle A}$;

Entonces podemos concluir que${\displaystyle A}$se cumple para la secuencia vacía.