Fórmula bem formada

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
Esse diagrama mostra as entidades sintáticas que podem ser construidas da linguagem formal. Os símbolos e as cadeias de caracteres podem ser 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 teoremas e não-teoremas.

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.

Introdução[editar | editar código-fonte]

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.

Lógica proposicional[editar | editar código-fonte]

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

(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 \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> | \neg<forma> | (<forma>\wedge<forma>) | (<forma>\vee<forma>) | (<forma>\rightarrow<forma>) | (<forma>\leftrightarrow<forma>)

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

(((p \rightarrow q) \wedge (r \rightarrow s)) \vee (\negq \wedge \negs))

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

((p \rightarrow q)\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. \neg   2. \rightarrow  3. \wedge  4. \vee. Então a fórmula

(((p \rightarrow q) \wedge (r \rightarrow s)) \vee (\negq \wedge \negs))

pode ser abreviada como

p \rightarrow q \wedge r \rightarrow s \vee \negq \wedge \negs

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. \neg   2. \wedge  3. \vee  4. \rightarrow, então a mesma fórmula acima (sem parênteses) poderia ser reescrita como

(p \rightarrow (q \wedge r)) \rightarrow (s \vee ((\negq) \wedge (\negs)))

Lógica de primeira ordem[editar | editar código-fonte]

A definição de fórmula bem formada em lógica de primeira ordem \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(t1,...,tn), onde f é uma n-ária função, e t1,...,tn são termos , é, novamente, um termo.

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

  1. Se t1 e t2 são termos, então t1=t2 é uma fórmula atômica
  2. Se R é um n-ário símbolo de relação, e t1,...,tn são termos, então R(t1,...,tn) é 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. \neg\phi é uma fórmula quando \ \phi é uma fórmula
  2. (\phi \land \psi) e (\phi \lor \psi) são fórmulas quando \ \phi e \ \psi são fórmulas;
  3. \exists x\, \phi é uma fórmula quando \ x é uma variável e \ \phi é uma fórmula;
  4. \forall x\, \phi é uma fórmula quando \ x éuma variável e \ \phi é uma fórmula (alternativamente, \forall x\, \phi pode ser definido como uma abreviação para \neg\exists x\, \neg\phi).

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

Fórmulas atômicas e abertas[editar | editar código-fonte]


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.

Fórmulas fechadas[editar | editar código-fonte]

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 v1, ..., vn tem ocorrências livres, então A precedida por v1 ... vn é um encerramento de A.

Propriedades aplicáveis ​​às fórmulas[editar | editar código-fonte]

Uso da terminologia[editar | editar código-fonte]

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]

Ver também[editar | editar código-fonte]

Portal A Wikipédia possui o portal:
  • Logic

Notas[editar | editar código-fonte]

  1. 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)
  2. Lógica de primeira ordem e teorema de prova automatizado, Melvin Fitting, Springer, 1996 [1]
  3. 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 [2].
  4. Alonzo Church, [1996] (1944), Introduction to mathematical logic, p. 49
  5. Hilbert, David; Ackermann, Wilhelm (1950) [1937], Principles of Mathematical Logic, New York: Chelsea
  6. Hodges, Wilfrid (1997), A shorter model theory, 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), Mathematical Logic: A Course with Exercises, Oxford University Press, ISBN 978-0-19-850048-3
  9. Enderton, Herbert [2001] (1972), A mathematical introduction to logic (2nd ed.), Boston, MA: Academic Press, ISBN 978-0-12-238452-3
  10. R. L. Simpson (1999), Essentials of Symbolic Logic, page 12
  11. Mendelson, Elliott [2010] (1964), An Introduction to Mathematical Logic (5th ed.), London: Chapman & Hall
  12. Ehrenburg 2002
  13. Mais apropriadamente, trata-se de lógica proposicional com o uso do estilo de Fitch.
  14. Allen (1965) agradece o trocadilho.

Referências[editar | editar código-fonte]

Ligações externas[editar | editar código-fonte]