3.3.1. Introdução🔗

Se usarmos lógica proposicional para formalizar a frase "Toda maçã é vermelha", teremos uma letra proposicional, um átomo indivisível que não nos permitiria capturar a idéia do quantificador e da dependencia declarada entre as coisas que são maçãs e a cor destas mesmas coisas. A lógica de predicados, também chamada lógica de primeira ordem (FOL, "first order logic") acrescenta os seguintes ingredientes a sintaxe da lógica proposicional:

• Termos para representar indivíduos de um domínio. Os termos poderão ser variáveis ou funções aplicadas sobre termos;

• Proposições básicas serão predicados n-ários sobre termos;

• Fórmulas universalmente quantificadas, ∀ seguido de variável e fórmula;

• Fórmulas existencialmente quantificadas, ∃ seguido de variável e fórmula.

3.3.2. Sintaxe de FOL🔗

Nossa sintaxe terá dois elementos principais, termos e fórmulas. Como fizemos em pl-syntax, nossa sintaxe será formalizada como tipos indutivos.

Os termos podem ser variáveis ou funções aplicadas a outros termos. Uma variável carrega nome e um índice (lista de naturais usada para gerar "novas" variáveis a partir de uma dada variável):

Termos denotam objetos do domínio, e diferentes termos podem denotar um mesmo objeto como os termos (5 + 3) × 4, 8 × 4 e 32. Para representar termos mais complexos que apenas variáveis, a solução é introduzir símbolos funcionais para as operações entre termos.

Constantes podem ser representadas como funções com aridade zero, ou seja, com a lista de argumentos vazia, Term.struct "c" []

As fórmulas usarão os mesmos conectivos da lógica proposicional, mas acrescentaremos os quantificadores existencial e universal. O nome lógica de primeira ordem vem da idéia de que estamos quantificando sobre indivíduous de um domínio, objetos de primeira ordem. O tipo Formula α é parametrizado no tipo dos termos que preenchem os predicados. Se usarmos Formula Variable nossos termos são apenas variáveis. Se usarmos Formula Term temos nossa sintaxe completa com termos arbitrários.

A conjunção e a disjunção são binárias, e top e bot são construtores próprios, o mesmo que fizemos para as fórmulas proposicionais.

Note que o tipo Formula é diferente do tipo PL.Formula definido em pl-syntax, cada um em seu próprio namespace. Mais uma vez, estamos usando Lean como metalinguagem para implementar FOL.. Em tipos dependentes, não fazemos a distinção entre termos e fórmulas. Como vimos em IntroL, em Lean toda expressão é um termo e todo termo tem um tipo. Então quando falarmos em termos, ora estamos falando do termo Lean que pode representar uma Formula ou Term de FOL.

Também como fizemos para PL.Formula, a notação n-ária de Formula.conj e Formula.disj introduzimos com as funções abaixo.

Um termo (Lean) do tipo Formula não é muito legível, vamos implementar a instância de Repr para controlar a exibição destes termos. Note que ela demanda que o tipo α tenha também uma instância de Repr, que já implementamos para Variable e Term.

A seguir, R_reflexive expressa que o predicado R é reflexivo enquanto R_simetric expressa que ele é simétrico. Note que para estes dois exemplos, não precisamos usar termos envolvendo funções, logo usamos apenas Formula Variable.

Assim como definimos em pl-syntax, chamamos de uma linguagem de primeira ordem o conjunto de todas as fórmulas que podem ser construídas a partir de um vocabulário de símbolos predicativos e funcionais.

Em uma fórmula ∀x F (ou ∃x F), o quantificador liga toda ocorrência de x em F que não esteja já ligada por um ∀x (ou ∃x) interno a F. Uma fórmula é aberta se tem ao menos uma ocorrência livre de variável, e fechada (também chamada sentença) caso contrário. Por exemplo, (P[x] ∧ ∃x, R[x,x]) é aberta, o x de P[x] está fora do escopo do ∃x. Mas ∃y (P[y] ∧ ∃x R[x,x]) é uma sentença.

Coletar as variáveis livres de uma fórmula é uma operação recorrente. Abaixo, definimos a função freeVars que recebe como parâmetro uma função que extrai as variáveis de um termo. Para R_reflexive, só precisamos de uma função que transforme uma variável em uma lista com ela mesma. Para fórmulas que podem conter termos complexos, Formula Term, nossa função terá que percorrer todo o termo coletando as variáveis. Nos quantificadores, filter preserva apenas as variáveis diferentes da variável que o quantificador introduz.

Um termo t é livre para a variável v na fórmula F se toda ocorrência livre de v em F pode ser substituída por t sem que nenhuma das variáveis de t fique ligada. Por exemplo, y é livre para x em P[x] → ∀x P[x], mas o mesmo termo não é livre para x em ∀y R[x,y] → ∀x R[x,x]. Da mesma forma, g[x,y] não é livre para x em ∀y R[x,y] → ∀x R[x,x].

Um termo livre para uma variável v pode ser substituído nas ocorrências livres de v sem uma mudança não intencional de significado. Considere a fórmula aberta ∀y R[x,y] → ∀x R[x,x]. Se substituirmos a ocorrência livre de x nessa fórmula por y, obtemos uma fórmula fechada ∀y R[y,y] → ∀x R[x,x], uma variável acabou capturada. Se t não é livre para v em F, podemos sempre renomear as variáveis ligadas de F para garantir que a substituição de t por v em F tenha o significado correto. Embora g[y,c] não seja livre para x em ∀y R[x,y] → ∀x R[x,x], o termo é livre para x em ∀z R[x,z] → ∀x R[x,x], que é uma chamada variante alfabética (nomes diferentes para as variáveis ligadas) da fórmula original.

A função isVar verifica se um termo é uma variável. As funções varsInTerm e varsInTerms retornam a lista das variáveis que ocorrem num termo ou em uma lista de termos, sem duplicatas.

3.3.3. Semântica de FOL🔗

Em PL, uma função de atribuição de valor de verdade para os símbolos proposicionais nos permite determinar o valor de verdade de uma fórmula. Em FOL, uma interpretação de um vocabulário é uma estrutura que atribui significado aos símbolos do vocabulário.

Uma estrutura 𝔸 é como um dicionário para traduzir a linguagem de primeira ordem L. Uma estrutura nos dirá sobre qual coleção de coisas os símbolos ∀ e ∃ quantificam, isto é, o conjunto D. A estrutura também associa os símbolos predicativos de L a relações no domínio e os símbolos funcionais a funções no domínio. Formalmente, a estrutura é o par, domínio e interpretação.

Mas nossos termos podem ser conter variáveis então também precisamos interpretar variávei em elementos do domínio. O tipo Assign mapea variávies em elementos do domínio. A função Assign.update atualiza um mapeamento de variáveis em elementos do domínio associando a variável v e um novo elemento d, normalmente escrevemos g[v := d] para representar esta idéia de que g

A idéia é demostrada nos exemplos a seguir. Em um domínio dos naturais, a partir de um mapeamento inicial onde qualquer variável é mapeada no 0, podemos atualizar indicando que se a variável x for passada, ela deve agora estar associada ao valor 1.

Definido o mapeamento de variáveis, definimos agora o tipo FInterp para a interpretação de termos em elementos de um domínio D.

A partir de FInterp, definimos a interpretação de um termo na função liftAssign, recursiva sobre a estrutura do termo. Nossa recursão é parecida com varsInTerm, avaliando cada argumento e combinando os resultados para interpretar os símbolos funcionais. Note que fint name tem tipo List D → D e (args.map (liftAssign fint g)) irá retornar um termo do tipo List D.

Agora podemos definir quando uma fórmula α é verdadeira em uma estrutura 𝔸. Vamos usar a notação 𝔸 ⊧ α [g] ou ⊧ α [𝔸,g] para indicar que esta relação de consequência depende da interpretação dos símbolos em α dada por 𝔸 e da atribuição de variáveis a elementos do domínio dada por g. A segunda notação é mais precisa, preservando a idéia de que consequência lógica é uma relação entre fórmulas β ⊧ α ou entre uma listas de fórmulas e uma fórmula Δ ⊧ α.

O tipo Interp define o que é a interpretação de símbolos predicativos e seus argumentos para um valor boleano.

Em seguida definimos como avaliar fórmulas. Como em lógica proposicional, a definição calcula o resultado Bool. As cláusulas dos quantificadores são as que alteram a atribuição de valores à variáveis. ∀v F vale quando F vale para toda escolha de valor de v, e ∃v F quando vale para ao menos uma.

Aqui aparece a diferença em relação à lógica proposicional. Em nossa implementação, para avaliar uma fórmula com quantificador é preciso percorrer o domínio, e percorrer exige que o domínio seja enumerável e finito. Por isso eval recebe um argumento a mais, dom, e usa List.all e List.any, versões computáveis de ∀ e ∃. Em FOL, domínios não precisam ser finitos, mas não existe processo de decisão para avaliação de fórmulas em domínios infinitos e não enumeráveis.

Uma fórmula Formula α tem termos do tipo α, que pode ser Variable ou Term. Quando os termos são apenas variáveis, basta consultar g; quando forem termos estruturados, será necessário promover, com liftAssign, um mapeamento de variáveis no domínio para um mapemanto de termos no domínio. Em vez de escrever duas funções de avaliação, passamos essa tarefa como um parâmetro tval, do mesmo modo que Formula.freeVars recebeu a função que extrai as variáveis de um termo.

Para Formula Variable, a interpretação de Variable é a própria g.

Vamos considerar uma linguagem FOL, tomado de  (Enderton, 2001)Herbert B. Enderton (2001). “A Mathematical Introduction to Logic”. 2ª edição. Harcourt/Academic Press, San Diego. ., com um único símbolo predicado binário, E. Chamaremos esta linguagem de L₁. Uma estrutura para L₁ deve conter um domínio de discurso D, formado por entidades e uma interpretação para E. O domínio tem quatro objetos, e uma única relação binária para interpretar o símbolo E da linguagem L₁.

O tipo indutivo Vertex determinar quais são os objetos do nosso domínio. Para avaliar uma fórmula quantificada, porém, será preciso percorrer o domínio, e para isso ele tem de estar disponível em uma coleção que possa ser percorrida, vamos usar uma lista. Então o tipo indutivo declara o domínio, a lista o exibe na ordem em que será percorrido.

O teorema mem_vertices nos garante que na lista estão todos os elementos do tipo Vertex. A tática decide é combinada com cases v, que abre um caso por construtor, ela verifica os quatro casos um a um.

Um domínio com um só predicado binário pode ser visto como um grafo direcionado: os objetos são os vértices, e E x y vale quando há uma aresta de x para y.

A seguir intB interpreta o predicado de E à relação no modelo edge.

Uma importante observação é que nomes fora da lista, ou usados com o número errado de argumentos, recebem false. Isto quer dizer que fórmulas mal formadas, como por exemplo ∃ x E[x] com o predicado E sendo usado com um único argumento, serão silenciosamente avaliadas como false.

Finalmente podemos declarar algumas fórmulas para avaliarmos em nossa estrutura.

A primeira é a sentença corresponde a afirmação de que existe um vértice para o qual nenhuma aresta aponta. É verdadeira, e a testemunha é o nó d. A segunda é falsa pelo mesmo motivo, de d não sai aresta alguma. A terceira é verdadeira por causa do laço em c. A quarta é falsa: há aresta de b para c, mas não de c para b. Vale notar como a primeira soa em língua natural mais complicada do que a versão simbólica.

Quando avaliamos fórmulas fechadas, sem variáveis livres, a atribuição g é irrelevante, mas ainda é preciso fornecer alguma para Formula.eval.

A seguir, vamos usar o tipo Fin que constrói um tipo dos números naturais menores que um limite superior. O Fin 2 corresponde aos naturais menores que 2. Quando escrevemos (1 : Fin 2), a instância OfNat (Fin 2) 1 normaliza o literal armazenando o resto da divisão 1 % 2.

Usando o construtor Fin.mk n (ou o construtor anônimo ⟨...⟩), temos que passar uma prova de que o número informado é menor que o limite do tipo. Não conseguimos abaixo construir uma prova de que 3 < 2.

Como segundo exemplo, vamos considerar uma linguagem L₂ com interpretação também sobre os naturais. Precisamos de uma interpretação para os símbolos funcionais, uma para o símbolo de relação, e uma atribuição.

Uma constante é um símbolo funcional de aridade zero, como zero acima. Seguem dois exemplos do que liftAssign calcula. O valor de s[zero] não depende de g, pois nenhuma variável ocorre nele, mas o de plus[x, zero] é g x, e muda com g. Note que os dois fecham por simp, e não por rfl. O casamento de strings não é processado por rfl.

Segue um exemplo de avaliação de uma fórmula de L₂ no domínio [0, 1, 2, 3, 4]. A fórmula diz que existe um número maior que 0.

Vale destacar os limites de nossa implemenação. Em FOL, frm₂ sob o domínio dos naturais é verdadeira. Nossa implementação, no entanto, para ser decidível, processa apenas domínios finitos, listas.

A definição de verdade faz uso essencial das atribuições e, ainda assim, para sentenças, a verdade ou a falsidade não depende da atribuição. O problema é que, ao aplicar a definição de verdade acima a uma sentença, por exemplo a ∀x (P[x] → ∃y R[x,y]), a cláusula que trata do quantificador universal faz referência à noção de verdade para a fórmula (P[x] → ∃y R[x,y]), que é uma fórmula aberta. Para determinar se ela é verdadeira temos de saber qual elemento do domínio associar a x. A situação é análoga à interpretação de pronomes nas linguas naturais.

1. Todo mestre tem um aprendiz.

2. Ele tem um aprendiz.

Assim como definimos em PL. Uma sentença α em FOL é válida, ⊨ α, se é verdadeira em toda possível interpretação para a linguagem de α. Uma sentença C é consequência lógica de uma sentença P (P de premissa, C de conclusão) se todo modelo que torna P verdadeira também torna C verdadeira. A notação é P ⊨ C.

Mas como julgar afirmações da forma P ⊨ C? Em FOL não temos a função PL.Formula.allVals, que enumera todas as possíveis valorações. Logo não podemos decidir P ⊧ C. Podemos refutar a afirmação achando um contraexemplo. Um contraexemplo para P ⊨ C é uma interpretação I com I ⊨ P mas I ⊭ C.

3.3.4. Traduzindo Formula para Prop🔗

Como fizemos em PL, agora podemos mapear termos do tipo Formula em Prop. Temos Formula.eval que calcula o valor verdade de uma fórmula para uma dada interpretação em Bool; Formula.denote produz a proposição que a fórmula afirma. O tipo para interpretaçõa também precisa mudar, Interp devolvia um Bool, Denot devolve uma Prop.

Cada caso troca um construtor de Formula pelo conectivo correspondente de Prop — o conj do dado vira o ∧ da proposição, e o forall_ vira o ∀ do próprio Lean.

O teorema a seguir nos diz que a denotação de uma fórmula conside com sua avaliação. Mas precisamos de uma hipótese que não aparecia em lógica proposicional. A função eval decide um quantificador percorrendo dom, então só podemos esperar que ele concorde com o ∀ do Lean, que fala de todo elemento do tipo D — se dom de fato listar todos eles. É isso que hdom exige.