La conexión entre el material condicional y provability es importante, y muy intuitivo una vez que las definiciones básicas se entiende. En una prueba formal asumimos un conjunto de instalaciones y derivar una conclusión en particular. Digamos que el conjunto de premisas $\Gamma$, y la conclusión de $\psi$. Ahora supongamos que queremos demostrar a $\varphi$, pero nuestras instalaciones son demasiado débiles para probarlo por sí mismos. Por lo que, además, asuma $\theta$, y gestionar para derivar $\varphi$. Se representa este simbólicamente diciendo que $\Gamma \cup \left\{\theta\right\} \vdash \varphi$.
Contraste esto con una instrucción condicional, como el siguiente: si $x + y < z$, a continuación, $x < z \wedge y < z$ ( $x,y,z \in \mathbb{N}$ ). Podemos formalizar esta en el predicado de cálculo utilizando el material condicional: $\forall{x}\forall{y}\forall{z} (x + y < z \rightarrow x < z \wedge y < z)$.
La deducción del teorema de los estados que, dada $\Gamma \cup \left\{\theta\right\} \vdash \varphi$, podemos afirmar que nuestra serie inicial de los locales de la $\Gamma$ demuestra la instrucción condicional $\theta \rightarrow \varphi$. Formalmente, $(\Gamma \cup \left\{\theta\right\} \vdash \varphi) \vdash (\Gamma \vdash \theta \rightarrow \varphi)$, sólo ligeramente, la versión más general de la prueba condicional regla de $(p \vdash q) \vdash (\vdash p \rightarrow q)$.
Es importante tener en mente la distinción entre el objeto de lenguaje, que es el idioma en el cual las premisas, la conclusión y la de todos los pasos de la prueba que se indican, y el metalenguaje que nos permite hacer afirmaciones acerca de lo que puede ser demostrado de qué. $\rightarrow$ es un símbolo de que el objeto del lenguaje, que de manera informal corresponde a la si...entonces locución en inglés. $\vdash$ es un símbolo de la metalengua, y corresponde a provability: a partir de estas premisas, esta conclusión puede ser derivado. La importancia de la deducción es el teorema que muestra un camino para nosotros para pasar de las declaraciones de la metalengua a las declaraciones de los objetos de lenguaje.
He aquí una respuesta actualizada a la segunda pregunta, después de haber visto el enlace de la página para más de un segundo. El ejemplo de la prueba es complicada sólo por lo que puede mostrar una cadena de razonamiento con pasos entre la hipótesis inicial y la derivación de $A \vdash A$.
- $A$ (Asunción)
- $A$ (A partir de 1)
- $A \vdash A$ (A partir del 1 y 2)
- $\vdash A \rightarrow A$ (A partir de 3 por CP)
Tan lejos, tan obvia. Y, por supuesto, por la simple inspección de la tabla de verdad para $A \rightarrow A$ podemos ver que es una tautología; esta es la semántica , mientras que la derivación se muestra en la página de la Wikipedia es un sintáctica enfoque.
El problema con la tabla de verdad es que no escala a la lógica de primer orden: ¿qué es la tabla de verdad para $\forall{x} \; P(x)$? Suponiendo que se nos asigna constantes a cada elemento del dominio, se podría plantear algún tipo de análogo de una tabla de verdad, pero si el dominio fuese infinito, a continuación, la tabla de verdad sería infinitamente amplia! Esta es la razón por la semántica de la lógica de primer orden son dadas por el modelo de la teoría, no en tablas de verdad. Sin embargo, la deducción del teorema aún se mantiene en la lógica de primer orden (por cerrado fórmulas).
