Esta página cita fontes, mas que não cobrem todo o conteúdo. Ajude a inserir referências (Encontre fontes: ABW  • CAPES  • Google (N • L • A)). (Abril de 2021)

Em lógica matemática, uma fórmula bem formada, abreviadamente fbf, é uma expressão (por exemplo, uma sequência finita de símbolos de determinado alfabeto) que é parte de uma Linguagem formal.^[1] Uma linguagem formal pode ser considerada como um conjunto contendo todas e apenas suas fórmulas.

Uma fórmula bem formada é um objeto formal sintático a que se pode dar um significado semântico.

Uma utilização chave das fórmulas bem formadas está na lógica proposicional e na lógica de predicados, tal como na lógica de primeira ordem. Nesses contextos, uma fórmula bem formada é um conjunto de símbolos φ que para cada um faz sentido perguntar "φ é verdadeiro?", uma vez que cada variável livre em φ tenha sido instanciada. Em lógica formal, provas podem ser representadas como sequências de fórmulas bem formadas com certas propriedades, e a última fórmula da sequência é o que está provado.

Embora o termo "fórmula" possa ser usada para marcas escritas (por exemplo, em um pedaço de papel ou num quadro-negro), ele é mais precisamente entendido como a sequência que está sendo expressa, com as marcas sendo um evento ou um caso (token) da fórmula. Não é necessária para a existência da fórmula que haja tokens reais dela. Uma linguagem formal pode, assim, ter um número infinito de fórmulas independentemente de cada fórmula ter um token. Além disso, uma mesma fórmula pode ter mais de um token, se ela for escrita mais de uma vez.

Fórmulas bem formadas são muitas vezes interpretadas como proposições (como, por exemplo, em Lógica proposicional). Porém, fórmulas bem formadas são entidades sintáticas e, assim devem ser especificadas numa linguagem formal sem levar em conta nenhuma interpretação. Uma fórmula interpretada pode ser o nome de algo, um adjetivo, um advérbio, uma preposição, uma frase, sentença imperativa, um conjunto de sentenças, um conjunto de nomes, etc. Uma fórmula pode até mesmo se tornar sem sentido se os símbolos da linguagem são especificados para que isso aconteça. Além disso, uma fórmula não precisa receber nenhuma interpretação.

As fórmulas da lógica proposicional, também chamadas de fórmulas proposicionais,^[2] são expressões como

${\displaystyle (A\land (B\lor C))}$

Suas definições começam com a escolha arbitrária de um conjunto V de variáveis proposicionais. O alfabeto consiste das letras em V juntamente com os símbolos para os conectivos e parênteses "(" e ")" - todos os quais, presume-se, não estão contidos em V. As fórmulas serão determinadas expressões (isto é, cadeias de símbolos) sobre este alfabeto.

As fórmulas são indutivamente definidas como se segue:

• Cada variável proposicional é, por si só, uma fórmula.
• Se φ é uma fórmula, então ${\displaystyle \lnot }$φ é uma fórmula.
• Se φ e ψ são fórmulas, e • é um conectivo binário, então ( φ • ψ) é uma fórmula. Aqui, • pode ser (mas não se limita a ser) os operadores ∨, ∧, →, ou ↔.

Essa definição também pode ser escrita como uma gramática formal na notação de Backus-Naur, desde que o conjunto de variáveis seja finito:

<conjunto alpha> ::= p | q | r | s | t | u | ... (o conjunto arbitrário finito de variáveis proposicionais)

<forma> ::= <conjunto alpha> | ${\displaystyle \neg }$<forma> | (<forma>${\displaystyle \wedge }$<forma>) | (<forma>${\displaystyle \vee }$<forma>) | (<forma>${\displaystyle \rightarrow }$<forma>) | (<forma>${\displaystyle \leftrightarrow }$<forma>)

Usando essa gramática, a sequência de símbolos

(((p ${\displaystyle \rightarrow }$ q) ${\displaystyle \wedge }$ (r ${\displaystyle \rightarrow }$ s)) ${\displaystyle \vee }$ (${\displaystyle \neg }$q ${\displaystyle \wedge }$ ${\displaystyle \neg }$s))

é uma fórmula bem formada, porque é gramaticalmente correta. A sequência de símbolos

((p ${\displaystyle \rightarrow }$ q)${\displaystyle \rightarrow }$(qq))p))

não é uma fórmula bem formada, porque não obedece à gramática.

Uma fórmula complexa pode ser difícil de ser lida, devido a, por exemplo, a proliferação de parênteses. Para aliviar este último fenômeno, regras de precedência (semelhante à ordem matemática de execução de operações) são assumidas entre os operadores, tornando alguns operadores mais vinculativos que outros. Por exemplo, assumindo a precedência (do mais vinculativo ao menos vinculativo) 1. ${\displaystyle \neg }$   2. ${\displaystyle \rightarrow }$  3. ${\displaystyle \wedge }$  4. ${\displaystyle \vee }$. Então a fórmula

(((p ${\displaystyle \rightarrow }$ q) ${\displaystyle \wedge }$ (r ${\displaystyle \rightarrow }$ s)) ${\displaystyle \vee }$ (${\displaystyle \neg }$q ${\displaystyle \wedge }$ ${\displaystyle \neg }$s))

pode ser abreviada como

p ${\displaystyle \rightarrow }$ q ${\displaystyle \wedge }$ r ${\displaystyle \rightarrow }$ s ${\displaystyle \vee }$ ${\displaystyle \neg }$q ${\displaystyle \wedge }$ ${\displaystyle \neg }$s

Isto é, porém, apenas uma convenção usada para simplificar a representação escrita da fórmula. Se a precedência for assumida, por exemplo, para ser esquerda-direita, na ordem: 1. ${\displaystyle \neg }$   2. ${\displaystyle \wedge }$  3. ${\displaystyle \vee }$  4. ${\displaystyle \rightarrow }$, então a mesma fórmula acima (sem parênteses) poderia ser reescrita como

(p ${\displaystyle \rightarrow }$ (q ${\displaystyle \wedge }$ r)) ${\displaystyle \rightarrow }$ (s ${\displaystyle \vee }$ ((${\displaystyle \neg }$q) ${\displaystyle \wedge }$ (${\displaystyle \neg }$s)))

A definição de fórmula bem formada em lógica de primeira ordem ${\displaystyle {\mathcal {QS}}}$ é semelhante à assinatura da teoria. Essa assinatura especifica as constantes, símbolos de relação, e símbolos de função dessa teoria, juntamente com suas aridades.

A definição de uma fórmula vem de partes individuais. Primeiro, o conjunto dos termos é definido recursivamente. Termos, informalmente, são expressões que representam objetos do domínio do discurso.

1. Qualquer variável é um termo.
2. Qualquer constante da assinatura é um termo.
3. Uma expressão da forma f(t₁,...,t_n), onde f é uma n-ária função, e t₁,...,t_n são termos , é, novamente, um termo.

O próximo passo é definir as fórmulas atômicas.

1. Se t₁ e t₂ são termos, então t₁=t₂ é uma fórmula atômica
2. Se R é um n-ário símbolo de relação, e t₁,...,t_n são termos, então R(t₁,...,t_n) é uma fórmula atômica

Finalmente, o conjunto de fórmulas é definindo como sendo o menor conjunto contendo o conjunto de fórmulas atômicas tal que seguem as seguintes regras:

1. ${\displaystyle \neg \phi }$ é uma fórmula quando ${\displaystyle \ \phi }$ é uma fórmula
2. ${\displaystyle (\phi \land \psi )}$ e ${\displaystyle (\phi \lor \psi )}$ são fórmulas quando ${\displaystyle \ \phi }$ e ${\displaystyle \ \psi }$ são fórmulas;
3. ${\displaystyle \exists x\,\phi }$ é uma fórmula quando ${\displaystyle \ x}$ é uma variável e ${\displaystyle \ \phi }$ é uma fórmula;
4. ${\displaystyle \forall x\,\phi }$ é uma fórmula quando ${\displaystyle \ x}$ éuma variável e ${\displaystyle \ \phi }$ é uma fórmula (alternativamente, ${\displaystyle \forall x\,\phi }$ pode ser definido como uma abreviação para ${\displaystyle \neg \exists x\,\neg \phi }$).

Se uma fórmula não tem ocorrências de ${\displaystyle \exists x}$ ou ${\displaystyle \forall x}$, para qualquer variável ${\displaystyle \ x}$, então ela é chamada livre de quantificadores. Uma fórmula existencial é uma fórmula começando com uma sequência de quantificação existencial seguida por uma fórmula livre de quantificadores.

Ver artigo principal: Fórmula atômica

Uma fórmula atômica é aquela que não contém conectivos lógicos nem quantificadores, ou seja, uma fórmula que não contém sub-fórmulas.

A forma exata das fórmulas atômicas depende do sistema formal considerado; para a lógica proposicional, por exemplo, as fórmulas atômicas são as variáveis proposicionais. Para lógica de predicados, os átomos são símbolos de predicados juntamente com seus argumentos - cada argumento sendo um termo.

De acordo com a terminologia, uma fórmula aberta é formada mediante a combinação de fórmulas atômicas, usando-se apenas conectivos lógicos, para a exclusão dos quantificadores.^[3] Isso não deve ser confundido com uma fórmula que não está fechada.

Uma fórmula fechada, também conhecida como fórmula de átomo básico ou sentença, é uma fórmula onde não há ocorrências livres de nenhuma variável. Se A é uma fórmula de uma linguagem de primeira ordem na qual as variáveis v₁, ..., v_n tem ocorrências livres, então A precedida por v₁ ... v_n é um encerramento de A.

• Uma fórmula A numa linguagem ${\displaystyle {\mathcal {Q}}}$ é válida se for verdadeira para toda interpretação de ${\displaystyle {\mathcal {Q}}}$.
• Uma fórmula A numa linguagem ${\displaystyle {\mathcal {Q}}}$ é satisfatível se ela for verdadeira para alguma interpretação de ${\displaystyle {\mathcal {Q}}}$.
• Uma fórmula A da linguagem aritmética é decidível se representa um conjunto decidível, isto é, se há algum método efetivo no qual, dada uma substituição de variáveis livres de A, tanto o resultado de A é provável como sua negação o é.

Em trabalhos anteriores sobre lógica matemática (por exemplo, Church, [1996], (1944)^[4]), fórmulas se referiam a quaisquer cadeias de símbolos e, entre essas cadeias, fórmulas bem formadas eram as cadeias que seguiam as regras de formação de fórmulas (corretas).

Vários autores dizem simplesmente "fórmula".^[5][6][7][8] Usos modernos (especialmente no contexto de ciência da computação com softwares matemáticos tais como verificadores de modelo, provadores automáticos de teoremas) tendem a reter da noção de fórmula apenas o conceito algébrico e deixar a questão da boa formação, isto é, da concreta representação de cadeia de fórmulas (usando este ou aquele símbolo como conectivos e quantificadores, usando esta ou aquela oderm de operações, usando notação polonesa ou notação infixa, etc.) como um mero problema de notação.

Entretanto, a "expressão fórmula bem formada" ainda pode ser encontrada em diversos trabalhos,^[9][10][11] em que os autores usam o termo "fórmula" ou "bem formada" sem opor necessariamente esses termos à antiga noção de fórmula como uma cadeia arbitrária de símbolos de modo que não é mais comum em lógica matemática referir-se a cadeias arbritárias de símbolos no antigo sentido de "fórmulas".

A expressão "fórmula bem formada" também acabou entrando na cultura popular. De fato, fórmula bem formulada é parte de uma trocadilho esotérico usado no nome de um jogo acadêmico WFF 'N PROOF: The Game of Modern Logic, desenvolvido por Layman Allen,^[12] enquanto ele estava na Escola de Direito de Yale (mais tarde, ele seria professor na Universidade de Michigan). A sequência de jogos foi concebida para ensinar os princípios da lógica simbólica para crianças (em notação polonesa).^[13] O nome do jogo é uma alusão a whiffenpoof, uma palavra nonsense usada como um grito de guerra na Universidade Yale e que se tornou popular na Whiffenpoof Song e de um grupo musical formado por graduandos de Yale, The Whiffenpoofs.^[14]

• Átomo básico

Notas e referências

• Allen, Layman E. (1965), «Toward Autotelic Learning of Mathematical Logic by the WFF 'N PROOF Games», Mathematical Learning: Report of a Conference Sponsored by the Committee on Intellective Processes Research of the Social Science Research Council, Monographs of the Society for Research in Child Development, 30 (1): 29–41 
• Boolos, George; Burgess, John; Jeffrey, Richard (2002), Computability and Logic, ISBN 978-0-521-00758-0 (pb.) Verifique |isbn= (ajuda) 4th ed. , Cambridge University Press 
• Ehrenberg, Rachel (primavera de 2002). «He's Positively Logical». Michigan Today. University of Michigan. Consultado em 19 de agosto de 2007 
• Enderton, Herbert (2001), A mathematical introduction to logic, ISBN 978-0-12-238452-3 2nd ed. , Boston, MA: Academic Press 
• Gamut, L.T.F. (1990), Logic, Language, and Meaning, Volume 1: Introduction to Logic, ISBN 0-226-28085-3, University Of Chicago Press 
• Hodges, Wilfrid (2001), Goble, Lou, ed., The Blackwell Guide to Philosophical Logic, ISBN 978-0-631-20692-7, Blackwell 
• Hofstadter, Douglas (1980), Gödel, Escher, Bach: An Eternal Golden Braid, ISBN 978-0-14-005579-5, Penguin Books 
• Kleene, Stephen Cole (2002) [1967], Mathematical logic, ISBN 978-0-486-42533-7, New York: Dover Publications, MR 1950307 
• Rautenberg, Wolfgang (2010), A Concise Introduction to Mathematical Logic, ISBN 978-1-4419-1220-6 3rd ed. , New York: Springer Science+Business Media, doi:10.1007/978-1-4419-1221-3 

• «Well-Formed Formula for First Order Predicate Logic». - inclui um quiz sobre Java. 
• «Well-Formed Formula at ProvenMath» 
• «WFF N PROOF game site» 
• Types and Tokens. Por Linda Wetzel. The Stanford Encyclopedia of Philosophy (Spring 2011 Edition), Edward N. Zalta (ed.).

• Portal da matemática