La visualización de los Conceptos de la Lógica Matemática

Question

Si usted estuviera obligado a especular ni ofrecer evidencia anecdótica, diría que excelentes profesionales de la lógica matemática coneptually comprender frases como:

$$ \vdash ((P \rightarrow Q) \rightarrow Q) \rightarrow Q $$

...en un nivel intuitivo?

En concreto, tengo curiosidad por si excelentes profesionales se suelen VISUALIZAR tales declaraciones en cualquier tipo de forma, que no implica mentalmente imaginando el literal declaración con su sintaxis como está escrito más arriba. Por ejemplo, son de Venn o Diagramas de Euler normalmente una buena manera de ir sobre las cosas, o que es una mala idea en el largo plazo?

Personalmente, yo sé que con el Análisis de Grupo/Teoría/Topología he tenido éxito en la búsqueda de áspero visualizaciones de casi todos los conceptos involucrados (con el entendimiento de que las imágenes mentales que no son LITERALES representaciones de los conceptos relevantes y, de hecho, a menudo puede ser muy engañoso si uno no es cuidadoso con ellos); sin embargo, con la lógica que me estoy encontrando esta más difícil, ya que los objetos matemáticos en cuestión parecen en muchos aspectos a ser, en gran medida, de forma explícita sintácticos. Lo que esto significa es que el más me rougly convertir declaraciones formales en "intuitiva" de imágenes, más de esas intuitiva imágenes comienzan a asemejarse mucho a una interpretación específica que se interpone en el camino de esas sentencias ser explícitamente sintáctica en la naturaleza.

Como consecuencia de este desastre, me encuentro caer en la confusión de no tener intuiciones sobre si elementales afirmaciones son verdaderas o falsas antes de intentar demostrar que, a diferencia de en otros temas matemáticos.

En definitiva, ¿alguien tiene alguna anecdótica o incluso especulativo consejos acerca de cómo tener éxito en visualizar o NO visualizar) los objetos de la Matemática, la Lógica? ¿Cómo hace uno para ganar un sentido intuitivo de este tema?

Gracias!

Answer 1

Algo que a veces me encuentro útil es considerar lo que se llama el Curry-Howard Isomorfismo: declaraciones de la lógica se corresponden con los tipos de programas de ordenador, y las declaraciones son teoremas si y sólo si el tipo correspondiente, que es el tipo de programa que puede existir realmente.

En esta correspondencia, $A\to B$ representa el tipo de una función en un programa que toma un argumento de tipo $A$ y calcula un valor de tipo $B$.

Una función de tipo de $A\to A$ es obviamente posible, debido a que la función sólo se lleva a la $A$ que lo tengo y se la da a la derecha de nuevo:

 define function f(a) {
   return a;
 }

Y $A\to(B\to A)$ es posible: la función debe tomar un argumento de tipo $A$ y, a continuación, dar la espalda a una función de tipo de $B\to A$. Se puede hacer esto, porque se puede volver a dar una segunda función, que ignora la $B$ que tenemos, y que da la espalda a la $A$ que la primera función llegó a comenzar con:

 define function f(a) {
   define function g(b) {
     return a;
   }
   return g;
 }

Pero en contraste, $A\to B$ es no un teorema, porque ¿cómo se puede escribir una función que recibe un argumento de tipo $A$ y da un resultado de algunos otros, completamente arbitraria tipo? Donde podría obtener un $B$ de si todo lo que tiene es una $A$?

El isomorfismo también se identifica la lógica Y con maridaje: un valor de tipo $A\land B$ es un par que contiene una $A$$B$, y cualquiera de ellos (o ambos) puede ser extraído. Se identifica con la lógica O con lo que se llama un discontinuo de la unión: Un valor de tipo $A\lor B$ es $A$ o $B$, pero no tanto, y el programa puede decir cual de las dos es. De la misma manera hay interpretaciones para la negación, para la constante de valores true y false, y así sucesivamente.

Para un ejemplo más elaborado, un programa que corresponde al teorema $\lnot\lnot(P\lor\lnot P)$, ver esta respuesta.

El único inconveniente es que no todos los clásicamente verdadero teorema corresponde a un programa completamente en una manera sencilla. Algunos teoremas de la lógica, como $((A\to B)\to A)\to A$, (de Peirce de la ley) no corresponden a un programa simple. En lugar corresponden a los programas que el uso de características avanzadas como continuaciones o excepciones.

Sin embargo, es a menudo útil pensar lógico teoremas como las especificaciones de los programas; si puedes pensar en un programa que realiza el cálculo correspondientes, a continuación, la instrucción debe ser un teorema.

Visto de esta manera, la declaración de la que originalmente se le preguntó acerca de, $((P\to Q)\to Q)\to Q$, parece bastante improbable: se necesita una función de $f$ que obtiene un argumento de $x$, la cual es en sí una función de tipo de $(P\to Q)\to Q$, e $f$ necesidades para producir un valor de tipo $Q$. Si $f$ podría llamar a $x$, $x$ devolvería el valor necesario. Pero no puede llamar a $x$ porque para hacerlo se necesita para darle un argumento de tipo $P\to Q$, y no tiene uno.

Answer 2

Creo que parte de lo que hace excelentes profesionales excelentes, es que tienen muchos diferentes intuitiva representaciones de las cosas con las que trabajan, y puede cambiar entre ellos fácilmente de acuerdo a lo que funciona bien en situaciones dadas. Lo importante es no quedarse con una sola visualización y el uso que de todo, pero para estar familiarizado con una amplia gama de posibilidades que puedes probar para ver si uno de ellos es útil para la tarea a mano.

El Curry-Howard isomorfismo (ver MJD respuestas) es excelente para conocer, especialmente si usted ya tiene (funcional) con experiencia en programación. Estrechamente relacionado con éste es el intuitionistic concepción de pruebas de conversación de juegos, una versión informal de la que se utiliza a menudo para explicar la semántica de los cuantificadores para los estudiantes principiantes ("el adversario elige un $\epsilon>0$, y luego tenemos que producir un $\delta>0$ tal que ..."). Esto puede ser extendido para las conectivas proposicionales: Si queremos demostrar a $P\land Q$, el adversario elige si quiere ver nuestra prueba de $P$ o de $Q$, pero para demostrar $P\lor Q$, podemos elegir cual de las pruebas a presentar. Si tenemos que probar que $P\to Q$, el adversario empieza por darnos su prueba de $P$, y luego se debe probar $Q$.

Más específicamente visuales, diagramas de Venn, de hecho pueden ser útiles, pero ser incómodo si hay muchas letras proposicionales. Personalmente creo que a menudo es sorprendentemente útil simplemente para visualizar el árbol de sintaxis abstracta de una fórmula, en lugar de sus lineal por escrito de la sintaxis. Esto se relaciona con el (pero distinto de) la visualización de una fórmula proposicional como un circuito Booleano que contienen puertas y cables.

Incluso algo tan primitivo como las tablas de verdad puede ser útil para algunos propósitos. Por ejemplo, mi mejor intuición acerca de cómo la posible dos variables Booleanas funciones se relacionan entre sí en términos de dos dimensiones de las tablas de verdad: $$ \begin{array}{c|cc} \to & 0 & 1 \\ \hline 0 & 1 & 1 \\ 1 & 0 & 1 \end{array} \quad \begin{array}{c|cc} \land & 0 & 1 \\ \hline 0 & 0 & 0 \\ 1 & 0 & 1 \end{array} \quad \begin{array}{c|cc} \oplus & 0 & 1 \\ \hline 0 & 0 & 1 \\ 1 & 1 & 0 \end{array} \quad \begin{array}{c|cc} \text{a} & 0 & 1 \\ \hline 0 & 0 & 0 \\ 1 & 1 & 1 \end{array} \quad \ldots $$ donde, por ejemplo, "$\to$ " y "$\land$" es similar debido a que sus tablas de verdad ambos tienen una cuña de tres idénticos plazas con un extraño en una de las esquinas. Puedo hacer uno en el otro por mover de un tirón y la inversión, lo cual me dice que una puerta puede convertirse en una IMPLICA la puerta por la adición de los inversores a algunas de las entradas y salidas, y viceversa.