8.13: Derivaciones con predicado de identidad
- Page ID
- 103679
Las derivaciones con predicado de identidad requieren secuestros iniciales adicionales y reglas de inferencia.
Definición\(\PageIndex{1}\): Initial sequents for \(\eq[][]\)
Si\(t\) es un término cerrado, entonces\({} \Sequent \eq[t][t]\) es un secuente inicial.
Las reglas para\(\eq[][]\) son (\(t_1\)y\(t_2\) son términos cerrados):
Ejemplo\(\PageIndex{1}\)
Si\(s\) y\(t\) son términos cerrados, entonces\(\eq[s][t], A(s) \Proves A(t)\):
Esto puede ser familiar como el principio de sustituibilidad de las mismas, o Ley de Leibniz.
\(\Log{LK}\)demuestra que\(\eq[][]\) es simétrico y transitivo:
En la prueba de la izquierda, la fórmula\(\eq[x][t_1]\) es nuestra\(A(x)\). A la derecha, tomamos\(A(x)\) para ser\(\eq[t_1][x]\).
Problema\(\PageIndex{1}\)
Dar derivaciones de los siguientes secuentes:
-
\(\Sequent \lforall{x}{\lforall{y}{((x = y \land A(x)) \lif A(y))}}\)
-
\(\lexists{x}{A(x)} \land \lforall{y}{\lforall{z}{((A(y) \land A(z)) \lif y = z)}} \Sequent \lexists{x}{(A(x) \land \lforall{y}{(A(y) \lif y = x)})}\)