Saltar al contenido principal

# 8.8: Nociones teóricas de prueba

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

$$\newcommand{\avec}{\mathbf a}$$ $$\newcommand{\bvec}{\mathbf b}$$ $$\newcommand{\cvec}{\mathbf c}$$ $$\newcommand{\dvec}{\mathbf d}$$ $$\newcommand{\dtil}{\widetilde{\mathbf d}}$$ $$\newcommand{\evec}{\mathbf e}$$ $$\newcommand{\fvec}{\mathbf f}$$ $$\newcommand{\nvec}{\mathbf n}$$ $$\newcommand{\pvec}{\mathbf p}$$ $$\newcommand{\qvec}{\mathbf q}$$ $$\newcommand{\svec}{\mathbf s}$$ $$\newcommand{\tvec}{\mathbf t}$$ $$\newcommand{\uvec}{\mathbf u}$$ $$\newcommand{\vvec}{\mathbf v}$$ $$\newcommand{\wvec}{\mathbf w}$$ $$\newcommand{\xvec}{\mathbf x}$$ $$\newcommand{\yvec}{\mathbf y}$$ $$\newcommand{\zvec}{\mathbf z}$$ $$\newcommand{\rvec}{\mathbf r}$$ $$\newcommand{\mvec}{\mathbf m}$$ $$\newcommand{\zerovec}{\mathbf 0}$$ $$\newcommand{\onevec}{\mathbf 1}$$ $$\newcommand{\real}{\mathbb R}$$ $$\newcommand{\twovec}[2]{\left[\begin{array}{r}#1 \\ #2 \end{array}\right]}$$ $$\newcommand{\ctwovec}[2]{\left[\begin{array}{c}#1 \\ #2 \end{array}\right]}$$ $$\newcommand{\threevec}[3]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \end{array}\right]}$$ $$\newcommand{\cthreevec}[3]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \end{array}\right]}$$ $$\newcommand{\fourvec}[4]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}$$ $$\newcommand{\cfourvec}[4]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}$$ $$\newcommand{\fivevec}[5]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}$$ $$\newcommand{\cfivevec}[5]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}$$ $$\newcommand{\mattwo}[4]{\left[\begin{array}{rr}#1 \amp #2 \\ #3 \amp #4 \\ \end{array}\right]}$$ $$\newcommand{\laspan}[1]{\text{Span}\{#1\}}$$ $$\newcommand{\bcal}{\cal B}$$ $$\newcommand{\ccal}{\cal C}$$ $$\newcommand{\scal}{\cal S}$$ $$\newcommand{\wcal}{\cal W}$$ $$\newcommand{\ecal}{\cal E}$$ $$\newcommand{\coords}[2]{\left\{#1\right\}_{#2}}$$ $$\newcommand{\gray}[1]{\color{gray}{#1}}$$ $$\newcommand{\lgray}[1]{\color{lightgray}{#1}}$$ $$\newcommand{\rank}{\operatorname{rank}}$$ $$\newcommand{\row}{\text{Row}}$$ $$\newcommand{\col}{\text{Col}}$$ $$\renewcommand{\row}{\text{Row}}$$ $$\newcommand{\nul}{\text{Nul}}$$ $$\newcommand{\var}{\text{Var}}$$ $$\newcommand{\corr}{\text{corr}}$$ $$\newcommand{\len}[1]{\left|#1\right|}$$ $$\newcommand{\bbar}{\overline{\bvec}}$$ $$\newcommand{\bhat}{\widehat{\bvec}}$$ $$\newcommand{\bperp}{\bvec^\perp}$$ $$\newcommand{\xhat}{\widehat{\xvec}}$$ $$\newcommand{\vhat}{\widehat{\vvec}}$$ $$\newcommand{\uhat}{\widehat{\uvec}}$$ $$\newcommand{\what}{\widehat{\wvec}}$$ $$\newcommand{\Sighat}{\widehat{\Sigma}}$$ $$\newcommand{\lt}{<}$$ $$\newcommand{\gt}{>}$$ $$\newcommand{\amp}{&}$$ $$\definecolor{fillinmathshade}{gray}{0.9}$$

Template:MathJaxZach

Así como hemos definido una serie de nociones semánticas importantes (validez, vinculación, satisfacción), ahora definimos nociones teóricas de prueba correspondientes. Estos no se definen por la apelación a la satisfacción de las sentencias en las estructuras, sino por la apelación a la derivabilidad o no derivabilidad de ciertos secuentes. Fue un descubrimiento importante que estas nociones coincidan. Lo que hacen es el contenido del teorema de solidez e integridad.

Definición$$\PageIndex{1}$$: Theorems

Una oración$$A$$ es un teorema si hay una derivación en$$\Log{LK}$$ del secuente$$\quad \Sequent A$$. Escribimos$$\Proves A$$ si$$A$$ es un teorema y$$\ProvesN A$$ si no lo es.

Definición$$\PageIndex{2}$$: Derivability

Una oración$$A$$ es derivable de un conjunto de oraciones$$\Gamma$$,$$\Gamma \Proves A$$, si hay un subconjunto finito$$\Gamma_0 \subseteq \Gamma$$ y una secuencia$$\Gamma_0'$$ de las oraciones de$$\Gamma_0$$ tal manera que$$\Log{LK}$$ deriva$$\Gamma_0' \Sequent A$$. Si no$$A$$ es derivable de$$\Gamma$$ escribimos$$\Gamma \ProvesN A$$.

Debido a las reglas de contracción, debilitamiento e intercambio, el orden y el número de oraciones en$$\Gamma_0'$$ no importa: si un secuente$$\Gamma_0' \Sequent A$$ es derivable, entonces también lo es$$\Gamma_0'' \Sequent A$$ para cualquiera$$\Gamma_0''$$ que contenga las mismas oraciones que $$\Gamma_0'$$. Por ejemplo, si$$\Gamma_0 = \{B, C\}$$ entonces ambos$$\Gamma_0' = \tuple{B, B, C}$$ y$$\Gamma_0'' = \tuple{C, C, B}$$ son secuencias que contienen solo las oraciones en$$\Gamma_0$$. Si un secuente que contiene uno es derivable, también lo es el otro, por ejemplo:

A partir de ahora diremos que si$$\Gamma_0$$ es un conjunto finito de oraciones entonces$$\Gamma_0 \Sequent A$$ es cualquier secuente donde el antecedente sea una secuencia de oraciones$$\Gamma_0$$ e incluya tácitamente contracciones, intercambios y debilitaciones si es necesario.

Definición$$\PageIndex{3}$$: Consistency

Un conjunto de oraciones$$\Gamma$$ es inconsistente si hay un subconjunto finito$$\Gamma_0 \subseteq \Gamma$$ tal que$$\Log{LK}$$ deriva$$\Gamma_0 \Sequent \quad$$. Si no$$\Gamma$$ es inconsistente, es decir, si por cada finito$$\Gamma_0 \subseteq \Gamma$$,$$\Log{LK}$$ no deriva$$\Gamma_0 \Sequent \quad$$, decimos que es consistente.

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

Si$$A \in \Gamma$$, entonces$$\Gamma \Proves A$$.

Prueba. El secuente inicial$$A \Sequent A$$ es derivable, y$$\{A\} \subseteq \Gamma$$. ◻

Proposición$$\PageIndex{2}$$: Monotony

Si$$\Gamma \subseteq \Delta$$ y$$\Gamma \Proves A$$, entonces$$\Delta \Proves A$$.

Prueba. Supongamos$$\Gamma \Proves A$$, es decir, hay un$$\Gamma_0 \subseteq \Gamma$$ tal finito que$$\Gamma_0 \Sequent A$$ es derivable. Ya que$$\Gamma \subseteq \Delta$$, entonces también$$\Gamma_0$$ es un subconjunto finito de$$\Delta$$. La derivación de$$\Gamma_0 \Sequent A$$ así también muestra$$\Delta \Proves A$$. ◻

Proposición$$\PageIndex{3}$$: Transitivity

Si$$\Gamma \Proves A$$ y$$\{A\} \cup \Delta \Proves B$$, entonces$$\Gamma \cup \Delta \Proves B$$.

Prueba. Si$$\Gamma \Proves A$$, hay un finito$$\Gamma_0 \subseteq \Gamma$$ y una derivación$$\pi_0$$ de$$\Gamma_0 \Sequent A$$. Si$$\{A\} \cup \Delta \Proves B$$, entonces para algún subconjunto finito$$\Delta_0 \subseteq \Delta$$, hay una derivación$$\pi_1$$ de$$A, \Delta_0 \Sequent B$$. Considere la siguiente derivación:

Ya que$$\Gamma_0 \cup \Delta_0 \subseteq \Gamma \cup \Delta$$, esto demuestra$$\Gamma \cup \Delta \Proves B$$. ◻

Tenga en cuenta que esto significa que en particular si$$\Gamma \Proves A$$ y$$A \Proves B$$, entonces$$\Gamma \Proves B$$. De ello se deduce también que si$$A_1, \dots, A_n \Proves B$$ y$$\Gamma \Proves A_i$$ para cada uno$$i$$, entonces$$\Gamma \Proves B$$.

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

$$\Gamma$$es inconsistente iff$$\Gamma \Proves {A}$$ para cada oración$$A$$.

Prueba. Ejercicio. ◻

Problema$$\PageIndex{1}$$

Proponer Proposición$$\PageIndex{4}$$.

Proposición$$\PageIndex{5}$$: Compactness

1. Si$$\Gamma \Proves A$$ entonces hay un subconjunto finito$$\Gamma_0 \subseteq \Gamma$$ tal que$$\Gamma_0 \Proves A$$.

2. Si cada subconjunto finito de$$\Gamma$$ es consistente, entonces$$\Gamma$$ es consistente.

Prueba.

1. Si$$\Gamma \Proves A$$, entonces hay un subconjunto finito$$\Gamma_0 \subseteq \Gamma$$ tal que el secuente$$\Gamma_0 \Sequent A$$ tiene una derivación. En consecuencia,$$\Gamma_0 \Proves A$$.

2. Si$$\Gamma$$ es inconsistente, hay un subconjunto finito$$\Gamma_0 \subseteq \Gamma$$ tal que$$\Log{LK}$$ deriva$$\Gamma_0 \Sequent \quad$$. Pero entonces$$\Gamma_0$$ es un subconjunto finito de$$\Gamma$$ eso es inconsistente.

This page titled 8.8: Nociones teóricas de prueba is shared under a CC BY license and was authored, remixed, and/or curated by Richard Zach et al. (Open Logic Project) .