sexta-feira, 13 de março de 2009

Lógica de primeira ordem

Origem: Wikipédia, a enciclopédia livre.

Ir para: navegação, pesquisa

A lógica de primeira ordem (LPO), conhecida também como cálculo de predicados de primeira ordem (CPPO), é um sistema lógico que estende a lógica proposicional (lógica sentencial) e que é estendida pela lógica de segunda ordem.

As sentenças atômicas da lógica de primeira ordem têm o formato P (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 é a quantificação: dada uma sentença φ qualquer, as novas construções \forall x\, \phi e \exists x\, \phi -- leia “para todo x, φ” e “para algum x, φ”, respectivamente -- são introduzidas. \forall x\, \phi significa que φ é verdadeiro para todo valor de x e \exists x\, \phi significa que há pelo menos um x tal que φ é verdadeiro. Os valores das variáveis são tirados de um universo 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. Uma teoria de primeira ordem consiste em um conjunto de axiomas (geralmente finitos ou recursivamente enumerável) e de sentenças dedutíveis a partir deles. A teoria dos conjuntos de Zermelo-Fraenkel é um exemplo de uma teoria de primeira ordem, e aceita-se geralmente que toda a matemá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 a aritmética de Peano.

Índice

[esconder]

[editar] Definindo a lógica de primeira ordem

Um cálculo de predicados consiste em

  • regras de formação (definições recursivas para dar origem a fórmulas bem-formadas ou fbfs).
  • regras de transformação (regras de inferência para derivar teoremas).
  • axiomas.

Os axiomas considerados aqui são os axiomas lógicos que fazem parte do cálculo de predicados. Além disso, os axiomas nã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 uma regra 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 axiomas não-lógicos).

[editar] Alfabeto

O alfabeto de 1ª ordem, Σ, tem a seguinte constituição:

\Sigma = X \cup \Sigma_C \cup \Sigma_F \cup \Sigma_R \cup \Sigma_L \cup \Sigma_P, onde

  1. X = {x,y,z,x1,x2,...,y1,y2,...,z1,z2,...} é um conjunto enumerável de variáveis;
  2. ΣC = {a,b,c,a1,a2,...,b1,b2,...,c1,c2,...} é um conjunto de símbolos chamados de constantes;
  3. ΣF = {F1,F2,...} é um conjunto de símbolos ditos sinais funcionais;
  4. ΣR = {R1,R2,...} é um conjunto de símbolos ditos sinais relacionais ou predicativos;
  5. \Sigma_L = \{\neg, \wedge, \vee, \rightarrow, \leftrightarrow, \forall, \exists\} é o conjunto de símbolos ditos sinais lógicos;
  6. ΣP = {(,),,} é o conjunto de símbolos de pontuação.

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:

  • O conjunto de símbolos primitivos (operadores e quantificadores) varia freqüentemente. Alguns símbolos primitivos podem ser omitidos, substituindo-os com abreviaturas adequadas; por exemplo (P ↔ Q) é uma abreviatura para (PQ) ∧ (QP). No sentido contrário, é possível incluir outros operadores como símbolos primitivos, como as constantes de verdade ⊤ para “verdadeiro” e o ⊥ para “falso” (estes são operadores do aridade 0). O número mínimo dos símbolos primitivos necessários é um, mas se nós nos restringirmos aos operadores listados acima, seria necessário três; por exemplo, o ¬, o ∧, e o ∀ bastariam.
  • Alguns livros mais velhos usam a notação φ ⊃ ψ para φ → ψ, ~φ para ¬φ, φ & ψ para φ ∧ ψ, e uma riqueza de notações para os quantificadores; por exemplo, ∀xφ pode ser escrito como (x)φ.
  • A igualdade é às vezes considerada como parte da lógica de primeira ordem; Neste caso, o símbolo da igualdade será incluído no alfabeto, e comportar-se-á sintaticamente como um predicado binário. Assim a LPO será chamada de lógica de primeira ordem com igualdade.
  • As constantes são na verdade funções de aridade 0, assim seria possível e conveniente omitir constantes e usar as funções que tenham qualquer aridade. Mas é comum usar o termo “função” somente para funções de aridade 1.
  • Na definição acima, as relações devem ter pelo menos aridade 1. É possível permitir relações de aridade 0; estas seriam consideradas variáveis proposicionais.
  • Há muitas convenções diferentes sobre onde pôr parênteses; por exemplo, se pode escrever ∀x ou (∀x). Às vezes se usa dois pontos ou ponto final ao invés dos parênteses para criar fórmulas não ambíguas. Uma convenção interessante, mas incomum, é a “notação polonesa”, onde se omite todos os parênteses, e escreve-se o ∧, ∨, e assim por diante na frente de seus argumentos. A notação polonesa é compacta e elegante, mas rara e de leitura complexa.
  • Uma observação técnica é que se houver um símbolo de função de aridade 2 que representa um par ordenado (ou símbolos de predicados de aridade 2 que representam as relações de projeção de um par ordenado) então se pode dispensar inteiramente as funções ou predicados de aridade > 2. Naturalmente o par ou as projeções necessitam satisfazer aos axiomas naturais.

Os conjuntos das constantes, das funções, e das relações compõem a assinatura 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. Uma estrutura dá o significado semântico de cada símbolo da assinatura. Por exemplo, a linguagem da teoria 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.

[editar] Regras de formação

As regras de formação definem os termos, fórmulas, e as variáveis livres como segue. O conjunto dos termos é definido recursivamente pelas seguintes regras:

  1. Qualquer constante é um termo (sem variáveis livres).
  2. Qualquer variável é um termo (cuja única variável livre é ela mesma).
  3. Toda expressão f (t1,…, tn) de n ≥ 1 argumentos (onde cada argumento ti é um termo e f é um símbolo de função de aridade n) é um termo. Suas variáveis livres são as variáveis livres de cada um dos termos ti.
  4. Cláusula de fechamento: Nada mais é um termo.

O conjunto das fórmulas bem-formadas (chamadas geralmente fbfs ou apenas fórmulas) é definido recursivamente pelas seguintes regras:

  1. Predicados simples e complexos: se P for uma relação de aridade n ≥ 1 e os ai são os termos então P (a1,…,an) é bem formada. Suas variáveis livres são as variáveis livres de quaisquer termos ai. Se a igualdade for considerada parte da lógica, então (a1 = a2) é bem formada. Tais fórmulas são ditas atômicas.
  2. Cláusula indutiva I: Se φ for uma fbf, então ¬φ é uma fbf. Suas variáveis livres são as variáveis livres de φ.
  3. Cláusula indutiva II: Se φ e ψ são fbfs, então (ψ ∧ φ), (ψ\veeφ), (ψ → φ), (ψ ↔ φ) são fbfs. Suas variáveis livres são as variáveis livres de φ e de ψ.
  4. Cláusula indutiva III: Se φ for uma fbf e x for um variável, então ∀xφ e ∃xφ são fbfs, cujas variáveis livres são as variáveis livres de φ com exceção de x. Ocorrências de x são ditas ligadas ou mudas (por oposição a livre) em ∀xφ e ∃xφ.
  5. Cláusula de fechamento: Nada mais é uma fbf.

Na prática, se P 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 se f 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 um x”, 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, uma função unária −, uma função binária +, e uma relação binária ≤. Assim:

  • 0, x, y são termos atômicos
  • + (x, y), + (x, + (y, − (z))) são termos, escritos geralmente como x + y, x + (y + (−z))
  • = (+ (x, y), 0), ≤ (+ (x, + (y, − (z))), + (x, y)) são fórmulas atômicas, escritas geralmente como x + y = 0, x + y - zx + y,
  • (∀xy ≤ (+ (x, y), z)) ∧ (∃x = (+ (x, y), 0)) é uma fórmula, escrita geralmente como (∀xy (x + yz)) ∧ (∃x (x + y = 0)).

[editar] Substituição

Se t é um termo e φ(x) é uma fórmula que contém possivelmente x como uma variável livre, então φ(t) se definido como o resultado da substituição de todas as instâncias livres de x por t, desde que nenhuma variável livre de t se torne ligada neste processo. Se alguma variável livre de t se tornar ligada, então para substituir t por x é primeiramente necessário mudar os nomes das variáveis ligadas de φ para algo diferente das variáveis livres de t. Para ver porque esta condição é necessária, considere a fórmula φ(x) dada por ∀y yx (“x é máximal”). Se t for um termo sem y como variável livre, então φ(t) diz apenas que t é maximal. Entretanto se t é y, a fórmula φ(y) é ∀y yy que não diz que y é máximal.O problema de que a variável livre y de t (=y) se transformou em ligada quando nós substituímos y por x em φ(x). Assim, para construir φ(y) nós devemos primeiramente mudar a variável ligada y de φ para qualquer outra coisa, por exemplo a variável z, de modo que o φ(y) seja então ∀z zy. Esquecer desta condição é uma causa notória de erros.

[editar] Igualdade

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 convenção mais comum para a igualdade é incluir o símbolo da igualdade como um símbolo lógico primitivo, e adicionar os axiomas da igualdade aos axiomas da lógica de primeira ordem. Os axiomas de igualdade são
x = x
x = yF(...,x,...) = F(...,y,...) para qualquer função F
x = y → (P(...,x,...) → P(...,y,...)) para qualquer relação P (incluindo a própria igualdade)
  • A próxima convenção mais comum é incluir o símbolo da igualdade como uma das relações de uma teoria, e adicionar os axiomas da igualdade aos axiomas da teoria. Na prática isto é quase idêntico à da convenção precedente, exceto no exemplo incomum de teorias com nenhuma noção de igualdade. Os axiomas são os mesmos, e a única diferença é se eles serão chamados de axiomas lógicos ou de axiomas de taoria.
  • Nas teorias sem funções e com um número finito de relações, é possível definir a igualdade em termos de relações, definindo os dois termos s e t como iguais se qualquer relação continuar inalterada ao se substituir s por t em qualquer argumento. Por exemplo, em teoria dos conjuntos com uma relação ∈, nós definiríamos s = t como uma abreviatura para ∀x (sxtx) ∧ ∀x (xsxt). Esta definição de igualdade satisfaz automaticamente os axiomas da igualdade.
  • Em algumas teorias é possível dar definições de igualdade ad hoc. Por exemplo, em uma teoria de ordens parciais com uma relação ≤ nós poderíamos definir s = t como uma abreviatura para stts.

[editar] Regras de Inferência

A regra de inferência modus ponens é a única necessária para a ló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 chamada Generalização Universal é característica da lógica de primeira ordem:

se \vdash \phi, então \vdash \forall x \, \phi

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 da lógica modal, que é:

se \vdash P, então \vdash \Box P.

[editar] Axiomas e Regras

Os cinco axiomas lógicos mais as duas regras de inferência seguintes caracterizam a lógica de primeira ordem:

Axiomas:

  • (A1) \alpha \rightarrow (\beta \rightarrow \alpha)
  • (A2) (\alpha \rightarrow (\beta \rightarrow \gamma)) \rightarrow ((\alpha \rightarrow  \beta) \rightarrow (\alpha \rightarrow \gamma))
  • (A3) (\neg \alpha \rightarrow \neg \beta) \rightarrow ((\neg \alpha \rightarrow \beta) \rightarrow \alpha)
  • (A4) \forall x.(\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow   \forall x.\beta), onde x não é livre em α
  • (A5) \forall x.\alpha \rightarrow \alpha{[}t\;{:=x}\;{]}, onde t é livre para x em α.

Regras de Inferência:

  • Modus Ponens:
 MP:\frac{\alpha, \alpha \rightarrow \beta}{\beta}



  • Generalização Universal:



 Gen:\frac{\alpha}{\forall x. \alpha}


Estes axiomas são na realidade esquemas 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 α[t: = x] denota o resultado da substituição de x por t na fórmula α.





[editar] Cálculo de Predicados



O cálculo de predicado é uma extensão da lógica proposicional que define quais sentenças da lógica de primeira ordem são demonstráveis. É um sistema formal usado para descrever as teorias matemáticas. Se o cálculo proposicional for definido por um conjunto adequado de axiomas e a única regra de inferência modus 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:




  • Os axiomas circunstanciais do cálculo proposicional (A1, A2 e A3 na seção anterior);


  • Os axiomas dos quantificadores (A4 e A5);


  • Os axiomas para a igualdade propostos em seção anterior, se a igualdade for considerada como um conceito lógico.



Uma sentença será definida como demonstrá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 teoria T (um conjunto de sentenças, às vezes chamadas axiomas) então uma sentença φ se define como demonstrável na teoria T se ab ∧ ... → φ é demonstrável na lógica de primeira ordem (relação de consequência formal), para algum conjunto finito de axiomas a, b,... da teoria T. 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 de Gö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 no estilo 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.





[editar] Algumas equivalências

\lnot \forall x \, P(x) \Leftrightarrow \exists x \, \lnot P(x)
\lnot \exists x \, P(x) \Leftrightarrow \forall x \, \lnot P(x)
\forall x \, \forall y \, P(x,y) \Leftrightarrow \forall y \, \forall x \, P(x,y)
\exists x \, \exists y \, P(x,y) \Leftrightarrow \exists y \, \exists x \, P(x,y)
\forall x \, P(x) \land \forall x \, Q(x) \Leftrightarrow \forall x \, (P(x) \land Q(x))
\exists x \, P(x) \lor \exists x \, Q(x) \Leftrightarrow \exists x \, (P(x) \lor Q(x))




[editar] Algumas regras de inferência

\exists x \, \forall y \, P(x,y) \Rightarrow \forall y \, \exists x \, P(x,y)
\forall x \, P(x) \lor \forall x \, Q(x) \Rightarrow \forall x \, (P(x) \lor Q(x))
\exists x \, (P(x) \land Q(x)) \Rightarrow \exists x \, P(x) \land \exists x \, Q(x)
\exists x \, P(x) \land \forall x \, Q(x) \Rightarrow \exists x \, (P(x) \land Q(x))
\forall x \, P(x) \Rightarrow P(c) (se c for uma variável, então não deve ser quantificada em P(x))
P(c) \Rightarrow \exists x \, P(x) (x não deve aparecer livre em P(c))




[editar] Metateoremas da lógica de primeira ordem



Alguns metateoremas lógicos importantes listam-se abaixo:




  1. Ao contrário da lógica proposicional, a lógica de primeira ordem é indecidível, desde que a linguagem contenha ao menos um predicado de aridade ao menos 2, para além da igualdade. Pode-se demonstrar que há um procedimento de decisão para determinar se uma fórmula arbitrária P é válida (veja problema da parada). (Estes resultados foram demonstrados, independentemente, por Church e Turing).


  2. O problema da decisão para validade é semidecidível, ou seja, há uma máquina de Turing que quando recebe uma sentença como entrada, parará se e somente se a sentença for válida (satisfeita em todos os modelos).


    • Como o teorema da completude de Gödel mostra, para toda fórmula válida P, P é demonstrável. Analogamente, assumindo a consistência da lógica, toda fórmula demonstrável é válida.


    • Para um conjunto finito ou semi-enumerável de axiomas, o conjunto das fórmulas demonstráveis pode ser explicitamente enumerado por uma máquina de Turing, donde segue o resultado de semidecidibilidade.




  3. A lógica de predicados monádica (i.e., a lógica de predicados somente com predicados de um argumento) é decidível.


  4. A classe de Bernays-Schönfinkel das fórmulas de primeira ordem é também decidível.





[editar] Comparação com outras lógicas





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 o teorema da compacidade e ao teorema de Lö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 nenhuma sentenç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 um par ordenado primitivo, e uma relação algébrica incluindo relações de projeção sobre pares ordenados são equivalentes.





[editar] Referências




  • Bedregal, B.R.C, and Acióly, B.M. Lógica para a Ciência da Computação. Versão preliminar, 2002.





[editar] Ver também







[editar] Fontes alternativas




  • SILVA, Flávio S. Correa da; FINGER, Marcelo; MELO, Ana Cristina V. de. Lógica Para Computação.ed. Thomson, 2006.


  • MORTARI, Cezar.Introdução à Lógica. 1. ed. Imprensa Oficial SP, 2001.


  • ABE, Jair Minoro;SCALZITTI, Alexandre;FILHO, joão inácio da silva.Introdução à Lógica para a Ciência da Computação. 2. ed. Arte e Ciência, 2002.


  • SOUZA, João de.Lógica para Ciência da Computação. 1. ed. Campus, 2002.


  • DETLEFSEN, Michael;MCCARTY, David Charles;BACON, John B.Glossário de Lógica. ed. Edições 70, 2004.








Obtido em "http://pt.wikipedia.org/wiki/L%C3%B3gica_de_primeira_ordem"



Categoria: Lógica matemática

Nenhum comentário: