Ya tenemos una buena cantidad de tipos de estructuras y para cada tipo hemos definido el concepto de fórmula elemental. Ahora definiremos el concepto de prueba elemental asociado a cada tipo de estructura. Obviamente nos inspiraremos en nuestro concepto de prueba elemental de reticulados cuaterna, ya definido y trabajado en la Sección de Reticulados Cuaterna. Primero es importante notar que para hablar del concepto de prueba elemental relativo a un tipo de estructura debemos tener un conjunto de sentencias elementales puras las cuales axiomaticen a tal tipo de estructura. A continuación daremos para cada tipo de estructura un conjunto de axiomas. El lector no tendrá problemas en corroborar que dichos conjuntos de axiomas caracterizan en cada caso al tipo de estructura en cuestión.
Axiomas elementales de posets
adhocprefixadhocsufix \(\forall x(x\leq x)\)
adhocprefixadhocsufix \(\forall x\forall y\forall z((x\leq y\wedge y\leq z)\rightarrow x\leq z)\)
adhocprefixadhocsufix \(\forall x\forall y((x\leq y\wedge y\leq x)\rightarrow x=y)\)
Axiomas elementales de reticulados terna
adhocprefixadhocsufix \(\forall x(x\;\mathsf{s}\;x=x)\)
adhocprefixadhocsufix \(\forall x(x\mathsf{\;i\;}x=x)\)
adhocprefixadhocsufix \(\forall x\forall y(x\mathsf{\;s\;}y=y\;\mathsf{s}\;x)\)
adhocprefixadhocsufix \(\forall x\forall y(x\mathsf{\;i\;}y=y\mathsf{\;i\;}x)\)
adhocprefixadhocsufix \(\forall x\forall y\forall z((x\mathsf{\;s\;}y)\;\mathsf{s}\;z=x\;\mathsf{s}\;(y\;\mathsf{s}\;z))\)
adhocprefixadhocsufix \(\forall x\forall y\forall z((x\mathsf{\;i\;}y)\mathsf{\;i\;}z=x\mathsf{\;i\;}(y\mathsf{\;i\;}z))\)
adhocprefixadhocsufix \(\forall x\forall y(x\;\mathsf{s}\;(x\mathsf{\;i\;}y)=x)\)
adhocprefixadhocsufix \(\forall x\forall y(x\mathsf{\;i\;}(x\;\mathsf{s}\;y)=x)\)
Axiomas elementales de reticulados ternaAxiomas elementales de reticulados acotados
adhocprefixadhocsufix \(\forall x(x\;\mathsf{s}\;x=x)\)
adhocprefixadhocsufix \(\forall x(x\mathsf{\;i\;}x=x)\)
adhocprefixadhocsufix \(\forall x\forall y(x\mathsf{\;s\;}y=y\;\mathsf{s}\;x)\)
adhocprefixadhocsufix \(\forall x\forall y(x\mathsf{\;i\;}y=y\mathsf{\;i\;}x)\)
adhocprefixadhocsufix \(\forall x\forall y\forall z((x\mathsf{\;s\;}y)\;\mathsf{s}\;z=x\;\mathsf{s}\;(y\;\mathsf{s}\;z))\)
adhocprefixadhocsufix \(\forall x\forall y\forall z((x\mathsf{\;i\;}y)\mathsf{\;i\;}z=x\mathsf{\;i\;}(y\mathsf{\;i\;}z))\)
adhocprefixadhocsufix \(\forall x\forall y(x\;\mathsf{s}\;(x\mathsf{\;i\;}y)=x)\)
adhocprefixadhocsufix \(\forall x\forall y(x\mathsf{\;i\;}(x\;\mathsf{s}\;y)=x)\)
adhocprefixadhocsufix \(\forall x(0\mathsf{\;s\;}x=x)\)
adhocprefixadhocsufix \(\forall x(x\mathsf{\;s\;}1=1)\)
Axiomas elementales de reticulados complementados
adhocprefixadhocsufix \(\forall x(x\;\mathsf{s}\;x=x)\)
adhocprefixadhocsufix \(\forall x(x\mathsf{\;i\;}x=x)\)
adhocprefixadhocsufix \(\forall x\forall y(x\mathsf{\;s\;}y=y\;\mathsf{s}\;x)\)
adhocprefixadhocsufix \(\forall x\forall y(x\mathsf{\;i\;}y=y\mathsf{\;i\;}x)\)
adhocprefixadhocsufix \(\forall x\forall y\forall z((x\mathsf{\;s\;}y)\;\mathsf{s}\;z=x\;\mathsf{s}\;(y\;\mathsf{s}\;z))\)
adhocprefixadhocsufix \(\forall x\forall y\forall z((x\mathsf{\;i\;}y)\mathsf{\;i\;}z=x\mathsf{\;i\;}(y\mathsf{\;i\;}z))\)
adhocprefixadhocsufix \(\forall x\forall y(x\;\mathsf{s}\;(x\mathsf{\;i\;}y)=x)\)
adhocprefixadhocsufix \(\forall x\forall y(x\mathsf{\;i\;}(x\;\mathsf{s}\;y)=x)\)
adhocprefixadhocsufix \(\forall x(0\mathsf{\;s\;}x=x)\)
adhocprefixadhocsufix \(\forall x(x\mathsf{\;s\;}1=1)\)
adhocprefixadhocsufix \(\forall x(x\mathsf{\;s\;}c(x)=1)\)
adhocprefixadhocsufix \(\forall x(x\mathsf{\;i\;}c(x)=0)\)
Axiomas elementales de reticulados cuaterna
adhocprefixadhocsufix \(\mathrm{A}_{\leq R}=\forall x(x\leq x)\)
adhocprefixadhocsufix \(\mathrm{A}_{\leq T}=\forall x\forall y\forall z((x\leq y\wedge y\leq z)\rightarrow x\leq z)\)
adhocprefixadhocsufix \(\mathrm{A}_{\leq A}=\forall x\forall y((x\leq y\wedge y\leq x)\rightarrow x=y)\)
adhocprefixadhocsufix \(\mathrm{A}_{\mathsf{s}esC}=\forall x\forall y(x\leq x\;\mathsf{s}\;y\wedge y\leq x\;\mathsf{s}\;y)\)
adhocprefixadhocsufix \(\mathrm{A}_{\mathsf{s}\leq C}=\forall x\forall y\forall z((x\leq z\wedge y\leq z)\rightarrow x\;\mathsf{s}\;y\leq z)\)
adhocprefixadhocsufix \(\mathrm{A}_{\mathsf{i}esC}=\forall x\forall y(x\;\mathsf{i}\;y\leq x\wedge x\;\mathsf{i}\;y\leq y)\)
adhocprefixadhocsufix \(\mathrm{A}_{\mathsf{i}\geq C}=\forall x\forall y\forall z((z\leq x\wedge z\leq y)\rightarrow z\leq x\;\mathsf{i}\;y)\)
Axiomas elementales de grafos
adhocprefixadhocsufix \(\forall x\neg r(x,x)\)
adhocprefixadhocsufix \(\forall x\forall y(r(x,y)\rightarrow r(y,x))\)
Axiomas elementales de grafos bicoloreados
adhocprefixadhocsufix \(\forall x\neg r(x,x)\)
adhocprefixadhocsufix \(\forall x\forall y(r(x,y)\rightarrow r(y,x))\)
adhocprefixadhocsufix \(\forall x\forall y(r(x,y)\rightarrow((R(x)\wedge\lnot R(y))\vee(\lnot R(x)\wedge R(y))))\)
Axiomas elementales de median algebras
adhocprefixadhocsufix \(\forall x\forall y\forall z(M(x,y,z)=M(x,z,y))\)
adhocprefixadhocsufix \(\forall x\forall y\forall z(M(x,y,z)=M(y,z,x))\)
adhocprefixadhocsufix \(\forall x\forall y(M(x,x,y)=x)\)
adhocprefixadhocsufix \(\forall x\forall y\forall z\forall u\forall v(M(M(x,y,z),u,v))=M(x,M(y,u,v),M(z,u,v)))\)
Ahora que tenemos para cada tipo de estructura sus axiomas elementales podemos describir el concepto de prueba elemental, relativo a un tipo de estructura. Las pruebas elementales deberán poseer las siguientes características:
adhocprefix(1)adhocsufix El enunciado a probar debe ser una sentencia elemental pura del tipo de estructura en cuestión.
adhocprefix(2)adhocsufix En la prueba se parte de una estructura del tipo en cuestión, fija pero arbitraria en el sentido que lo único que sabemos es que ella satisface los axiomas elementales correspondientes (o sea esta es la única información particular que podemos usar).
adhocprefix(3)adhocsufix Las deducciones en la prueba son muy simples y obvias de justificar con mínimas frases en castellano.
adhocprefix(4)adhocsufix En la escritura de la prueba lo concerniente a la matemática misma se expresa usando solo sentencias elementales del tipo de estructura en cuestión
Dado que en una prueba se parte de una estructura fija de la que solo se asume que satisface los axiomas elementales y dado que las deducciones en una prueba elemental son muy simples y obvias de justificar, la sentencia elemental pura probada debe ser verdadera en todas las estructuras del tipo en cuestión.
A continuación damos ejemplos para cada uno de los tipos de estructuras analizados previamente.
Sea \[\mu=\forall x\forall y\left((\forall z\ z\leq x\wedge\forall z\ z\leq y)\rightarrow x=y\right)\] Nótese que \(\mu\) es una sentencia elemental pura de posets la cual se cumple en todos los posets ya que ella expresa que si en un poset \(x\) e \(y\) son elementos máximos, entonces \(x=y\). Veamos una prueba elemental de posets de \(\mu\). Notar que, tal como lo aclara el ítem (2) arriba, debemos partir de un poset \((P,\leq)\), fijo pero arbitrario y solo usar la información que nos brindan los axiomas.
Proof. Sean \(a,b\in P\) fijos pero arbitrarios. Supongamos \[(\forall z\ z\leq a\wedge\forall z\ z\leq b)\] En particular \(\forall z\ z\leq b\) nos dice que \(a\leq b\) y \(\forall z\ z\leq a\) nos dice que \(b\leq a\), por lo cual tenemos que \[a\leq b\wedge b\leq a\] Pero el axioma \[\forall x\forall y((x\leq y\wedge y\leq x)\rightarrow x=y)\] nos dice que \[(a\leq b\wedge b\leq a)\rightarrow a=b\] obteniendo de esta forma que \(a=b\). O sea que hemos probado que \[(\forall z\ z\leq a\wedge\forall z\ z\leq b)\rightarrow a=b\] Como \(a\) y \(b\) eran elementos fijos pero arbitrarios, obtenemos que vale \(\mu\).
adhocprefixEjercicio:adhocsufix De pruebas elementales de posets de las siguientes sentencias
adhocprefix-adhocsufix \((\exists x\exists y\ \lnot(x=y)\rightarrow\exists x\exists y\ \lnot(x\leq y))\)
adhocprefix-adhocsufix \(\forall x\forall y\forall z\ ((x\leq y\wedge y\leq z\wedge x=z)\rightarrow x=y)\)
adhocprefix-adhocsufix \((\forall x\exists y(\lnot(x=y)\wedge x\leq y)\rightarrow\exists x\exists y\exists z(\lnot(x=y)\wedge\lnot(x=z)\wedge\lnot(y=z)))\)
A continuación daremos una prueba elemental de reticulados terna de la sentencia \[\eta=\forall x\forall y(x\;\mathsf{s}\;y=y\rightarrow x\;\mathsf{i}\;y=x)\] Notar que, tal como lo aclara el ítem (2) de la descripción de prueba elemental, debemos partir de un reticulado terna \((L,\mathsf{s},\mathsf{i})\), fijo pero arbitrario y solo usar la información que nos brindan los axiomas.
Proof. Sean \(a,b\in L\) fijos pero arbitrarios. Supongamos \[(a\;\mathsf{s}\;b=b)\] El axioma \[\forall x\forall y(x\mathsf{\;i\;}(x\;\mathsf{s}\;y)=x)\] nos dice que \[a\mathsf{\;i\;}(a\;\mathsf{s}\;b)=a\] O sea que reemplazando en esta igualdad \(a\;\mathsf{s}\;b\) por \(b\) obtenemos: \[a\mathsf{\;i\;}b=a\] Ya que habíamos supuesto que \(a\;\mathsf{s}\;b=b\) hemos probado en realidad que \[a\;\mathsf{s}\;b=b\rightarrow a\mathsf{\;i\;}b=a\] Como \(a\) y \(b\) eran elementos fijos pero arbitrarios, obtenemos que vale \(\forall x\forall y(x\;\mathsf{s}\;y=y\rightarrow x\;\mathsf{i}\;y=x)\).
Nótese que las sentencias elementales de reticulados terna son sentencias elementales de reticulados cuaterna también. Sin embargo la prueba elemental de reticulados terna de arriba no es una prueba elemental de reticulados cuaterna (por que?).
Recordemos que \[\begin{aligned} Dis_{1} & =\forall x\forall y\forall z(x\mathsf{\;i\;}(y\;\mathsf{s}\;z)=(x\mathsf{\;i\;}y)\;\mathsf{s}\;(x\mathsf{\;i\;}z))\\ Dis_{2} & =\forall x\forall y\forall z(x\;\mathsf{s}\;(y\mathsf{\;i\;}z)=(x\mathsf{\;s\;}y)\mathsf{\;i\;}(x\;\mathsf{s}\;z)) \end{aligned}\] El lector no tendrá problema para obtener de la prueba del Lema 5.24 las ideas para hacer una prueba elemental de reticulados terna de la sentencia elemental \((Dis_{1}\rightarrow Dis_{2})\).
Encontrar pruebas elementales de reticulados terna tiene cierta dificultad ya que solo podemos usar los axiomas de reticulados terna y además no podemos escribir el símbolo \(\leq\). Podemos escribir \(t\;\mathsf{s}\;s=s\) en lugar de \(t\leq s\) y de esta manera simular en nuestras fórmulas elementales de reticulados terna al símbolo \(\leq\). De todas maneras el escollo que tendremos es que de los axiomas de reticulados terna no es obvio que las operaciones \(\mathsf{s}\) e \(\mathsf{i}\) sean supremo e ínfimo respecto del orden dado por la ecuación \(x\;\mathsf{s}\;y=y\). Esto puede ser resuelto si nos inspiramos en la prueba del Teorema de Dedekind que prueba justamente eso usando solo los axiomas elementales de los reticulados terna. Es decir, la prueba de dicho teorema parte de un reticulado terna fijo pero arbitrario y luego usando solo esta información prueba que la relación dada por “\(x\;\mathsf{s}\;y=y\)” es un orden parcial respecto del cual las operaciones \(\mathsf{s}\) e \(\mathsf{i}\) son supremo e ínfimo. Podríamos usar las ideas de dicha demostración para dar pruebas elementales de reticulados terna de las siguientes sentencias \[\begin{aligned} & \forall x\forall y((x\mathsf{\;s\;}y=y\wedge y\mathsf{\;s\;}x=x)\rightarrow x=y)\\ & \forall x\forall y\forall z((x\mathsf{\;s\;}y=y\wedge y\mathsf{\;s\;}z=z)\rightarrow x\;\mathsf{s}\;z=z) \end{aligned}\] las cuales esencialmente dicen que la relación dada por “\(x\;\mathsf{s}\;y=y\)” es antisimétrica y transitiva. También podríamos extraer de dicha prueba las ideas para probar las sentencias elementales \[\begin{aligned} & \forall x\forall y(x\mathsf{\;s\;}(x\;\mathsf{s}\;y)=x\;\mathsf{s}\;y\wedge y\;\mathsf{s}\;(x\;\mathsf{s}\;y)=x\;\mathsf{s}\;y)\\ & \forall x\forall y\forall z((x\mathsf{\;s\;}z=z\wedge y\mathsf{\;s\;}z=z)\rightarrow(x\mathsf{\;s\;}y)\mathsf{\;s\;}z=z) \end{aligned}\] las cuales se corresponden con los axiomas \(\mathrm{A}_{\mathsf{s}esC}\) y \(\mathrm{A}_{\mathsf{s}\leq C}\) vía “escribir \(t\;\mathsf{s}\;s=s\) en lugar de \(t\leq s\)”. Dejamos esto como ejercicio opcional.
También tenemos el problema de no poder escribir el símbolo \(\leq\) en las pruebas elementales de reticulados acotados y también el escollo de que los axiomas no hacen referencia obvia a que las operaciones \(\mathsf{s}\) e \(\mathsf{i}\) sean operaciones supremo e ínfimo respecto del orden dado por la ecuación \(x\;\mathsf{s}\;y=y\). Por supuesto que podemos hacer el truco hecho para los reticulados terna y ganar poder expresivo. Notar que toda prueba elemental de reticulados terna es también una prueba elemental de reticulados acotados, por lo cual tenemos pruebas elementales de reticulados acotados de las sentencias \[\begin{aligned} \forall x\forall y(x\;\mathsf{s}\;y & =y\rightarrow x\;\mathsf{i}\;y=x)\\ (Dis_{1} & \rightarrow Dis_{2}) \end{aligned}\] Veamos una prueba elemental de reticulados acotados de la sentencia \(\forall x(x\mathsf{\;i\;}1=x)\). Notar que, tal como lo aclara el ítem (2) de la descripción de prueba elemental, debemos partir de un reticulado acotado \((L,\mathsf{s},\mathsf{i},0,1)\), fijo pero arbitrario y solo usar la información que nos brindan los axiomas de reticulados acotados.
Proof. Sea \(a\in L\) fijo pero arbitrario. El axioma \[\forall x(x\mathsf{\;s\;}1=1)\] nos dice que \[a\mathsf{\;s\;}1=1\] Ya que \[\forall x\forall y(x\;\mathsf{s}\;y=y\rightarrow x\;\mathsf{i}\;y=x)\] (teorema ya probado) tenemos que \[a\;\mathsf{s}\;1=1\rightarrow a\;\mathsf{i}\;1=a\] O sea que \[a\;\mathsf{i}\;1=a\] Ya que \(a\) era arbitrario, hemos probado que \[\forall x(x\;\mathsf{i}\;1=x)\]
Por supuesto la anterior no es una prueba elemental estrictamente hablando porque en una parte introduce la sentencia \(\forall x\forall y(x\;\mathsf{s}\;y=y\rightarrow x\;\mathsf{i}\;y=x)\) y lo justifica diciendo “teorema ya probado” lo cual no es una justificación simple y obvia (de hecho dicho teorema podría ser muy difícil de probar). Obviamente esto se soluciona de manera muy simple: agregamos antes de la sentencia \(\forall x\forall y(x\;\mathsf{s}\;y=y\rightarrow x\;\mathsf{i}\;y=x)\) la prueba elemental que ya hicimos de ella. Dejamos al lector que inspirándose en el Lema 5.25 de una prueba elemental de reticulados acotados de la sentencia elemental pura: \[Dis_{1}\rightarrow\forall x\forall u\forall v((x\mathsf{\;s\;}u=1\wedge x\mathsf{\;i\;}u=0\wedge x\mathsf{\;s\;}v=1\wedge x\mathsf{\;i\;}v=0)\rightarrow u=v)\]
También tenemos el problema de no poder escribir el símbolo \(\leq\) en las pruebas elementales de reticulados acotados y también el escollo de que los axiomas no hacen referencia obvia a que las operaciones \(\mathsf{s}\) e \(\mathsf{i}\) sean operaciones supremo e ínfimo respecto del orden dado por la ecuación \(x\;\mathsf{s}\;y=y\). Por supuesto que podemos hacer el truco hecho para los reticulados terna y ganar poder expresivo. Notar que toda prueba elemental de reticulados terna o de reticulados acotados es también una prueba elemental de reticulados complementados, por lo cual tenemos ya varias pruebas elementales de este tipo de estructuras.
Dejamos al lector que inspirándose en los resultados probados en la Sección de Reticulados Complementados de pruebas elementales de reticulados complementados de las siguientes sentencias elementales puras:
adhocprefix-adhocsufix \(Dis_{1}\rightarrow\forall x\forall u((x\mathsf{\;s\;}u=1\wedge x\mathsf{\;i\;}u=0)\rightarrow u=c(x))\)
adhocprefix-adhocsufix \(Dis_{1}\rightarrow\forall x(c(c(x))=x)\)
adhocprefix-adhocsufix \(Dis_{1}\rightarrow\forall x\forall y(c(x\mathsf{\;i\;}y)=c(x)\mathsf{\;s\;}c(y))\)
adhocprefix-adhocsufix \(Dis_{1}\rightarrow\forall x\forall y(c(x\mathsf{\;s\;}y)=c(x)\mathsf{\;i\;}c(y))\)
adhocprefix-adhocsufix \(Dis_{1}\rightarrow\forall x\forall y(x\mathsf{\;i\;}y=0\leftrightarrow y\mathsf{\;s\;}c(x)=c(x))\)
adhocprefix-adhocsufix \(Dis_{1}\rightarrow\forall x\forall y(x\mathsf{\;s\;}y=y\leftrightarrow c(y)\mathsf{\;s\;}c(x)=c(x))\)
Es difícil encontrar pruebas elementales de grafos que no sean complicadas. Aceptando cierto grado de complejidad hay muchas. Un dato interesante es que el conjunto de sentencias elementales de grafos que tienen una prueba elemental es no recursivo, es decir no hay un procedimiento efectivo que decida si una sentencia elemental de grafos dada tiene una prueba elemental. Esto habla acerca de cuan complicada puede ser la estructura o fisonomía de las sentencias elementales de grafos que pueden ser probadas elementalmente. Otro problema para hacer pruebas elementales de grafos es que en general son tediosas ya que suelen involucrar el análisis de muchos casos. De todas maneras muchas veces aunque la prueba sea tediosa por la cantidad de casos, la idea de la sentencia a probar es bastante geométrica y simple. Veamos un ejemplo. Supongamos que tenemos dos sucesiones \(x_{1},x_{2},...,x_{n}\) y \(y_{1},y_{2},...,y_{n}\) de vértices de un grafo \((G,r)\), con \(n\geq3\) tales que
adhocprefix-adhocsufix \(x_{i}\text{ es distinto de }x_{j}\), siempre que \(i\text{ sea distinto de }j\)
adhocprefix-adhocsufix \(y_{i}\text{ es distinto de }y_{j}\), siempre que \(i\text{ sea distinto de }j\)
adhocprefix-adhocsufix \((x_{i},x_{i+1}),(y_{i},y_{i+1})\in r\), para \(i=1,...,n-1\)
adhocprefix-adhocsufix \(x_{1}=y_{1}\) y \(x_{n}=y_{n}\)
adhocprefix-adhocsufix \(x_{i}\text{ es distinto de }y_{i}\), para algún \(i\in\{2,...,n-1\}\)
Entonces haciendo un dibujo uno rápidamente se convence que en \((G,r)\) debe haber un \(k\)-ciclo, con \(k\) tal que \(2n-2\geq k\geq4\). Por supuesto esta verdad acerca de los grafos todavía no esta escrita en forma de sentencia elemental y si quisiéramos hacerlo nos toparíamos con el problema que \(n\) es variable en el enunciado de dicho resultado. Sin embargo para el caso de un \(n\) concreto, digamos \(n=10\), con un poco de trabajo, podemos hacer una sentencia elemental que simule el enunciado anterior. Y con bastante mas trabajo podríamos hacer una prueba elemental de grafos que pruebe dicha sentencia elemental.
También es difícil encontrar pruebas elementales de median algebras que no sean complicadas. Veamos una prueba elemental de median algebras de la sentencia \(\forall x\forall y(M(x,y,y)=y)\). Notar que, tal como lo aclara el ítem (2) de la descripción de prueba elemental, debemos partir de una median algebra \((A,M)\), fija pero arbitraria y solo usar la información que nos brindan los axiomas de median algebras.
Proof. Sean \(a,b\in A\) fijos pero arbitrarios. Por el axioma \(\forall x\forall y\forall z(M(x,y,z)=M(y,z,x))\) tenemos que \[M(a,b,b)=M(b,b,a)\] Por el axioma \(\forall x\forall y(M(x,x,y)=x)\) tenemos que \[M(b,b,a)=b\] O sea que \[M(a,b,b)=b\] Ya que \(a,b\) eran arbitrarios, hemos probado que \(\forall x\forall y(M(x,y,y)=y)\).
Veamos una prueba elemental de grafos bicoloreados de la sentencia \(\forall x\forall y((r(x,y)\wedge R(x))\rightarrow\lnot R(y))\).
Proof. Sean \(a,b\in G\) fijos pero arbitrarios. Supongamos \(r(a,b)\wedge R(a)\). En particular tenemos que se da \(r(a,b)\). Por el axioma \(\forall x\forall y(r(x,y)\rightarrow((R(x)\wedge\lnot R(y))\vee(\lnot R(x)\wedge R(y))))\) tenemos que \(r(a,b)\rightarrow((R(a)\wedge\lnot R(b))\vee(\lnot R(a)\wedge R(b)))\), por lo cual tenemos que \(((R(a)\wedge\lnot R(b))\vee(\lnot R(a)\wedge R(b)))\). Pero ya que se da \(R(a)\), tenemos que no puede darse \((\lnot R(a)\wedge R(b))\), por lo cual obtenemos que se da \((R(a)\wedge\lnot R(b))\). Esto en particular nos dice que se da \(\lnot R(b)\). O sea que hemos probado que \((r(a,b)\wedge R(a))\rightarrow\lnot R(b)\). Ya que \(a\) y \(b\) eran arbitrarios tenemos que vale \(\forall x\forall y((r(x,y)\wedge R(x))\rightarrow\lnot R(y))\).