9.7: Nociones teóricas de prueba
- Page ID
- 103642
\( \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}\)Así como hemos definido una serie de nociones semánticas importantes (validez, vinculación, satisfacción), ahora definimos nociones teóricas de prueba correspondientes. Éstas no se definen por la apelación a la satisfacción de sentencias en estructuras, sino por la apelación a la derivabilidad o no derivabilidad de ciertas oraciones de otras. Fue un descubrimiento importante que estas nociones coincidan. Lo que hacen es el contenido de los teoremas de solidez e integridad.
Definición\(\PageIndex{1}\): Theorems
Una oración\(A\) es un teorema si existe una derivación de\(A\) en deducción natural en la que se descargan todos los supuestos. 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 una derivación con conclusión\(A\) y en la que cada suposición es descargada o está en\(\Gamma\). Si no\(A\) es derivable de\(\Gamma\) escribimos\(\Gamma \ProvesN A\).
Definición\(\PageIndex{3}\): Consistency
Un conjunto de oraciones\(\Gamma\) es inconsistente iff\(\Gamma \Proves \lfalse\). Si no\(\Gamma\) es inconsistente, es decir\(\Gamma \ProvesN \lfalse\), si, decimos que es consistente.
Proposición\(\PageIndex{1}\): Reflexivity
Si\(A \in \Gamma\), entonces\(\Gamma \Proves A\).
Prueba. La suposición\(A\) por sí misma es una derivación de\(A\) donde se encuentra cada suposición no descargada (es decir,\(A\))\(\Gamma\). ◻
Proposición\(\PageIndex{2}\): Monotony
Si\(\Gamma \subseteq \Delta\) y\(\Gamma \Proves A\), entonces\(\Delta \Proves A\).
Prueba. Cualquier derivación\(A\) de\(\Gamma\) es también una derivación\(A\) de\(\Delta\). ◻
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 una derivación\(\delta_0\) de\(A\) con todos los supuestos no descargados en\(\Gamma\). Si\(\{A\} \cup \Delta \Proves B\), entonces hay una derivación\(\delta_1\) de\(B\) con todos los supuestos no descargados en\(\{A\} \cup \Delta\). Ahora considere:
Los supuestos no descargados están ahora todos entre\(\Gamma \cup \Delta\), así que esto demuestra\(\Gamma \cup \Delta \Proves B\). ◻
Cuando\(\Gamma = \{A_1, A_2, \ldots, A_k\}\) es un conjunto finito podemos usar la notación simplificada\(A_1,A_2,\ldots,A_k \Proves B\) para\(\Gamma \Proves B\), en particular\(A \Proves B\) significa que\(\{A\} \Proves B\).
Tenga en cuenta que 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\).
Los siguientes son equivalentes.
-
\(\Gamma\)es inconsistente.
-
\(\Gamma \Proves {A}\)por cada oración\({A}\).
-
\(\Gamma \Proves {A}\)y\(\Gamma \Proves \lnot {A}\) para alguna sentencia\({A}\).
Prueba. Ejercicio. ◻
Problema\(\PageIndex{1}\)
Probar Proposición\(\PageIndex{4}\).
Proposición\(\PageIndex{5}\): Compactness
-
Si\(\Gamma \Proves A\) entonces hay un subconjunto finito\(\Gamma_0 \subseteq \Gamma\) tal que\(\Gamma_0 \Proves A\).
-
Si cada subconjunto finito de\(\Gamma\) es consistente, entonces\(\Gamma\) es consistente.
Prueba.
-
Si\(\Gamma \Proves A\), entonces hay una derivación\(\delta\)\(A\) de\(\Gamma\). \(\Gamma_0\)Sea el conjunto de supuestos no descargados de\(\delta\). Dado que cualquier derivación es finita, sólo\(\Gamma_0\) puede contener finitamente muchas oraciones. Entonces,\(\delta\) es una derivación\(A\) de una finita\(\Gamma_0 \subseteq \Gamma\).
-
Este es el contrapositivo de (1) para el caso especial\(A \ident \lfalse\).
◻