8.14: Validez con predicado de identidad

Última actualización
Guardar como PDF

Page ID: 103628

\( \newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} } \) \( \newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}} \)\(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\) \(\newcommand{\id}{\mathrm{id}}\) \( \newcommand{\Span}{\mathrm{span}}\) \( \newcommand{\kernel}{\mathrm{null}\,}\) \( \newcommand{\range}{\mathrm{range}\,}\) \( \newcommand{\RealPart}{\mathrm{Re}}\) \( \newcommand{\ImaginaryPart}{\mathrm{Im}}\) \( \newcommand{\Argument}{\mathrm{Arg}}\) \( \newcommand{\norm}[1]{\| #1 \|}\) \( \newcommand{\inner}[2]{\langle #1, #2 \rangle}\) \( \newcommand{\Span}{\mathrm{span}}\)\(\newcommand{\AA}{\unicode[.8,0]{x212B}}\)

Template:MathJaxZach

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)}\). ◻