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 determinado que forma parte de un lenguaje formal. 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 se encuentran en 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 cuales tiene sentido preguntar “¿es φ verdadera?”, una vez que se han instanciado las variables libres en φ. En lógica formal, las pruebas pueden representarse mediante secuencias de fórmulas con ciertas propiedades, y la fórmula final de la secuencia es lo que se prueba.

Aunque el término "fórmula" puede usarse para 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 una 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 "Uber die Definiciónen der mathematischen Grundbegriffe". Así, la misma fórmula puede escribirse más de una vez y, en principio, una fórmula puede ser tan larga que no puede escribirse en absoluto dentro del universo físico.

Las fórmulas en sí mismas son objetos sintácticos. Se les da 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 general exprese 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

Las fórmulas del cálculo proposicional, también llamadas fórmulas proposiciones, son expresiones como ()A∧ ∧ ()BAlternativa Alternativa C)){displaystyle (Aland (Blor C)}. Su definición comienza con la elección arbitraria de un conjunto V de variables proposicionales. El alfabeto consta de las letras en V junto con los símbolos para los conectores proposicionales y paréntesis "(" y ")", todos los cuales se supone que no están V. Las fórmulas serán ciertas expresiones (es decir, cuerdas de símbolos) sobre este alfabeto.

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 conectividad binaria, 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 de alfa■ ::= p Silencio q Silencio r Silencio s Silencio t Silencio u Silencio... (el conjunto finito arbitrario de variables proposicionales)
.forma■ ::= .conjunto de alfa■ ¬.forma■ Silencio.forma■∧.forma■Silencio..forma■Alternativa.forma■Silencio..forma■→.forma■Silencio..forma■Administración.forma■)

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 aliviar este último fenómeno, se asumen reglas de precedencia (similares al orden matemático estándar de las 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 fórmula

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

puede abreviarse como

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

Sin embargo, esto es sólo una convención utilizada para simplificar la representación escrita de una fórmula. Si se supusiera que la precedencia, por ejemplo, fuera 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 la lógica de primer orden QS{displaystyle {fnMithcal {}}} es relativo a la firma de la teoría a la mano. Esta firma especifica los símbolos constantes, símbolos predicados y símbolos de función de la teoría a mano, junto con las aridades de la función y símbolos predicados.

La definición de 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 n- Símbolo de función diario, y t₁,...t_n son términos, es otra vez 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 n- Símbolo predicado, 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 tales 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 ()φ φ Alternativa Alternativa ↑ ↑ ){displaystyle (phi lor psi)} son fórmulas cuando φ φ {displaystyle phi } y ↑ ↑ {displaystyle psi } son fórmulas;
3. ∃ ∃ xφ φ {displaystyle exists x,phi } es una fórmula cuando x{displaystyle x} es una variable y φ φ {displaystyle phi } es una fórmula;
4. О О xφ φ {displaystyle forall x,phi } es una fórmula cuando x{displaystyle x} es una variable y φ φ {displaystyle phi } es una fórmula (alternativamente, О О xφ φ {displaystyle forall x,phi } podría definirse como una abreviatura para ¬ ¬ ∃ ∃ x¬ ¬ φ φ {displaystyle neg exists x,neg phi }).

Si una fórmula no tiene ocurrencias de ∃ ∃ x{displaystyle exists x} o О О x{displaystyle forall x}, para cualquier variable x{displaystyle x}, entonces se llama quantifier-free. An fórmula existencial es una fórmula que comienza con una secuencia de cuantificación existencial seguida de una fórmula libre de cuantificadores.

Fórmulas atómicas y abiertas

Una fórmula atómica es una fórmula que no contiene conectivos 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 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 predicados 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 conectivos lógicos, excluyendo los cuantificadores. Esto no debe confundirse con una fórmula que no es cerrada.

Fórmulas cerradas

Una fórmula cerrada, también fórmula básica o oración, 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, luego A precedido por ∀v₁ ⋯ ∀v_n es una clausura de A.

Propiedades aplicables a las fórmulas

• Una fórmula A en un idioma Q{displaystyle {fnMithcal}} es válido si es verdad para cada interpretación de Q{displaystyle {fnMithcal}}.
• Una fórmula A en un idioma Q{displaystyle {fnMithcal}} es satisfizo si es verdad para alguna interpretación de Q{displaystyle {fnMithcal}}.
• Una fórmula A de la lengua aritmética es decidable si representa un conjunto decidable, es decir, si hay un método eficaz que, dada una sustitución de las variables libres de A, dice que o la instancia resultante de A es provable o su negación es.

Uso de la terminología

En trabajos anteriores sobre lógica matemática (por ejemplo, de Church), 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. Los usos modernos (especialmente en el contexto de la informática con software matemático como verificadores de modelos, probadores de teoremas automatizados, probadores de teoremas interactivos) tienden a retener de la noción de fórmula sólo el concepto algebraico y a dejar la cuestión de la buena formación, es decir, de la la representación en cadena concreta de fórmulas (usando este o aquel símbolo para conectivos 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.

Si bien la expresión fórmula bien formada todavía está en uso, estos autores no la usan necesariamente en contraposición al antiguo sentido de fórmula, que ya no es común. en lógica matemática.

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," por Layman Allen, 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). Su nombre es un eco de whiffenpoof, una palabra sin sentido utilizada como alegría en la Universidad de Yale y que se hizo popular en The Whiffenpoof Song y The Whiffenpoofs.