Lógica de predicados
# Lógica de predicados

Para o termo específico, ver Lógica de primeira ordem
Na lógica matemática, a lógica de predicados é um termo genérico para sistemas formais simbólicos como lógica de primeira ordem, lógica de segunda ordem, many-sorted logic ou infinitary logic. Este sistema formal se distingue de outros sistemas em que suas fórmulas contêm variáveis que podem ser quantificadas. Dois quantificadores comuns são: os quantificadores existencial ∃ ("existe um") e universal ∀ ("para todo"). As variáveis poderiam ser elementos no domínio do discurso, ou talvez as relações ou funções sobre este universo. Por exemplo, um quantificador existencial sobre um símbolo de função poderia ser interpretado como um modificador "Existe uma função".
No uso informal, o termo "lógica de predicados" ocasionalmente se refere à lógica de primeira ordem. Alguns autores consideram que o cálculo de predicados seja a forma axiomática da lógica de predicados, e a lógica de predicados para ser derivado de uma informal, num desenvolvimento mais intuitivo.
Na lógica de predicados também se incluem lógicas misturando operadores modais e quantificadores. Ver lógica modal, Saul Kripke, fórmulas Barcan Marcus, A. N. Prior e Nicholas Rescher.

## Sintaxe

Símbolos de cálculos de predicados podem representar tanto variáveis, constantes, funções ou predicados.
* Constantes nomes específicos de objetos ou propriedades no domínio do discurso Universo de discurso. Portanto, Paulo, folha, altura e azul são exemplos de símbolos constantes bem-formadas. As constantes $\top$ (verdadeiro) e $\bot$ (falso) são incluídas algumas vezes.
* Símbolos de variáveis são usados ​​para designar classes gerais, objetos ou propriedades no domínio do discurso.
* Funções denotam um mapeamento de um ou mais elementos de um conjunto (chamado de domínio da função) em um único elemento de outro conjunto(o alcance da função). Elementos do domínio de uma função e o alcance são objetos no mundo de discurso. Todo símbolo de função tem uma associação de aridade, indicando o número de elementos do domínio mapeados em cada elemento do alcance.
Uma expressão da função é um símbolo de função seguido por seus argumentos. Os argumentos são elementos do domínio de uma função; o número de argumentos é a aridade da função. Os argumentos ficam dentro dos parênteses, separados por vírgulas, por exemplo:
* f(X,Y)
* pai(david)
* preço(apple)
todas as expressões acima são expressões bem-formadas (EBF).
Lógica de predicados podem ser visualizadas sintaticamente pela gramática de Noam Chomsky. Como tal, lógica de predicados (assim como lógicas modais e mistura de modais da lógica de predicados) podem ser vistas numa gramática sensível ao contexto, ou mais tipicamente livre de contexto. Cada um dos quatro tipos da gramática de Chomsky têm uma equivalência na Teoria dos autômatos, portanto estas lógicas podem ser vistas como autômatos também.