Lógica formal detrás de la definición de variables en una prueba (no E.I. o U.G., etc.)

Question

Esto es algo por lo que he sentido curiosidad y espero que tenga una respuesta sencilla. A menudo, cuando miro las pruebas, me encuentro con un paso que va en la línea de "definir y = ..." y luego proceder a utilizar la y definida para mostrar alguna conclusión. Por ejemplo, en el teorema del infinito de los primos de Euclides

define "sea k el producto de todos los números primos menores que n"

seguido de "ahora dejemos m = k + 1".

y procede a razonar con estas definiciones para llegar a los resultados deseados. Mi pregunta es qué tipo de restricciones existen para definir nuevos objetos en una prueba. Estoy al tanto de la regla de generalización universal que requiere algunas restricciones en la introducción de una constante arbitraria, así como las otras reglas de inferencia del cuantificador, como la instanciación existencial y así sucesivamente. Sin embargo, todo esto de definir una variable no parece ser ninguna de estas reglas.

Así que, al final, ¿se pueden definir los objetos de esta manera a voluntad? ¿Qué tipo de justificación se puede escribir para tal paso? Me parece problemático porque tengo la impresión de que hay que asegurarse de la existencia de tales objetos antes de poder introducirlos así, y en particular un paso como "que k sea el producto de todos los números primos menores que n" parece definir un objeto que tiene más significado que una simple definición dada por una ecuación que define el objeto de términos previamente definidos (como "definir m = k + 1").

Así que esto plantea la cuestión de si se pueden definir arbitrariamente objetos que tengan propiedades no confirmadas. Esto no parece correcto porque entonces podrías estar razonando con afirmaciones que son falsas pero como las "definiste" sin restricción dedujiste por error algo que resulta ser falso.

Resumiendo: ¿qué es este método conocido formalmente y qué tipo de restricciones se asocian a él?

Answer 1

Me parece que está buscando el $\exists$ -Elimianción regla de Deducción natural .

Véase Ian Chiswell y Wilfrid Hodges, Lógica matemática (2007), página 179 :

Nos dirigimos a ( $\exists$ E). Esta es la más complicada de las reglas de deducción natural, y muchos primeros cursos de lógica la omiten.

¿Cómo podemos deducir algo a partir de la suposición de que "Hay un snark"? Si somos matemáticos, empezamos por escribir :

(*) Dejemos que $c$ ser un snark

y entonces utilizamos la suposición de que $c$ es un snark para derivar otras afirmaciones, por ejemplo,

(§) $c$ es un boojum [ animal peligroso imaginario ].

Si pudiéramos estar seguros de que (§) se basa únicamente en la suposición de que existe un snark, y no en la suposición más fuerte de que existe un snark llamado ' $c$ ', entonces podríamos descargar la suposición (*) y derivar (§) . Desgraciadamente, (§) menciona explícitamente $c$ por lo que no podemos descartar que dependa del supuesto más fuerte. Aunque no mencionara $c$ Hay otras dos cosas que debemos tener en cuenta. En primer lugar, ninguno de los otros supuestos debe mencionar $c$ ; de lo contrario (§) estaría diciendo tácitamente que algún otro elemento ya mencionado es un snark, y esto no era parte de la suposición de que hay un snark. En segundo lugar, el nombre $c$ debe estar libre de cualquier implicación; por ejemplo, no podemos escribir $cos \theta$ en lugar de $c$ porque entonces estaríamos asumiendo que algún valor de $cos$ es un snark, y de nuevo esto supone algo más que la existencia de un snark. Sin embargo, estos son todos los puntos que debemos tener en cuenta en una regla para eliminar $\exists$ .

Así, la norma para $\exists$ -La eliminación se formaliza de la siguiente manera:

de una derivación $\Gamma \vdash \exists \phi$ y una derivación de $\Delta, \phi[t/x] \vdash \chi$ donde t es un término [símbolo constante o una variable] que no aparece en $\chi, \phi$ o en cualquier supuesto no liquidado en $\Gamma$ o $\Delta$ excepto en $\phi[t/x]$ podemos deducir $\Gamma, \Delta \vdash \chi$ es decir, podemos deducir $\chi$ de los supuestos no descargados de las dos derivaciones anteriores, excepto $\phi[t/x]$ .

---

En su ejemplo, tomado de Euclides, Libro IX,Prop.20 :

Los números primos son más que cualquier multitud asignada de números primos.

Siempre que Euclides defina [Libro VII, Def.11 ] :

A número primo es la que se mide por una sola unidad [es decir, su único divisor que no es igual a sí mismo es el unidad ]

y así sabemos que hay prime números [ $1$ es], Euclides hace la suposición :

Supongamos que hay $n$ primos, $a_1, a_2,\ldots, a_n$ . (Euclides, como siempre, toma un número específico pequeño, $n = 3$ de los primos para ilustrar el caso general).

Dejemos que $m$ sea el mínimo común múltiplo de todos ellos. Considere el número $m + 1$ . Si es primo, entonces hay al menos $n + 1$ primos.

Supongamos que $m + 1$ no es primo. Entonces, según VII.31 , algún primo $g$ lo divide. Pero $g$ no puede ser ninguno de los primos $a_1, a_2,\ldots, a_n$ ya que todos se dividen $m$ y no dividir $m + 1$ . Por lo tanto, hay al menos $n + 1$ primos. Q.E.D.

La prueba es la siguiente:

• dejar $a_1, a_2,\ldots, a_n$ primos; entonces $\exists x (x = lcm(a_1, a_2,\ldots, a_n))$ Esto es $\exists x \phi$

• dejar $k=lcm(a_1, a_2,\ldots, a_n)$ Esto es $\phi[k/x]$

• dejar $m=k+1$ claramente $m \ne a_1, a_2,\ldots, a_n$ ; si $m$ es un primo hemos terminado;

• de lo contrario, hay un primo $g$ que divide $m+1$ y $g \ne a_1, a_2,\ldots, a_n$ .

En ambos casos tenemos que :

$\exists x (x \ne a_1, a_2,\ldots, a_n \, \text {and} \, x \, \text {is prime} \, )$ y esto es $\chi$ .

La sentencia $\chi$ no contiene $k$ y, por lo tanto, las condiciones para $\exists$ -E se satisfacen y la conclusión se mantiene.

---

En cuanto al nuevo ejemplo : "No hay un mayor real [o natural ] número", podemos "formalizarlo" de la siguiente manera.

1) $\forall x(x < x+1)$ -- teorema de teoría de los números

2) $x < x+1$ --- de 1) por $\forall$ E

3) $\exists y(x < y)$ --- de 2) por $\exists$ I

4) $\forall x \exists y(x < y)$ --- de 3) --- por $\forall$ I, $x$ no es libre en 1).

Por lo tanto, como ha señalado, no necesitamos la regla de eliminación existencial.

---

---

Si busca otro ejemplo de uso en la "vida real" de $\exists$ E, considere :

$a < b \land b < c \to a < c$ --- $a,b,c \in \mathbb N$

Prueba :

1) asumir : $a < b$ y : $b < c$ es decir $\exists d(s(d)+a=b)$ y $(\exists e)(s(e)+b=c)$ , donde $s(x)$ es el sucesor función

2) asumir para $\exists$ E : $s(d)+a=b$ y $s(e)+b=c$

3) $(s(e)+s(d))+a=c$ --- por propiedad de igualdad

4) $s((s(e)+d))+a=c$ --- por recursivo axioma para $+$ : $n+s(x)=s(n+x)$ e igualdad

5) $(\exists f)(s(f)+a=c)$ --- por $\exists$ Es decir $a < c$ .

La última fórmula no contiene $d$ ni $e$ y, por tanto, podemos aplicar $\exists$ E dos veces, descargando los supuestos "temporales" en 2), y podemos concluir de 1) con :

$a<b, b<c \vdash a<c$ .

Entonces, por $\to$ Yo dos veces y equivalencia tautológica :

$(a<b \land b<c) \to a<c$ .

Answer 2

Los objetos recién definidos son válidos si y sólo si existen . Es decir, si se define un objeto $o$ que satisface el predicado $P$ debe demostrar que $\exists a, P(a)$ .

Explicaciones: Los objetos recién definidos en una prueba ya existen antes de que los definas, sólo que a veces no piensas en ellos porque son irrelevantes. Pero si se definen objetos absurdos ("que $n$ sea un número entero que sea a la vez par e impar") entonces se puede derivar una contradicción.

Answer 3

Al formalizar un argumento de este tipo, la línea de la prueba será algo así como $\exists x (x=\prod_{p\in P}p)$ , donde $P$ ya está definido como el conjunto de primos menores que $n$ . A continuación, procede a razonar sobre $x$ como siempre. Que yo sepa, esto no tiene ningún nombre especial: simplemente se introduce una variable para razonar sobre un término. Las restricciones son que ya has definido algún término que modela correctamente lo que quieres razonar, en este caso $\prod_{p\in P}p$ - por lo que quiere un término de su lengua, $t(n)$ con una variable libre $n$ que será un número natural, tal que $t(1)=1$ , $t(n+1)=\begin{cases} t(n) &\mbox{ if } n \text{ not prime} \\ t(n)\cdot n &\mbox{ if } n \text{ prime}\end{cases} $

La cuestión es cómo definir dicho término; esto dependerá del sistema formal que se utilice. No es demasiado difícil en ZFC, donde se puede definir $\prod_{i\in I}i$ para cualquier subconjunto finito de un monoide (como los números naturales multiplicativos); la definición utilizará las técnicas estándar para definir funciones por recursión, lo que no es del todo trivial. Es esencialmente la misma forma en que se definiría, por ejemplo, la suma y la multiplicación en los números naturales (y otros ordinales). No puedo encontrar ninguna referencia especialmente buena buscando en Google, pero si buscas definiciones por recursión sobre los ordinales en cualquier libro de texto de teoría de conjuntos decente te harás una idea.

En PA, puedes utilizar las técnicas estándar para codificar funciones y conjuntos recursivos, lo cual es bastante astuto. Debe haber muchas referencias para codificar esas cosas (me gusta el libro 2 de Lógica matemática de Cori y Lascar)