Porque pensé que para demostrar este tipo de equivalencias había que usar formalismo.
Depende de lo que entiendas por "demostrar". Si te refieres a encontrar una demostración, entonces nadie usa formalismo para demostrar nada. Si tienes un problema y para preguntarlo en el foro lo formalizas y pides una respuesta formalizada, quien lea la respuesta tiene que seguir los pasos siguientes:
1) Eliminar la formalización, es decir, entender lo que significan las afirmaciones que has formalizado.
2) Resolver el problema.
3) Formalizar la respuesta porque la quieres formalizada.
Naturalmente, si alguien tiene práctica, 1) y 3) pueden ser casi inmediatas. Es como si cambias "formalizar" por "traducir al inglés". Si alguien (un hispanohablante) domina el inglés (pero piensa en español) no tendrá dificultad en traducir al español tu traducción al inglés, resolver el problema y luego traducir la respuesta al inglés, pero sería más sencillo si directamente preguntaras en español y te valiera la respuesta en español. La analogía no es exacta, porque sí que es plausible que un hispanohablante piense en inglés, pero no es plausible que un matemático razone formalmente, salvo en problemas muy, muy simples.
Si por "demostrar" te referías a "presentar la demostración formalmente", entonces todo depende de lo que entiendas por "había que".
Pregunta: En el hipotético caso de que hiciera falta formalizar, cuando decimos cosas como "X es Y si X=0 o X=1"
Esto no lo entiendo.
o como en nuestro caso: "\( a\in A \) es un átomo si \( a\neq0 \) y...", ¿esa X o la \( a \) llevan cuantificador? ¿Cuál iría? Porque usé Existe:
1º) \( \color{red}\exists a\in A\color{black}\,\forall x\in A((x\leq a\to x=a\lor x=0)\land a\neq0) \)
2º) \( \color{red}\exists a\neq0\in A\color{black}\,\forall x\in A(x\leq a\to x=a\lor x=0) \)
pero no sé si es correcto.
No, si pones un "existe" ahí, pasa lo que te ha dicho geómetracat:
En 1) y 2) lo que estás escribiendo es una proposición que afirma que existe un átomo, que no es lo mismo que las definiciones de átomo del principio. Si demostraras la equivalencia entre 1) y 2) lo que probarías es que si existe un átomo en el sentido de 1) también existe uno en el sentido de 2) y viceversa, pero esa equivalencia no te dice que un átomo en sentido de 1) sea también uno en sentido de 2) (podrían existir ambos tipos de átomo pero ser distintos).
La respuesta depende de cómo interpretes las definiciones. Si las interpretas como abreviaturas (que es lo que hago yo) entonces en principio no tienes que poner ningún cuantificador. Puedes poner:
\( a \mbox{ es un átomo}\equiv a\in A\land \forall x\in A((x\leq a\to x=a\lor x=0)\land a\neq0) \),
con lo que estás diciendo que la fómula de la derecha, que tiene libre la variable \( a \), la vas a abreviar como se indica a la izquierda.
Ahora bien, si adoptas esa definición, entonces se cumple que
\( \forall a\in A(a \mbox{ es un átomo}\leftrightarrow \forall x\in A((x\leq a\to x=a\lor x=0)\land a\neq0)) \).
Otra alternativa es considerar que las definiciones son axiomas que introducen nuevos signos formales. En tal caso la formalización de la definición sería directamente la última fórmula que he escrito, o más precisamente:
\( \forall a(a \mbox{ es un átomo de } (A, \leq, 0)\leftrightarrow a\in A\land \forall x\in A((x\leq a\to x=a\lor x=0)\land a\neq0)) \).
