demostrando{¬(∀x)α→α¬(∀x)α→α\neg(\forall x)\alpha \rightarrow \alpha}⊨⊨\models(∀x)α(∀x)α(\forall x )\alfa

Ver Elliott Mendelson, Introducción a la lógica matemática (4ed - 1997), página 69.

Necesitamos al menos un tercer axioma proposicional , como:

(A3) ---$(\lnot γ → \lnot β) → ((\lnot γ → β) → γ)$

poder probar todas las tautologías .

Además, asumo dos axiomas para el cálculo de predicados (y otros dos axiomas para la igualdad : no los necesitamos aquí):

(A4) ---$\forall x \alpha(x) \rightarrow \alpha (t)$, dónde$t$es un término libre para$x$en$\alpha(x)$

(A5) ---$(∀x(\alpha → \beta) → (\alpha → ∀x \beta))$, dónde$x$no es gratis en$\alpha$.

También necesitamos reglas de inferencia :

• modus ponens

• generalización : forma$\alpha$,$\forall x \alpha$sigue.

Prueba

(1) $\lnot \forall x \alpha \rightarrow \alpha$--- asumido

(2) $\lnot \alpha \rightarrow \forall x \alpha$--- forma (1) usando la tautología :$(\lnot \varphi \rightarrow \psi) \rightarrow (\lnot \psi \rightarrow \varphi)$y modus ponens

(3) $\forall x \alpha \rightarrow \alpha$--- por axión (A4), con$x$como$t$

(4) $\lnot \alpha \rightarrow \lnot \forall x \alpha$--- de (3) como arriba

(5) $\alpha$--- del axioma (A3) con (4) y (2), por mp dos veces

(6) $\forall x \alpha$--- de (5) por generalización

Así, forma (1) y (6) :

$\lnot \forall x \alpha \rightarrow \alpha \vdash \forall x \alpha$.

Nota

Para concluir de la fórmula anterior, por solidez , que:

$\lnot \forall x \alpha \rightarrow \alpha \vDash \forall x \alpha$

tenemos que comprobar si los detalles finos con respecto a las definiciones de satisfacción y consecuencia lógica son consistentes con los del libro de Mendelson.

Comentario

Para probar la tautología :$(\lnot \varphi \rightarrow \psi) \rightarrow (\lnot \psi \rightarrow \varphi)$necesitamos algo de trabajo extra.

Consulte esta publicación para conocer las "herramientas básicas" según el sistema de prueba de Mendelson:

$\vdash \varphi \rightarrow \varphi$, Teorema de la Deducción , Silogismo y Leyes de la Doble Negación .

Con estos teoremas disponibles, es fácil probar la tautología anterior.