Buscar

Loading [MathJax]/jax/output/HTML-CSS/jax.js

8.11: Derivabilidad y los cuantificadores
https://espanol.libretexts.org/Humanidades/Filosofia/Conjuntos_Logica_Computacion_(Zach)/02%3A_Logica_de_primer_orden/08%3A_El_Calculo_Secuente/8.11%3A_Derivabilidad_y_los_cuantificadores
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)}$ . Dejar $\pi_0$ ser una $\Log{LK}$ -derivación de\(\Gamma_0 \Seque...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)}$ . 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. ◻

Search