Una lógica de primer orden extendida con términos vinculantes como los descriptores de conjuntos familiares$\{x:\varphi\}$

Question

De primer orden de la lógica viene equipado con dos tipos de términos:

1. Variable: los términos de la forma $x$ de alguna variable $x$, de los cuales no son infinitos.
2. La función de la aplicación: los términos de la forma $f(t_1,\dots,t_n)$ para algunos $n$lugar de función símbolo $f$, de los cuales no son infinitos, y algunos $n$ términos de $t_1, \dots, t_n$.

En la práctica, una especie más de las que normalmente se utiliza de manera informal en el contexto de la teoría de conjuntos: conjunto de descriptores de la forma $\{x:\varphi\}$, donde $x$ es una variable, y $\varphi$ es de primer orden, bien formados fórmula. Este término no puede escribirse como una función de la aplicación, ya que $\varphi$ no es un término. Este término se crea un ámbito en el que la variable $x$ está vinculado, de forma similar a la cuantificado las fórmulas de la forma $\forall x\varphi$ e $\exists x\varphi$ trabajo.

Una forma de introducir conjunto de descriptores los términos de la lógica, que entonces ya no será un primer orden de la lógica, así que vamos a llamarlo extendido de primer orden de la lógica, es mediante la introducción de un conjunto infinito de la unión plazo de constructores , que es distinto, desde el primer orden de la lógica de vocabulario (que consiste en la lógica de los símbolos, variables, símbolos de función y relación de símbolos), y una nueva manera de formar términos: $Cx\varphi$, para cada enlace plazo constructor $C$, cada variable $x$, y cada extendido de primer orden, bien formados fórmula $\varphi$ (la definición de la función de la aplicación y de una bien formada fórmula debe ser modificado para dar cabida a este nuevo tipo de término). Vamos a llamar a tales términos términos de enlace.

Ahora podemos establecer a un lado uno de los novedosos unión plazo de constructores, decir $\sigma$, e interpretar cada unión término de la forma $\sigma x\varphi$ como $\{x:\varphi\}$.

Conjunto de descriptores son probablemente el ejemplo más familiar de los términos de enlace, pero hay otros dos que conozco que se han propuesto en el pasado por los principales matemáticos, igual que en el contexto de la teoría de conjuntos: de Hilbert epsilon operador y Bourbaki s $\tau$ operador, que, aunque similares, no son el mismo operador, como que satisfacer ligeramente diferentes axiomas.

Tenga en cuenta que la ampliación de la lógica de primer orden con condiciones vinculantes requiere la extensión correspondiente del sistema de inferencia, decir Gentzen de la Deducción Natural.

Tiene la combinación de extendido de primer orden de la lógica, con el correspondiente sistema de inferencia se ha estudiado? ¿Tiene un nombre? Donde puedo leer mas sobre esto?

Answer 1

Esta es una excelente pregunta, y es algo que debe ser tratada explícitamente en la lógica básica de los textos (y en mi experiencia, no lo es). Lamentablemente, o de forma satisfactoria en función de lo que buscas, de la lógica de primer orden ya es suficiente - al menos, inicialmente (ver debajo de la tapa).

Todos los constructores de las que estamos hablando son definibles en un sentido apropiado, y para que puedan ser implementadas en el estándar de la lógica de primer orden con sólo ajustar la sintaxis adecuada: básicamente, nos gustaría añadir infinitamente muchos de los nuevos símbolos de la función, cada uno correspondiente a una instancia de la deseada constructor, y los axiomas diciendo cómo funcionan. En todos los ejemplos que usted ha descrito, esto se puede hacer sin dificultad.

Por ejemplo, echemos un vistazo a la de Hilbert $\epsilon$-operador. En lugar de tener una sola $\epsilon$, vamos a tener un $\epsilon_A$ para cada fórmula $A$ con al menos una variable libre, y estos se comportan de la siguiente forma:

• El caso más sencillo es de una sola variable (por lo tanto, el parámetro libre) $A$. En este caso, $\epsilon_A$ es nullary - es sólo una constante. Y nuestra correspondiente axioma es $$\exists xA(x)\implies A(\epsilon_A).$$

• Veamos ahora el caso en que $A$ tiene dos variables libres, $x$ e $y$. Es posible que ahora quiero escribir algo que para cada una de las $b$ coge $a$ tal que $A(a,b)$ tiene (si $a$ existe). Así que nuestro $\epsilon_A$ es ahora una única función, y la correspondiente axioma es $$\forall y(\exists xA(x,y)\implies A(\epsilon_A(y),y)).$$

• Más generalmente, una $(n+1)$-ary $A$ los rendimientos de una $n$-ary $\epsilon_A$, con el correspondiente axioma $$\forall y_1,...,y_n(\exists xA(x,y_1,...,y_n)\implies A(\epsilon_A(y_1,...,y_n), y_1,...,y_n)).$$

Observe la similitud entre este tipo de aplicación y las funciones de Skolem - es exactamente la misma idea. Por cierto, es en este punto podría decirse que mejor adoptar una versión de la lógica de primer orden que permite funciones parciales y vacío estructuras, sólo por la simplicidad; el deductivo aparato de curso se hace más molesto, pero muy manageably así, y se puede limpiar en ciertos aspectos. Pero eso no es un punto esencial.

---

Por supuesto, hay una pregunta más general aquí que el anterior no dirección: de lo que si estamos buscando una teoría general que permite (esencialmente) formas arbitrarias para construir los términos de las fórmulas?

En este caso parece que no hay, en realidad no se mucho de literatura por ahí. Me pidió un MO pregunta acerca de esto hace un tiempo, ya que este es un tema que ya he empezado a trabajar y yo quería evitar reinventar la rueda. Algunos modelo básico de la teoría de la resultante lógica es bastante fácil de preparar, pero parece que no se han hecho explícitamente aún, el trabajo existente parece ser en la ciencia de la computación lado, y no se centra en estos temas. (Por cierto, Andrej la respuesta a esa pregunta es un gran ejemplo de cómo los lógicos, debe prestar atención a la ciencia de la computación.)

Si estás interesado, te puedo decir lo que sé acerca de la resultante lógica. Pero que se vuelve un poco lejos para esta respuesta, lo voy a dejar aquí por ahora.

(Por cierto, parece que me olvidé de mencionar el motivo específico en que se trate; brevemente, yo era - y soy - jugando con el resumen de la numeración de Gödel nociones en el contexto de generalizada de la teoría de la recursividad.)

Answer 2

En plural lógica que hacer una cosa similar pero sin el singularismo que es inherente en el conjunto de la notación. Las obras de la ampliación mediante la adición de términos en plural ( "las soluciones a $x^2 - 4 = 0$", "estados-nación", "los soldados que rodean el fuerte").

Lo que es especialmente interesante es la expansión natural de los descriptores: además de la notoria Russel definitiva (en singular) descripción, agregar descripción exhaustiva $x:\phi x$ ( en tu ejemplo "la $x$s que singularmente $\phi$), plural descripción definitiva y plural descripción exhaustiva.

¿Responde esto a tu pregunta de alguna manera?