9.3: Reglas del cuantificador

Última actualización
Guardar como PDF

Page ID: 103634

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

9.3.1.png

En las reglas para\(\lforall{}{}\),\(t\) es un término suelo (un término que no contiene ninguna variable), y\(a\) es un símbolo constante que no ocurre en la conclusión\(\lforall{x}{A(x)}\), o en cualquier supuesto que no se descarga en la derivación que termina con la premisa\(A(a)\). Llamamos a\(a\) la variable propia de la\(\Intro{\lforall{}{}}\) inferencia.

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

9.3.2.png

Nuevamente,\(t\) es un término suelo, y\(a\) es una constante que no ocurre en la premisa\(\lexists{x}{A(x)}\), en la conclusión\(C\), o cualquier supuesto que no se descarga en las derivaciones que terminan con las dos premisas (distintas de las suposiciones \(A(a)\)). Llamamos a\(a\) la variable propia de la\(\Elim{\lexists{}{}}\) inferencia.

La condición de que una variable propia no se produzca en las instalaciones ni en ningún supuesto que no se descargue en las derivaciones que conducen a las premisas para la\(\Intro{\lforall{}{}}\) o\(\Elim{\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 una constante. Esto tiene razones históricas.

En\(\Intro{\lexists{}{}}\) y no\(\Elim{\lforall{}{}}\) hay restricciones, y el término\(t\) puede ser cualquier cosa, así que no tenemos que preocuparnos por ninguna condición. Por otro lado, en las\(\Intro{\lforall{}{}}\) reglas\(\Elim{\lexists{}{}}\) y, la condición de variable propia requiere que el símbolo constante\(a\) no se presente en ninguna parte de la conclusión o en una suposición no descargada. La condición es necesaria para asegurar que el sistema sea sólido, es decir, sólo deriva oraciones de supuestos no descargados de los que siguen. Sin esta condición, se permitiría lo siguiente:

9.3.3.png

Sin embargo,\(\lexists{x}{A(x)} \EntailsN \lforall{x}{A(x)}\).