¿sistema formal de Semantics(Truth) vs?

Question

mi primera pregunta es ¿se puede definir la semántica de la lógica y de no definir un sistema formal ?

¿por qué necesitamos un sistema formal para demostrar una proposición, por ejemplo, cuando sabemos que la proposición es verdadera ?

e.g. ( A ^ (A->B) ) -> B    if A is true and A->B is true then B is true

y esto también puede ser mostrado por la tabla de verdad. así que ¿por qué utilizamos un sistema formal para mostrar que el argumento es válido cuando podemos utilizar la semántica para mostrar que . (por la construcción de tablas de verdad)

desde las fórmulas y las leyes de la semántica bien definidas, no es posible llegar a cualquier incoherencias (en el sentido de la semántica !)

creo que la contraparte mi pregunta es respondida en el Sistema Formal y Formal de la Lógica del Sistema pero, ¿y los otros?.

mi secound pregunta es: ShyPerson al responder a la pregunta de arriba se mencionó que necesitamos un poco de sentido para nuestras fórmulas proposicionales así, podemos definir la semántica. no se puede simplemente usamos el mismo significado de las conectivas en el lenguaje humano para describir nuestras propuestas . lo que significa que describen las conectivas como el lenguaje de los humanos ?

Answer 1

En la lógica proposicional se puede "mostrar" validez mediante la tabla de verdad.

Tabla de verdad de suministro de un algoritmo para calcular el valor de verdad de cada proposición fórmula;

en particular, las tablas de verdad pueden ser utilizados para determinar si una expresión proposicional es verdadera para todos los valores de entrada, que es, lógicamente válido [también llamado : una tautología].

Para la lógica de primer orden, tenemos no un algoritmo similar.

F-o lógica es indecidible :

a diferencia de la lógica proposicional, lógica de primer orden es indecidible (aunque semidecidable), a condición de que el lenguaje tiene al menos un predicado de arity al menos $2$ (distinto de la igualdad). Esto significa que no hay ningún procedimiento de decisión que determina si arbitraria fórmulas son lógicamente válidos.

Esta es la principal razón por la que necesitamos un cálculo deductivo para la f-o lógica :

porque para mostrar que el argumento es válido cuando nosotros no sólo el uso de la semántica para mostrar que .

Answer 2

Tengo la impresión de que ya es muy común fuera de la lógica de no preocuparte por la formalización de provability, sino sólo sobre la semántica de la verdad. Por ejemplo, cuando estudiamos las declaraciones acerca de los grupos o de los anillos en nuestras clases de álgebra, lo hacemos por considerar arbitraria realización/modelo del concepto de grupo o un anillo dentro de nuestro ambiente de la teoría de conjuntos y demostrar la instrucción para todos ellos. Una vez que logramos con eso, creemos que la declaración es 'demostrado'. Sin embargo, lo que hacemos en realidad es para verificar su semántica de la verdad, y una aplicación de Goedel integridad del teorema sería necesaria para concluir provability - aún así, esto no me ha pasado nunca en mi las clases de pregrado, y en ese momento yo ni siquiera sabía acerca de la definición precisa de primer orden de la lógica, solidez, integridad y así sucesivamente.

Para la fundación de las matemáticas, sin embargo, creo que usted realmente necesita lógica de los cálculos. Considerando clásica de la lógica proposicional, estoy de acuerdo en que usted puede definir una semántica a través de la prueba de las tablas no de la construcción en cualquier otro sistema formal. Sin embargo, al definir la semántica de intuitionistic lógica proposicional o de la lī ogica de primer orden, tendrá que explicar lo que constituye un conjunto, que la operación de conjuntos son permitidos, y así sucesivamente. Mientras que usted podría hacer esto en lenguaje natural en lugar de fórmulas, creo que siempre terminan con algún tipo de lógica y eficaz de cálculo.

Me gustaría decir por lo tanto que para la fundación de las matemáticas, usted no será capaz de eliminar la introducción, ya sea formalmente o en el nivel de lenguaje natural, de una eficaz a prueba de cálculo. Sin embargo, una vez que aclaró su ambiente teoría de conjuntos a través de un cálculo, estoy de acuerdo en que a veces uno puede, y de hecho esto se hace a menudo, ignoran provability y trabajar con la semántica de la verdad.

Dos comentarios finales:

Sobre la computabilidad, usted podría estar interesado en la búsqueda de un (semi-)para el algoritmo de comprobación de la semántica de la verdad. Entonces, sabiendo eficaz, sólido y completo a prueba de cálculo para su teoría le dará un semi-algoritmo de la verdad, y si usted incluso sabe que su teoría es completa (como la teoría de la algebraicamente cerrado campos de algunos característica fija), incluso obtendrá un algoritmo de decisión para la verdad.

Incluso si usted no tiene cuidado acerca de la lógica o de la computabilidad en todo, hay otras aplicaciones de la presencia de los efectivos, el sonido y la evidencia completa de los cálculos, por ejemplo, el Lefschetz principio, o Ax del teorema.

Answer 3

Hay muchas razones. Pero uno de ellos radica en que mediante un sistema formal puede venir como más fácil y más rápido que el sistema semántica. Una tabla de verdad de una proposición con 22 variables pueden hacer ejercicio como que implica mucho más trabajo que una prueba de la misma fórmula que utiliza un sistema formal.

Answer 4

Sintáctica de vista de la Lógica es la que permite el procesamiento mecánico de fórmulas, por ejemplo, la verificación de la prueba o la búsqueda de pruebas. Se describe inferencias con precisión que no deja espacio para la interpretación. Usted acaba de transformar las fórmulas de acuerdo a algunas reglas.

En el otro lado de la estructura es de construcción de un conjunto de objetos que obedece a ciertas reglas por ejemplo, los axiomas descritos por sintáctica parte.

De primer orden de la lógica de esos dos conceptos son equivalentes en el sentido de que si se puede demostrar algo sintácticamente, a continuación, sistemática vinculación a la voluntad de seguir y de la otra manera alrededor. Este es el llamado teorema de completitud.

Por orden superior de la lógica de la integridad teorema no se cumple. Sintáctica es la prueba de sonido, lo que significa que sistemática vinculación es implícita por no toda la verdad acerca de la estructura (semántica) puede ser probado semánticamente.

Answer 5

Esto es más un comentario que una respuesta completa; es simplemente demasiado grande para encajar bien en un comentario. Estoy sobre todo frente a la la pregunta de por qué no usamos las conectivas de lenguaje natural en la lógica. Además, mis oídos estaban quemando. :)

En primer lugar, los idiomas humanos (o de los lenguajes naturales) son muy ambiguas y vagas. Esto hace que sea difícil ponerse de acuerdo sobre de qué estamos hablando.

Luego vienen algunos problemas sintácticos. Considerar el inglés conjunción y. En la lógica, la conjunción es sintácticamente limitado a conjuntan sólo dos bien formado fórmulas. En inglés, puede unirse a la mayoría de las categorías gramaticales. Aquí están algunos ejemplos. Sustantivos: Barbara y Marvin bailó toda la noche de largo. Verbos: Barbara cantó y bailó toda la noche. Adverbios: Barbara cantó muy bien y con precisión. Adjetivos: El rojo y blanco de la bola rodó hacia abajo de la colina. Auxiliares: se puede y se debe hacer esta prueba. Cláusulas: Barbara paseaba el perro y Marvin caminó el gato. Y así sucesivamente. Tengo pocas dudas de que la mayoría de los lenguajes naturales permitir que este así. El problema es: ¿cómo podemos definir la semántica de la conjunción y a través de todas estas categorías?

Podemos esquivar este problema formalmente ya que podemos escribir una diferente interpretación semántica para cada categoría, pero que deja con el problema de que no hemos definido el núcleo de significado de y a través de todas estas categorías. Y también se supone que cada categoría tiene un significado específico. No. Considere la posibilidad de cláusulas. En el ejemplo Barbara paseaba el perro y Marvin caminó el gato, las cláusulas son más o menos independientes, como el proposicional caso. Pero ¿qué hay de esto: Barbara conducía a gran velocidad y ella estacionado y ella salió del coche. Aquí la secuencia es esencial para la semántica: ella no salir del coche mientras ella conducía a alta velocidad. El proposicional caso de no representar todo esto en un ingenuo de representación; es un esfuerzo de captura en más lógicas y parece bastante difícil de construir en la semántica de y por sí mismo.

Ahora, de vuelta a la necesidad de la prueba. Como otros han señalado, a veces es simplemente no es factible comprobar las tablas de verdad. De hecho, es matemáticamente imposible, porque si pudiéramos comprobar las tablas de verdad para todo, todas las matemáticas que se convertiría decidable. Pero no podemos, desde la teoría de los números por sí mismo es indecidible. "Decidable" se traduce, podríamos escribir un programa de ordenador para responder a cada pregunta de interés. Para la prueba, se convierte en la única alternativa para llegar a la verdad matemática.

Finalmente, dado que la matemática es una ciencia, las matemáticas deben, por tanto, proporcionar una explicación científica, básicamente, una historia que nos ayuda a entender, no sólo un revoltijo de bits o números. Probablemente estoy destrozando esta cita maravillosa de Yuri I. Manin, pero es algo como esto: "las Pruebas son entendimientos, nos hacen más sabios".