Fórmula bem formada

Esse diagrama mostra as entidades sintáticas que podem ser construidas da Linguagem formal. Os símbolos e as cadeias de caracteres podem ser amplamente divididas em nonsense e 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 podem ser amplamente divididos 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. 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

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 sequencias 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 bem formada" possa ser usado para marcas escritas (por exemplo, em um pedaço de papel ou um quadro-negro), o termo é mais precisamente entendido como uma sequência sendo expressa , por símbolos de instância da fórmula. Não é necesssária para a existência da fórmula que hajam símbolos dela. Uma linguagem formal pode, assim, ter um número infinito de fórmulas independentemente desde que cada fórmula tenha um símbolo a instanciando. Além disso, uma mesma Fórmula pode ter mais de um símbolo a instanciando, 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 nonsense,se os símbolos da linguagem são especificados para que isso aconteça. Além disso, uma fórmula nao precisa receber nenhuma interpretação.

Lógica proposicional

As fórmulas da Lógica proposicional, também chamadas de fórmulas proposicionais, 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 se presume que não estejam 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 ∨, ∧, →, or ↔.

Essa definição também pode ser escrita como uma gramática formal em Formalismo 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$ ($\neg$q $\wedge$ $\neg$s))

é 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$ ($\neg$q $\wedge$ $\neg$s))

pode ser abreviada como

p $\rightarrow$ q $\wedge$ r $\rightarrow$ s $\vee$ $\neg$q $\wedge$ $\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. $\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$ (($\neg$q) $\wedge$ ($\neg$s)))

Lógica de primeira ordem

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(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. $\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

Ver artigo principal: Fórmula atômica

Uma fórmula atômica é uma fórmula que não contém Conectivos lógicos nem quantificadores, ou equivalentemente, uma fórmula que não tem sub-fórmulas. A forma precisa das fórmulas atômicas depende do sistema formal sob consideração; para 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 em conjunto com seus argumentos, cada argumento sendo um termo.

De acordo com a terminologia, uma fórmula aberta é formada combinando fórmulas atômicas usando apenas conectivos lógicos, para a exclusão dos quantificadores. Isso não pode ser confundido com uma fórmula que não pode ser 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á 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.

Propriedades aplicáveis ​​às fórmulas

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

Uso da terminologia

Em trabalhos anteriores sobre lógica matemática (exemplo, por Church ), fórmulas se referem a quaisquer cadeias de símbolos e dentre esses símbolos, enquanto Fórmulas bem formadas são essas cadeias que seguem as regras de formação de fórmulas (corretas).

Vários autores falam simplesmente fórmula. Usos modernos (especialmente no contexto de ciência da computação com softwares matemáticostais como verificadores de modelo, provadores automáticos de teoremas, provadores de teoremas interativos) tendem a reter a noção de fórmula apenas ao conceito algébrico e deixar a questão de bem-formadas, isto é, o uso concreto da representação das fórmulas (usando esse ou aquele símbolo para conectivos e quantificadores, usando essa ou aquela oderm de operações, usando notação polonesa ou notação infix, etc.) como um mero problema de notação.

Entretanto, a expressão Fórmulas bem formadas ainda pode ser encontrada em diversos trabalhos, esses autores usando o termo Fórmula bem formada sem necessariamente à antigo noção de fórmula como uma cadeia arbitrária de simbolos de modo que ela não é mais comun em lógica matemática para se referir às cadeias arbritárias de símbolos da antiga noção de fórmulas.

A expressão "Fórmula bem formada" também foi impregnado na cultura popular. De fato, Fórmula bem formulada é [arte de uma paranomásia esóterica em nome de "WFF 'N PROOF: The Game of Modern Logic," por Layman Allen, desenvolvido enquanto ele estava na Escola de Direito de Yale (ele mais tarde foi professor na Universidade de Michigan). O conjunto de jogos é desenvolvido para ensinar os principios da lógica simbólica para crianças (em Notação polonesa). Seu nome é um eco de whiffenpoof, uma palavra sem sentido usada como um grito de guerra na Universidade Yale que tornou-se popular na Canção Whiffenpoof e do grupo musical dos graduandos de Yale The Whiffenpoofs.

Veja também

A Wikipédia possui o portal: Logic {{{Portal2}}} {{{Portal3}}} {{{Portal4}}} {{{Portal5}}}

• Átomo básico

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 (4th ed.), Cambridge University Press, ISBN 978-0-521-00758-0 (pb.) 
• Ehrenberg, Rachel. "He's Positively Logical", Michigan Today, University of Michigan, Spring 2002. Página visitada em 2007-08-19.
• Enderton, Herbert (2001), A mathematical introduction to logic (2nd ed.), Boston, MA: Academic Press, ISBN 978-0-12-238452-3 
• Gamut, L.T.F. (1990), Logic, Language, and Meaning, Volume 1: Introduction to Logic, University Of Chicago Press, ISBN 0-226-28085-3 
• Goble, Lou, ed. (2001), 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], Mathematical logic, New York: Dover Publications, ISBN 978-0-486-42533-7 
• Rautenberg, Wolfgang (2010), A Concise Introduction to Mathematical Logic (3rd ed.), New York: Springer Science+Business Media, doi:10.1007/978-1-4419-1221-3, ISBN 978-1-4419-1220-6, http://www.springerlink.com/content/978-1-4419-1220-6/ 

Links externos

• Well-Formed Formula for First Order Predicate Logic - includes a short Java quiz.
• Well-Formed Formula at ProvenMath
• WFF N PROOF game site