¿Cuál es la definición de teoría equacional? ¿Por qué la lógica es libre?

Question

Un libro dice que "es libre de lógica: es una teoría ecuacional". Pero no entiendo qué significa "libre de lógica" y "teoría ecuacional". ¿Puedes ayudarme?

Answer 1

Puedes ver a Ian Chiswell & Wilfrid Hodges, Mathematical Logic (2007), Capítulo 5: Lógica libre de cuantificadores, página 101 en adelante.

Se utiliza un lenguaje de primer orden sin cuantificadores y se estudia un cálculo de deducción natural para fórmulas libres de cuantificadores:

Las fórmulas atómicas de la forma $(s = t)$ se llaman ecuaciones, y el símbolo ‘$=$’ se conoce como igualdad o identidad.

Las reglas de deducción natural para fórmulas libres de cuantificadores son exactamente las mismas que para $LP$ [lógica proposicional], excepto que también tenemos reglas de introducción y eliminación ($=$I), ($=$E) para igualdad.

Así, básicamente, podemos construir derivaciones "hechas de" ecuaciones.

Añadido

Ver Henk Barendregt, The Lambda Calculus. Its Syntax and Semantics (2da ed revisada - 1985), página 6:

La teoría $\lambda$ [del cálculo lambda puro] tiene como términos el conjunto $\Lambda$ (términos $\lambda$) construidos a partir de variables usando aplicación y abstracción. Las afirmaciones de $\lambda$ son ecuaciones entre términos $\lambda$ [...].

Ver página 23:

Señalar que $\lambda$ es libre de lógica [énfasis añadido]: es una teoría de ecuaciones. Conectivos y cuantificadores se usarán en el metalenguaje informal al discutir sobre $\lambda$.

De estas citas, la intención del autor es clara. La teoría matemática del cálculo lambda puro se basa en una sintaxis de términos, donde el conjunto $\Lambda$ está construido a partir de variables ($v_0, v_1, ...$), los paréntesis y el abstractor $\lambda$ [ver Def.2.1.1, página 22], y las fórmulas del cálculo son ecuaciones entre términos de la forma $M=N$ donde $M,N \in \Lambda$ [ver Def.2.1.4, página 23].

Las fórmulas no tienen conectivos lógicos: $\lnot$, $\land$, $\rightarrow$, ni los cuantificadores "habituales": $\forall$, $\exists$; en este sentido es "libre de lógica".

Expresiones como:

$M = N \implies N = M$

o:

$\forall M \, (\lambda x.x) M = M$

con conectivos y cuantificadores, no son fórmulas del lenguaje, sino afirmaciones en el meta-lenguaje describiendo el cálculo $\lambda$.

Answer 2

Considera una amplia clase de "sistemas formales": cada uno viene con un conjunto de símbolos, un conjunto de declaraciones o fórmulas bien formadas, axiomas y reglas sobre cómo definir nuevas fórmulas a partir de los axiomas. Las fórmulas derivables en un sistema formal dado se llaman "la teoría del sistema".

Luego, "lógica proposicional" o "lógica de primer orden" se refiere a una subclase de sistemas formales, cuyo conjunto de símbolos contiene operadores que pueden ser llamados "lógicos", y ya sea los axiomas o las reglas contendrán razonamiento "lógico"; estamos hablando de conjunción, disyunción, implicación, equivalencia lógica, negación, forall, exists (no necesariamente todos).

(Note que a menudo hay varias formas equivalentes de hacer razonamiento: axiomático ("estilo Hilbert"), donde hay axiomas "lógicos" y la única regla de inferencia es Modus Ponens, o en Deducción Natural o Cálculo de Secuentes donde obtenemos razonamiento a través de las reglas de inferencia y los únicos axiomas son los "no lógicos")

El cálculo lambda es un sistema formal donde las únicas fórmulas bien formadas son ecuaciones. Por lo tanto, las reglas sirven para derivar nuevas ecuaciones a partir de las existentes, la teoría es "ecuacional".

Para usar el cálculo lambda para razonamiento lógico, uno puede agregar conectores "lógicos" en forma de constantes, con axiomas (ecuaciones) que les dan a estos conectores su significado esperado. Consulta el artículo de Farmer "The seven virtues of simple type theory" o el libro de Andrews "An Introduction to Mathematical Logic and Type Theory"