Fórmula bien formada

En lógica matemática , lógica proposicional y lógica de predicados , una fórmula bien formada , abreviada WFF o wff , a menudo simplemente fórmula , es una secuencia finita de símbolos de un alfabeto dado , construida siguiendo la gramática definida de un lenguaje formal . ^{[ 1 ]}

La abreviatura wff se pronuncia "woof", o a veces "wiff", "weff" o "whiff". ^{[ 12 ]}

Un lenguaje formal se identifica con el conjunto de fórmulas que lo componen. Una fórmula es un objeto sintáctico al que se le puede asignar un significado semántico mediante una interpretación . Dos usos clave de las fórmulas se encuentran en la lógica proposicional y la lógica de predicados.

Un uso clave de las fórmulas se encuentra en la lógica proposicional y la lógica de predicados, como la lógica de primer orden . En estos contextos, una fórmula es una cadena de símbolos φ para la cual tiene sentido preguntar "¿es φ verdadera?", una vez que se han instanciado las variables libres en φ. En lógica formal, las demostraciones pueden representarse mediante secuencias de fórmulas con ciertas propiedades, y la fórmula final de la secuencia es la que se demuestra.

Aunque el término «fórmula» puede usarse para referirse a marcas escritas (por ejemplo, en un papel o una pizarra), se entiende con mayor precisión como la secuencia de símbolos que se expresa, siendo las marcas una instancia simbólica de la fórmula. Esta distinción entre la vaga noción de «propiedad» y la noción definida inductivamente de fórmula bien formada tiene sus raíces en el artículo de Weyl de 1910 «Über die Definitionen der mathematischen Grundbegriffe». ^{[ 13 ]} Así, la misma fórmula puede escribirse más de una vez, y una fórmula podría, en principio, ser tan larga que no pueda escribirse en absoluto dentro del universo físico.

Las fórmulas son, en sí mismas, objetos sintácticos. Adquieren significado mediante interpretaciones. Por ejemplo, en una fórmula proposicional, cada variable proposicional puede interpretarse como una proposición concreta, de modo que la fórmula en su conjunto expresa una relación entre dichas proposiciones. Sin embargo, una fórmula no necesita ser interpretada para ser considerada simplemente como tal.

Las fórmulas del cálculo proposicional , también llamadas fórmulas proposicionales , ^{[ 14 ]} son ​​expresiones tales como${\displaystyle (A\land (B\lor C))}$Su definición comienza con la elección arbitraria de un conjunto V de variables proposicionales . El alfabeto consta de las letras de V junto con los símbolos de los conectores proposicionales y los paréntesis "(" y ")", los cuales se supone que no pertenecen a V. Las fórmulas serán ciertas expresiones (es decir, cadenas de símbolos) sobre este alfabeto.

Las fórmulas se definen inductivamente de la siguiente manera:

• Cada variable proposicional es, por sí misma, una fórmula.
• Si φ es una fórmula, entonces ¬ φ es una fórmula.
• Si φ y ψ son fórmulas, y • es cualquier conectivo binario, entonces ( φ • ψ) es una fórmula. Aquí, • puede ser (pero no se limita a) los operadores habituales ∨, ∧, → o ↔.

Esta definición también puede escribirse como una gramática formal en forma de Backus-Naur , siempre que el conjunto de variables sea finito:

< conjunto alfa > ::= p | q | r | s | t | u | ... (el conjunto finito arbitrario de variables proposicionales) < forma > ::= < conjunto alfa > | ¬ < forma > | ( < forma > ∧ < forma > ) | ( < forma > ∨ < forma > ) | ( < forma > → < forma > ) | ( < forma > ↔ < forma > ) 

Utilizando esta gramática, la secuencia de símbolos

((( p → q ) ∧ ( r → s )) ∨ ( ¬ q ∧ ¬ s ))

es una fórmula, porque es gramaticalmente correcta. La secuencia de símbolos

(( p → q ) → ( qq )) p ))

no es una fórmula, porque no se ajusta a la gramática.

Una fórmula compleja puede ser difícil de leer, debido, por ejemplo, a la proliferación de paréntesis. Para mitigar este último problema, se asumen reglas de precedencia (similares al orden estándar de las operaciones matemáticas ) entre los operadores, haciendo que algunos operadores sean más vinculantes que otros. Por ejemplo, asumiendo la precedencia (de mayor a menor vinculación) 1. ¬  2. →  3. ∧  4. ∨ . Entonces la fórmula

((( p → q ) ∧ ( r → s )) ∨ ( ¬ q ∧ ¬ s ))

puede abreviarse como

p → q ∧ r → s ∨ ¬ q ∧ ¬ s

Sin embargo, esto es solo una convención utilizada para simplificar la representación escrita de una fórmula. Si se asumiera, por ejemplo, que la precedencia es asociativa izquierda-derecha, en el siguiente orden: 1. ¬  2. ∧  3. ∨  4. → ​​, entonces la misma fórmula anterior (sin paréntesis) se reescribiría como

( p → ( q ∧ r )) → ( s ∨ ( ¬ q ∧ ¬ s ))

La definición de una fórmula en lógica de primer orden${\displaystyle {\mathcal {QS}}}$es relativo a la signatura de la teoría en cuestión. Esta signatura especifica los símbolos constantes, los símbolos de predicado y los símbolos de función de la teoría en cuestión, junto con las aridades de los símbolos de función y predicado.

La definición de una fórmula consta de varias partes. Primero, el conjunto de términos se define recursivamente. Los términos, de manera informal, son expresiones que representan objetos del dominio del discurso .

1. Cualquier variable es un término.
2. Cualquier símbolo constante de la firma es un término
3. una expresión de la forma f ( t ₁ ,..., t _n ), donde f es un símbolo de función n-aria , y t ₁ ,..., t _n son términos, es de nuevo un término.

El siguiente paso es definir las fórmulas atómicas .

1. Si t ₁ y t ₂ son términos, entonces t ₁ = t ₂ es una fórmula atómica.
2. Si R es un símbolo de predicado n -ario, y t ₁ ,..., t _n son términos, entonces R ( t ₁ ,..., t _n ) es una fórmula atómica.

Finalmente, el conjunto de fórmulas se define como el conjunto más pequeño que contiene el conjunto de fórmulas atómicas tal que se cumple lo siguiente:

1. ${\displaystyle \neg \phi }$es una fórmula cuando${\displaystyle \phi }$es una fórmula
2. ${\displaystyle (\phi \land \psi )}$y${\displaystyle (\phi \lor \psi )}$son fórmulas cuando${\displaystyle \phi }$y${\displaystyle \psi }$son fórmulas;
3. ${\displaystyle \exists x\,\phi }$es una fórmula cuando${\displaystyle x}$es una variable y${\displaystyle \phi }$es una fórmula;
4. ${\displaystyle \forall x\,\phi }$es una fórmula cuando${\displaystyle x}$es una variable y${\displaystyle \phi }$es una fórmula (alternativamente,${\displaystyle \forall x\,\phi }$podría definirse como una abreviatura de${\displaystyle \neg \exists x\,\neg \phi }$).

Si una fórmula no tiene ocurrencias de${\displaystyle \exists x}$o${\displaystyle \forall x}$, para cualquier variable${\displaystyle x}$, entonces se llamalibre de cuantificadores . Una fórmula existencial es una fórmula que comienza con una secuencia de cuantificación existencial seguida de una fórmula libre de cuantificadores.

Una fórmula atómica es una fórmula que no contiene conectores lógicos ni cuantificadores , o equivalentemente, una fórmula que no tiene subfórmulas estrictas. La forma precisa de las fórmulas atómicas depende del sistema formal que se esté considerando; para la lógica proposicional , por ejemplo, las fórmulas atómicas son las variables proposicionales . Para la lógica de predicados , los átomos son los símbolos de predicado junto con sus argumentos, siendo cada argumento un término .

Según cierta terminología, una fórmula abierta se forma combinando fórmulas atómicas utilizando únicamente conectores lógicos, excluyendo los cuantificadores. ^{[ 15 ]} Esto no debe confundirse con una fórmula que no sea cerrada.

Una fórmula cerrada , también fórmula base o sentencia , es una fórmula en la que no hay ocurrencias libres de ninguna variable . Si A es una fórmula de un lenguaje de primer orden en el que las variables v ₁ , …, v _n tienen ocurrencias libres, entonces A precedida por ∀ v ₁ ⋯ ∀ v _n es un cierre universal de A.

• Una fórmula A en un idioma${\displaystyle {\mathcal {Q}}}$es válido si es cierto para cada interpretación de${\displaystyle {\mathcal {Q}}}$.
• Una fórmula A en un idioma${\displaystyle {\mathcal {Q}}}$es satisfacible si es verdadero para alguna interpretación de${\displaystyle {\mathcal {Q}}}$.
• Una fórmula A del lenguaje de la aritmética es decidible si representa un conjunto decidible , es decir, si existe un método efectivo que, dada una sustitución de las variables libres de A , dice que o bien la instancia resultante de A es demostrable o bien su negación lo es.

En trabajos anteriores sobre lógica matemática (por ejemplo, por Church ^{[ 16 ]} ), las fórmulas se referían a cualquier cadena de símbolos y, entre estas cadenas, las fórmulas bien formadas eran las que seguían las reglas de formación de fórmulas (correctas).

Varios autores simplemente dicen fórmula. ^{[ 17 ] [ 18 ] [ 19 ] [ 20 ]} Los usos modernos (especialmente en el contexto de la informática con software matemático como verificadores de modelos , demostradores de teoremas automatizados , demostradores de teoremas interactivos ) tienden a conservar de la noción de fórmula solo el concepto algebraico y a dejar la cuestión de la buena formación , es decir, de la representación de cadena concreta de fórmulas (usando este o aquel símbolo para conectores y cuantificadores, usando esta o aquella convención de paréntesis , usando notación polaca o infija , etc.) como un mero problema de notación.

La expresión «fórmulas bien formadas» (FBF) también se infiltró en la cultura popular. FBF forma parte de un juego de palabras esotérico utilizado en el nombre del juego académico « FBF 'N PROOF : El juego de la lógica moderna», de Layman Allen, ^{[ 21 ]} desarrollado mientras estudiaba en la Facultad de Derecho de Yale (más tarde fue profesor en la Universidad de Michigan ). El conjunto de juegos está diseñado para enseñar los principios de la lógica simbólica a los niños (en notación polaca ). ^{[ 22 ]} Su nombre es un eco de «whiffenpoof» , una palabra sin sentido utilizada como grito de ánimo en la Universidad de Yale , popularizada en «The Whiffenpoof Song» y «The Whiffenpoofs» . ^{[ 23 ]}

• Expresión del suelo
• Expresión bien definida
• Lenguaje formal
• Glosario de lógica
• WFF 'N Prueba

• Allen, Layman E. (1965), "Hacia el aprendizaje autotélico de la lógica matemática mediante los juegos WFF 'N PROOF", Aprendizaje matemático: Informe de una conferencia patrocinada por el Comité de Investigación de Procesos Intelectuales del Consejo de Investigación en Ciencias Sociales , Monografías de la Sociedad para la Investigación del Desarrollo Infantil, 30 (1): 29– 41
• Boolos, George ; Burgess, John; Jeffrey, Richard (2002), Computabilidad y lógica (4.ª  ed.), Cambridge University Press , ISBN 978-0-521-00758-0
• Ehrenberg, Rachel (Primavera de 2002). "Es sumamente lógico" . Michigan Today . Universidad de Michigan. Archivado del original el 8 de febrero de 2009. Consultado el 19 de agosto de 2007 .
• Enderton, Herbert (2001), Introducción matemática a la lógica (2.ª  ed.), Boston, MA: Academic Press , ISBN 978-0-12-238452-3
• Gamut, LTF (1990), Lógica, lenguaje y significado, Volumen 1: Introducción a la lógica , University of Chicago Press, ISBN 0-226-28085-3
• Hodges, Wilfrid (2001), «Lógica clásica I: Lógica de primer orden», en Goble, Lou (ed.), The Blackwell Guide to Philosophical Logic , Blackwell, ISBN 978-0-631-20692-7
• Hofstadter, Douglas (1980), Gödel, Escher, Bach: Una eterna trenza dorada , Penguin Books , ISBN 978-0-14-005579-5
• Kleene, Stephen Cole (2002) [1967], Lógica matemática , Nueva York: Dover Publications , ISBN 978-0-486-42533-7, MR 1950307 
• Rautenberg, Wolfgang (2010), Introducción concisa a la lógica matemática (3.ª  ed.), Nueva York: Springer Science+Business Media , doi : 10.1007/978-1-4419-1221-3 , ISBN 978-1-4419-1220-6

• Fórmula bien formada para la lógica de predicados de primer orden : incluye un breve cuestionario de Java .
• Fórmula bien formulada en ProvenMath