Los términos de reticulado son monótonos

El enunciado, textual: «Sea $\tau =(\varnothing ,\{{\mathrm{s}}^2,{\mathrm{i}}^2\},\{{\le }^2\},a)$. Sea $t{=}_{d}t(v_1,v_2)\in T^{\tau }$. Sea $𝐀$ una estructura de tipo $\tau$ tal que $(A,{\mathrm{s}}^{𝐀},{\mathrm{i}}^{𝐀},{\le }^{𝐀})$ es un reticulado cuaterna. Pruebe que cualesquiera sean $a_1,a_2,b_1,b_2\in A$, se tiene que si $a_1{\le }^{𝐀}{b}_1$ y $a_2{\le }^{𝐀}{b}_2$ entonces $t^{𝐀}[a_1,a_2]{\le }^{𝐀}{t}^{𝐀}[b_1,b_2]$.» Es el Ejercicio 31 de la Guía 11.

Está enunciado con ${=}_d$, así que, como pide el encabezado de la lista para los ejercicios 21 a 30, se resuelve dentro de la notación declaratoria: con los lemas y convenciones de la sección «Manejo técnico de la notación declaratoria» de la Guía 11, sin asignaciones infinitas.

01 · Qué dice, antes de probar

$t$ es un término armado con $v_1$, $v_2$ y los nombres $\mathrm{s}$ e $\mathrm{i}$; el tipo no tiene constantes. $t^{𝐀}[a_1,a_2]$ es lo que vale $t$ en $𝐀$ cuando $v_1$ vale $a_1$ y $v_2$ vale $a_2$ (Convención Notacional 2 de la Guía 11, p. 2). El enunciado compara el mismo término en dos pares de argumentos: si cada argumento sube o se queda, el valor sube o se queda.

Un ejemplo. En el pentágono, con $0<p<q<1$ y $0<r<1$ ($r$ no comparable con $p$ ni con $q$), sea $t=\mathrm{i}(v_1,\mathrm{s}(v_2,\mathrm{i}(v_1,v_2)))$. Con $(a_1,a_2)=(p,q)$ y $(b_1,b_2)=(q,1)$ se cumplen $p\le q$ y $q\le 1$, y $t^{𝐀}[p,q]=p$, $t^{𝐀}[q,1]=q$: el valor subió. Si en cambio $(b_1,b_2)=(q,r)$, la segunda hipótesis se cae —$q$ no está debajo de $r$— y $t^{𝐀}[q,r]=0$, que no está arriba de $p$.

Las dos hipótesis hacen falta. Medido en el pentágono, sobre los 202 términos en $v_1,v_2$ de nivel a lo sumo 2 y las 625 cuaternas $(a_1,a_2,b_1,b_2)$: con las dos hipótesis la conclusión vale en los 34 138 casos; con una sola, falla en 26 872 de 63 024. En el diamante $M_3$ da lo mismo: ninguna falla con las dos, 24 784 con una sola.

02 · Las herramientas

Los lemas y las convenciones de la sección «Manejo técnico de la notación declaratoria» son lo que el encabezado de la lista manda usar en los ejercicios 21 a 30: se enuncian y se citan. Lo que haga falta de otra parte se enuncia y se prueba.

La Regla de Inducción desde 0. Si para cada $k\in \omega$ hay un enunciado ${\mathrm{Enu}}_k$, y se prueba que ${\mathrm{Enu}}_0$ es verdadero y que ${\mathrm{Enu}}_k$ implica ${\mathrm{Enu}}_{k+1}$ para cada $k$, entonces ${\mathrm{Enu}}_k$ es verdadero para todo $k$. Se usa con $T_k^{\tau }$, los términos de nivel $k$: $T_0^{\tau }=\mathrm{Var}\cup 𝒞$, los $T_k^{\tau }$ crecen con $k$, y todo término está en alguno.

Lema 1 de la Guía 11, p. 8 (lectura única de términos declarados). Si $t\in T^{\tau }$ y $t{=}_{d}t(v_1,\dots ,v_n)$, se da una y sólo una de: (1) $t=c$ para algún $c\in 𝒞$; (2) $t=v_j$ para algún $j\in \{1,\dots ,n\}$; (3) $t=f(t_1,\dots ,t_m)$ con $f\in {ℱ}_m$, $m\ge 1$ y $t_1,\dots ,t_m\in T^{\tau }$ únicos. Más aún, si $t\in T_{k+1}^{\tau }$, en el caso (3) los $t_1,\dots ,t_m$ están en $T_k^{\tau }$. Es un teorema de lectura única: la lista deja usarlo sin probarlo.

Convención Notacional 5 de la Guía 11, p. 8. Si $t{=}_{d}t(v_1,\dots ,v_n)$ y se da el caso (3) del Lema 1, se supone hecha también la declaración $t_j{=}_d{t}_j(v_1,\dots ,v_n)$ para cada $j$. Las variables de cada $t_j$ están entre las de $t$.

Lema 3 de la Guía 11, p. 9 (carácter recursivo de $t^{𝐀}[a_1,\dots ,a_n]$). Si $t{=}_{d}t(v_1,\dots ,v_n)$, $𝐀$ es un modelo de tipo $\tau$ y $a_1,\dots ,a_n\in A$: (1) si $t=c$, $t^{𝐀}[a_1,\dots ,a_n]=c^{𝐀}$; (2) si $t=v_j$, $t^{𝐀}[a_1,\dots ,a_n]=a_j$; (3) si $t=f(t_1,\dots ,t_m)$, entonces

$$t^{𝐀}[a_1,\dots ,a_n]=f^{𝐀}(t_1^{𝐀}[a_1,\dots ,a_n],\dots ,t_m^{𝐀}[a_1,\dots ,a_n])$$

Los axiomas del reticulado cuaterna, con los nombres de la Guía 6. Que $(A,{\mathrm{s}}^{𝐀},{\mathrm{i}}^{𝐀},{\le }^{𝐀})$ sea un reticulado cuaterna quiere decir que cumple los siete; la prueba usa cinco, escritos acá con ${\mathrm{s}}^{𝐀}$ e ${\mathrm{i}}^{𝐀}$ como funciones, que es como los escribe el Lema 3:

• A≤T: si $x{\le }^{𝐀}y$ e $y{\le }^{𝐀}z$, entonces $x{\le }^{𝐀}z$.
• AsesC: $x{\le }^{𝐀}{\mathrm{s}}^{𝐀}(x,y)$ e $y{\le }^{𝐀}{\mathrm{s}}^{𝐀}(x,y)$.
• As≤C: si $x{\le }^{𝐀}z$ e $y{\le }^{𝐀}z$, entonces ${\mathrm{s}}^{𝐀}(x,y){\le }^{𝐀}z$.
• AiesC: ${\mathrm{i}}^{𝐀}(x,y){\le }^{𝐀}x$ e ${\mathrm{i}}^{𝐀}(x,y){\le }^{𝐀}y$.
• Ai≥C: si $z{\le }^{𝐀}x$ y $z{\le }^{𝐀}y$, entonces $z{\le }^{𝐀}{\mathrm{i}}^{𝐀}(x,y)$.

Lo que no está en la Guía 11: la monotonía de $\mathrm{s}$ e $\mathrm{i}$. Es el paso de la inducción, y es un resultado de reticulados —la mitad de $\mathrm{s}$ es el Ejercicio 1 de la lista del parcial 2—, no un lema de la notación declaratoria ni un teorema de lectura única. Por la regla del encabezado, se enuncia y se prueba adentro de la resolución. Está hecho en el escarabajo, antes de la inducción.

03 · La mariposa: el término se desarma y el orden se arma

Lo que se afirma es para todo término, así que la prueba es por inducción en el nivel: la Regla de Inducción desde 0, con ${\mathrm{Enu}}_k$ diciendo lo pedido para los términos de $T_k^{\tau }$.

Qué va adentro de ${\mathrm{Enu}}_k$. La estructura, el término con su declaración, los cuatro elementos y las dos hipótesis. La declaración $t{=}_{d}t(v_1,v_2)$ tiene que estar en la hipótesis de ${\mathrm{Enu}}_k$: en el paso, ${\mathrm{Enu}}_k$ se aplica a los dos argumentos de $t$, y lo que garantiza que ellos también están declarados con $(v_1,v_2)$ es la Convención 5. Los cuatro elementos pasan iguales a los argumentos, así que dejarlos afuera no rompería nada en este ejercicio; adentro es la forma que sirve siempre, y la que se escribe.

El caso base. Un término de $T_0^{\tau }$ es una variable o una constante, y $\tau$ no tiene constantes: por el Lema 1, $t=v_1$ o $t=v_2$. Ahí se usa cada hipótesis, una por variable: $t^{𝐀}[a_1,a_2]=a_1{\le }^{𝐀}{b}_1=t^{𝐀}[b_1,b_2]$, y lo mismo con $v_2$.

El paso. Un término de $T_{k+1}^{\tau }-T_k^{\tau }$ no es una variable —las variables están en $T_0^{\tau }\subseteq T_k^{\tau }$— y el tipo tiene dos nombres de función, los dos de aridad 2: por el Lema 1, $t=\mathrm{s}(t_1,t_2)$ o $t=\mathrm{i}(t_1,t_2)$, con $t_1,t_2\in T_k^{\tau }$. ${\mathrm{Enu}}_k$ da, para cada argumento, $t_j^{𝐀}[a_1,a_2]{\le }^{𝐀}{t}_j^{𝐀}[b_1,b_2]$. El Lema 3 (3) pasa de $t^{𝐀}[a_1,a_2]$ a ${\mathrm{s}}^{𝐀}$ aplicado a esos dos valores. Queda

$${\mathrm{s}}^{𝐀}(t_1^{𝐀}[a_1,a_2],t_2^{𝐀}[a_1,a_2]){\le }^{𝐀}{\mathrm{s}}^{𝐀}(t_1^{𝐀}[b_1,b_2],t_2^{𝐀}[b_1,b_2])$$

sabiendo que cada argumento de la izquierda está debajo del de la derecha. Eso, con nombres más cortos, es la monotonía: si $x{\le }^{𝐀}y$ y $z{\le }^{𝐀}w$, entonces ${\mathrm{s}}^{𝐀}(x,z){\le }^{𝐀}{\mathrm{s}}^{𝐀}(y,w)$. Y lo mismo con $\mathrm{i}$.

La monotonía, de atrás para adelante. La meta ${\mathrm{s}}^{𝐀}(x,z){\le }^{𝐀}{\mathrm{s}}^{𝐀}(y,w)$ tiene un supremo a la izquierda: As≤C la parte en $x{\le }^{𝐀}{\mathrm{s}}^{𝐀}(y,w)$ y $z{\le }^{𝐀}{\mathrm{s}}^{𝐀}(y,w)$. La primera pasa por $y$: $x{\le }^{𝐀}y$ es la hipótesis, $y{\le }^{𝐀}{\mathrm{s}}^{𝐀}(y,w)$ es AsesC, y A≤T las junta. La segunda pasa por $w$. Para $\mathrm{i}$ es lo mismo dado vuelta: la meta ${\mathrm{i}}^{𝐀}(x,z){\le }^{𝐀}{\mathrm{i}}^{𝐀}(y,w)$ tiene un ínfimo a la derecha, y Ai≥C la parte en ${\mathrm{i}}^{𝐀}(x,z){\le }^{𝐀}y$ y ${\mathrm{i}}^{𝐀}(x,z){\le }^{𝐀}w$, que pasan por $x$ y por $z$ con AiesC y A≤T.

Abajo, el pentágono y cuatro términos. Cada fila es un subtérmino, del más chico al término entero, con su valor en los dos pares de argumentos: es la inducción hecha a mano, de abajo para arriba. Arranca con la segunda hipótesis rota.

Con las dos hipótesis no aparece ninguna fila roja, elijas el término y los argumentos que elijas: es el teorema. Con una rota, la primera fila roja es siempre la variable cuya hipótesis falta, y desde ahí puede subir o perderse. En el término que arranca, la fila de $v_2$ se rompe y el término entero también.

04 · El escarabajo: la prueba escrita

Monotonía. Sea $𝐀$ una estructura de tipo $\tau$ tal que $(A,{\mathrm{s}}^{𝐀},{\mathrm{i}}^{𝐀},{\le }^{𝐀})$ es un reticulado cuaterna. Si $x,y,z,w\in A$ cumplen $x{\le }^{𝐀}y$ y $z{\le }^{𝐀}w$, entonces ${\mathrm{s}}^{𝐀}(x,z){\le }^{𝐀}{\mathrm{s}}^{𝐀}(y,w)$ e ${\mathrm{i}}^{𝐀}(x,z){\le }^{𝐀}{\mathrm{i}}^{𝐀}(y,w)$.

Prueba. Sean $x,y,z,w\in A$ con $x{\le }^{𝐀}y$ y $z{\le }^{𝐀}w$.

• Por AsesC, $y{\le }^{𝐀}{\mathrm{s}}^{𝐀}(y,w)$ y $w{\le }^{𝐀}{\mathrm{s}}^{𝐀}(y,w)$. Por A≤T, de $x{\le }^{𝐀}y$ e $y{\le }^{𝐀}{\mathrm{s}}^{𝐀}(y,w)$ sale $x{\le }^{𝐀}{\mathrm{s}}^{𝐀}(y,w)$, y de $z{\le }^{𝐀}w$ y $w{\le }^{𝐀}{\mathrm{s}}^{𝐀}(y,w)$ sale $z{\le }^{𝐀}{\mathrm{s}}^{𝐀}(y,w)$. Por As≤C, tomando $z$ del axioma como ${\mathrm{s}}^{𝐀}(y,w)$, ${\mathrm{s}}^{𝐀}(x,z){\le }^{𝐀}{\mathrm{s}}^{𝐀}(y,w)$.
• Por AiesC, ${\mathrm{i}}^{𝐀}(x,z){\le }^{𝐀}x$ e ${\mathrm{i}}^{𝐀}(x,z){\le }^{𝐀}z$. Por A≤T, de ${\mathrm{i}}^{𝐀}(x,z){\le }^{𝐀}x$ y $x{\le }^{𝐀}y$ sale ${\mathrm{i}}^{𝐀}(x,z){\le }^{𝐀}y$, y de ${\mathrm{i}}^{𝐀}(x,z){\le }^{𝐀}z$ y $z{\le }^{𝐀}w$ sale ${\mathrm{i}}^{𝐀}(x,z){\le }^{𝐀}w$. Por Ai≥C, tomando $z$ del axioma como ${\mathrm{i}}^{𝐀}(x,z)$, ${\mathrm{i}}^{𝐀}(x,z){\le }^{𝐀}{\mathrm{i}}^{𝐀}(y,w)$. ∎

El ejercicio. Prueba. Usaremos la Regla de Inducción desde 0. Para cada $k\in \omega$ sea ${\mathrm{Enu}}_k$ el enunciado:

${\mathrm{Enu}}_k$: Sea $𝐀$ una estructura de tipo $\tau$ tal que $(A,{\mathrm{s}}^{𝐀},{\mathrm{i}}^{𝐀},{\le }^{𝐀})$ es un reticulado cuaterna. Si $t\in T_k^{\tau }$ y $t{=}_{d}t(v_1,v_2)$, entonces para cualesquiera $a_1,a_2,b_1,b_2\in A$, si $a_1{\le }^{𝐀}{b}_1$ y $a_2{\le }^{𝐀}{b}_2$, se tiene que $t^{𝐀}[a_1,a_2]{\le }^{𝐀}{t}^{𝐀}[b_1,b_2]$.

• ${\mathrm{Enu}}_0$ es verdadero. Sean $𝐀$ como en el enunciado, $t\in T_0^{\tau }$ con $t{=}_{d}t(v_1,v_2)$, y $a_1,a_2,b_1,b_2\in A$ con $a_1{\le }^{𝐀}{b}_1$ y $a_2{\le }^{𝐀}{b}_2$. Por el Lema 1 de la Guía 11, $t=c$ para algún $c\in 𝒞$, o $t=v_j$ con $j\in \{1,2\}$, o $t=f(t_1,\dots ,t_m)$; esto último no puede ser, porque los términos de $T_0^{\tau }=\mathrm{Var}\cup 𝒞$ no tienen paréntesis, y lo primero tampoco, porque $𝒞=\varnothing$.
  • Si $t=v_1$, por el Lema 3 (2) de la Guía 11, $t^{𝐀}[a_1,a_2]=a_1$ y $t^{𝐀}[b_1,b_2]=b_1$, y $a_1{\le }^{𝐀}{b}_1$ es hipótesis.
  • Si $t=v_2$, por el Lema 3 (2), $t^{𝐀}[a_1,a_2]=a_2$ y $t^{𝐀}[b_1,b_2]=b_2$, y $a_2{\le }^{𝐀}{b}_2$ es hipótesis.
• ${\mathrm{Enu}}_k$ implica ${\mathrm{Enu}}_{k+1}$. Supongamos ${\mathrm{Enu}}_k$. Sean $𝐀$ como en el enunciado, $t\in T_{k+1}^{\tau }$ con $t{=}_{d}t(v_1,v_2)$, y $a_1,a_2,b_1,b_2\in A$ con $a_1{\le }^{𝐀}{b}_1$ y $a_2{\le }^{𝐀}{b}_2$.
  • Caso $t\in T_k^{\tau }$. Vale por ${\mathrm{Enu}}_k$.
  • Caso $t\in T_{k+1}^{\tau }-T_k^{\tau }$. Por el Lema 1 de la Guía 11, $t$ no es una constante, porque $𝒞=\varnothing$, ni una variable, porque $\mathrm{Var}\subseteq T_0^{\tau }\subseteq T_k^{\tau }$. Luego $t=f(t_1,\dots ,t_m)$ con $f\in {ℱ}_m$, $m\ge 1$, y como $ℱ={ℱ}_2=\{\mathrm{s},\mathrm{i}\}$, $t=\mathrm{s}(t_1,t_2)$ o $t=\mathrm{i}(t_1,t_2)$; por la segunda parte del Lema 1, $t_1,t_2\in T_k^{\tau }$. Por la Convención Notacional 5, $t_1{=}_d{t}_1(v_1,v_2)$ y $t_2{=}_d{t}_2(v_1,v_2)$. Aplicando ${\mathrm{Enu}}_k$ a $t_1$ y a $t_2$, con la misma $𝐀$ y los mismos $a_1,a_2,b_1,b_2$, $$t_1^{𝐀}[a_1,a_2]{\le }^{𝐀}{t}_1^{𝐀}[b_1,b_2]\text{ y }{t}_2^{𝐀}[a_1,a_2]{\le }^{𝐀}{t}_2^{𝐀}[b_1,b_2]$$
    • Si $t=\mathrm{s}(t_1,t_2)$, por el Lema 3 (3) de la Guía 11, $t^{𝐀}[a_1,a_2]={\mathrm{s}}^{𝐀}(t_1^{𝐀}[a_1,a_2],t_2^{𝐀}[a_1,a_2])$ y $t^{𝐀}[b_1,b_2]={\mathrm{s}}^{𝐀}(t_1^{𝐀}[b_1,b_2],t_2^{𝐀}[b_1,b_2])$. Por la monotonía, tomando $x=t_1^{𝐀}[a_1,a_2]$, $y=t_1^{𝐀}[b_1,b_2]$, $z=t_2^{𝐀}[a_1,a_2]$ y $w=t_2^{𝐀}[b_1,b_2]$, se tiene $t^{𝐀}[a_1,a_2]{\le }^{𝐀}{t}^{𝐀}[b_1,b_2]$.
    • Si $t=\mathrm{i}(t_1,t_2)$, por el Lema 3 (3), $t^{𝐀}[a_1,a_2]={\mathrm{i}}^{𝐀}(t_1^{𝐀}[a_1,a_2],t_2^{𝐀}[a_1,a_2])$ y $t^{𝐀}[b_1,b_2]={\mathrm{i}}^{𝐀}(t_1^{𝐀}[b_1,b_2],t_2^{𝐀}[b_1,b_2])$. Por la monotonía, con los mismos $x,y,z,w$, se tiene $t^{𝐀}[a_1,a_2]{\le }^{𝐀}{t}^{𝐀}[b_1,b_2]$.

Por la Regla de Inducción desde 0, ${\mathrm{Enu}}_k$ vale para todo $k\in \omega$. Sea ahora $t{=}_{d}t(v_1,v_2)\in T^{\tau }$, y sea $k$ tal que $t\in T_k^{\tau }$: ${\mathrm{Enu}}_k$ dice que para cualesquiera $a_1,a_2,b_1,b_2\in A$ con $a_1{\le }^{𝐀}{b}_1$ y $a_2{\le }^{𝐀}{b}_2$, $t^{𝐀}[a_1,a_2]{\le }^{𝐀}{t}^{𝐀}[b_1,b_2]$. ∎

05 · Lo que se lleva a otros ejercicios

El molde es el de toda inducción declaratoria en términos. Caso base con el Lema 1 y el Lema 3 (1) y (2); paso con el Lema 1 (y su «más aún» para bajar de nivel), la Convención 5 para declarar los argumentos y el Lema 3 (3) para pasar del valor del término a la operación aplicada a los valores. Lo único propio de cada ejercicio es lo que se hace con esa operación. En el Ejercicio 21 es ver que $\{a,b,asb,aib\}$ es cerrado por $\mathrm{s}$ e $\mathrm{i}$; en el Ejercicio 23, que $S$ es cerrado por las operaciones, y ahí sí hay constantes en el caso base; acá es la monotonía.

Lo que hace perder puntos. Escribir «por monotonía» sin enunciarla y probarla: no es de la Guía 11. Escribir ${\mathrm{Enu}}_k$ sin la declaración $t{=}_{d}t(v_1,v_2)$, y entonces no poder usar el Lema 3 en los argumentos. Olvidar el caso $t\in T_k^{\tau }$ del paso. Usar el Lema 3 (3) sobre $t_1$ y $t_2$ sin decir que la Convención 5 los declara. Despachar el caso de $\mathrm{i}$ con «análogamente» cuando la monotonía de $\mathrm{i}$ usa otros dos axiomas. Y probar sólo una de las dos hipótesis en el caso base: cada variable usa la suya.

Para tener a mano

1. ${\mathrm{Enu}}_k$: para toda $𝐀$ reticulado cuaterna, todo $t\in T_k^{\tau }$ con $t{=}_{d}t(v_1,v_2)$ y todos $a_1,a_2,b_1,b_2$ con $a_1{\le }^{𝐀}{b}_1$ y $a_2{\le }^{𝐀}{b}_2$, $t^{𝐀}[a_1,a_2]{\le }^{𝐀}{t}^{𝐀}[b_1,b_2]$.
2. Caso base: sin constantes, $t=v_1$ o $t=v_2$; cada uno usa su hipótesis.
3. Paso: $t=\mathrm{s}(t_1,t_2)$ o $\mathrm{i}(t_1,t_2)$ con $t_1,t_2\in T_k^{\tau }$ (Lema 1), declarados con $(v_1,v_2)$ (Convención 5), y el Lema 3 (3) deja la monotonía como única cuenta.
4. Monotonía de $\mathrm{s}$: AsesC, A≤T dos veces, As≤C. De $\mathrm{i}$: AiesC, A≤T dos veces, Ai≥C. Se enuncia y se prueba.
5. Con una sola hipótesis es falso: $t=v_2$ con $a_2\nleqq b_2$.