Em lógica e matemática , uma fórmula é uma série finita de objetos, dotados de propriedades particulares que tornam a sintaxe possível em todos esses campos.
Dado um conjunto E e uma função de peso p: E → N , uma fórmula é uma palavra extraída de E obtida pelas seguintes duas regras de construção:
Reconhecemos as "palavras significativas" que formam um subconjunto do monóide livre Lo (E) construído em E.
A notação teórica aqui apresentada é conhecida como Łukasiewicz ou “notação polonesa”; mas a notação comumente usada em álgebra e em análise é aquela com parênteses t (F 2 , ...., F n ); se t for de peso 2, escrevemos (F 1 ) t (F 2 ) em vez de tF 1 F 2 , e
[r (F 1 , ...., F m )] t [s (G 1 , ...., G n )] em vez de trF 1 .... F m sG 1 .... G n .
Dada uma fórmula F, qualquer intervalo de F que seja uma fórmula é uma sub-fórmula . Assim, F 1 , rF 1 .... F m , sG 1 .... G n são sub-fórmulas de trF 1 .... F m sG 1 .... G n .
Se F = tF 1 F 2 .... F n , os F i 1≤i≤n são as subfórmulas imediatas de F.
Em qualquer conjunto de fórmulas, a relação binária "F é uma subfórmula de G" é uma relação de ordem : reflexiva , antissimétrica e transitiva .
De tudo isso segue-se que a relação de inclusão nas ocorrências de subfórmulas de uma fórmula é uma ordem ramificada , ou árvore sintática , na qual, para qualquer elemento, os elementos anteriores são todos comparáveis.
As fórmulas são definidas em relação a uma linguagem formal , que é uma coleção de símbolos constantes de símbolos de função e símbolos de relação , onde cada um dos símbolos de funções e relação vem com uma aridade que indica o número de argumentos que ela leva.
Em seguida, definimos recursivamente um termo como
Finalmente, uma fórmula assume uma das seguintes formas:
Os primeiros dois casos são chamados de fórmulas atômicas .