¿Cuál es la justificación formal de la inducción finita?

Question

Dejemos que $P(k)$ sea un enunciado matemático bien formulado (en el lenguaje FOL de ZFC) que implique $k\in \mathbb{N}$ . Supongamos que quiero demostrar que $P(k)$ es válida para todos los $1\leq k \leq m$ para algunos fijos $m\in \mathbb{N}$ .

Un enfoque es utilizar la inducción. Para ello puedo definir $A=\{ k \in \mathbb{N} :1\leq k \leq m \wedge P(k) \}$ y $B=\{ k \in \mathbb{N}: n> m \}$ . Entonces puedo demostrar que $A\cup B = \mathbb{N}$ por inducción matemática y obtener el resultado.

Pero otro enfoque (por ejemplo Inducción sobre un subconjunto finito de números naturales ) dice que no necesitamos la inducción en este caso. La idea es que si se puede demostrar que $P(1)$ se mantiene y que $P(k)\implies P(k+1)$ es válida para todos los $1\leq k <m$ entonces se puede aplicar el modus ponens un número finito de veces para obtener el resultado.

Sé que la primera prueba se puede escribir en lenguaje formal, pero no estoy seguro del segundo enfoque. El problema parece ser la frase "aplicar el modus ponens un número finito de veces para obtener el resultado" porque no me queda claro cómo se puede formalizar en FOL.

¿Es realmente válido el segundo enfoque?

EDITAR. De hecho, utilizando el segundo enfoque puedo probar el propio PMI:

Supongamos que $P(1)$ se mantiene y que $P(k)\implies P(k+1)$ para todos $k \in \mathbb{N}$ . Supongamos que existe $m \in \mathbb{N}$ tal que $P(m)$ no se sostiene. Aplicando el modus ponens $m$ veces deduzco que $P(m)$ se mantiene, una contradicción. Por lo tanto, $P(k)$ es válida para todos los $k \in \mathbb{N}$ .

Answer 1

En un dominio de discurso finito (con digamos, $k$ objetos), la noción de inducción $(1)$ se puede capturar en la forma de $(2)$ , que es un conjunto finito de listas de implicaciones, y un único caso base, como premisas.

$$p(1),\forall n.\big(p(n)\implies p(n+1)\big)\vdash \forall n. p(n)\tag{1}$$

$$p(x_1),\big(p(x_1)\implies p(x_2)\big),\dots,\big(p(x_{k-1})\implies p(x_k)\big)\vdash \forall x. p(x)\tag{2}$$

Para demostrar que $(2)$ es una regla de inferencia válida ( en un lenguaje finito *), basta con construir una prueba formal desde sus premisas hasta su conclusión. Esto se hace aplicando el modus ponens a cada una de las implicaciones, y luego aplicando cierre del dominio para obtener el resultado deseado.

\begin{align} &1.&p(x_1)&~~\text{P}\\ &2.&p(x_1)\implies p(x_2)&\text{P}\\ &&\dots\\ &k.&p(x_{k-1})\implies p(x_{k})&\text{P}\\ &k+1.&p(x_2)&\text{Modus ponens } 1,k-1\\ &&\dots\\ &2k-1.&p(x_k)&\text{Modus ponens } 2k-3,2k-2\\ &2k.&\forall x.\big(p(x)\big)&~~\text{Domain closure } 1,k+1,\dots,2k-1 \end{align}

---

Por ejemplo, en una lengua con sólo $3$ objetos, abby, bess, cody podemos escribir:

\begin{align} &1.&p(abby)&~~\text{P}\\ &2.&p(abby)\implies p(bess)&\text{P}\\ &3.&p(bess)\implies p(cody)&\text{P}\\ &4.&p(bess)&\text{Modus ponens } 1,2\\ &5.&p(cody)&\text{Modus ponens } 3,4\\ &6.&\forall x.\big(p(x)\big)&~~\text{Domain closure } 1,4,5 \end{align}

---

Editar: Se puede aplicar esta misma técnica a un conjunto finito, pero hay que especificar el conjunto en cuestión.

\begin{align} &0.&X=\{abby,bess,cody\}&~~\text{P}\\ &1.&p(abby)&\text{P}\\ &2.&p(abby)\implies p(bess)&\text{P}\\ &3.&p(bess)\implies p(cody)&\text{P}\\ &4.&p(bess)&\text{Modus ponens } 1,2\\ &5.&p(cody)&\text{Modus ponens } 3,4\\ &6.&\forall x\in X.\big(p(x)\big)&~~1,4,5 \end{align}