Cálculo secuencial y derivación por deducción natural

Question

Dada la fórmula $\exists x(\exists yA(y) \rightarrow A(x))$ de la lógica clásica. Proporcione una derivación de cálculo secuencial y una derivación de deducción natural de la fórmula.

Empecé a hacer algo así para la deducción natural, pero luego me atasqué: $$\dfrac{\dfrac{[\exists y\; A(y)] \quad, \quad A(t)}{A(t)}}{\dfrac{[\exists y\; A(y)] \rightarrow A(t)}{\exists x\;\big(\exists y\;A(y) \rightarrow A(x)\big)}}$$

No sé cómo seguirá la derivación natural, y tampoco sé cómo será la derivación del cálculo secuencial. Perdón por la mala tipografía, pero no veo ninguna forma fácil de escribir derivaciones en MathExchange, y no puedo seguir ningún otro método que no sea la derivación estilo árbol. ¿Alguna idea?

EDITAR:

$$\dfrac{\dfrac{A(y) \vdash A(y)}{\exists x A(x), A(y) \vdash A(y), A(x)}}{\dfrac{A(y) \vdash \exists y A(y) \to A(y), A(x)}{A(y) \vdash \exists x \big( \exists y A(y) \to A(x) \big), A(x)}}$$

No entiendo cómo desde $\exists x(\exists y A(y) \rightarrow A(x))$ ha obtenido $\exists y A(y) \rightarrow A(y)$ . Claramente, usted ha eliminado $\exists$ Pero, ¿por qué el $x$ se cambia a $y$ ? También cuando se ha pasado de la segunda a la tercera línea $\exists y A(y) \rightarrow A(y)$ se ha transformado en $\exists x A(x)$ , está claro que has hecho $(\rightarrow r)$ Pero, ¿por qué $y$ cambió a $x$ ? Y al final, ¿cómo te deshiciste de $\exists x A(x)$ y $A(x) en el otro lado completamente?

Answer 1

Es más bien: $$ \dfrac{ \dfrac{\dfrac{A(t)\mid^t_x\;\vdash\; A(t)\mid^t_x} {\exists y\;A(y)\; \vdash\; A(t)\mid^t_x} } {\vdash\;\big(\exists y\;A(y)\to A(t)\big)\mid^t_x}{\to\mathsf I}} {\vdash\; \exists x\;\big(\exists y\;A(y)\to A(x)\big)}{\exists\mathsf I}$$

O algo así. (Estoy fuera de práctica)

---

Estoy más familiarizado con este formato:

$$\begin{array}{l|l:l} \qquad 1. & \exists y\;A(y) & \textsf{Assume} \\ \qquad 2. & A(t) & 1, \exists\textsf{Elim} \\ \hline \quad 3. & \exists y\;A(y) \to A(t) & 1,2, \to\textsf{Intro} \\ \hline 4. & \exists x\;(\exists y\;A(y)\to A(x)) & 3, \exists\textsf{Intro} \\ \Box \end{array}$$

Answer 2

Deducción natural

Me parece que hay que "complicar" un poco la derivación, para evitar lo "inválido" : $\exists y A(y) \to A(x)$ .

1) $\exists y A(y)$ --- premisa

2) $A(x)$ --- asumido a partir de 1) para $\exists$ -elim

3) $\exists x A(x)$ --- de 2) por $\exists$ -intro, seguido de $\exists$ -elim con 1) y 2)

4) $\vdash \exists y A(y) \to \exists x A(x)$ --- de 1) y 3) por $\to$ -intro.

Ahora podemos utilizar $\vdash \exists y A(y) \to \exists x A(x)$ en la segunda parte de la derivación :

5) $\exists y A(y)$ --- asumido [a]

6) $\exists x A(x)$ --- de 4) y 5) por $\to$ -elim

7) $A(x)$ --- asumido [b] para $\exists$ -elim

8) $\exists y A(y) \to A(x)$ --- de 5) y 7) por $\to$ -intro, descargando [a]

9) $\exists x (\exists y A(y) \to A(x))$ --- de 8) por $\exists$ -intro

10) $\vdash \exists x (\exists y A(y) \to A(x))$ --- de 6) y 7)-9) por $\exists$ -elim, descargando [b].

---

Cálculo secuencial

Para el cálculo secuencial normas, véase :

• Gaisi Takeuti, Teoría de la prueba (2ª ed. - 1987)

La derivación engañosamente "simple" :

$$\dfrac{\dfrac{A(x) \vdash A(x)}{\exists y \ A(y) \vdash A(x)}}{\dfrac{\vdash \exists y \ A(y) \rightarrow A(x)}{\vdash \exists x \ \big(\exists y \ A(y) \rightarrow A(x) \big)}}$$

es equivocado porque en la segunda línea estamos violando la provisión de la $\exists$ -regla l : el eigenvariable $x$ no debe aparecer libre en el secuencial inferior.

Me parece que la forma de solucionarlo es la siguiente :

$$\dfrac{\dfrac{A(y) \vdash A(y)}{\exists y A(y), A(y) \vdash A(y), A(x)}}{\dfrac{A(y) \vdash \exists y A(y) \to A(y), A(x)}{A(y) \vdash \exists x \big( \exists y A(y) \to A(x) \big), A(x)}}$$

Primero necesitamos $\text{Weakining}$ en ambos lados, seguido de $\to\text{-r}$ y $\exists\text{-r}$ .

Ahora, aplicamos $\exists\text{-l}$ con la condición de que se cumpla, seguido de $\to\text{-r}$ y $\exists\text{-r}$ de nuevo; finalmente, necesitamos $\text{Contraction}$ :

$$\dfrac{\dfrac{\exists y A(y) \vdash \exists x \big( \exists y A(y) \to A(x) \big), A(x)}{\vdash \exists x \big( \exists y A(y) \to A(x) \big), \exists y A(y) \to A(x)}}{\dfrac{\vdash \exists x \big( \exists y A(y) \to A(x) \big), \exists x \big( \exists y A(y) \to A(x) \big)}{\vdash \exists x \big( \exists y A(y) \to A(x) \big)}}$$

Answer 3

Aquí hay algo que huele mal: ¿cómo se supone que una función puede mostrar $A(x)$ con un "conocido" $x$ de simplemente $\exists y A(y)$ , donde $y$ ¿se "olvida"? Esto parece muy contra intuitivo . Como la descripción del problema dice "lógica clásica", considero que no hay ninguna prueba intuitiva/constructiva de este teorema. Cualquier intento que no implique una clásico axioma (ley del medio excluido, eliminación de la doble negación, o equivalente) está destinado a fallar.

Aquí está mi solución en notación secuencial. Comienza con la ley del medio excluido (XM):

$$\dfrac{ \dfrac{ }{ \vdash \exists z A(z) \lor \lnot \exists w A(w) }\mathrm{XM} \quad \dfrac{ }{ \exists z A(z) \vdash \cdots }(1) \quad \dfrac{ }{ \lnot \exists w A(w) \vdash \cdots }(2) }{ \vdash \exists x (\exists y A(y) \to A(x)) }\mathrm{E}_\lor$$

Para mantener la amplitud de la prueba, la divido en partes separadas (1) y (2), cada una de ellas responsable de tratar uno de los dos casos posibles que resultan de XM. Para evitar confusiones, utilizo letras distintas para las diferentes variables ligadas, pero hay que tener en cuenta que $\exists z A(z)$ y $\exists w A(w)$ son exactamente lo mismo .

Caso (1), donde $\exists z A(z)$ se mantiene:

$$ \dfrac{ \dfrac{ }{ \exists z A(z) \vdash \exists u A(u) }\mathrm{Id} \quad \dfrac{ \dfrac{ \dfrac{ \dfrac{ }{ A(u) \vdash A(u) }\mathrm{Id} }{ A(u), \exists y A(y) \vdash A(u) }\mathrm{Wk} }{ A(u) \vdash \exists y A(y) \to A(u) }\mathrm{I}_\to }{ A(u) \vdash \exists x (\exists y A(y) \to A(x)) }\mathrm{I}_\exists }{ \exists z A(z) \vdash \exists x (\exists y A(y) \to A(x)) }\mathrm{E}_\exists $$

Caso (2), donde $\exists w A(w)$ no se sostiene:

$$ \dfrac{ \dfrac{ \dfrac{ }{ \lnot \exists w A(w) \vdash \lnot \exists v A(v) }\mathrm{Id} }{ \lnot \exists w A(w) \vdash \exists v A(v) \to \bot }\mathrm{E}_\lnot \quad \dfrac{ }{ \exists y A(y) \vdash \exists v A(v) }\mathrm{Id} }{ \dfrac{ \dfrac{ \dfrac{ \lnot \exists w A(w), \exists y A(y) \vdash \bot }{ \lnot \exists w A(w), \exists y A(y) \vdash A(x) }\mathrm{E}_\bot }{ \lnot \exists w A(w) \vdash \exists y A(y) \to A(x) }\mathrm{I}_\to }{ \lnot \exists w A(w) \vdash \exists x (\exists y A(y) \to A(x)) }\mathrm{I}_\exists }\mathrm{E}_\to $$

Y sólo para probar que esta derivación no es completamente loca, aquí está de nuevo, escrita como un programa Haskell que comprueba correctamente el tipo:

{-# LANGUAGE GADTs #-}
module Foo where
import Data.Void (Void, absurd)

data Exists a where
  Exists :: a x -> Exists a

data Theorem a where
  Theorem :: (Exists a -> a x) -> Theorem a

excludedMiddle :: Either (p -> Void) p
excludedMiddle = error "you'll just have to trust me!"

theorem :: Theorem a
theorem =
  case excludedMiddle of
    Left notExists -> Theorem (\ exists -> absurd (notExists exists))
    Right (Exists evidence) -> Theorem (\ _ -> evidence)