Recientemente me llegó descubierto Metamath.
Supuestamente el idioma es uno de los que un equipo puede la prueba de verificación.
Entonces empecé a mirar a los conceptos que estoy familiarizado con, y decidió buscar la encasillar principio.
En su prueba, en la línea 5 que me llegó a través de un uso de la desigualdad de la que me siento incómodo.
Supuestamente dados dos conjuntos a $A$ y $B$, "$A\neq B$ iff $\lnot A = B$".
En particular, están utilizando esto para el conjunto vacío: no es igual al conjunto vacío si y sólo si a no es igual al conjunto vacío.
Puedo encontrar una contraejemplo a esta declaración.
Deje $U = \{1,2,3,4,5,6\} , A = \{1,3,5\}, B = \{4,6\}$.
Claramente $A\neq\varnothing$, e $A \neq B$.
Sin embargo, $ (\lnot A) \neq \varnothing$, e $ (\lnot A) \neq B $
Hay un caso particular en el que la definición del meta-matemáticas da por la desigualdad definición válida? Otros que Un ser igual al conjunto universal?
Actualización: he añadido el uso de algunos símbolos, y se ha corregido un par de errores que he tomado en el proceso de edición de este post. Daniel ha hecho un excelente entrada que el problema probablemente está en la sintaxis del lenguaje y el uso ambiguo de precedencia.
