2.3: Los axiomas lógicos

Que se dé un lenguaje\(\mathcal{L}\) de primer orden. En esta sección reuniremos una colección\(\Lambda\) de axiomas lógicos para\(\mathcal{L}\). Este conjunto de axiomas, aunque infinito, será decidible. Aproximadamente esto significa que si se nos da una fórmula de la\(\phi\) que se alega que es un elemento de\(\Lambda\), podremos decidir si\(\phi \in \Lambda\) o\(\phi \notin \Lambda\). Además, podríamos, en principio, diseñar un programa de computadora que pudiera decidir la membresía\(\Lambda\) en un tiempo finito.

Después de haber establecido el conjunto de axiomas lógicos\(\Lambda\) y queremos comenzar a hacer matemáticas, vamos a querer agregar axiomas adicionales que están diseñados para permitirnos deducir declaraciones sobre cualquier sistema matemático que podamos tener en mente. Estos constituirán la colección de axiomas no lógicos,\(\Sigma\). Por ejemplo, si estamos trabajando en teoría de números, usando el lenguaje\(\mathcal{L}_{NT}\), junto con los axiomas lógicos también\(\Lambda\) vamos a querer usar otros axiomas que atañen a las propiedades de suma y a la relación de ordenación denotada por el símbolo\(<\). Estos axiomas adicionales son las fórmulas en las que colocaremos\(\Sigma\). Entonces, a partir de este conjunto ampliado de axiomas\(\Lambda \cup \Sigma\) intentaremos escribir deducciones de fórmulas que hagan declaraciones de interés teórico-numérico. Para reiterar:\(\Lambda\), se fijará el conjunto de axiomas lógicos, al igual que el acervo de reglas de inferencia. Pero el conjunto de axiomas no lógicos debe especificarse para cada deducción. En la sección actual exponemos únicamente los axiomas lógicos, abordando las reglas de inferencia en la Sección 2.4, y aplazando nuestra discusión de los axiomas no lógicos hasta la Sección 2.8.

Axiomas de Igualdad

Hemos tomado la ruta de asumir que el símbolo de igualdad\(=\),, es parte del lenguaje\(\mathcal{L}\). Hay tres grupos de axiomas que están diseñados para este símbolo. El primero solo dice que cualquier objeto es igual a sí mismo:

\[x = x \: \text{for each variable} \: x. \tag{E1}\]

Para el segundo grupo de axiomas, supongamos que\(x_1, x_2, \ldots, x_n\) son variables,\(y_1, y_2, \ldots, y_n\) son variables, y\(f\) es un símbolo de función\(n\) -aria.

\[\left[ \left( x_1 = y_1 \right) \land \left( x_2 = y_2 \right) \land \cdots \land \left( x_n = y_n \right) \right] \rightarrow \left( f \left( x_1, x_2, \ldots, x_n \right) = f \left( y_1, y_2, \ldots, y_n \right) \right). \tag{E2}\]

Los supuestos para el tercer grupo de axiomas son los mismos que para el segundo grupo, excepto que\(R\) se supone que es un símbolo de relación\(n\) -aria (\(R\)podría ser el símbolo de igualdad, que se ve como un símbolo de relación binaria).

\[\left[ \left( x_1 = y_1 \right) \land \left( x_2 = y_2 \right) \land \cdots \land \left( x_n = y_n \right) \right] \rightarrow \left( R \left( x_1, x_2, \ldots, x_n \right) \rightarrow R \rightarrow R \left( y_1, y_2, \ldots, y_n \right) \right). \tag{E3}\]

Los axiomas (E2) y (E3) son axiomas diseñados para permitir la sustitución de iguales por iguales. Nada más elegante que eso.

Axiomas cuantificadores

Los axiomas cuantificadores están diseñados para permitir una especie de entrada muy razonable en una deducción. Supongamos que sabemos\(\forall x P \left( x \right)\). Entonces, si\(t\) es algún término del idioma, deberíamos ser capaces de afirmar\(P \left( t \right)\). Para evitar problemas del tipo esbozado al inicio de la Sección 1.8, vamos a exigir que el término\(t\) sea sustituible por la variable\(x\).

\[\left( \forall x \phi \right) \rightarrow \phi_t^x, \: \text{if} \: t \: \text{is substitutable for} \: x \: \text{in} \: \phi. \tag{Q1}\]

\[\phi_t^x \rightarrow \left( \exists x \phi \right), \: \text{if} \: t \: \text{is substitutable for} \: x \: \text{in} \: \phi. \tag{Q2}\]

En muchos textos lógicos, el axioma (Q1) se llamaría instanciación universal, mientras que (Q2) se conocería como generalización existencial. Evitaremos este lenguaje impresionante y nos quedaremos con los más mundanos (Q1) y (Q2).

Recapitulación

Sólo para reunir todos los axiomas lógicos juntos en un solo lugar, vamos a expresarlos una vez más. El conjunto\(\Lambda\) de axiomas lógicos es la colección de todas las fórmulas que caen en una de las siguientes categorías:

\[x = x \: \text{for each variable} \: x. \tag{E1}\]

\[\left[ \left( x_1 = y_1 \right) \land \left( x_2 = y_2 \right) \land \cdots \land \left( x_n = y_n \right) \right] \rightarrow \left( f \left( x_1, x_2, \ldots, x_n \right) = f \left( y_1, y_2, \ldots, y_n \right) \right). \tag{E2}\]

\[\left[ \left( x_1 = y_1 \right) \land \left( x_2 = y_2 \right) \land \cdots \land \left( x_n = y_n \right) \right] \rightarrow \left( R \left( x_1, x_2, \ldots, x_n \right) \rightarrow R \left( y_1, y_2, \ldots, y_n \right) \right). \tag{E3}\]

\[\left( \forall x \phi \right) \rightarrow \phi_t^x, \: \text{if} \: t \: \text{is substitutable for} \: x \: \text{in} \: \phi. \tag{Q1}\]

\[\phi_t^x \rightarrow \left( \exists x \phi \right), \: \text{if} \: t \: \text{is substitutable for} \: x \: \text{in} \: \phi. \tag{Q2}\]

Observe que\(\Lambda\) es decidible. Podríamos escribir un programa de cómputos que, dada una fórmula\(\phi\), puede decidir en una cantidad finita de tiempo si\(\phi\) es o no un elemento de\(\Lambda\).