Saltar al contenido principal
Library homepage
 
LibreTexts Español

8.3: Reglas del cuantificador

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

    Reglas para\(\lforall{}{}\)

    8.3.1.png

    En\(\LeftR{\lforall{}{}}\),\(t\) es un término cerrado (es decir, uno sin variables). En\(\RightR{\lforall{}{}}\),\(a\) es un símbolo constante que no debe ocurrir en ninguna parte del secuente inferior de la\(\RightR{\lforall{}{}}\) regla. Llamamos a\(a\) la variable propia de la\(\RightR{\forall}\) inferencia.

    Reglas para\(\lexists{}{}\)

    8.3.2.png

    Nuevamente,\(t\) es un término cerrado, y\(a\) es un símbolo constante que no ocurre en el secuente inferior de la\(\LeftR{\lexists{}{}}\) regla. Llamamos a\(a\) la variable propia de la\(\LeftR{\lexists{}{}}\) inferencia.

    La condición de que una variable propia no ocurra en el secuente inferior de la\(\RightR{\lforall{}{}}\) o\(\LeftR{\lexists{}{}}\) inferencia se denomina condición de variable propia.

    Utilizamos el término “variable propia” a pesar de que\(a\) en las reglas anteriores es un símbolo constante. Esto tiene razones históricas.

    En\(\RightR{\lexists{}{}}\) y no\(\LeftR{\lforall{}{}}\) hay restricciones sobre el término\(t\). Por otro lado, en las\(\RightR{\lforall{}{}}\) reglas\(\LeftR{\lexists{}{}}\) y, la condición de variable propia requiere que el símbolo constante\(a\) no se presente en ningún lugar fuera de\(A(a)\) en el secuente superior. Es necesario asegurar que el sistema sea sano, es decir, sólo deriva secuentes que sean válidos. Sin esta condición, se permitiría lo siguiente:

    8.3.3.png

    Sin embargo, no\(\lexists{x}{A(x)} \Sequent \lforall{x}{A(x)}\) es válido.


    This page titled 8.3: Reglas del cuantificador is shared under a CC BY license and was authored, remixed, and/or curated by Richard Zach et al. (Open Logic Project) .