Inducción formal sobre dos variables

El argumento de mi ejemplo, si es correcto, necesita que la inducción se pueda aplicar a predicados de la forma$P(m,n)$.$(1)$¿Por qué se puede hacer esto/Por qué es esto formalmente posible?

Tenga en cuenta que en la prueba de ejemplo que dio, corrige el$n$, y luego hacer inducción sobre$m$. Así que en ese sentido la fórmula$P(m,n)$realmente solo tiene una variable:$m$.

$(2)$También he leído la siguiente pregunta Inducción completa sobre dos variables , en la que la respuesta define$Q(x)=\forall y P(x,y)$. Sin embargo, es$Q(x)$entonces un predicado unario válido, es decir, si$P(x,y)$es un predicado, entonces$\forall y P(x,y)$es un predicado unario?

Aquí es aún más claro que$Q(x) = \forall y P(x,y)$es una fórmula con una variable ilimitada$x$. el predicado $P(x,y)$sigue siendo un predicado de 2 lugares, pero la fórmula $\forall y P(x,y)$tiene una sola variable libre. Así que sí, eso encaja muy bien con el esquema del Axioma de Peano.

$(3)$También he leído la siguiente pregunta Doble inducción . Aquí la respuesta dice que la fórmula$\forall m P(m,n)$no es una oración y, por lo tanto, no puede probarse. Sin embargo, en$(*)$Tengo una expresión similar. ¿Hice algo mal en mi argumento anterior?

Una vez más, su argumento comenzó diciendo que el$n$es un número arbitrario: es el comienzo de cualquier prueba universal, donde tratamos de probar$\phi(n)$y desde$n$se asumió que fue elegido arbitrariamente, entonces podemos concluir$\forall n \ \phi(n)$. Entonces, dentro de ese contexto de una prueba universal , podemos tratar$\forall m P(m,n)$como una oración, incluso si no sabemos qué$n$es exactamente, y por lo tanto tampoco sé qué$\forall m P(m,n)$exactamente dice.

Una razón simple por la que la inducción funciona en$n$-ary formulae/predicates es que puede usar la inducción iterada en fórmulas unarias para derivar la inducción en$n$predicados -arios. También está el método que usted indica. Veamos lo primero. Supongamos que quiere probar$\forall n\in\mathbb{N} \forall m\in\mathbb{N} \phi(n,m)$. Podemos hacer esto por inducción en$n$en la fórmula$\forall m\in\mathbb{N} \phi(n,m)$. Esto es de hecho una fórmula. Dado que es una fórmula con una variable libre, es similar a un predicado unario. Puede que no sea atómico. Ahora, por inducción, nuestro problema se ha reducido a probar$\forall m\in\mathbb{N}\phi(0,m)$y mostrando que$\forall n\in\mathbb{N}(\forall m\in\mathbb{N}\phi(n,m)\rightarrow\forall m\in\mathbb{N}\phi(S(n),m))$. Prueba$\forall m\in\mathbb{N}\phi(0,m)$se puede hacer por inducción sobre la fórmula$\phi(0,m)$, es decir, mostrar$\phi(0,0)$y$\phi(0,m)$implica$\phi(0,S(m))$. De manera similar, asumiendo la hipótesis inductiva, uno puede probar$\forall m\in\mathbb{N}\phi(S(n),m)$por inducción en$m$.

Entonces, formalmente,$n$-La inducción aria se puede reducir a la inducción unaria iterada. Sin embargo, esto no siempre se hace en la práctica. Verá, como mencionó, demostraciones de la forma "tomar un$n\in\mathbb{N}$, y probar$\phi(n,m)$por inducción en$m$. Esto suele ser más económico que la inducción iterada. La razón formal de este trabajo se debe al constructor de funciones dependientes ($\Pi$-tipos). Algunas veces (principalmente en el contexto de la deducción natural) esto se llama$\forall$-introducción.

Aparte: la razón por la que la inducción funciona se debe a las reglas de eliminación para el tipo$\mathbb{N}$. Usando las reglas de eliminación para$\mathbb{N}$y usando el constructor para$\Pi$-tipos con la suposición$(n : \mathbb{N})$ambos sirven para hacer lo mismo: definir una función dependiente a partir de$\mathbb{N}$.