Fórmula bem formada - Well-formed formula

Em lógica matemática , lógica proposicional e lógica de predicados , uma fórmula bem formada , abreviada WFF ou wff , geralmente simplesmente fórmula , é uma sequência finita de símbolos de um determinado alfabeto que faz parte de uma linguagem formal . Uma linguagem formal pode ser identificada com o conjunto de fórmulas da linguagem.

Uma fórmula é um objeto sintático que pode receber um significado semântico por meio de uma interpretação. Dois usos principais de fórmulas são na lógica proposicional e na lógica de predicados.

Introdução

Um uso chave das fórmulas é na lógica proposicional e na lógica de predicados , como a lógica de primeira ordem . Nesses contextos, uma fórmula é uma cadeia de símbolos φ para a qual faz sentido perguntar "é φ verdadeiro?", Uma vez que quaisquer variáveis ​​livres em φ tenham sido instanciadas. Na lógica formal, as provas podem ser representadas por sequências de fórmulas com certas propriedades, e a fórmula final na sequência é o que é provado.

Embora o termo "fórmula" possa ser usado para marcas escritas (por exemplo, em um pedaço de papel ou quadro-negro), ele é mais precisamente entendido como a seqüência de símbolos sendo expressa, com as marcas sendo uma instância simbólica da fórmula. Assim, a mesma fórmula pode ser escrita mais de uma vez, e uma fórmula pode, em princípio, ser tão longa que não pode ser escrita de forma alguma dentro do universo físico.

As próprias fórmulas são objetos sintáticos. Eles recebem significados por meio de interpretações. Por exemplo, em uma fórmula proposicional, cada variável proposicional pode ser interpretada como uma proposição concreta, de modo que a fórmula geral expressa uma relação entre essas proposições. Uma fórmula não precisa ser interpretada, entretanto, para ser considerada apenas como uma fórmula.

Cálculo proposicional

As fórmulas do cálculo proposicional , também chamadas de fórmulas proposicionais , são expressões como . Sua definição começa com a escolha arbitrária de um conjunto V de variáveis ​​proposicionais . O alfabeto é constituído pelas letras em V , juntamente com os símbolos para os conectivos proposicional e parênteses "(" e ")", os quais são assumidos para não estar em V . As fórmulas serão certas expressões (isto é, cadeias de símbolos) sobre este alfabeto. ${\ displaystyle (A \ land (B \ lor C))}$

As fórmulas são definidas indutivamente da seguinte forma:

• Cada variável proposicional é, por si só, uma fórmula.
• Se φ é uma fórmula, então ¬φ é uma fórmula.
• Se φ e ψ são fórmulas e • é qualquer conectivo binário, então (φ • ψ) é uma fórmula. Aqui • poderia ser (mas não está limitado a) os operadores usuais ∨, ∧, → ou ↔.

Esta definição também pode ser escrita como uma gramática formal na forma Backus-Naur , desde que o conjunto de variáveis ​​seja finito:

<alpha set> ::= p | q | r | s | t | u | ... (the arbitrary finite set of propositional variables)
<form> ::= <alpha set> | ¬<form> | (<form>∧<form>) | (<form>∨<form>) | (<form>→<form>) | (<form>↔<form>)

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

((( p → q ) ∧ ( r → s )) ∨ (¬ q ∧ ¬ s ))

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

(( p → q ) → ( qq )) p ))

não é uma fórmula, porque não está em conformidade com a gramática.

Uma fórmula complexa pode ser difícil de ler, devido, por exemplo, à proliferação de parênteses. Para aliviar este último fenômeno, regras de precedência (semelhantes à ordem matemática padrão de operações ) são assumidas entre os operadores, tornando alguns operadores mais vinculativos do que outros. Por exemplo, assumindo a precedência (de mais vinculativo para menos vinculativo) 1. ¬ 2. → 3. ∧ 4. ∨. Então a fórmula

((( p → q ) ∧ ( r → s )) ∨ (¬ q ∧ ¬ s ))

pode ser abreviado como

p → q ∧ r → s ∨ ¬ q ∧ ¬ s

Esta é, no entanto, apenas uma convenção usada para simplificar a representação escrita de uma fórmula. Se a precedência fosse assumida, por exemplo, como associativa esquerda-direita, na seguinte ordem: 1. ¬ 2. ∧ 3. ∨ 4. →, então a mesma fórmula acima (sem parênteses) seria reescrita como

( p → ( q ∧ r )) → ( s ∨ ((¬ q ) ∧ (¬ s )))

Lógica de predicado

A definição de uma fórmula na lógica de primeira ordem é relativa à assinatura da teoria em questão. Essa assinatura especifica os símbolos constantes, símbolos de predicado e símbolos de função da teoria em questão, junto com as aridades dos símbolos de função e predicado. ${\ displaystyle {\ mathcal {QS}}}$

A definição de uma fórmula vem em várias partes. Primeiro, o conjunto de 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 símbolo constante da assinatura é um termo
3. uma expressão da forma f ( t ₁ ,…, t _n ), onde f é um símbolo de função n -ary e t ₁ ,…, t _n são termos, é novamente um termo.

A próxima etapa é 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 símbolo de predicado n -ary e t ₁ , ..., t _n são termos, então R ( t ₁ , ..., t _n ) é uma fórmula atômica

Finalmente, o conjunto de fórmulas é definido como o menor conjunto que contém o conjunto de fórmulas atômicas de modo que o seguinte seja válido:

1. ${\ displaystyle \ neg \ phi}$ é uma fórmula quando é uma fórmula ${\ displaystyle \ phi}$
2. ${\ displaystyle (\ phi \ land \ psi)}$ e são fórmulas quando e são fórmulas; ${\ displaystyle (\ phi \ lor \ psi)}$${\ displaystyle \ phi}$${\ displaystyle \ psi}$
3. ${\ displaystyle \ exists x \, \ phi}$ é uma fórmula quando é uma variável e é uma fórmula; ${\ displaystyle x}$${\ displaystyle \ phi}$
4. ${\ displaystyle \ forall x \, \ phi}$ é uma fórmula quando é uma variável e é uma fórmula (como alternativa, pode ser definida como uma abreviatura de ). ${\ displaystyle x}$${\ displaystyle \ phi}$${\ displaystyle \ forall x \, \ phi}$${\ displaystyle \ neg \ exists x \, \ neg \ phi}$

Se uma fórmula não tem ocorrências de ou , para qualquer variável , ela é chamada de livre de quantificador . Uma fórmula existencial é uma fórmula que começa com uma sequência de quantificação existencial seguida por uma fórmula livre de quantificador. ${\ displaystyle \ existe x}$${\ displaystyle \ forall x}$${\ displaystyle x}$

Fórmulas atômicas e abertas

Uma fórmula atômica é uma fórmula que não contém conectivos lógicos nem quantificadores ou, de forma equivalente, uma fórmula que não possui subfórmulas estritas. A forma precisa das fórmulas atômicas depende do sistema formal em consideração; para a lógica proposicional , por exemplo, as fórmulas atômicas são as variáveis ​​proposicionais . Para a lógica de predicado , os átomos são símbolos de predicado junto com seus argumentos, cada argumento sendo um termo .

De acordo com alguma terminologia, uma fórmula aberta é formada pela combinação de fórmulas atômicas usando apenas conectivos lógicos, com a exclusão de quantificadores. Isso não deve ser confundido com uma fórmula que não é fechada.

Fórmulas fechadas

Uma fórmula fechada , também moído fórmula ou frase , é uma fórmula na qual não existam ocorrências livres de qualquer variável . Se A é uma fórmula de uma linguagem de primeira ordem na qual as variáveis v ₁ , ..., v _n têm ocorrências livres, então Um precedido por v ₁ ⋯ v _n é um fecho de A . ${\ displaystyle \ forall}$${\ displaystyle \ forall}$

Propriedades aplicáveis ​​a fórmulas

• Uma fórmula A em um idioma é válida se for verdadeira para todas as interpretações de . ${\ displaystyle {\ mathcal {Q}}}$${\ displaystyle {\ mathcal {Q}}}$
• Uma fórmula A em uma linguagem é satisfatória se for verdadeira para alguma interpretação de . ${\ displaystyle {\ mathcal {Q}}}$${\ displaystyle {\ mathcal {Q}}}$
• Uma fórmula A da linguagem da aritmética é decidível se representar um conjunto decidível , ou seja, se houver um método eficaz que, dada uma substituição das variáveis ​​livres de A , diga que ou a instância resultante de A é demonstrável ou sua negação é .

Uso da terminologia

Em trabalhos anteriores sobre lógica matemática (por exemplo, por Church ), fórmulas referiam-se a quaisquer cadeias de símbolos e, entre essas cadeias, fórmulas bem formadas eram as cadeias que seguiram as regras de formação de fórmulas (corretas).

Vários autores simplesmente dizem fórmula. Usos modernos (especialmente no contexto da informática com software matemático, como damas modelo , provadores de teoremas automatizadas , provadores de teoremas interativos ) tendem a reter da noção de fórmula apenas o conceito algébrica e deixar a questão de boa formação , ou seja, de a representação concreta de fórmulas em string (usando este ou aquele símbolo para conectivos e quantificadores, usando esta ou aquela convenção de parênteses , usando notação polonesa ou infixa , etc.) como um mero problema de notação.

Embora a expressão fórmula bem formada ainda esteja em uso, esses autores não a usam necessariamente em oposição ao antigo sentido de fórmula , que não é mais comum na lógica matemática.

A expressão "fórmulas bem formadas" (WFF) também se infiltrou na cultura popular. WFF é parte de um trocadilho esotérico usado no nome do jogo acadêmico " WFF 'N PROOF : The Game of Modern Logic", de Layman Allen, desenvolvido enquanto ele estava na Escola de Direito de Yale (mais tarde ele foi professor na Universidade de Michigan ). O conjunto de jogos é projetado para ensinar os princípios da lógica simbólica às crianças (em notação polonesa ). Seu nome é um eco de whiffenpoof , uma palavra sem sentido usada como um elogio na Universidade de Yale que se tornou popular em The Whiffenpoof Song e The Whiffenpoofs .

Veja também

• Expressão fundamental

Notas

Referências

• Allen, Layman E. (1965), "Toward Autotelic Learning of Mathematical Logic by the WFF 'N PROOF Games", Mathematical Learning: Report of a Conference Patrocinado pelo Committee on Intellective Processes Research do 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 (4ª ed.), Cambridge University Press , ISBN   978-0-521-00758-0
• Ehrenberg, Rachel (primavera de 2002). "Ele é positivamente lógico" . Michigan hoje . Universidade de Michigan. Arquivado do original em 08/02/2009 . Página visitada em 2007-08-19 .
• Enderton, Herbert (2001), Uma introdução matemática à lógica (2ª ed.), Boston, MA: Academic Press , ISBN   978-0-12-238452-3
• Gamut, LTF (1990), Logic, Language, and Meaning, Volume 1: Introduction to Logic , University Of Chicago Press, ISBN   0-226-28085-3
• Hodges, Wilfrid (2001), "Classical Logic I: First-Order Logic", em Goble, Lou (ed.), 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 , MR   1950307
• 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

links externos

• Fórmula bem formada para lógica de predicado de primeira ordem - inclui um pequeno questionário Java .
• Fórmula bem formada em ProvenMath