Edit page

Lógica de Primeira Ordem - Introdução

Lógica cuja linguagem nos permite considerar o "interior" (ao qual não podemos aceder) das proposições. As proposições elementares deixam de ser um todo e passam a ter uma estrutura, na qual podem existir constantes, variáveis e funções. Contém dois símbolos adicionais em relação à lógica proposicional, os quantificadores existencial e universal, que já conhecemos da matemática: \exists e \forall, respetivamente.

Componentes da linguagem

A linguagem abordada nesta secção é constituída por algumas componentes novas, diferentes das da lógica proposicional.

Variáveis

Símbolos que desempenham o papel de designações (sem ser propriamente designações). A noção de variável está associada ao conceito de função à frente apresentado, mais concretamente ao seu domínio - uma variável pode tomar todos os valores do domínio de uma dada função, no contexto dessa função. Só por si não correspondem a entidades.

Funções

No contexto estudado, corresponde a um conjunto de pares ordenados, potencialmente infinito, que não contém dois pares distintos com o mesmo primeiro elemento - não existe aqui "não determinismo", mapear uma função a um dado valor corresponde sempre ao mesmo resultado. Tal como na matemática, as funções têm um domínio (conjunto de todos os primeiros elementos dos pares) e um contradomínio (segundos elementos dos pares). Recebem um elemento do domínio, o argumento da função, e calculam o elemento correspondente do contradomínio, o valor da função. Sendo que correspondem a transformações, podemos utilizar funções para descrever entidades.

A aridade de uma função corresponde à quantidade de argumentos que esta recebe. Uma função de aridade 0 diz-se uma constante, claro.

Apesar de usualmente irmos estudar funções que recebem um argumento - que formam pares ordenados - é importante realçar que essa não é a única aridade possível de uma função. De um modo geral, em vez de consideramos que funções são conjuntos de pares ordenados, consideramo-las sim conjuntos de tuplos ordenados. Uma função que recebe nn argumentos é um conjunto de tuplos ordenados que não contém 2 tuplos com os mesmos nn primeiros elementos!

A expressão designatória de uma função pode ser, por exemplo:

capital(x)=a capital de xn(x)=o ano de nascimento de xs(x)=x+1capital(x)=\text{a capital de }x\\ n(x)=\text{o ano de nascimento de }x\\ s(x) = x + 1

Exemplos de conjuntos de pares ordenados que correspondem a "aplicações" das funções acima são, respetivamente:

{(Portugal,Lisboa),(Franc¸a,Paris),(Espanha,Madrid),}{(Augustus_De_Morgan,1806),(Alonzo_Church,1903),}{(1,2),(2,3),(3,4),}\{(\text{Portugal}, \text{Lisboa}), (\text{França}, \text{Paris}), (\text{Espanha}, \text{Madrid}),\dots\}\\ \{(\text{Augustus\_De\_Morgan}, 1806), (\text{Alonzo\_Church}, 1903),\dots\}\\ \{(1,2),(2,3),(3,4),\dots\}

Relações

Servem para representar qualquer relação (passo a redundância) entre elementos de conjuntos. Não são funções, visto que um primeiro elemento pode estar associado a mais que um segundo elemento. É usualmente definida através da especificação dos conjuntos aos quais os primeiro e segundo elementos pertencem, juntamente com uma expressão proposicional que faz uma afirmação sobre a sua relação. Relações com apenas um argumento também se chamam classes ou propriedades.

Exemplo - Relação

A relação correspondendo ao conjunto dos países que partilham fronteira terrestre podia ter, por exemplo:

{(Portugal,Espanha),(Espanha,Portugal),(Espanha,Franca),}\{(Portugal, Espanha), (Espanha, Portugal), (Espanha, Franca),\dots\}

Como podemos observar, Espanha é primeiro elemento duas vezes, pelo que não podemos estar na presença de uma função!

Esta relação pode ser definida tal que:

Tem_fronteira(x,y)=x tem fronteira terrestre com yTem\_fronteira(x,y)=x\text{ tem fronteira terrestre com }y

onde tem fronteira terrestre com é a tal expressão designatória.

Alfabeto básico da linguagem

  • Símbolos de pontuação: , ( ) [ ]

  • Símbolos lógicos:

    • ¬\neg, que corresponde à negação;
    • \wedge, que corresponde à conjunção;
    • \vee, que corresponde à disjunção inclusiva, vulgo OR;
    • \to, que corresponde à implicação.
    • \exists, que corresponde ao quantificador existencial.
    • \forall que corresponde ao quantificador universal.
  • finf^{n}_{i}, para n0,i1n \geq 0, i \geq 1 - funções de aridade nn. Funções com aridade 00 (n=0n = 0, portanto) são constantes. A i-gésima função diz-se com nn argumentos. Começam com letra minúscula.

  • PinP^{n}_{i}, para n0,i1n \geq 0, i \geq 1 - letras de predicado com aridade nn. Uma letra de predicado com nn argumentos representa uma relação nn-ária (por exemplo, a relação de fronteira entre 2 países é uma relação binária). Começam com letra maiúscula.

  • Variáveis individuais, xix_{i}, como as usuais x,y,zx, y, z.


Depois de apresentadas as principais componentes da linguagem da LPO, podemos então começar a falar dos seus termos, das suas fbfs, e daí prosseguir.

Termos

Correspondem às entidades sobre as quais queremos falar.

  • cada letra de constante é um termo;

  • cada variável é um termo;

  • se t1,,tnt_{1}, \dots, t_{n} são termos, então a função que aceita esses argumentos é também um termo.

Um termo fechado/chão é um termo que não contém variáveis.

Exemplos de termos fechados seriam, por exemplo:

PortugalAugustus_De_Morgancapital(Portugal)pai(Augustus_De_Morgan)pai(pai(pai(Augustus_De_Morgan)))\begin{array}{c} Portugal\\ Augustus\_De\_Morgan\\ capital(Portugal)\\ pai(Augustus\_De\_Morgan)\\ pai(pai(pai(Augustus\_De\_Morgan))) \end{array}

Enquanto que termos que aceitam variáveis poderiam ser:

xcapital(x)pai(x)\begin{array}{c} x\\ capital(x)\\ pai(x) \end{array}

Fórmulas bem formadas

O conceito de fórmula bem formada, fbf, é redefinido para a lógica de primeira ordem. Corresponde ao menor conjunto definido através das seguintes regras de formação:

  • se t1,,tnt_{1}, \dots, t_{n} são termos, então o predicado que aceita esses argumentos é uma fbf, sendo que esta fbf é atómica;

  • Se α\alpha é uma fbf, ¬α\neg\alpha é também uma fbf; a conjunção, disjunção e implicação de fbfs é também uma fbf;

  • Se α\alpha é uma fbf, então x[α]\forall x[\alpha] e x[α]\exists x[\alpha] são também fbfs.

Dizemos que uma fbf sem variáveis é chã.

Resta notar que, sempre que possível, tentamos abreviar uma sequência de quantificadores do mesmo tipo numa só ocorrência do mesmo - por exemplo, x[y[]]\forall x[\forall y[\dots]] é igual a x,y[]\forall x, y[\dots].

Exemplo - Fórmulas bem formadas

Apresenta-se, de seguida, um conjunto de fórmulas bem formadas. Note-se que os terceiro e quartos exemplos correspondem a fórmulas chãs!

¬P(a,g(a,b,c))P(a,b)¬Q(f(d))RSTem_fronteira(Portugal,Espanha)Tem_fronteira(x,y)x [y [Tem_fronteira(x,y)g [Travaram_guerra(g,x,y)]]]Vive_em(x,capital(Portugal))\neg P (a,g(a,b,c))\\ P(a,b)\rightarrow \neg Q(f(d))\\ R \wedge S\\ Tem\_fronteira(Portugal, Espanha)\\ Tem\_fronteira(x,y)\\ \forall x\ [\forall y\ [Tem\_fronteira(x,y) \rightarrow \exists g\ [Travaram\_guerra(g,x,y)]]]\\ Vive\_em(x,capital(Portugal))

Nas fbfs x[α]\forall x[\alpha] e x[α]\exists x[\alpha], α\alpha é o domínio do quantificador. Diz-se que o quantificador liga a variável xx.
Uma ocorrência da variável xx diz-se ligada numa fbf caso esta ocorrência apareça dentro do domínio do quantificador que a introduz. Caso contrário, a variável diz-se livre. Uma fbf sem variáveis livres diz-se fechada - basta uma livre para não o ser. Caso não ocorram quantificadores no âmbito da variável em questão (caso falemos de uma relação, por exemplo), a variável é livre.

A título de exemplo, podemos dizer que a fbffbf P(x)x[Q(x)]P(x) \rightarrow \exists x [Q(x)] contém uma ocorrência livre de xx, em P(x)P(x), e uma ocorrência ligada de xx, em Q(x)Q(x).

Substituição

Conjunto finito de pares ordenados {t1/x1,,tn/xn}\{t_{1}/x_{1}, \dots, t_{n}/x_{n}\}, em que cada xix_{i} é uma variável individual e cada tit_{i} é um termo. Numa substituição, todas as variáveis individuais são diferentes, e nenhuma variável individual é igual ao termo correspondente. Cada um dos pares ti,xit_{i}, x_{i} é uma ligação.

Podem ser consideradas substituições, visto que todas as variáveis individuais são diferentes e não há termos iguais à variável associada:

{f(x)/x,z/y}{a/x,g(y)/y,f(g(h(b)))/z}\{f(x)/x,\hspace{0.1cm} z/y\}\\ \{a/x,\hspace{0.1cm} g(y)/y,\hspace{0.1cm} f(g(h(b)))/z\}

Por outro lado, não podem ser substituições:

{x/x,z/y}\{x/x,\hspace{0.1cm} z/y\}

(visto que o termo xx está ligado à variável xx - iguais, não representando portanto uma substituição)

{a/x,g(y)/y,b/x}\{a/x,\hspace{0.1cm} g(y)/y,\hspace{0.1cm} b/x\}

(visto que a variável individual xx aparece 2 vezes).

Existem dois casos especiais de substituições:

  • Substituição chã, caso nenhum dos termos contenha variáveis.

  • Substituição vazia, correspondendo ao conjunto vazio. Representada por ϵ\epsilon.

A ideia subjacente ao conceito de substituição é que cada variável individual será substituída (lá está) pelo termo que lhe está associado. É aplicada substituindo todas as ocorrências livres de variáveis individuais pelo termo a elas associado. Qualquer ocorrência ligada de uma variável não pode ser substituída!

Escrevemos α(x1,,xn)\alpha(x_{1}, \dots, x_{n}) para indicar que a fbf α\alpha tem x1,,xnx_{1}, \dots, x_{n} como variáveis livres.

Exemplo - Aplicar uma substituição

Consideremos:

P(x,f(a,y)){a/x,f(a,b)/y}=P(a,f(a,f(a,b)))P(x, f(a, y)) \cdot \{a/x,\hspace{0.1cm} f(a, b)/y\} = P(a, f(a, f(a, b)))

Como podemos observar, as ocorrências das variáveis individuais xx e yy são substituídas pelos termos a que estão ligados, sendo que todas as ocorrências dessas variáveis são ambas livres.

(A(x)x[B(x)]){a/x,f(a,b)/y}=A(a)x[B(x)](A(x) \to \exists x[B(x)]) \cdot \{a/x, f(a,b)/y\} = A(a) \to \exists x[B(x)]

Aqui, só uma das ocorrências da variável xx é livre, e só nessa é que ocorre substituição. Ora, o facto da substituição não ocorrer sempre pode originar problemas futuros, abordados mais à frente.

Dizemos, finalmente, que temos em mãos um termo livre tt para uma variável xx numa fbf α\alpha caso nenhuma ocorrência livre de xx em α\alpha ocorra dentro do domínio de um quantificador em ordem yy (onde yy é uma variável em tt). Um termo sem variáveis é, claro, sempre livre para qualquer variável em qualquer fbf. O termo g(y,f(b))g(y, f(b)) é livre para xx na fbf P(x,y)P(x, y), por exemplo, mas não o é na fbf y[P(x,y)]\forall y[P(x, y)].

Sistema dedutivo

O sistema dedutivo da Lógica de Primeira Ordem difere do da Lógica Proposicional no que às regras de inferência diz respeito. Todas as regras de inferência introduzidas anteriormente (conjunção, disjunção, negação, implicação) são aqui aplicáveis - iremos apenas adicionar regras de inferência adicionais, sobre os quantificadores introduzidos pela LPO.

Regras para o quantificador universal

Introdução do quantificador universal

Abreviada por II\forall, pode ser utilizada quando uma propriedade arbitrária, α(t)\alpha(t), for provada para t.t. Utilizamos, para tal, uma técnica semelhante à regra da introdução da implicação, criando um novo "contexto" no qual aparece um novo termo, que nunca apareceu na prova, e tentamos provar que esse termo arbitrário tem essa propriedade. A regra afirma, portanto, que se numa prova iniciada pela introdução da variável x0x_{0} pudermos derivar a fbf α(x0)\alpha (x_{0}), então podemos escrever x[α(x)]\forall x[\alpha(x)], precisamente porque o termo introduzido é arbitrário!

nx0mα(x0)m+1x[α(x)]I,(n,m)\def\arraystretch{1.5} \begin{array}{lll} n & x_0 \bigg\vert\\ \vdots & \enspace\enspace\bigg\vert\enspace\vdots\\ m & \enspace\enspace\bigg\vert\enspace \alpha (x_0)\\ m + 1 & \forall x[\alpha (x)] && I\forall, (n, m) \end{array}

Resta notar que aqui não estamos a trabalhar diretamente com as usuais provas hipotéticas, mas com um contexto iniciado por um qualquer termo (podemos, contudo, iniciar provas hipotéticas dentro desse contexto sem qualquer problema). A sua apresentação é também diferente, tal como pode ser observado acima.

Eliminação do quantificador Universal

Abreviada por EE\forall, indica que a partir de x[α(x)]\forall x[\alpha(x)] podemos inferir α(t)\alpha(t), onde tt é qualquer termo.

nx[α(x)]mα(t)E,n\def\arraystretch{1.5} \begin{array}{lll} n & \forall x[\alpha (x)]\\ \vdots & \vdots\\ m & \alpha (t) && E\forall, n \end{array}

Recorrendo às duas regras descritas acima, conseguimos agora provar o argumento

(x[P(x)Q(x)],x[Q(x)R(x)],x[P(x)R(x)]).({\forall x[P(x) \to Q(x)], \forall x[Q(x) \to R(x)]}, \forall x[P(x) \to R(x)]).

Note-se que há mais que uma maneira de fazer esta prova!

1x[P(x)Q(x)]Prem2x[Q(x)R(x)]Prem3x0P(x0)Hip4x[P(x)Q(x)]Rei,15P(x0)Q(x0)E,46Q(x0)E,(3,5)7x[Q(x)R(x)]Rei,28Q(x0)R(x0)E,79R(x0)E,(6,8)10P(x0)R(x0)I,(3,9)11x[P(x)R(x)]I,(4,10)\def\arraystretch{1.5} \begin{array}{lll} 1 & \forall x[P(x) \to Q(x)] && Prem\\ 2 & \forall x[Q(x) \to R(x)] && Prem\\ 3 & x_0 \bigg\vert\enspace\bigg\vert\underline{\enspace P(x_0) \enspace} && Hip\\ 4 & \enspace\enspace\bigg\vert\enspace\bigg\vert\enspace \forall x[P(x) \to Q(x)] && Rei, 1\\ 5 & \enspace\enspace\bigg\vert\enspace\bigg\vert\enspace P(x_0) \to Q(x_0) && E\forall , 4\\ 6 & \enspace\enspace\bigg\vert\enspace\bigg\vert\enspace Q(x_0) && E\to, (3, 5)\\ 7 & \enspace\enspace\bigg\vert\enspace\bigg\vert\enspace \forall x[Q(x) \to R(x)] && Rei, 2\\ 8 & \enspace\enspace\bigg\vert\enspace\bigg\vert\enspace Q(x_0) \to R(x_0) && E\forall, 7\\ 9 & \enspace\enspace\bigg\vert\enspace\bigg\vert\enspace R(x_0) && E\to, (6, 8)\\ 10 & \enspace\enspace\bigg\vert\enspace P(x_0) \to R(x_0) && I\to, (3, 9)\\ 11 & \forall x[P(x) \to R(x)] && I\forall, (4, 10) \end{array}

Regras para o quantificador existencial

Introdução do quantificador existencial

Abreviada por II\exists, afirma que a partir de uma propriedade arbitrária α(t)\alpha(t), podemos inferir x[α(x)]\exists x[\alpha(x)] - se provámos a propriedade para um termo, provámos que existe pelo menos um termo para a qual esta se aplica.

nα(t)mx[α(x)]I,n\def\arraystretch{1.5} \begin{array}{lll} n & \alpha (t)\\ \vdots & \vdots\\ m & \exists x[\alpha (x)] && I\exists, n \end{array}

Eliminação do quantificador existencial

Abreviada por EE\exists, é, porventura, a mais complicada das quatro regras introduzidas. Temos, a partir de x[α(t)]\exists x[\alpha(t)], que existe pelo menos uma entidade que satisfaz a propriedade α\alpha - só não sabemos qual. Como não sabemos nada sobre essa entidade, nada podemos afirmar sobre ela, para além de α(t)\alpha(t). Na prova, o objetivo será criar um "contexto" em que surge uma entidade nunca mencionada anteriormente; se dentro desse contexto formos capazes de derivar uma fbf β\beta, que não menciona tt, então β\beta verificar-se-á independentemente de tt.

nx[α(x)]mx0α(x0)Hipkβk+1βE,(n,(m,k))\def\arraystretch{1.5} \begin{array}{lll} n & \exists x[\alpha (x)]\\ m & x_0 \bigg\vert\underline{\enspace \alpha(x_0) \enspace} && Hip\\ \vdots & \enspace\enspace\bigg\vert\enspace\vdots\\ k & \enspace\enspace\bigg\vert\enspace\beta\\ k + 1 & \enspace\beta && E\exists, (n, (m, k)) \end{array}

A prova de x[P(x)]¬x[¬P(x)]\exists x[P(x)] \to \neg\forall x[\neg P(x)] passa por algo deste género:

1x[P(x)]Hip2x0P(x0)Hip3x[¬P(x)]Hip4P(x0)Rei,25¬P(x0)E,36¬x[¬P(x)]I¬,(3,(4,5))7¬x[¬P(x)]E,(1,(2,6))8x[P(x)]¬x[¬P(x)]I,(1,7)\def\arraystretch{1.5} \begin{array}{lll} 1 & \bigg\vert\underline{\enspace \exists x[P(x)] \enspace} && Hip\\ 2 & \bigg\vert\enspace x_0 \bigg\vert\underline{\enspace P(x_0) \enspace} && Hip\\ 3 & \bigg\vert\enspace\enspace\enspace\bigg\vert\enspace\bigg\vert\underline{\enspace \forall x[\neg P(x)] \enspace} && Hip\\ 4 & \bigg\vert\enspace\enspace\enspace\bigg\vert\enspace\bigg\vert\enspace P(x_0) && Rei, 2\\ 5 & \bigg\vert\enspace\enspace\enspace\bigg\vert\enspace\bigg\vert\enspace \neg P(x_0) && E\forall, 3\\ 6 & \bigg\vert\enspace\enspace\enspace\bigg\vert\enspace \neg\forall x[\neg P(x)] && I\neg, (3, (4, 5))\\ 7 & \bigg\vert\enspace \neg \forall x[\neg P(x)] && E\exists, (1, (2, 6))\\ 8 & \exists x[P(x)] \to \neg\forall x[\neg P(x)] && I\to, (1, 7) \end{array}