¿Cómo se corresponde la formalización finitamente axiomatizada de la lógica de predicados con la deducción natural para la lógica de predicados?

Question

Estoy realmente interesado en usar Metamath, pero Metamath viene con una versión funky de la lógica de predicados. La sustitución no está permitida en Metamath, así que Metamath emplea el sistema S2 de Tarski que está "finitamente axiomatizado", es decir, una axiomatización completa de la lógica de predicados que no requiere sustitución. En lugar de dar una mala explicación del teorema, puedes hacerte una idea con Artículo de Norm Megill sobre el tema y Artículo original de Tarski .

Estoy tan confundido acerca de cómo puedo utilizar este sistema para simular la lógica de predicados normal que ni siquiera estoy seguro de qué tipo de preguntas debo hacer aquí. Pero lo intentaré:

• Parece que sólo hay dos predicados en este sistema, $=$ y $\in$ . ¿Cómo podemos utilizarlos para obtener cualquier predicado que necesitemos?
• ¿Cómo podemos ampliar el sistema para obtener predicados con tres o más argumentos? ¿Y las funciones?
• ¿Existe algún recurso fácil que un principiante pueda utilizar para hacer corresponder la deducción natural tradicional en lógica de predicados que conoce con la S2 de Tarski?

Muchas gracias a todos por la ayuda.

Answer 1

El punto clave es que SI restringimos a sólo un número finito de símbolo de predicado (Megill utiliza sólo $\in$ además de la igualdad) podemos sustituir los axiomas "esquemáticos" por una lista finita.

Por ejemplo, el axioma de sustitución esquema para la igualdad : $x=y \to (\varphi[u/x] \to \varphi[u/y])$ puede sustituirse por los dos axiomas siguientes:

$x = y (x z y z)$ y $x = y (z x z y)$ .

Gestionan los dos únicos casos de atómica fórmulas utilizando $\in$ : $u \in z$ y $z \in u$ [el "patrón" es más claro si los escribimos como: $\in (x,u)$ y $\in (u,x)$ ], y son suficientes porque el caso "general" se puede demostrar por inducción.

Este "procedimiento" puede iterarse para cubrir un número finito de símbolos de predicado, porque sólo tenemos que gestionar un número finito de casos.

La "restricción" sólo a las fórmulas atómicas es necesaria para poner en práctica la idea de Tarski de evitar la compleja regla de sustitución (más exactamente: la sustitución adecuada, que se ocupa de los cuantificadores).

Según Página de Metamath: Apéndice 1: Nota sobre los axiomas :

El sistema de Tarski es exactamente equivalente a la formalización tradicional de los libros de texto, pero (mediante el uso inteligente de axiomas de igualdad) elimina las nociones primitivas de "sustitución adecuada" y "variable libre", sustituyéndolas por la sustitución directa y la noción de variable que no aparece en una fórmula (que expresamos con restricciones de variable distinta).

El truco consiste simplemente en que en una fórmula atómica siempre se permite la sustitución "simple", debido a la ausencia de cuantificadores.