¿Cómo sé lo que ya sabemos en una prueba cuando las suposiciones que podemos usar son aún más complejas?

Question

Creo que una razón por la que encuentro las demostraciones tan difíciles es que no sé qué se nos permite saber y qué asumimos que no sabemos.

Por ejemplo, "demostrar $0x = 0$" parece increíblemente obvio y aún así tengo que probarlo con suposiciones "más simples" e intentar encontrar una solución ingeniosa:

$$\begin{array} {rcll} 0x &=& 0x &\text{ por la reflexividad $x=x$}\\ (0+0)x &=& 0x &\text{ por la identidad aditiva $x+0=x$ y... ¿sustitución?}\\ 0x + 0x &=& 0x &\text{ por el axioma distributivo}\\ 0x + 0x &=& 0x + 0 &\text{ nuevamente por la identidad aditiva}\\ 0x &=& 0 &\text{ por la ley de cancelación}\\ \end{array}$$

Pero de todos modos estas demostraciones ya me resultan insatisfactorias. ¿Cómo sé con qué "reglas" se me permite trabajar? Por ejemplo, la ley distributiva siendo un axioma nunca hubiera imaginado en cien años que era un axioma porque parece mucho más "complicado" que la idea de demostrar $0x=0$.

¿Hay una manera general de saber qué podemos y qué no podemos usar para demostrar algo? ¿Por qué se permiten estas suposiciones "más complicadas" como la ley distributiva (que parece abarcar varias reglas a la vez, como la adición, la multiplicación, la reestructuración de la afirmación, etc.)?

Answer 1

Como han dicho otros en los comentarios, sabes qué reglas y axiomas puedes usar porque se te da o eliges una colección particular. Uno de los malentendidos más comunes que veo es pensar que hay un conjunto de reglas y axiomas en los que todos los matemáticos están de acuerdo. Esto es especialmente pernicioso en lógica pero también existe en otras áreas. Por lo general, lo que sucede es que un estudiante ve una definición y asume que esa es la definición. Por lo general, pasa un tiempo antes de que se den cuenta de que todas estas cosas tienen una variedad de definiciones diferentes pero equivalentes, y en la mayoría de los casos también tienen definiciones genuinamente diferentes. En el caso de la lógica, solo con mirar la gran cantidad de entradas bajo "lógica" en la Enciclopedia de Filosofía de Stanford, muchas de las cuales corresponden a lógicas diferentes, se puede tener una idea. Y no es para nada exhaustivo.

Para tu ejemplo, todo el razonamiento es ecuacional, por lo que no es tan crítico qué lógica estamos usando. Necesitamos las leyes para la igualdad que podrían describirse aproximadamente como "una congruencia con respecto a todo". Primero, la igualdad es una relación de equivalencia, lo que significa que es reflexiva, $x=x$; simétrica, si $x = y$ entonces $y = x$; y transitiva, si $x = y$ y $y = z$ entonces $x = z. Luego, lo que hace que la igualdad sea igualdad es la indiscernibilidad de lo idéntico, que generalmente se expresa como una regla en lugar de un axioma y establece: si $x = y$ y $P$ es algún predicado con la variable libre $z$, entonces si es demostrable $P[x/z]$ también lo es $P[y/z]$, donde $P[x/z]$ significa que $P$ con todas las ocurrencias libres de $z$ reemplazadas por $x$, es decir, sustituyendo $x$ por $z, y similarmente para $P[y/z]$. (Nuevamente, hay otras formas de presentar estas reglas y axiomas. De hecho, este conjunto es redundante...)

La demostración de una afirmación como $0x=0$ es común en la teoría de anillos. Por ejemplo, usando la definición de anillo dada en Wikipedia, esto es un teorema pero no un axioma. El aspecto que mencioné antes también aparece aquí. Hay otras opciones que podrías tomar para los axiomas de un anillo, incluyendo aquellos donde $0x=0$ se toma axiomáticamente. Además, el término "anillo" es ambiguo ya que muchos autores consideran "anillos sin unidad" (es decir, que no necesariamente tienen un elemento que se comporte como $1). La definición que da Wikipedia es la de un anillo con unidad. Estas definiciones no son equivalentes.

De todas formas, usando la definición en Wikipedia, una forma de demostrar $0x=0$ es la siguiente: $$\begin{align} &0x-0x=0 \tag{inverso aditivo} \\ \iff & (0+0)x-0x=0 \tag{identidad aditiva} \\ \iff & (0x+0x)-0x = 0 \tag{distributividad izquierda} \\ \iff & 0x+(0x-0x) = 0 \tag{asociatividad aditiva} \\ \iff & 0x + 0 = 0 \tag{inverso aditivo} \\ \iff & 0x = 0 \tag{identidad aditiva} \end{align}$$

Cada $\iff$ está ocultando un uso de la indiscernibilidad de idénticos. Por ejemplo, el primer paso es: sea $P$ igual a $zx-0x=0$, el axioma de la identidad aditiva para $0$ establece $0+0=0$ o, por simetría, $0=0+0$, si es demostrable $P[0/z]$, entonces es demostrable $P[(0+0)/z]$. Esto da la dirección $\Rightarrow$, la dirección $\Leftarrow$ simplemente usa la misma igualdad en la otra dirección.

Entonces, ¿por qué no tomamos simplemente $0x=0$ como un axioma? Bueno, podríamos. Sin embargo, al hacerlo no nos permitiría derivar los otros axiomas y dado los otros axiomas podemos derivar este. Usar una colección mínima de axiomas facilita verificar si algo es un anillo (o un homomorfismo de anillos). Tendríamos que verificar explícitamente $0x=0$ mientras tenerlo como teorema significa que podemos derivarlo de una vez por todas para todos los anillos. Otro factor que afecta la elección de axiomas también es evidente en la presentación de Wikipedia. A menudo queremos construir nuestras definiciones de manera modular (lo que a menudo conduce a listas no mínimas de axiomas). En este caso, la definición de Wikipedia comienza con los axiomas de un grupo conmutativo. Es decir, un anillo es un grupo conmutativo y simultáneamente un monoide cuya "multiplicación" se distribuye sobre la operación de grupo. Esta forma de presentar los anillos nos permite "importar" teoremas sobre grupos conmutativos y monoides y aplicarlos a los anillos. Podríamos, por supuesto, seguir haciendo esto si tuviéramos una presentación diferente de los axiomas de un anillo, pero tendríamos que derivar primero la estructura de grupo conmutativo/monoide, y esta estructura puede no ser obvia desde la presentación alternativa.

Si realmente quieres tener una percepción visceral de todo esto, recomiendo familiarizarte con un asistente de pruebas como Agda, Coq, LEAN, u otros. Recomiendo especialmente Agda ya que muestra todos los detalles de las pruebas de manera directa. La mayoría de los otros asistentes de pruebas utilizan un enfoque basado en tácticas, lo que significa que generalmente escribes "scripts de prueba" que son pequeños programas que buscan pruebas por ti. Típicamente no ves las pruebas en esos sistemas. Sin embargo, cualquiera de ellos dejará bastante claro lo que significa trabajar con una definición dada, qué está disponible y qué no lo está en un momento dado, y por qué estructurar definiciones de una manera u otra puede ser deseable. Todos tienen curvas de aprendizaje bastante pronunciadas, aunque LEAN y Coq tienen mejor material introductorio que Agda.

Answer 2

Usando la teoría de conjuntos, las reglas de la lógica y los Axiomas de Peano (para $N, S$ y $0$), es posible probar la existencia de las funciones de suma y multiplicación en $N$ y que son asociativas, conmutativas, distributivas, etc. Sin embargo, se requerirían cientos de líneas de prueba formal para hacer esto, por lo que la mayoría de los libros de texto suelen omitir todo eso y simplemente "definen" la suma y multiplicación y sus propiedades algebraicas en solo unas pocas líneas. Y las definiciones variarán un poco de un libro de texto a otro dependiendo del público objetivo y las preferencias del autor. Es inevitable. Si tienes dudas sobre qué definiciones se te permite usar para una tarea específica, pregunta a tu instructor para aclararlo.