Dos sistemas en los que se altera la operación de sucesión son la aritmética de Sazonov sobre una fila finita, en "Una aproximación lógica al problema "¿P=NP?"". http://www.csc.liv.ac.uk/~sazonov/papers.html y "Aritmética sin el axioma sucesor" de Boucher, http://www.andrewboucher.com/papers/ .
En el sistema de Sazonov, existe una operación de sucesión total que se supone explícitamente que se detiene en el último número $\square+1 = \square$ mientras que en el sistema de Boucher la relación de sucesión no se supone total.
Luego hay formas de designar números hasta $2^\square$ mediante cadenas binarias o variables de segundo orden. Porque, por supuesto, a pesar de que no es factible llegar a, digamos, $2^{1000}$ partiendo de cero y añadiendo uno repetidamente, los ordenadores manipulan representaciones binarias de números de ese orden y mayores todo el tiempo, y deberíamos ser capaces de demostrar teoremas sobre estas representaciones.
Pero si no te gustan las restricciones a la inducción, hay un problema. Con la inducción sin restricciones incluso hasta $\square$ parece que basta con definir un cero de segundo orden y un sucesor, y derivar una inducción no restringida hasta $2^\square$ . Ahora bien, si de $P(0)$ y $\forall n . P(n) \to P(n+1)$ concluyes, $P(2^{1000})$ entonces lo estás admitiendo, en principio puede llegar a $2^{1000}$ a partir de cero sumando repetidamente uno.
Lo que me permite pasar a una idea que tuve. Advertencia lector.
Comience con inducción cíclica : si $\exists n. P(n)$ y $\forall n . P(n) \to P(S(n))$ entonces $\forall n. P(n)$ . Si $X$ y $Y$ son tipos con inducción cíclica no restringida, entonces $X^Y$ (el tipo de todas las funciones de $Y$ a $X$ ) tiene inducción cíclica sin restricciones. Y, por supuesto, la inducción cíclica no restringida es válida para un dominio de dos elementos. Así que esto sugiere la teoría de tipos de orden finito sobre 2 (algo como $\mathbf{HA}^\omega$ la teoría constructiva de tipos de orden finito sobre $\mathbb{N}$ .)
Una forma en que esto puede ser interesante es que, como menciona Theo Johnson-Freyd, los ordenadores generalmente trabajan con un dominio cíclico como $2^{32} = (2^{2^{2^2}})^2$ . También pueden trabajar con enteros de mayor tamaño. Y de hecho hay implementaciones de "enteros grandes" que a veces se dice que funcionan con enteros arbitrarios. Y me he dado cuenta de que alguien afirma más arriba que el modelo de programación C tiene memoria infinita. Pero eso es una especie de insulto a $\mathbb{N}$ . Si se implementan con, digamos, punteros de 32 bits, entonces su tipo entero grande realmente tiene un tamaño aproximado de $2^{2^{32}}$ - aunque tu ordenador tenga más de 4 GB de memoria no podrás utilizarla. Llevando esto aún más lejos, si puedes imaginar un ordenador con un espacio de direcciones realmente vasto, al que hay que acceder usando "grandes punteros" hechos a partir de pequeños punteros de 32 bits, y luego definir "enteros realmente grandes" sobre eso, bueno, eso sigue siendo sólo un tipo finito de algo como $2^{2^{2^{32}}}$ .
Por otro lado, se puede aceptar un número entero verdaderamente arbitrario con una speficación interactiva, pero en realidad se trata de algo parecido a la compactificación en un punto de $\mathbb{N}$ . No parece haber manera de expresar la especificación de que el flujo de entrada debe terminar "eventualmente" sin cortarlo en un límite grande pero finito, o referirse circularmente a $\mathbb{N}$ .
Otra forma en que esto puede ser de interés es que en lugar de hablar de los tipos "finitos" sobre 2 en términos de una metateoría que involucra a $\mathbb{N}$ podemos usarla como su propia metateoría, de modo que estamos tratando con un conjunto grande pero finito de fórmulas. Eso debería ser una teoría de la prueba viable.
Por supuesto, esta aritmética alternativa puede convenir a un finitistas, pero tú eres un ultrafinitistas y esto no es lo que realmente quieres. Creo que lo que realmente quieres no existe: como he despotricado en otra parte, parece que necesitamos la inducción hasta números no factibles para demostrar teoremas sobre cálculos factibles.
