Saltar al contenido principal
LibreTexts Español

8.8: Nociones teóricas de prueba

  • Page ID
    103647
  • \( \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

    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:

    8.1.png

    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:

    8.2.png

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