Saltar al contenido principal

$$\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}}$$

$$\newcommand{\vectorA}[1]{\vec{#1}} % arrow$$

$$\newcommand{\vectorAt}[1]{\vec{\text{#1}}} % arrow$$

$$\newcommand{\vectorB}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} }$$

$$\newcommand{\vectorC}[1]{\textbf{#1}}$$

$$\newcommand{\vectorD}[1]{\overrightarrow{#1}}$$

$$\newcommand{\vectorDt}[1]{\overrightarrow{\text{#1}}}$$

$$\newcommand{\vectE}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash{\mathbf {#1}}}}$$

$$\newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} }$$

$$\newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}}$$

Template:MathJaxZach

Teorema$$\PageIndex{1}$$

Si$$c$$ es una constante que no ocurre en$$\Gamma$$ o$$A(x)$$ y$$\Gamma \Proves A(c)$$, entonces$$\Gamma \Proves \lforall{x}{A(x)}$$.

Comprobante. Dejar$$\pi_0$$ ser una$$\Log{LK}$$ -derivación de$$\Gamma_0 \Sequent A(c)$$ para algunos finitos$$\Gamma_0 \subseteq \Gamma$$. Al agregar una$$\RightR{\lforall{}{}}$$ inferencia, obtenemos una prueba de$$\Gamma_0 \Sequent \lforall{x}{A(x)}$$, ya que$$c$$ no ocurre en$$\Gamma$$ o$$A(x)$$ y por lo tanto se cumple la condición de variable propia. ◻

Proposición$$\PageIndex{1}$$

1. $$A(t) \Proves \lexists{x}{A(x)}$$.

2. $$\lforall{x}{A(x)} \Proves A(t)$$.

Comprobante.

1. El secuente$$A(t) \Sequent \lexists{x}{A(x)}$$ es derivable:

2. El secuente$$\lforall{x}{A(x)} \Sequent A(t)$$ es derivable:

This page titled 8.11: Derivabilidad y los cuantificadores is shared under a CC BY license and was authored, remixed, and/or curated by Richard Zach et al. (Open Logic Project) .