Semántica de Kripke y Joyal
Ahora que ya tenemos una interpretación para todos los símbolos de un lenguaje de primer orden podemos presentar la semántica. En lógica, se hace esto con la definición de verdad de Tarski. El objetivo de esta sección es dar algo similar. Como no estamos un lugar con lógica clásica, entonces nuestra definición de verdad cumplirá cosas diferentes a la descrita por Tarski en lógica clásica. En nuestro caso obtendremos que la satisfacción se comporta de la misma manera que la relación de forzar en teoría de conjuntos, de donde tomaremos la notación, que a su vez se comporta como la semántica para la lógica modal propuesta por Kripke.
Así como una flecha \(1\to A\) se puede interpretar como un elemento del objeto \(A\), una flecha \(U\to A\) también es otro tipo de elemento de \(A\). Como si en el objeto \(A\) no sólo hubiera puntos, sino también figuras. Para hacer distinción entre los tipos de “elementos” de un objeto \(A\), los que tienen dominio \(1\) serán llamados elementos globales y los de dominio arbitrario, elementos generalizados. Como en esta sección casi todos los elementos que usaremos son generalizados, entonces a estos últimos sólo los llamaremos elementos.
Sean \(a\colon U\to X\) un elemento y \(\varphi(x)\colon X\to\Omega\) una fórmula. Para decir cuándo \(a\) satisface \(\varphi(x)\) lo haremos por medio del subobjeto \(\{x\mid\varphi(x)\}\), es decir, diremos cuando \(a\) es elemento de este subobjeto. Si recordamos que el subobjeto mencionado se obtiene con un producto fibrado, entonces obtenemos:
Definición
\(a\colon U\to X\) satisface \(\varphi(x)\colon X\to\Omega\) si \(a\) se factoriza a través del subobjeto \(\{x\mid\varphi(x)\}\).
No es difícil ver que la condición de la definición es equivalente a que \(Im(a)\leq\{x\mid\varphi(x)\}\).
Cuando se cumpla la condición de la definición escribiremos \(U\Vdash\varphi(a)\) y lo leeremos como en teoría de conjuntos: \(U\) fuerza \(\varphi(a)\).
Algunas propiedades fáciles de la relación de forzar son:
Monotonía Sean \(a\colon U\to X\) un elemento, \(p\colon V\to U\) una flecha y \(\varphi(x)\colon X\to\Omega\) una fórmula. Si \(U\Vdash\varphi(x)\) entonces \(V\Vdash\varphi(x)\).
Carácter local Sean \(a\colon U\to X\) un elemento, \(p\colon V\to U\) un epi y \(\varphi(x)\colon X\to\Omega\) una fórmula. Si \(V\Vdash\varphi(x)\) entonces \(U\Vdash\varphi(x)\).
Finalmente, las propiedades análogas a la definición de verdad de Tarski, es decir, cómo se comporta la relación de forzar con los conectivos y cuantificadores.
Teorema
Sean \(a\colon U\to X\) un elemento y \(\varphi(x),\psi(x)\colon X\to\Omega\) fórmulas.
- \(U\Vdash\varphi(a)\land\psi(a)\) si y sólo si \(U\Vdash\varphi(a)\) y \(U\Vdash\psi(a)\);
- \(U\Vdash\varphi(a)\lor\psi(a)\) si y sólo si hay flechas \(p\colon V\to U\) y \(q\colon W\to U\) tales que la flecha inducida \(V+W\to U\) es epi, \(V\Vdash\varphi(ap)\) y \(W\Vdash\psi(aq)\);
- \(U\Vdash\varphi(a)\Rightarrow\psi(a)\) si y sólo si para cualquier \(p\colon V\to U\) tal que \(V\Vdash\varphi(ap)\) se cumple \(V\Vdash\psi(ap)\);
- \(U\Vdash\neg\varphi(a)\) si y sólo si para cualquier \(p\colon V\to U\) tal que \(V\Vdash\varphi(ap)\) se cumple \(V\cong 0\);
Ahora supongamos que tenemos una variable libre más, \(\varphi(x,y)\colon X\times Y\to\Omega\),
- \(U\Vdash\exists y\varphi(a,y)\) si y sólo si existe un epi \(p\colon V\to U\) y un elemento \(b\colon V\to Y\) tales que \(V\Vdash\varphi(ap,b)\).
- \(U\Vdash\forall y\varphi(a,y)\) si y sólo si para cualesquiera \(p\colon V\to U\) epi \(b\colon V\to Y\) se tiene que \(V\Vdash\varphi(ap,b)\).
- \(U\Vdash\forall y\varphi(a,y)\) si y sólo si \(U\times Y\Vdash\varphi(a\pi_1,\pi_2)\).
