8.14: Validez con predicado de identidad
- Page ID
- 103628
Proposición\(\PageIndex{1}\)
\(\Log{LK}\)con secuentes iniciales y reglas para la identidad es sólida.
Comprobante. Los secuentes iniciales de la forma\({} \Sequent \eq[t][t]\) son válidos, ya que para cada estructura\(\Struct M\),\(\Sat{M}{\eq[t][t]}\). (Tenga en cuenta que asumimos que el término se va\(t\) a cerrar, es decir, no contiene variables, por lo que las asignaciones de variables son irrelevantes).
Supongamos que la última inferencia en una derivación es\(=\). Entonces la premisa es\(\eq[t_1][t_2], \Gamma \Sequent \Delta, A(t_1)\) y la conclusión es\(\eq[t_1][t_2], \Gamma \Sequent \Delta, A(t_2)\). Considera una estructura\(\Struct M\). Tenemos que demostrar que la conclusión es válida, es decir, si\(\Sat{M}{\eq[t_1][t_2]}\) y\(\Sat{M}{\Gamma}\), entonces ya sea\(\Sat{M}{C}\) para algunos\(C \in \Delta\) o\(\Sat{M}{A(t_2)}\).
Por hipótesis de inducción, la premisa es válida. Esto significa que si\(\Sat{M}{\eq[t_1][t_2]}\) y\(\Sat{M}{\Gamma}\) ya sea (a) para algunos\(C \in \Delta\),\(\Sat{M}{C}\) o (b)\(\Sat{M}{A(t_1)}\). En caso de que (a) hayamos terminado. Considerar el caso b). Dejar\(s\) ser una asignación variable con\(s(x) = \Value{t_1}{M}\). Por Proposición 5.12.3,\(\Sat[,s]{M}{A(t_1)}\). Dado que\(\varAssign{s}{s}{x}\), por la Proposición 5.13.3,\(\Sat[,s]{M}{A(x)}\). Ya que\(\Sat{M}{\eq[t_1][t_2]}\), tenemos\(\Value{t_1}{M} = \Value{t_2}{M}\), y por lo tanto\(s(x) = \Value{t_2}{M}\). Al aplicar nuevamente la Proposición 5.13.3, también tenemos\(\Sat[,s]{M}{A(t_2)}\). Por Proposición 5.12.3,\(\Sat{M}{A(t_2)}\). ◻