Fórmula bem formada

Imagem: Jefferson Carlos De Bragança · BY-SA · Openverse

As fórmulas da lógica proposicional, também chamadas de fórmulas proposicionais, são expressões como ( A ∧ ( B ∨ C ) ) {\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: 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: Usando essa gramática, a sequência de símbolos é uma fórmula bem formada, porque é gramaticalmente correta. A sequência de símbolos 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

A definição de fórmula bem formada em lógica de primeira ordem Q S {\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. O próximo passo é definir as fórmulas atômicas. 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: Se uma fórmula não tem ocorrências de ∃ x {\displaystyle \exists x} ou ∀ x {\displaystyle \forall x} , para qualquer variável x {\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.

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

Em trabalhos anteriores sobre lógica matemática (por exemplo, Church, , (1944)), 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". 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, 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".