La lógica Formal de los sistemas, ¿cómo podemos demostrar teoremas acerca de ellos?

Question

Una de las razones para la existencia de la lógica formal de los sistemas es el de establecer los fundamentos de las matemáticas. Para tener todas las teorías construido y probado el uso particular de reglas sintácticas basado en una prueba de la teoría.

Si es así, ¿cómo podemos probar que una lógica formal del sistema cumple cierta propiedad, Solidez, por ejemplo? No podemos usar las reglas de deducción que se definen en nuestra lógica formal del sistema en sí mismo (no hemos establecido su validez aún), así que tenemos que escribir una prueba en "humanos" idioma antes de poder usar el sistema.

¿Cómo puede este sentido? Fundamentos de las matemáticas dependen actualmente de los "humanos" lenguaje informal de las pruebas en su base.

Answer 1

El lenguaje Informal es (de manera informal), que se considera un "atajo" que puede ser, en principio, traducido de la lógica formal. Así que, en teoría, nunca estamos confiando en el lenguaje humano, aunque en la práctica, rara vez realmente escribe una prueba formal (aunque hay proyecto a gran escala para hacer exactamente esto con la ayuda de computadoras).

En el comienzo del siglo 20, algunas personas a pesar de que es importante establecer las matemáticas sobre un fundamento formal; otras personas no estuvieron de acuerdo. Desde el punto de vista de la actuación matemático, fundaciones son necesarias sólo si son de su especialidad. Ocasionalmente entran en juego, y que definitivamente no puede ser ignorada - matemáticas se ha convertido en un juego, pero normalmente se deja en la sombra.

En cualquier caso, el sueño se hizo añicos por Gödel, que demostró que no trivial (en algún sentido exacto) prueba del sistema no puede probar su propia consistencia, y no digamos la consistencia de un sistema más fuerte. Así que para todos los sabemos, la matemática es inconsistente, como suele pensarse. Tendrá que ser tan malo? De verdad que no. Tal vez algunas de las "fundaciones" cosas tendrá que ser revisado, pero $\sin^2\alpha + \cos^2\alpha = 1$ permanecerá cierto, sin embargo.

Cuando la gente demostrar teoremas acerca de los sistemas de prueba, siempre "trabajar" en una prueba fehaciente del sistema, que puede ser adoptada formalmente como un subconjunto de ZFC en la mayoría de los casos (pero no nos preocupa realmente la mayoría del tiempo). Esta es la razón que sólo puede ser incondicional resultados sobre los débiles sistemas de prueba. Mejores resultados son relativos, por ejemplo obligando a todos los argumentos.

Finalmente, una última súplica de mí: por favor, no tome este formales cosas demasiado en serio. Si bien entretenida y fructífera, es sólo una manera de ver las matemáticas. Guarde el pensamiento y reconsiderar en un par de años. (Como un aparte, soy una lógica y teoría de conjuntos de ventilador a mí mismo.)