Prueba formal de un hecho muy simple.

Question

Sea $L$ un lenguaje de primer orden con el símbolo predicado $R$, y sean $x,y$ variables en $L.

Quiero demostrar que

$\forall x \forall y R(x,y) \vdash R(y,x)$

Donde $\vdash$ significa formalmente probar.

Estoy usando Introducción Matemática a la Lógica de Enderton, por lo que estoy utilizando su sistema deductivo. Puedo utilizar cualquier teorema para demostrar que hay una derivación formal, excepto el teorema de completitud.

Lo mejor que puedo hacer es $\forall x \forall y R(x,y) \vdash R(z,y)$

donde $z$ es una variable distinta de $x$ e $y$. He estado intentando durante horas, por favor ayuda. Ten en cuenta que en realidad no estoy buscando una prueba formal, solo necesito demostrar que una existe.

Answer 1

Ref a :

• Herbert Enderton, A Mathematical Introduction to Logic (2da edición - 2001), página 112.

El primer paso es :

$∀x∀yR(x,y) ⊢ ∀yR(z,y)$, usando Axioma 2 con $z$ como $t$ (y la regla de Modus Ponens, por supuesto).

El segundo paso es :

$∀yR(z,y) ⊢ R(z,x)$, utilizando nuevamente Axioma 2 con $x$ como $t$.

Luego usamos el Teorema de Generalización [página 117] para obtener :

$R(z,x) ⊢ ∀zR(z,x)$

y finalmente aplicamos nuevamente Axioma 2 para tener :

$∀zR(z,x) ⊢ R(y,x)$.

---

Axioma 2 es :

$\forall x \alpha \to \alpha^x_t$, donde $t$ es un término sustituible por $x$ en $\alpha$.