Mostrar código-fonte de Fórmula bem formada

{{mais fontes|ciência=sim|data=abril de 2021}}
[[Imagem:Formula Bem Formada.png|300px|direita|Esse diagrama mostra as [[Sintaxe (lógica)|entidades sintáticas]] que podem ser construidas da [[linguagem formal]]. Os [[símbolo (formal)|símbolos]] e as [[Cadeia de caracteres|cadeias de caracteres]] podem ser  [[nonsense|formulações sem sentido]] ou fórmulas bem formadas. Uma linguagem formal pode ser interpretada como sendo o conjunto de suas fórmulas bem formadas. O conjunto de fórmulas bem formadas pode ser dividido em [[teorema]]s e não-teoremas.]]

Em [[lógica matemática]], uma '''fórmula bem formada''', abreviadamente '''fbf''', é uma [[Cadeia de caracteres|expressão]] (por exemplo, uma [[Sequência (matemática)|sequência]] finita de [[símbolo (formal)|símbolos]] de determinado [[Alfabeto (ciência da computação)|alfabeto]]) que é parte de uma [[Linguagem formal]].<ref>Fórmulas bem formadas são um tema padrão na introdução à lógica, e são cobertas por vários livros introdutórios, incluindo Enderton (2001), Gamut (1990), and Kleene (1967)</ref> Uma linguagem formal pode ser considerada como um conjunto contendo todas e apenas suas fórmulas.

Uma fórmula bem formada é um objeto formal [[Sintaxe (lógica)|sintático]] a que se pode dar um significado [[Semântica formal|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 "&phi; é verdadeiro?", uma vez que cada [[Variáveis livres e ligadas|variável livre]] em φ tenha sido instanciada. Em [[lógica formal]], [[Prova matemática|prova]]s 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 [[distinção caso-tipo| 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 [[Interpretação (lógica)|interpretada]]s como [[Proposição|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 [[Sintagma|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.

== Lógica proposicional ==
As fórmulas da [[lógica proposicional]], também chamadas de fórmulas proposicionais,<ref>Lógica de primeira ordem e teorema de prova automatizado, Melvin Fitting, Springer, 1996 [http://books.google.com/books?id=T8OMqvXvWWQC&lpg=PA11&dq=%22propositional%20formula%22&hl=fr&pg=PA11#v=onepage&q=%22propositional%20formula%22&f=false]</ref> são expressões como

<math>(A \land (B \lor C))</math>

Suas definições começam com a escolha arbitrária de um conjunto ''V'' de  [[Variável proposicional (matemática)|variáveis proposicionais]]. O alfabeto consiste das letras em ''V'' juntamente com os símbolos para os [[Conectivos lógicos|conectivo]]s 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 [[Definição recursiva|indutivamente]] definidas como se segue:
* Cada variável proposicional é, por si só, uma fórmula.
* Se φ é uma fórmula, então <math>\lnot</math>φ é 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 [[Formalismo de Backus-Naur|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> | <math>\neg</math><forma> | (<forma><math>\wedge</math><forma>) | (<forma><math>\vee</math><forma>) | (<forma><math>\rightarrow</math><forma>) | (<forma><math>\leftrightarrow</math><forma>)

Usando essa gramática, a sequência de símbolos
:(((''p'' <math>\rightarrow</math> ''q'') <math>\wedge</math> (''r'' <math>\rightarrow</math> ''s'')) <math>\vee</math> (<math>\neg</math>''q'' <math>\wedge</math> <math>\neg</math>''s''))
'''é uma fórmula bem formada''', porque é gramaticalmente correta. A sequência de símbolos
:((''p'' <math>\rightarrow</math> ''q'')<math>\rightarrow</math>(''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 de operações|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. <math>\neg</math> &nbsp; 2. <math>\rightarrow</math>&nbsp; 3. <math>\wedge</math>&nbsp; 4. <math>\vee</math>. Então a fórmula
:(((''p'' <math>\rightarrow</math> ''q'') <math>\wedge</math> (''r'' <math>\rightarrow</math> ''s'')) <math>\vee</math> (<math>\neg</math>''q'' <math>\wedge</math> <math>\neg</math>''s''))
pode ser abreviada como
:''p'' <math>\rightarrow</math> ''q'' <math>\wedge</math> ''r'' <math>\rightarrow</math> ''s'' <math>\vee</math> <math>\neg</math>''q'' <math>\wedge</math> <math>\neg</math>''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. <math>\neg</math> &nbsp; 2. <math>\wedge</math>&nbsp; 3. <math>\vee</math>&nbsp; 4. <math>\rightarrow</math>, então a mesma fórmula acima (sem parênteses) poderia ser reescrita como
:(''p'' <math>\rightarrow</math> (''q'' <math>\wedge</math> ''r'')) <math>\rightarrow</math> (''s'' <math>\vee</math> ((<math>\neg</math>''q'') <math>\wedge</math> (<math>\neg</math>''s'')))

== Lógica de primeira ordem ==
A definição de fórmula bem formada em [[lógica de primeira ordem]] <math>\mathcal{QS}</math> é semelhante à [[Assinatura (lógica)|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.
#Qualquer variável é um termo.
#Qualquer constante da assinatura é um termo.
#Uma expressão da forma ''f''(''t''<sub>1</sub>,...,''t''<sub>''n''</sub>), onde ''f'' é uma ''n''-ária função, e ''t''<sub>1</sub>,...,''t''<sub>''n''</sub> são termos , é, novamente, um termo.

O próximo passo é definir as [[Fórmula atômica|fórmulas atômicas]].
#Se ''t''<sub>1</sub> e ''t''<sub>2</sub> são termos, então ''t''<sub>1</sub>=''t''<sub>2</sub> é uma fórmula atômica
#Se ''R'' é um ''n''-ário símbolo de relação, e ''t''<sub>1</sub>,...,''t''<sub>''n''</sub> são termos, então ''R''(''t''<sub>1</sub>,...,''t''<sub>''n''</sub>) é 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:
#<math>\neg\phi</math> é uma fórmula quando <math>\ \phi</math> é uma fórmula
#<math>(\phi \land \psi)</math> e <math>(\phi \lor \psi)</math> são fórmulas quando <math>\ \phi</math> e <math>\ \psi</math> são fórmulas;
#<math>\exists x\, \phi</math> é uma fórmula quando <math>\ x</math> é uma variável e <math>\ \phi</math> é uma fórmula;
#<math>\forall x\, \phi</math> é uma fórmula quando <math>\ x</math> éuma variável e <math>\ \phi</math> é uma fórmula (alternativamente, <math>\forall x\, \phi</math> pode ser definido como uma abreviação para <math>\neg\exists x\, \neg\phi</math>).

Se uma fórmula não tem ocorrências de <math>\exists x</math> ou <math>\forall x</math>, para qualquer variável <math>\ x</math>, 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.

== Fórmulas atômicas e abertas ==
{{Artigo principal|Fórmula atômica}}

<!--According to some terminology, an open formula is formed by combining atomic formulas using only logical connectives, to the exclusion of quantifiers.[3] This has not to be confused with a formula which is not closed. -->

Uma fórmula atômica é aquela que não contém [[conectivos lógicos]] nem [[Quantificação|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ável proposicional|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.<ref>''Handbook of the history of logic''. Vol 5 - ''Logic from Russell to Church'', "Tarski's logic" por Keith Simmons, D. Gabbay e J. Woods Eds, p.568 [http://books.google.fr/books?id=K5dU9bEKencC&lpg=PA568&dq=%22open%20formula%22&pg=PA568#v=onepage&q=open%20formula&f=false].</ref> Isso não deve ser confundido com uma fórmula que não está fechada.

== Fórmulas fechadas ==
Uma ''fórmula fechada'', também conhecida como ''fórmula de [[átomo básico]]'' ou ''sentença'', é uma fórmula onde não há [[Variáveis livres e ligadas|ocorrências livres]] de nenhuma [[Variável (matemática)|variável]]. Se '''A''' é uma fórmula de uma linguagem de primeira ordem na qual as variáveis ''v<sub>1</sub>'', ..., ''v<sub>n</sub>'' tem ocorrências livres, então '''A''' precedida por ''v<sub>1</sub>'' ... ''v<sub>n</sub>'' é um encerramento de '''A'''.

== Propriedades aplicáveis às fórmulas ==
* Uma fórmula '''A''' numa linguagem <math>\mathcal{Q}</math> é ''[[Satisfatibilidade|válida]]'' se for verdadeira para toda [[Interpretação (lógica)|interpretação]] de <math>\mathcal{Q}</math>.
* Uma fórmula '''A''' numa linguagem <math>\mathcal{Q}</math> é ''[[Satisfatibilidade|satisfatível]]'' se ela for verdadeira para alguma [[Interpretação (lógica)|interpretação]] de <math>\mathcal{Q}</math>.
* Uma fórmula '''A''' da linguagem [[Axiomas de Peano|aritmética]] é ''decidível'' se representa um [[Conjunto recursivo|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 é.

== Uso da terminologia ==
Em trabalhos anteriores sobre [[lógica matemática]] (por exemplo, Church, [1996], (1944)<ref>Alonzo Church, [1996] (1944), ''Introduction to mathematical logic'', p. 49</ref>), 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".<ref>Hilbert, David; Ackermann, Wilhelm (1950) [1937], Principles of Mathematical Logic, New York: Chelsea</ref><ref>Hodges, Wilfrid (1997), A shorter model theory, Cambridge University Press, ISBN 978-0-521-58713-6</ref><ref>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</ref><ref>Cori, Rene; Lascar, Daniel (2000), Mathematical Logic: A Course with Exercises, Oxford University Press, ISBN 978-0-19-850048-3</ref> Usos modernos (especialmente no contexto de [[ciência da computação]] com [[software]]s matemáticos tais como [[verificadores de modelo]], [[Prova automática de teoremas|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 [[Ordem de operações|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,<ref>Enderton, Herbert [2001] (1972), A mathematical introduction to logic (2nd ed.), Boston, MA: Academic Press, ISBN 978-0-12-238452-3</ref><ref>R. L. Simpson (1999), Essentials of Symbolic Logic, page 12</ref><ref>Mendelson, Elliott [2010] (1964), An Introduction to Mathematical Logic (5th ed.), London: Chapman & Hall</ref> 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 [[Paranomásia|trocadilho]] esotérico usado no nome de um jogo acadêmico ''WFF 'N PROOF: The Game of Modern Logic,'' desenvolvido por Layman Allen,<ref>Ehrenburg 2002</ref> enquanto ele estava na [[Yale Law School|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).<ref>Mais apropriadamente, trata-se de [[lógica proposicional]] com o uso do [[estilo de Fitch]].</ref> O nome do jogo é uma alusão a  ''whiffenpoof'', uma [[Nonsense|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''.<ref>Allen (1965) agradece o trocadilho.</ref>

== Ver também ==
{{Portal|Logic}}
* [[Átomo básico]]

{{Referências|Notas e referências}}

== Referências ==
*{{citation
  |primeiro1 =Layman E.
  |último1 = Allen
  |título=Toward Autotelic Learning of Mathematical Logic by the WFF 'N PROOF Games
  |periódico= Mathematical Learning: Report of a Conference Sponsored by the Committee on Intellective Processes Research of the Social Science Research Council
  |series= Monographs of the Society for Research in Child Development
  |volume=30
  |número=1
  |ano=1965
  |páginas=29–41
}}
* {{Citation
  |último1 =Boolos
  |primeiro1 =George
  |último2 =Burgess
  |primeiro2 =John
  |último3 =Jeffrey
  |primeiro3 =Richard
  |título=Computability and Logic
  |publicado=[[Cambridge University Press]]
  |edição=4th
  | isbn=978-0-521-00758-0 (pb.)
  |ano=2002}}
* {{citar jornal
  |primeiro =Rachel
  |último =Ehrenberg
  |título=He's Positively Logical
  |data=primavera de 2002
  |publicado=University of Michigan
  | url=http://www.umich.edu/~newsinfo/MT/02/Spr02/mt9s02.html
  |obra=Michigan Today
  |acessodata=2007-08-19
}}
* {{Citation
  |último1 =Enderton
  |primeiro1 =Herbert
  |título=A mathematical introduction to logic
  |publicado=Academic Press
  |local=Boston, MA
  |edição=2nd
  | isbn=978-0-12-238452-3
  |ano=2001
}}
* {{Citation
  |último1 =Gamut
  |primeiro1 =L.T.F.
  |título=Logic, Language, and Meaning, Volume 1: Introduction to Logic
  |publicado= University Of Chicago Press
  |ano= 1990
  | isbn=0-226-28085-3
}}
*{{Citation
 |ultimo=Hodges
 |primeiro=Wilfrid
 |seção=Classical Logic I: First-Order Logic
 |editor-sobrenome1 =Goble
 |editor-nome1 =Lou
 |título=The Blackwell Guide to Philosophical Logic
 |publicado=Blackwell
 | isbn=978-0-631-20692-7
 |ano=2001
}}
*{{Citation
  |último1 =Hofstadter
  |primeiro1 =Douglas
  |autorlink1 =Douglas Hofstadter
  |título=Gödel, Escher, Bach: An Eternal Golden Braid
  |publicado=[[Penguin Books]]
  | isbn=978-0-14-005579-5
  |ano=1980
}}
* {{Citation
  |último1 =Kleene
  |primeiro1 =Stephen Cole
  |autorlink1 =Stephen Kleene
  |título=Mathematical logic
  |anooriginal=1967
  |publicado=[[Dover Publications]]
  |local=New York
  | isbn=978-0-486-42533-7
  | mr=1950307
  |ano=2002
}}
* {{Citation|último =Rautenberg|primeiro =Wolfgang|autorlink=Wolfgang Rautenberg|doi=10.1007/978-1-4419-1221-3|título=A Concise Introduction to Mathematical Logic|url=http://www.springerlink.com/content/978-1-4419-1220-6/|publicado=[[Springer Science+Business Media]]|local=[[New York City|New York]]|edição=3rd|isbn=978-1-4419-1220-6|ano=2010}}

== Ligações externas ==
*{{Link||2=http://www.cs.odu.edu/~toida/nerzic/content/logic/pred_logic/construction/wff_intro.html |3=Well-Formed Formula for First Order Predicate Logic |4=- inclui um [[quiz]] sobre [[Java (linguagem de programação)|Java]].}}
*{{Link||2=http://www.apronus.com/provenmath/formulas.htm |3=Well-Formed Formula at ProvenMath}}
*{{Link||2=http://wffnproof.com/ |3=WFF N PROOF game site}}
* [http://plato.stanford.edu/entries/types-tokens/#DisBetTypTok Types and Tokens]. Por Linda Wetzel. ''[[The Stanford Encyclopedia of Philosophy]]'' (Spring 2011 Edition), Edward N. Zalta (ed.).

{{lógica}}

{{Portal3|Matemática}}

{{DEFAULTSORT:Fórmula bem formada}}
[[Categoria:Ciência da computação]]
[[Categoria:Linguagens formais]]
[[Categoria:Metateoria]]
[[Categoria:Metafilosofia]]
[[Categoria:Dedução]]
[[Categoria:Lógica matemática]]