Podemos tener diferentes "sabores" en el set-up de Primer Orden Predicado Cálculo de Hilbert-estilo :
1) el uso de modus ponens como única regla de inferencia (por supuesto, con adecuado axiomas);
de esta manera tenemos un "proposicional" Teorema de la Deducción, sin restricciones respecto a variables libres en el supuesto de ser dado de alta: ver Herbert Enderton, Matemáticas, Introducción a la Lógica (2ª ed Harcourt - 2001).
Alternativamente :
2) utilizar también la generalización de la regla;
de esta manera tenemos las restricciones habituales en el Teorema de la Deducción para el Cálculo de Predicado, con el fin de evitar las falacias [para evitar que $\vdash P(x) \rightarrow \forall x P(x)$] : véase Elliott Mendelson, Introducción a la Lógica Matemática (4ª ed - 1997).
Podemos tener también dos enfoques para la definición de la semántica básica de la relación :
$\vDash_{\mathfrak{A}} \varphi$, es decir, " $\varphi$ es verdadero en $\mathfrak{A}$".
a) Enderton (página 83) estados como :
deje $\varphi$ ser una fórmula de nuestro idioma,
$\mathfrak{A}$ estructura de la lengua,
deje $s : V \rightarrow |\mathfrak{A}|$ una función de un conjunto de $V$ de todas las variables [de la lengua] en el universo,$|\mathfrak{A}|$$\mathfrak{A}$.
A continuación, vamos a definir lo que significa para $\mathfrak{A}$ a satisfacer $\varphi$ con $s$:
$\vDash_{\mathfrak{A}} \varphi[s]$.
Como se puede ver, $\varphi$ es una fórmula; no hay ninguna restricción en tener variables libres en ella. A continuación, vamos a tener el "caso especial" de las sentencias, es decir, cerrado fórmulas [página 87] :
una pena $\sigma$, (a) $\mathfrak{A}$ satisface $\sigma$ con cada función $s$ $V$ a $|\mathfrak{A}|$, o (b) $\mathfrak{A}$ no satisface $\sigma$ con cualquier función. Si la alternativa (a) se mantiene, entonces decimos que $\sigma$ es verdadero en $\mathfrak{A}$ (escrito $\vDash_{\mathfrak{A}} \sigma$) o $\mathfrak{A}$ es un modelo de $\sigma$.
b) Dirk van Dalen en la Lógica y Estructura (5ª ed - 2013), página 64, "da sentido" a las frases.
La cláusula fundamental es :
$| \forall x \varphi|_{\mathfrak{A}} := min \{ |\varphi [a/x]_\mathfrak{A} | : a \in |\mathfrak{A}| \}$.
Luego, en la página 66 :
Por ahora sólo hemos definido la verdad de las frases de [el lenguaje] $L$. Con el fin de extender $\vDash$ arbitraria de las fórmulas se introduce una nueva notación.
Deje $FV(\varphi) = \{z_1, . . . , z_k \}$, $Cl(\varphi) := \forall z_1 . . . \forall z_k \varphi$ es el universal el cierre de $\varphi$.
Decimos que :
$\vDash_{\mathfrak{A}} \varphi$ fib $\vDash_{\mathfrak{A}} Cl(\varphi)$.
De esta manera, la semántica para abrir fórmulas es un "derivado".
La siguiente opción es acerca de consecuencia lógica: se puede definir sólo por frases (van Dalen, página 67 : semántica de consecuencia), o de fórmulas en general (Eenderton, página 88, y Mendelson, página 65 : implica lógicamente).
Pero el anterior "ingredientes" se mezclan.
Básicamente, cuando definimos un sistema a prueba, que queremos, que es el sonido y completa. En el "más general", esperamos que :
$\Gamma \vdash \varphi$ fib $\Gamma \vDash \varphi$.
Acerca de soundenss: no hay problema, esta es la tarea fácil, mientras que con respecto a la integridad, podemos tener un poco de "imperfección".
Por ejemplo, en Mendelson prueba de sistema tenemos la generalización y la (estándar) definición de derivación nos permite tener :
$P(x) \vdash \forall x P(x)$.
Por supuesto, M del sistema a prueba de sonido; debido a las restricciones en el Teorema de la Deducción, no podemos derivar la (inválidas) : $\vdash P(x) \rightarrow \forall x P(x)$.
Pero, de acuerdo a M semántica, tenemos : $P(x) \nvDash \forall x P(x)$.
Por qué ? Porque la semántica nos da : $B$ implica lógicamente $A$ fib $B \rightarrow A$ es válido, y sabemos que $P(x) \rightarrow \forall x P(x)$ es no válido !
En conclusión, Mendelson no está autorizado a afirmar que, en general :
si $\Gamma \vdash \varphi$, $\Gamma \vDash \varphi$
y él no estado en el que se ...
Comentario
Con respecto a :
Si $\varphi$ falla en $\mathbf M$ (es decir, no $\mathbf M \vDash \varphi$], luego escribimos $\mathbf M \nvDash \varphi$, lo que equivale a $\mathbf M \vDash \lnot \varphi$ (esto es debido a que para cualquier $\mathcal L$-fórmula $\varphi$ le tienen o $\mathbf M \vDash \varphi$ o $\mathbf M \vDash \lnot \varphi$)
es sin duda la frase en lugar de la fórmula.
Considere de nuevo el "basic" semántica de la cláusula :
A continuación, una $\mathcal L$estructura $\mathfrak A$ es un modelo de $\varphi$ si para cada asignación de $s$ $\mathfrak A$ tenemos $(\mathfrak A,s) \models \varphi$, es decir, $\varphi$ retenciones en la $\mathcal L$-interpretación $(\mathfrak A,s)$.
Veamos ahora la estructura de $\mathfrak A = (\mathbb N, 0, <)$ y la fórmula $\varphi$ :
$0 < x$.
Claramente, con el encargo $s : Var \mapsto \mathbb N$ tal que $s(x)=0$ tenemos que :
$(\mathfrak A,s) \nvDash \varphi$;
por lo tanto, no es cierto que para cada asignación de s en $\mathfrak A$, $\varphi$ sostiene que en el $\mathcal L$-interpretación $(\mathfrak A,s)$. Por lo tanto, no es cierto que $\mathfrak A$ es un modelo de $\varphi$ (es decir, que $\mathfrak A \vDash \varphi$).
Considere ahora su negación : $\lnot \varphi$, la cual es :
$\lnot (0 < x)$, es decir,$0 \ge x$.
Con el encargo $s^* : Var \mapsto \mathbb N$ tal que $s^*(x)=1$ tenemos :
$(\mathfrak A,s^*) \nvDash \lnot \varphi$.
De nuevo, no es cierto que $\mathfrak A \vDash \lnot \varphi$.
