 | Este artigo carece dereciclagem de acordo com olivro de estilo. Sinta-se livre para editá-lo(a) para que este(a) possa atingir umnível de qualidade superior. |
 | Esta páginacita fontes, mas quenão cobrem todo o conteúdo. Ajude ainserir referências (Encontre fontes:Google (N • L • A • I • WP refs) • ABW • CAPES). |
Alógica de primeira ordem (LPO), conhecida também comocálculo de predicados de primeira ordem (CPPO),[1] é um sistema lógico que estende alógica proposicional[2] (lógica sentencial) e que é estendida pelalógica de segunda ordem.
Assentenças atômicas da lógica de primeira ordem têm o formatoP (t1,…,tn) (um predicado com um ou mais "argumentos") ao invés de serem símbolos sentenciais sem estruturas.
O ingrediente novo da lógica de primeira ordem não encontrado na lógica proposicional é aquantificação: dada uma sentença φ qualquer, as novas construções e -- leia "para todox, φ" e "para algumx, φ", respectivamente—são introduzidas. significa que φ é verdadeiro para todo valor dex e significa que há pelo menos umx tal que φ é verdadeiro. Os valores das variáveis são tirados de umuniverso de discurso pré-determinado. Um refinamento da lógica de primeira ordem permite variáveis de diferentes tipos, para tratar de diferentes classes de objetos.
A lógica de primeira ordem tem poder expressivo suficiente para formalizar praticamente toda a matemática. Umateoria de primeira ordem consiste em um conjunto deaxiomas (geralmente finito ourecursivamente enumerável) e de sentenças dedutíveis a partir deles. Ateoria dos conjuntos deZermelo-Fraenkel é um exemplo de uma teoria de primeira ordem, e aceita-se geralmente que toda amatemática clássica possa ser formalizada nela. Há outras teorias que são normalmente formalizadas na lógica de primeira ordem de maneira independente(embora elas admitam a implementação na teoria dos conjuntos) tais como aaritmética de Peano.
Um cálculo de predicados consiste em:
Osaxiomas considerados aqui são os axiomaslógicos que fazem parte do cálculo de predicados. Além disso, os axiomasnão-lógicos são adicionados em teorias de primeira ordem específicas: estes não são considerados como verdades da lógica, mas como verdades da teoria particular sob consideração.
Quando o conjunto dos axiomas é infinito, requer-se que haja um algoritmo que possa decidir para uma fórmula bem-formada dada, se ela é um axioma ou não. Deve também haver um algoritmo que possa decidir se uma aplicação dada de umaregra de inferência está correta ou não.
É importante notar que o cálculo de predicados pode ser formalizado de muitas maneiras equivalentes; não há nada canônico sobre os axiomas e as regras de inferência propostos aqui, mas toda a formalização dará origem aos mesmos teoremas da lógica (e deduzirá os mesmos teoremas a partir de um conjunto qualquer de axiomasnão-lógicos).
O alfabeto de primeira ordem,, tem a seguinte constituição:
, onde
As constantes, sinais funcionais e sinais predicativos constituem a coleção de sinais ditos símbolos não lógicos.
Há diversas variações menores listadas abaixo:
Os conjuntos das constantes, das funções, e das relações compõem aassinatura e são geralmente considerados para dar forma a uma linguagem, enquanto as variáveis, os operadores lógicos, e os quantificadores são geralmente considerados para pertencer à lógica. Umaestrutura dá o significado semântico de cada símbolo da assinatura. Por exemplo, a linguagem dateoria dos grupos consiste de uma constante (elemento da identidade), de uma função de aridade 1 (inverso), de uma função de aridade 2 (produto), e de uma relação de aridade 2 (igualdade), que seria omitida pelos autores que incluem a igualdade na lógica subjacente.
Asregras de formação definem os termos, fórmulas, e as variáveis livres como segue.O conjunto dostermos é definido recursivamente pelas seguintes regras:
O conjunto dasfórmulas bem-formadas (chamadas geralmente FBFs ou apenas fórmulas) é definido recursivamente pelas seguintes regras:
Na prática, seP for uma relação de aridade 2, nós escrevemos frequentemente "a P b" em vez de "P a b"; por exemplo, nós escrevemos 1 < 2 em vez de < (1 2). Similarmente sef for uma função de aridade 2, nós escrevemos às vezes "a f b" em vez de "f (a b)"; por exemplo, nós escrevemos 1 + 2 em vez de + (1 2). É também comum omitir alguns parênteses se isto não conduzir à ambigüidade.Às vezes é útil dizer que "P (x) vale para exatamente umx", o que costuma ser denotado por ∃!xP(x). Isto também pode ser expresso por ∃x (P (x) ∀y (P (y) → (x =y))).
Exemplos: A linguagem dos grupos abelianos ordenados tem uma constante 0, umafunção unária −, umafunção binária +, e umarelação binária ≤. Assim:
Set é um termo e φ(x) é uma fórmula que contém possivelmentex como uma variável livre, então φ(t) se definido como o resultado da substituição de todas as instâncias livres dex port,desde que nenhuma variável livre det se torne ligada neste processo. Se alguma variável livre det se tornar ligada, então para substituirt porx é primeiramente necessário mudar os nomes das variáveis ligadas de φ para algo diferente das variáveis livres det. Para ver porque esta condição é necessária, considere a fórmula φ(x) dada por ∀yy≤x ("x é máximal"). Set for um termo semy como variável livre, então φ(t) diz apenas quet é maximal. Entretanto set éy, a fórmula φ(y) é ∀yy≤y quenão diz quey é máximal.O problema de que a variável livrey det (=y) se transformou em ligada quando nós substituímosy porx em φ(x). Assim, para construir φ(y) nós devemos primeiramente mudar a variável ligaday de φ para qualquer outra coisa, por exemplo a variávelz, de modo que o φ(y) seja então ∀zz≤y. Esquecer desta condição é uma causa notória de erros.
Há diversas convenções diferentes para se usar a igualdade (ou a identidade) na lógica de primeira ordem. Esta seção resume as principais. Todas as convenções resultam mais ou menos no mesmo com mais ou menos a mesma quantidade de trabalho, e diferem principalmente na terminologia.
A regra de inferênciamodus ponens é a única necessária para alógica proposicional de acordo com a formalização proposta aqui. Ela diz que se φ e φ → ψ são ambos demonstrados, então pode-se deduzir ψ.A regra de inferência chamadaGeneralização Universal é característica da lógica de primeira ordem:
onde se supõe que é um teorema já demonstrado da lógica de primeira ordem. Observe que a Generalização é análoga àregra da necessitação dalógica modal, que é:
Apesar da Lógica de Primeira Ordem ser suficiente para formalizar uma grande parte da matemática, e também ser comumente usada emCiência da Computação e outras áreas, ela tem as suas limitações. Suas limitações incluem limitações em sua expressividade e limitações com relação aos fragmentos das línguas naturais que pode descrever.
O teorema de Löwenheim–Skolem mostra que se uma teoria de primeira ordem tem um modelo infinito, então a teoria também tem modelos de todas as cardinalidades infinitas. Em particular, nenhuma teoria de primeira ordem com um modelo infinito pode ser categórica. Assim, não há uma teoria de primeira ordem cujo único modelo tem o conjunto dos números naturais como domínio, ou cujo único modelo tem o conjunto dos números reais como domínio.Várias extensões da Lógica de Primeira-Ordem, incluindo a Lógica de Ordem Superior e a Lógica Infinitária, são mais expressivas no sentido de que elas admitem axiomatizações categóricas dos números naturais ou reais. Essa expressividade tem um custo em relação às propriedades meta-lógicas; de acordo com o Teorema de Lindström, qualquer lógica que seja mais forte que a lógica de primeira ordem falhará em validar oteorema da compacidade ou em validar o teorema de Löwenheim–Skolem.
A lógica de primeira ordem é capaz de formalizar vários quantificadores na língua natural, como “todas as pessoas que moram em Paris, moram na França”. Mas existem várias características que não podem ser expressas na lógica de primeira ordem. “Qualquer sistema lógico que é apropriado para analisar línguas naturais, precisa de uma estrutura muito mais rica que a lógica de primeira ordem" (Gamut 1991, p 75).
| Tipo | Exemplo | Comentário |
|---|---|---|
| Quantificadores sobre as propriedades | Se Rafael for satisfeito consigo mesmo, então ele tem pelo menos uma coisa em comum com Roberta | Requer quantificadores sobre os predicados, os quais não podem ser implementados com a lógica de primeira ordem (unicamente ordenada): Zj→ ∃X(Xj∧Xp) |
| Quantificadores sobre as propriedades | Papai Noel tem todos os atributos de um sadista | Requer quantificadores sobre os predicados, os quais não podem ser implementados com a lógica de primeira ordem (unicamente ordenada): ∀X(∀x(Sx → Xx)→Xs) |
| Predicado adverbial | Luiz está andando rápido | Não pode ser analisado como Wj ∧ Qj; predicados adverbiais não são a mesma coisa que predicados de segunda ordem , como cores |
| Adjetivo Relativo | Jumbo é um elefante pequeno | Não podem ser analisados como Sj ∧ Ej; predicados adjetivados não são a mesma coisa que predicados de segunda ordem , como cores |
| Modificador do predicado adverbial | Anderson está andando muito rápido | - |
| Modificador do adjetivo relativo | Roberta é extremamente pequena | Uma expressão como "extremamente" , quando usado com um adjetivo relativo "pequena", resulta em um novo adjetivo relativo: "extremamente pequena" |
| Preposições | Alberto está sentado ao lado de Danilo | A preposição "ao lado de" quando aplicada a Luiz, resulta em um predicado adverbial "ao lado de Luiz" |
Os cincoaxiomas lógicos mais as duas regras de inferência seguintes caracterizam a lógica de primeira ordem:
Axiomas:
Regras de Inferência:
Estes axiomas são na realidadeesquemas de axiomas. Cada letra grega pode ser uniformemente substituída, em cada um dos axiomas acima, por uma FBF qualquer, e uma expressão do tipo denota o resultado da substituição de x por t na fórmula.
O cálculo de predicado é uma extensão dalógica proposicional que define quais sentenças da lógica de primeira ordem sãodemonstráveis. É umsistema formal usado para descrever asteorias matemáticas. Se o cálculo proposicional for definido por um conjunto adequado de axiomas e a única regra de inferênciamodus ponens (isto pode ser feito de muitas maneiras diferentes, uma delas já ilustrada na seção anterior), então o cálculo de predicados pode ser definido adicionando-se alguns axiomas e uma regra de inferência "generalização universal" (como, por exemplo, na seção anterior). Mais precisamente, como axiomas para o cálculo de predicado, teremos:
Uma sentença será definida comodemonstrável na lógica de primeira ordem se puder ser obtida começando com os axiomas do cálculo de predicados e aplicando-se repetidamente as regras de inferência "modus ponens" e "generalização universal". Se nós tivermos uma teoriaT (um conjunto de sentenças, às vezes chamadas axiomas) então uma sentença φ se define comodemonstrável na teoriaT sea ∧b ∧ … → φ é demonstrável na lógica de primeira ordem (relação de consequência formal), para algumconjunto finito de axiomasa,b,… da teoriaT.Um problema aparente com esta definição de "demonstrabilidade" é que ela parece um tanto ad hoc: nós tomamos uma coleção aparentemente aleatória de axiomas e de regras de inferência, e não é óbvio que não tenhamos acidentalmente deixado de fora algum axioma ou regra fundamental. O teorema da completude deGödel nos assegura de que este não é realmente um problema: o teorema diz que toda sentença verdadeira em todos os modelos é demonstrável na lógica de primeira ordem. Em particular, toda definição razoável de "demonstrável" na lógica de primeira ordem deve ser equivalente à definição acima (embora seja possível que os comprimentos das derivações difira bastante para diferentes definições de demonstrabilidade).Há muitas maneiras diferentes (mas equivalentes) de definir provabilidade. A definição acima é um exemplo típico do cálculo noestilo de Hilbert, que tem muitos axiomas diferentes, mas poucas regras de inferência. As definições de demonstrabilidade para a lógica de primeira ordem nos estilos de Gentzen (dedução natural e cálculo de sequentes) são baseadas em poucos ou nenhum axiomas, mas muitas regras de inferência.
Alguns metateoremas lógicos importantes listam-se abaixo:
A maioria destas lógicas são de certa forma extensões da lógica de primeira ordem: elas incluem todos os quantificadores e operadores lógicos da lógica de primeira ordem com os mesmos significados. Lindström mostrou que a lógica de primeira ordem não tem extensões (com exceção dela própria) que satisfazem oteorema da compacidade e ao teorema deLöwenheim-Skolem descendente. Uma formulação precisa deste teorema requer a listagem de vários páginas de condições técnicas que a lógica deve satisfazer, por exemplo, a mudança dos símbolos de uma linguagem não deve fazer nenhuma diferença essencial nas sentenças que são verdadeiras.
A lógica de primeira ordem em que nenhumasentença atômica se encontra sob o escopo de mais de três quantificadores, tem o mesmo poder expressivo que aálgebra de relação de Tarski e de Givant (1987). Estes autores também mostram que a LCPO (Lógica Clássica de Primeira Ordem) com umpar ordenado primitivo, e uma relação algébrica incluindorelações de projeção sobre pares ordenados são equivalentes.
ex:pt.x (Homem(x)→Mortal(x)), que é uma fórmula válida