Fórmula bien formada

Secuencia finita de símbolos de un alfabeto dado que forma parte de un lenguaje formal.

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 que forma parte de un lenguaje formal . ^[1] Un lenguaje formal se puede identificar con el conjunto de fórmulas del lenguaje.

Una fórmula es un objeto sintáctico al que se le puede dar un significado semántico mediante una interpretación. Dos usos clave de las fórmulas son la lógica proposicional y la lógica de predicados.

Introducción

Un uso clave de las fórmulas es la lógica proposicional y la lógica de predicados, como la lógica de primer orden . En esos contextos, una fórmula es una cadena de símbolos φ para los que tiene sentido preguntar "¿es φ verdadero?", Una vez que se ha instanciado cualquier variable libre en φ. En lógica formal, las demostraciones se pueden representar mediante secuencias de fórmulas con ciertas propiedades, y la fórmula final de la secuencia es la que se prueba.

Aunque el término "fórmula" se puede utilizar para las marcas escritas (por ejemplo, en una hoja de papel o pizarra), se entiende más precisamente como la secuencia de símbolos que se expresan, siendo las marcas una instancia simbólica de la fórmula. Por lo tanto, la misma fórmula puede escribirse más de una vez y, en principio, una fórmula puede ser tan larga que no se puede escribir en absoluto dentro del universo físico.

Las fórmulas en sí mismas son objetos sintácticos. Reciben significados 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 general expresa una relación entre estas proposiciones. Sin embargo, no es necesario interpretar una fórmula para considerarla únicamente como una fórmula.

Cálculo proposicional

Artículo principal: cálculo proposicional

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

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

• Cada variable proposicional es, por sí sola, 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í • podría ser (pero no se limita a) los operadores habituales ∨, ∧, → o ↔.

Esta definición también se puede escribir como una gramática formal en forma 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) < formulario >  :: =  < conjunto alfa > | ¬ < formulario > | ( < formulario > ∧ < formulario > ) | ( < formulario > ∨ < formulario > ) | ( < formulario > → < formulario > ) | ( < formulario > ↔ < formulario > )

Usando 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 resultar difícil de leer debido, por ejemplo, a la proliferación de paréntesis. Para paliar este último fenómeno, se asumen reglas de precedencia (similares al orden matemático estándar de operaciones ) entre los operadores, lo que hace que algunos operadores sean más vinculantes que otros. Por ejemplo, asumiendo la precedencia (de más vinculante a menos vinculante) 1. ¬ 2. → 3. ∧ 4. ∨. Entonces la formula

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

puede abreviarse como

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

Sin embargo, esta 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 de izquierda a 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 )))

Lógica de predicados

La definición de una fórmula en lógica de primer orden es relativa a la firma de la teoría en cuestión. Esta firma 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 la función y los símbolos de predicado.${\displaystyle {\mathcal {QS}}}$

La definición de una fórmula se divide en varias partes. Primero, el conjunto de términos se define de forma recursiva. Los términos, informalmente, 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, de nuevo es 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 de modo que se cumple lo siguiente:

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

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

Fórmulas atómicas y abiertas

Artículo principal: fórmula atómica

Una fórmula atómica es una fórmula que no contiene conectivos lógicos ni cuantificadores , o lo que es lo mismo, una fórmula que no tiene subfórmulas estrictas. La forma precisa de las fórmulas atómicas depende del sistema formal considerado; 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 símbolos de predicado junto con sus argumentos, siendo cada argumento un término .

De acuerdo con alguna terminología, una fórmula abierta se forma combinando fórmulas atómicas utilizando solo conectivos lógicos, con exclusión de los cuantificadores. ^[3] Esto no debe confundirse con una fórmula que no es cerrada.

Fórmulas cerradas

Artículo principal: Sentencia (lógica)

Una fórmula cerrada , también tierra fórmula o frase , es una fórmula en la que no existen ocurrencias libres de cualquier variable de . Si A es una fórmula de un lenguaje de primer orden en el que las variables v ₁ , ..., v _n tener ocurrencias libres, entonces A precedido por v ₁ ⋯ v _n es un cierre de A .${\displaystyle \forall }$${\displaystyle \forall }$

Propiedades aplicables a fórmulas

• Una fórmula A en un idioma es válida si es cierta para todas las interpretaciones de .${\displaystyle {\mathcal {Q}}}$${\displaystyle {\mathcal {Q}}}$
• Una fórmula A en un idioma es satisfactoria si es cierta para alguna interpretación de .${\displaystyle {\mathcal {Q}}}$${\displaystyle {\mathcal {Q}}}$
• Una fórmula A del lenguaje aritmético es decidible si representa un conjunto decidible , es decir, si hay un método efectivo que, dada una sustitución de las variables libres de A , dice que la instancia resultante de A es demostrable o su negación es .

Uso de la terminología

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

Varios autores simplemente dicen fórmula. ^{[5] [6] [7] [8]} Los usos modernos (especialmente en el contexto de la informática con software matemático como verificadores de modelos , probadores automatizados de teoremas , probadores interactivos de teoremas ) tienden a retener de la noción de fórmula solo el concepto algebraico y dejar la cuestión de la forma bien formada , es decir, de la representación concreta en cadena de fórmulas (usando este o aquel símbolo para conectivos y cuantificadores, usando esta o aquella convención entre paréntesis , usando notación polaca o infija , etc.) como un mero problema de notación .

Si bien la expresión fórmula bien formada todavía está en uso, ^{[9] [10] [11]} estos autores no necesariamente ^{[ palabras de comadreja ] la} usan en contraposición al antiguo sentido de fórmula , que ya no es común en la lógica matemática. ^{[ cita requerida ]}

La expresión "fórmulas bien formadas" (WFF) también se coló en la cultura popular. WFF es parte de un juego de palabras esotérico utilizado en el nombre del juego académico " WFF 'N PROOF : The Game of Modern Logic", de Layman Allen, ^[12] desarrollado mientras estaba 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 ). ^[13] Su nombre es un eco de whiffenpoof , una palabra sin sentido usada para animar en la Universidad de Yale que se hizo popular en The Whiffenpoof Song.y The Whiffenpoofs . ^[14]

Ver también

• Expresión de tierra

Notas

1. Las fórmulas son un tema estándar en la lógica introductoria y están cubiertas por todos los libros de texto introductorios, incluidos Enderton (2001), Gamut (1990) y Kleene (1967)
2. Lógica de primer orden y demostración automatizada de teoremas, Melvin Fitting, Springer, 1996 [1]
3. Manual de historia de la lógica, (Vol. 5, Lógica de Russell a Church), Lógica de Tarski por Keith Simmons, D. Gabbay y J. Woods Eds, p568 [2] .
4. Alonzo Church, [1996] (1944), Introducción a la lógica matemática, página 49
5. Hilbert, David ; Ackermann, Wilhelm (1950) [1937], Principles of Mathematical Logic, Nueva York: Chelsea
6. Hodges, Wilfrid (1997), Una teoría de modelo más corta, Cambridge University Press, ISBN  978-0-521-58713-6
7. Barwise, Jon , ed. (1982), Handbook of Mathematical Logic, Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, ISBN 978-0-444-86388-1 
8. Cori, Rene; Lascar, Daniel (2000), Lógica matemática: un curso con ejercicios, Oxford University Press, ISBN 978-0-19-850048-3 
9. Enderton, Herbert [2001] (1972), Una introducción matemática a la lógica (2ª ed.), Boston, MA: Academic Press, ISBN 978-0-12-238452-3 
10. RL Simpson (1999), Fundamentos de la lógica simbólica, página 12
11. Mendelson, Elliott [2010] (1964), Introducción a la lógica matemática (5ª ed.), Londres: Chapman & Hall
12. Ehrenburg 2002
13. Más técnicamente, lógica proposicional utilizando el cálculo al estilo de Fitch .
14. Allen (1965) reconoce el juego de palabras.

Referencias

• Allen, Layman E. (1965), "Toward Autotelic Learning of Mathematical Logic by the WFF 'N PROOF Games", Aprendizaje matemático: Informe de una conferencia patrocinada por el Comité de Investigación de Procesos Intelectivos del Consejo de Investigación de Ciencias Sociales , Monografías Society for Research in Child Development, 30 (1): 29–41
• Boolos, George ; Burgess, John; Jeffrey, Richard (2002), Computability and Logic (4a ed.), Cambridge University Press , ISBN 978-0-521-00758-0
• Ehrenberg, Rachel (primavera de 2002). "Es positivamente lógico" . Michigan hoy . Universidad de Michigan. Archivado desde el original el 8 de febrero de 2009 . Consultado el 19 de agosto de 2007 .
• Enderton, Herbert (2001), Una introducción matemática a la lógica (2a 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: An Eternal Golden Braid , 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, Señor  1950307
• Rautenberg, Wolfgang (2010), A Concise Introduction to Mathematical Logic (3.a ed.), Nueva York : Springer Science + Business Media , doi : 10.1007 / 978-1-4419-1221-3 , ISBN 978-1-4419-1220-6

enlaces externos

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