Mikhail Katz y Mauro ALLEGRANZA ya dio respuestas para el contexto histórico, pero voy a tratar de dar una respuesta centrándose en la intuición.
¿Por qué la visualización de las pruebas puramente sintáctica ayuda con el rigor matemático? Ejemplos?
Para ser riguroso necesitamos seguir un conjunto de reglas sin objeción (con el fin de crear un consenso entre las personas) y sintácticos objetos proporcionan una forma adecuada de objetividad (como pura sintaxis es imparcial, no "participan").
Sin consenso en la elección de un lenguaje formal/sintaxis cómo puede uno puede convencer a alguien acerca de algo ?
¿Por qué la gente quiere una lógica independiente del lenguaje de los modelos que representa?
Creo que la gente no quería eso. Esa elección fue influenciado principalmente por Frege ideas filosóficas. En los primeros días de la moderna Lógica queríamos para el estudio de la lógica como un objeto de modo que acabamos de poner en la forma de un objeto formal.
Cuando hacemos un estudio de la lógica como un objeto a veces hacemos uso de la lógica en sí misma para demostrar propiedades sobre ella. Ya no tiene sentido que hemos dividido el mundo en dos partes :
- el objeto (lenguaje de la lógica como un objeto con un lenguaje formal)
- la meta de la lengua (sobre el objeto de idioma, nuestra intuición acerca de la lógica, lo que uso para probar cosas acerca de la lógica formal, algo que no es necesario explicar).
La sintaxis de la vida en el objeto, el lenguaje y la semántica (dando un significado a la sintaxis) vive en el "meta-nivel". Proporcionar un conjunto de reglas lógicas, a menudo se desea probar la Solidez y la Integridad para asegurar que la sintaxis de la siguiente manera semántica que representa nuestra intuición (y prejuicios) de la lógica.
Esa distinción no es algo que quería a propósito. Hicimos esto porque de nuestras creencias y de gestión (sig)de la concepción de la lógica.
¿Por qué el sistema axiomático de conseguir más y más de relieve en la historia de la
desarrollo matemático?
No sé mucho sobre el sistema axiomático, pero una gran cantidad de problemas que se plantea a partir de ella porque ya no podemos saber si algo que no podía probar que debe ser tomado como un axioma y no sabíamos a qué axioma a elegir : el estado de los axiomas no estaban claras.
En el comienzo del siglo 20, Poincaré sugiere que no se vea axiomas como "hechos evidentes", pero como "definiciones", una bastante satisfactoria respuesta.
Un montón de teoría matemática ahora se fundó en el sistema axiomático en un productivas y satisfactorias.
Por último, señalar que la distinción entre sintaxis y la semántica no es necesario.
Intuitionistic lógica de proporcionar una interpretación de la lógica de las pruebas en el plazo de construcciones/programas a través de la de Curry-Howard isomorfismo. Por ejemplo, la implicación $A \rightarrow B$ no es interpretado de una semántica mundo, pero visto como un programa funcional de la producción de una prueba de $B$ a partir de una prueba de $A$.
Trabajos recientes sobre la Lógica Lineal, Ludics, la Geometría de la Interacción dar una interpretación de la lógica a través de la idea de "interacción" con el corte de la regla de procedimiento de eliminación como el núcleo. Estas obras están libres de cualquier externa explicaciones y tratar de encontrar el significado de reglas lógicas en las propias reglas.
