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

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