¿Existe una definición para variables libres y enlazadas en lógica?

Las variables libres y vinculadas se definen en el contexto de la sintaxis de la lógica de primer orden , considerando términos (es decir, "nombres" para objetos) y formularios (es decir, declaraciones).

La definición formal del conjunto.$\text {FV}(φ)$de variables libres de una fórmula$φ$es definido por :

todas las variables que aparecen en un término o fórmula atómica son libres.

$\text {FV}(¬φ) = \text {FV}(φ)$;

$\text {FV}(φ ∨ ψ) = \text {FV}(φ) \cup \text {FV}(ψ)$, (y lo mismo para los demás conectores binarios);

$\text {FV}(∀xφ) = \text {FV}(∃xφ) = \text {FV}(φ) \setminus \{ x \}$.

Una variable que no es libre está ligada .

Una fórmula$φ$se llama cerrado si$\text {FV}(φ)=\emptyset$.

en fórmula$\forall x P(x)$, La variable$x$está atado.

en fórmula$\forall x R(x,y)$La variable$x$está atado mientras que la variable$y$es gratis.

Una fórmula cerrada, cuando se interpreta, expresa una oración, es decir, tiene un valor de verdad definido.

$\forall n (n \ge 0)$es cierto en$\mathbb N$, mientras$\exists n (n < 0)$es falso en ella.

¿Cuál es el valor de verdad de una fórmula con una variable libre, como por ejemplo$(x > 0)$?

Depende... Depende del valor que le demos a la variable$x$.

Una variable libre actúa como un pronombre del lenguaje natural: su referencia debe identificarse según el contexto: si digo "es rojo", el valor de verdad del enunciado depende del objeto que estoy señalando con el dedo: el libro rojo o la pluma azul en mi mesa.

Del mismo modo, existen formas (definidas por las especificaciones semánticas formales del lenguaje de primer orden: ver función de asignación de variables ) para dar referencia "temporal" a variables libres de una fórmula.

Considere la fórmula:

$x+2=5$;

si sustituimos a$x$el (nombre del) número$3$, obtenemos una oración verdadera (es decir,$3+2=5$).

Si en cambio sustituimos a$x$el (nombre del) número$4$, obtenemos una oración falsa (es decir,$4+2=5$).

Una fórmula con var libre se llama "abierta" porque no tiene un significado (fijo): está "abierta a" diferentes interpretaciones; para darle significado, tenemos que transformarlo en una oración (es decir, una fórmula cerrada).

Desafortunadamente, las variables son realmente complicadas.

El problema de las variables surge mucho en informática con respecto a teorías como el cálculo lambda que maneja perfectamente la unión y la sustitución. Si permite un marco de lógica de orden superior de clasificación múltiple, puede axiomizar y definir cuantificadores en términos del cálculo lambda simplemente tipado. A un cuantificador sobre un dominio de discurso se le puede dar directamente un tipo de$\text{join} \colon (\text{domain} \rightarrow \text{prop}) \rightarrow \text{prop}$. Este fundamento de la teoría de tipos simples se utiliza en la práctica en probadores de teoremas como Isabelle/HOL. Consulte Las siete virtudes de la teoría de tipos simples para obtener un poco más de información.

El STLC no resuelve directamente el enlace de variables, pero proporciona un buen ejemplo para formalizar y generalizar. Una de las técnicas más simples para lidiar con la fealdad de las variables y capturar evitando la sustitución que se usa a menudo en la práctica en metateoría es el uso de índices de Bruijn. Básicamente, las variables se manejan como la indexación de números se indexa en el ámbito local y, por ejemplo, la función constante$\lambda x y. x$se convierte$\lambda. \lambda. 1$. Si está interesado en este tipo de cosas, hay una buena publicación de blog sobre carpetas de Jesper Cockx .

Si no está satisfecho con este tipo de enfoque, puede compilar el STLC a categorías cerradas cartesianas. Consulte Compilar en categorías por Conal Elliott . BCKW es probablemente un conjunto más tradicional de combinadores para compilar. Desafortunadamente, el tratamiento completo de la teoría de categorías de tipos dependientes y cuantificadores en términos de rebanadas y subobjetos es bastante extraño. Creo que realmente una de las únicas áreas en las que se usa un enfoque combinatorio en la práctica es el metateorema de comprensión de clases de la teoría de conjuntos NBG, donde las fórmulas para las clases se compilan hasta permutaciones de tuplas y demás.

Los enfoques más directos para tratar con variables son el área de la lógica algebraica. Probablemente desee consultar las Álgebras cilíndricas de Alfred Tarski, donde básicamente puede tratar los cuantificadores existenciales como una especie de operador modal. También hay otros enfoques del problema, como las álgebras poliádicas, pero tampoco los entiendo.

Por último, creo que debería mencionar el operador de descripción indefinida de Hilbert, que podría decirse que empeora algunos problemas con las variables al intercalar proposiciones y términos, pero puede simplificar la metateoría.$\varepsilon x. P(x)$se usa para describir "un término indefinido tal que P es verdadero". La cuantificación existencial se puede definir entonces como$\exists x. P(x) \equiv P(\varepsilon x. P(x))$.

No menciona el problema, pero además de las variables libres y vinculadas, también existen los problemas de las definiciones globales y locales y la expansión definitoria. En algunos casos, puede convertir definiciones locales en expresiones lambda.$\textbf{let} \, x := e \, \textbf{in} \, e' \equiv (\lambda x. e) e'$aunque por razones técnicas muy propias de los programas de ordenador esto no siempre funciona. El método más sucinto para tratar con variables globales podría ser abusar de un operador de descripción definida .

Además, esto no es realmente un problema para la lógica de primer orden, pero la ciencia de la computación necesita lidiar con el flujo de control/continuaciones como otro tipo de variable. Sin embargo, el enfoque como en el cálculo lambda bar mu mu-tilde no es determinista.

Espero haberlo convencido de que es posible, si no real, que alguien haya formalizado la captura evitando la sustitución de variables correctamente y que si usted es un Cylon puede Schonfinkle todo en un lío ilegible libre de carpetas de nombres. Desafortunadamente, las variables son realmente complicadas.