Matemática y lógica: síntesis y desafíos

Resumen

Esta clase cierra la cuarta unidad del curso, dedicada a la matemática y a la lógica. Reconstruye la cadena de principios y mecanismos que va del modo matemático a los árboles de deducción, señalando en cada eslabón qué principio se usa y en qué clase se establece; sitúa lo logrado respecto del plan del curso y precisa qué cuestiones, apenas anticipadas, quedan para las unidades siguientes; repite en su evaluación de salida las destrezas de la evaluación de entrada; y termina con seis desafíos, de dificultad superior a la de los problemas de las clases, que exigen combinar varias de ellas para componer un apunte con enunciados, demostración y remisiones, diagnosticar documentos que compilan con defectos que nada denuncia, trasladar una notación lógica de una tradición a otra, construir y depurar una deducción con varias ramas, predecir la numeración y las magnitudes de un informe de física, y reunir dos preámbulos incompatibles.

Objetivos de aprendizaje

Reconstruir el orden de los mecanismos de la unidad, identificando el principio en que se apoya cada uno.
Explicar por qué tantos defectos de la escritura matemática compilan sin aviso, y dónde buscar su huella en el resultado o en el registro.
Distinguir lo que la unidad estableció de lo que solo anticipó y que las unidades siguientes desarrollarán.
Predecir los números, las remisiones y las magnitudes que produce una fuente con ecuaciones, enunciados y unidades, y corregirla.
Diseñar un preámbulo que fije la notación, los enunciados y el orden de los paquetes de un trabajo, y que permita cambiar de convención sin tocar el cuerpo.

Lo logrado en la unidad

La unidad se propuso que cada signo de una fórmula se componga según lo que significa, y que la notación de un trabajo sea la misma en todas sus páginas. El propósito se ha cumplido apoyándose en lo que la introducción declaró por sabido de las unidades anteriores: las remisiones, que dependen de lo que registra una etiqueta; las instrucciones propias, que concentran las decisiones de forma en el preámbulo; y la lectura del registro. Con ello, el camino recorrido puede leerse como una sola cadena en cinco tramos.

Fórmulas en línea y aparte

La clase sobre las fórmulas en línea y aparte estableció el principio del que dependen casi todas las demás: en el modo matemático los espacios de la fuente no cuentan, y el motor separa cada signo según su clase, ordinario, operador binario, relación, puntuación, apertura o cierre. De él dedujo por qué una variable no se escribe con \textit, por qué $3,5$ da «3, 5» y por qué la puntuación de la oración va fuera de la fórmula en línea. Mostró que en LuaLaTeX una letra griega fuera de su modo no produce error, sino que desaparece o aparece sin control, con una sola línea «Missing character» en el registro; puntuó la fórmula aparte como parte de la oración, sin líneas en blanco y sin $$; numeró con equation, \eqref, \numberwithin y \tag; distinguió \text de \mathrm; y estudió la coma decimal que babel pone al punto seguido de una cifra, la opción es-nodecimaldot que la suprime y el paquete siunitx, que necesita su propia declaración del separador.

Símbolos y notación

La clase sobre los símbolos y la notación partió de una regla de agrupación: ^ y _ actúan sobre un solo elemento o sobre un grupo entre llaves. Recorrió fracciones, raíces, letras griegas y alfabetos, entre ellos las combinaciones que con fontspec se pierden sin error, como \mathbf{\Gamma}; los operadores con nombre, con lo que babel en español cambia (\lim con tilde, \sen nuevo, \sin intacto) y lo que suprime es-minimal; los grandes operadores, los delimitadores y sus tamaños; la búsqueda de un símbolo desconocido; y unicode-math, con sus cuatro precauciones. Terminó llevando la notación al preámbulo, en instrucciones propias que se deciden una vez.

Ecuaciones de varias líneas

La clase sobre las ecuaciones de varias líneas sustituyó las fórmulas apiladas y eqnarray por align, con el & antes de la relación, y estableció que un entorno de alineación es una tabla: una fila por cada \\ y una celda por cada tramo entre dos &. De ello dedujo sus defectos silenciosos (el =&, el & de más, la barra doble final que numera una línea vacía, la etiqueta en una línea con \notag) y sus errores ruidosos; eligió entre gather, multline, split, aligned y gathered según el número que debe llevar el conjunto; compuso tramos con cases y dcases, texto con \intertext, matrices y matrices ampliadas; numeró grupos con subequations y permitió el corte de página.

Teoremas y demostraciones

La clase sobre los teoremas y las demostraciones llevó al enunciado la idea de declarar en lugar de imitar: con amsthm, \newtheorem fija el rótulo, el número y el estilo de cada clase de enunciado. Dedujo cuándo conviene el contador compartido y cuándo los separados, cuándo la numeración por sección o por capítulo, y qué estilo corresponde a lo que se afirma, a lo que se estipula y a lo que acompaña. Compuso las demostraciones con proof, cuyo rótulo viene de babel, y corrigió con \qedhere el cuadrado huérfano; remitió con cleveref, cargado después de amsthm, con un \crefname por entorno, y descubrió que con el contador compartido de \newtheorem cleveref llama «teorema» a todo enunciado, defecto que thmtools corrige.

Lógica y deducciones

La clase sobre la lógica y las deducciones separó el lenguaje objeto del metalenguaje, con \to frente a \Rightarrow y los signos \vdash, \models y \equiv; aplicó el principio de la clase del signo a la tilde de negación, a la barra de los conjuntos y a los dos puntos de las funciones; propuso una instrucción por conectivo, sin argumentos para cambiar de signos y con argumentos para cambiar de sintaxis; reunió los paquetes de los signos modales; compuso tablas de verdad con array; y construyó árboles de deducción natural con bussproofs, cuya lógica de pila explica sus dos errores, junto con las cajas de Fitch y los argumentos en forma estándar.

La figura siguiente reúne los cinco tramos en una sola cadena. Cada nudo de la columna es un mecanismo o una regla, numerado según el orden en que se apoyan unos en otros y unido por un arco a los eslabones anteriores que usa; alrededor flotan los apoyos, es decir, los principios a los que la cadena recurre una y otra vez, cada uno unido con un trazo firme a los eslabones que se apoyan en él y con uno punteado al eslabón donde se establece, salvo los que se establecieron en unidades anteriores, que se dibujan como anillos. Al pulsar un apoyo se destacan todos los eslabones que lo usan, y cada eslabón remite a la clase en que se estudia.

Apoyos de la cadena

ALo que registra una etiqueta. Una etiqueta registra el último número asignado antes de ella, dentro de su entorno, sin saber a qué está unida. Se establece en la unidad anterior. Se admite sin demostración en esta unidad.
BInstrucciones propias. Una instrucción propia nombra una función, y su definición, escrita una vez en el preámbulo, fija su forma; cambiarla cambia todo el documento. Se establece en la unidad anterior. Se admite sin demostración en esta unidad.
COrden de carga. Los paquetes se cargan en el orden en que se leen, y uno posterior ajusta, conserva o deshace lo que hizo uno anterior. Se establece en la unidad anterior. Se admite sin demostración en esta unidad.
DLa clase del signo. En el modo matemático el motor separa cada signo según su clase (ordinario, operador binario, relación, puntuación, apertura, cierre) e ignora los espacios de la fuente. Se establece en: 1. Dos modos.
ELo que desaparece sin error. En LuaLaTeX, un signo que la fuente en uso no contiene no detiene la compilación: desaparece, y solo deja en el registro una línea «Missing character». Se establece en: 2. Signos en el modo equivocado.
FUn elemento o un grupo. Los índices, los exponentes y los argumentos actúan sobre el elemento que sigue o sobre un grupo entre llaves, que no se imprimen. Se establece en: 6. Índices y exponentes.
GUna alineación es una tabla. Un entorno de alineación arma una fila por cada \\ y una celda por cada tramo entre dos &, aunque la fila quede vacía. Se establece en: 11. Alinear con align.
HLa pila de árboles. Una inferencia de n premisas toma los n últimos árboles de la pila y devuelve uno; la prueba se imprime si al final queda exactamente uno. Se establece en: 23. Árboles de deducción.

Tramo 1 Fórmulas en línea y aparte
- Predecir el resultado de un signo, una variable o una palabra escritos en el modo equivocado.
- Puntuar las fórmulas en línea y aparte como partes de la oración.
- Numerar las fórmulas aparte y remitir a ellas.
- Escribir decimales y magnitudes según la norma española, con babel o sin su conversión.
1. Dos modos. En el modo matemático las letras son variables, los espacios de la fuente no cuentan, la separación la decide la clase de cada signo y no se admite una línea en blanco.
  Se apoya en: D (La clase del signo). Se demuestra en: Fórmulas en línea y aparte.
2. Signos en el modo equivocado. Un _ en el texto da «Missing $ inserted»; \alpha fuera de fórmula desaparece o aparece pegado; una palabra dentro de la fórmula es un producto de variables y va en \text o en \mathrm, que no son intercambiables.
  Usa: 1. Dos modos. Se apoya en: E (Lo que desaparece sin error). Se demuestra en: Fórmulas en línea y aparte.
3. La fórmula en la oración. La fórmula en línea limita su altura y deja fuera la puntuación de la oración; la fórmula aparte se puntúa dentro, sin líneas en blanco, con \[…\] o equation y nunca con $$.
  Usa: 1. Dos modos. Se apoya en: D (La clase del signo). Se demuestra en: Fórmulas en línea y aparte.
4. Numerar y remitir. equation numera y su etiqueta va dentro; \eqref pone los paréntesis; \numberwithin numera por sección; \tag pone un rótulo sin consumir número.
  Usa: 3. La fórmula en la oración. Se apoya en: A (Lo que registra una etiqueta). Se demuestra en: Fórmulas en línea y aparte.
5. Coma decimal. La coma de la fórmula es puntuación; babel en español convierte en coma el punto seguido de cifra, salvo con es-nodecimaldot y las opciones que la incluyen; {,} vale siempre, y siunitx pide output-decimal-marker.
  Usa: 1. Dos modos. Se apoya en: D (La clase del signo). Se demuestra en: Fórmulas en línea y aparte.
Tramo 2 Símbolos y notación
- Agrupar índices y exponentes y predecir lo que falta sin llaves.
- Elegir alfabeto, variante y operador según la convención de la disciplina.
- Prever lo que babel en español cambia en los operadores.
- Fijar la notación del documento en su preámbulo.
1. Índices y exponentes. x^10 eleva solo el 1; x^{10} eleva el grupo; dos índices del mismo tipo seguidos dan «Double subscript» o «Double superscript».
  Usa: 1. Dos modos. Se apoya en: F (Un elemento o un grupo). Se demuestra en: Símbolos y notación.
2. Letras y alfabetos. Cada alfabeto dice qué clase de objeto se nombra; con fontspec, \mathbf{\Gamma} desaparece y \mathbf{\alpha} no sale en negrita, y la negrita de un símbolo es \boldsymbol.
  Usa: 6. Índices y exponentes. Se apoya en: E (Lo que desaparece sin error). Se demuestra en: Símbolos y notación.
3. Operadores con nombre. Los operadores van en redonda con su espacio; babel en español pone tilde a \lim, \max, \min e \inf, define \sen y no toca \sin; es-minimal lo suprime todo.
  Usa: 6. Índices y exponentes. Se apoya en: D (La clase del signo). Se demuestra en: Símbolos y notación.
4. Delimitadores. \left y \right miden lo que encierran y van en pareja; los tamaños manuales dan un control fino; mathtools define pares como \abs.
  Usa: 6. Índices y exponentes. Se apoya en: D (La clase del signo), F (Un elemento o un grupo). Se demuestra en: Símbolos y notación.
5. La notación en el preámbulo. \R, \vect, \dd o \abs se definen una vez; unicode-math va después de amsmath, sin amssymb detrás, y pide \symbf para la negrita.
  Usa: 7. Letras y alfabetos, 8. Operadores con nombre, 9. Delimitadores. Se apoya en: B (Instrucciones propias), C (Orden de carga), E (Lo que desaparece sin error). Se demuestra en: Símbolos y notación.
Tramo 3 Ecuaciones de varias líneas
- Alinear cadenas y sistemas con align, con el & antes de la relación.
- Decidir qué líneas se numeran y predecir los números.
- Elegir el entorno según la estructura y el número del conjunto.
- Componer tramos, matrices y texto intercalado.
1. Alinear con align. El & va antes de la relación y \\ abre una fila; =& y un & de más cambian el resultado sin aviso, y una línea en blanco detiene la compilación.
  Usa: 3. La fórmula en la oración. Se apoya en: G (Una alineación es una tabla), D (La clase del signo). Se demuestra en: Ecuaciones de varias líneas.
2. Qué líneas se numeran. align numera cada fila, también la vacía que deja un \\ final; \notag quita el número sin consumirlo, y una etiqueta en esa línea registra el de la línea numerada siguiente.
  Usa: 11. Alinear con align, 4. Numerar y remitir. Se apoya en: G (Una alineación es una tabla), A (Lo que registra una etiqueta). Se demuestra en: Ecuaciones de varias líneas.
3. Un número para el conjunto. split dentro de equation da un número a la cadena; aligned y gathered son bloques sin número; subequations da letras a un grupo que consume un solo número.
  Usa: 11. Alinear con align, 12. Qué líneas se numeran. Se apoya en: A (Lo que registra una etiqueta). Se demuestra en: Ecuaciones de varias líneas.
4. Tramos, matrices y texto. cases tiene dos columnas y convierte un & de más en fin de fila; dcases compone a tamaño aparte; las matrices admiten diez columnas; array traza barras; \intertext no rompe la alineación.
  Usa: 11. Alinear con align. Se apoya en: G (Una alineación es una tabla). Se demuestra en: Ecuaciones de varias líneas.
Tramo 4 Teoremas y demostraciones
- Declarar los enunciados con su estilo y su contador.
- Predecir la numeración de una serie compartida o separada.
- Cerrar las demostraciones con el símbolo en su lugar.
- Remitir a los enunciados con su nombre.
1. Enunciados declarados. \newtheorem de amsthm, en el preámbulo, fija rótulo, número y aspecto; el rótulo lo escribe el autor, y la forma con asterisco no numera.
  Se apoya en: B (Instrucciones propias). Se demuestra en: Teoremas y demostraciones.
2. Contadores y estilos. [teorema] hace una sola serie, cuyo número dice el lugar; [section] o [chapter] numera por división; plain, definition y remark responden a lo que se afirma, se estipula o acompaña.
  Usa: 15. Enunciados declarados. Se apoya en: B (Instrucciones propias). Se demuestra en: Teoremas y demostraciones.
3. Demostraciones. proof toma su rótulo de babel y pone el cuadrado al terminar el último párrafo; si termina en una fórmula o una lista, \qedhere lo pone en su lugar, salvo junto a un número.
  Usa: 15. Enunciados declarados, 11. Alinear con align. Se demuestra en: Teoremas y demostraciones.
4. Remitir a los enunciados. La etiqueta va dentro del entorno; amsthm se carga antes de cleveref, con un \crefname por entorno; con el contador compartido de \newtheorem todo se llama «teorema», y thmtools lo corrige.
  Usa: 16. Contadores y estilos, 4. Numerar y remitir. Se apoya en: A (Lo que registra una etiqueta), C (Orden de carga). Se demuestra en: Teoremas y demostraciones.
Tramo 5 Lógica y deducciones
- Distinguir el lenguaje objeto del metalenguaje en la notación.
- Corregir el espaciado de la tilde, la barra, los dos puntos y los cuantificadores.
- Cambiar de tradición desde el preámbulo.
- Construir y depurar árboles de deducción, tablas de verdad y argumentos.
1. Dos niveles de lenguaje. \to es el conectivo del lenguaje objeto y \Rightarrow la flecha del metalenguaje; \vdash afirma la deducción y \models la consecuencia semántica.
  Usa: 8. Operadores con nombre. Se demuestra en: Lógica y deducciones.
2. El espaciado lógico. \sim es una relación y va entre llaves; la barra del teclado es ordinaria y \mid relación; : es relación y \colon puntuación; el alcance de un cuantificador lo decide un paréntesis.
  Usa: 19. Dos niveles de lenguaje, 5. Coma decimal. Se apoya en: D (La clase del signo). Se demuestra en: Lógica y deducciones.
3. Una instrucción por conectivo. Sin argumentos, la instrucción cambia el signo de una tradición a otra; con argumentos, la definición decide además el orden y los paréntesis, y permite la notación polaca.
  Usa: 20. El espaciado lógico, 10. La notación en el preámbulo. Se apoya en: B (Instrucciones propias), F (Un elemento o un grupo). Se demuestra en: Lógica y deducciones.
4. Signos modales y tablas de verdad. \Box, \Diamond y \vDash exigen amssymb, y latexsym cargado antes cambia el rombo; la tabla de verdad es un array con V y F en redonda.
  Usa: 19. Dos niveles de lenguaje, 14. Tramos, matrices y texto. Se apoya en: C (Orden de carga), G (Una alineación es una tabla). Se demuestra en: Lógica y deducciones.
5. Árboles de deducción. En bussproofs, \AxiomC pone una hoja y las inferencias toman los últimos árboles; si faltan, «Hypotheses missing!»; si sobran, «Proof tree badly specified.» al imprimir.
  Usa: 19. Dos niveles de lenguaje. Se apoya en: H (La pila de árboles). Se demuestra en: Lógica y deducciones.
6. Cajas y forma estándar. logicproof compone las cajas de Fitch como una tabla con subproof; un argumento en forma estándar numera las premisas y separa la conclusión con una raya y \therefore.
  Usa: 23. Árboles de deducción, 22. Signos modales y tablas de verdad. Se apoya en: G (Una alineación es una tabla). Se demuestra en: Lógica y deducciones.

Hacia las tablas y las figuras. La cadena se detiene donde las fórmulas, los enunciados y las deducciones están completos y numerados: la tabla, que aquí solo sirvió a las matrices, a las tablas de verdad y a las pruebas, crece en la unidad siguiente hasta las tablas y las figuras del documento, con sus pies, sus números y su lugar en la página.