Saltar al contenido principal
LibreTexts Español

8.13: Derivaciones con predicado de identidad

  • Page ID
    103679
  • \( \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

    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):

    8.13.1.png

    Ejemplo\(\PageIndex{1}\)

    Si\(s\) y\(t\) son términos cerrados, entonces\(\eq[s][t], A(s) \Proves A(t)\):

    8.13.2.png

    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:

    8.13.3.png

    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:

    1. \(\Sequent \lforall{x}{\lforall{y}{((x = y \land A(x)) \lif A(y))}}\)

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


    This page titled 8.13: Derivaciones con predicado de identidad is shared under a CC BY license and was authored, remixed, and/or curated by Richard Zach et al. (Open Logic Project) .