3.2.1. Introdução🔗

Em "Proof" as fórmulas proposicionais foram escritas diretamente como termos do tipo Prop, e usando táticas construimos provas de proposições α a partir de um conjunto de hipóteses Γ. Isto é, mostramos como derivar α a partir de Γ, isto é Γ ⊢ α.

Em Lean, Prop é um tipo assim como qualquer particular proposição também é um tipo. A variável h abaixo pode ser entendida como um identificador para uma "prova qualquer" da proposição p ∧ q. E Lean adota o princípio da "irrelevância da prova", ou seja, Lean não distingue diferentes provas de uma proposição. Como consequência, o tipo Prop não é computável, não é um "dado" que pode ser manipulado. Por exemplo, não conseguimos extrair os componentes de uma conjunção a ∧ b. Lean sabe que todas as provas de a ∧ b são irrelevantes e iguais, então ele não permite que você use uma prova como qualquer outro dado de um Type. Não podemos, por exemplo, realizar casamento de padrões em h abaixo.

Nesta seção, queremos manipular fórmulas e decidir quando uma fórmula α é consequência lógica de β, isto é, β ⊧ α . A noção de consequência lógica é semântica. Para toda possível escolha de valores verdade para os símbolos proposicionais em α e β, sempre que β for verdade, α deve ser verdade. Para computar o valor verdade de uma fórmula, vamos precisar manipula a formula como dado, e calcular seu valor verdade a partir do mapeamento de variáveis proposicionais em valores verdade.

Em um problema com um número finito de proposições, e os números costumam ser pequenos o suficiente para que a análise sistemática de todas as combinações de valores verdade seja viável na prática.

3.2.2. Sintaxe de Lógica Proposicional🔗

Para construir fórmulas, não poderemos mais usar a notação de Lean disponível para Prop. Quando escrevemos p ∧ q, o símbolo ∧ é um operador infixado (aparece no meio dos argumentos) e representa o construtor And.intro do tipo And. Os operadores, para serem usados de forma infixada, precisam ter um mecanismo de precedência para permitir que termos como p ∧ q ∧ r sejam interpretados como p ∧ (q ∧ r) e não (p ∧ q) ∧ r, ou seja, tenham sempre uma leitura não ambigua. Nada disso estará ao nosso dispor na sintaxe que iremos introduzir nesta seção.

Nossas fórmulas serão representadas por termos do tipo indutivo Formula. Um átomo é identificado por um nome, e o nome é uma String.

Os contrutores Formula.top e Formula.bot representam as proposições "sempre verdadeira" e "sempre falsa". São objetos sintáticos que serão sempre interpretados como os valores verdade true e false na semântica. Com este tipo, podemos representar fórmulas arbitrariamente complexas.

Como não temos símbolos infixados, não temos ambiguidade. As duas possíveis interpretações para a sentença ambigua em português "Maira é jovem e bonita ou triste" seriam:

Na lógica proposicional (PL, "propotional logic"), uma linguagem proposicional é o conjunto de todas as fórmulas que podem ser construídas a partir de um vocabulário de símbolos não lógicos (os átomos representados por Formula.atom). Acima, a partir dos átomos construídos com as strings "MJ", "MB" e "MT", infinitas fórmulas de complexidade arbitrária podem ser construídas pela combinação dos demais construtores de Formula. Cada um destes construtores representam um operador lógico.

Podemos também pensar que uma dada fórmula (ou conjunto de fórmulas) induz um vocabulário, o conjunto de todos os símbolos que ocorreram na fórmula (ou conjunto de fórmulas). No exemplo anterior, j, b e t são identificadores em Lean para termos do tipo Formula, representam fórmulas em PL mas não estão em PL, estão na metalinguagem. As strings "MJ", "MB" e "MT" são os nomes dos átomos usados nas formulas, o vocabulário destas fórmulas.

A função names abaixo extrai o vocabulário de uma fórmula. A lista resultante deve estar ordenada e sem repetições.

Nem todos os conectivos precisam ser definidos como "primitivos". Como vimos na seção pl-lean a implicação pode ser definida como uma dijunção. E a dupla implicação como uma conjunção de implicações.

A conjunção e a disjunção são binárias. Poderiam receber uma lista de fórmulas conj (fs : List Formula), mas um construtor que guarda uma List Form dentro do próprio tipo o torna um indutivo nested, mais complicado de manipular em Lean. Mas podemos definir funções que recebem listas de fórmulas e constrem conjunções e disjunções. Abaixo top/bot são a base da recursão de conjs/disjs.

Note que Formula.bot é o elemento neutro da dijunção, bot ∨ a. E Formula.top é o elemento neutro da conjunção, top ∧ a. Uma conjunção vazia é sempre verdadeira, uma disjunção vazia é sempre falsa. O que sugere as implementações alternativas a seguir.

Um termo do tipo Formula é um dado. Nenhum dos exercícios abaixo seriam possíveis em Prop. Não há como perguntar "quantos ∧ tem esta proposição" a um valor de tipo Prop, porque Prop não guarda a fórmula que o provou. Vamos definir duas fórmulas para usar nos exercícios seguintes.

3.2.3. Semântica de Lógica Proposicional🔗

Todas as regras de derivação que usamos em "Proof" são justificadas por uma noção semântica de consequência lógica. Entendemos que P deve ser verdade sempre que P ∧ Q for verdade, para qualquer possível tradução de P e Q de volta para expressões em uma linguagem natural, por isso aceitamos P ∧ Q ⊧ P. Para formalizar esta noção de "todas as possíveis traduções", vamos precisar de um processo para avaliar fórmulas lógicas em valores verdade.

A partir de um mapeamento inicial de símbolos proposicionais em valores boleanos, o tipo Bool em Lean, obtemos de forma recursiva o valor verdade de qualquer termo do tipo Formula. Os construtores Formula.top e Formula.bot são constantes, nenhuma valoração os afeta. Podemos perceber que, de todos os casos da recursão, só o caso do átomo (construtor Formula.atom) consulta a valoração passada; os outros casos apenas combinam os valores verdade das subfórmulas.

A função Formula.eval faz a recursão e recebe como parâmetro a função que dá o valor verdade de um átomo. Toda a semântica que construímos a seguir passa por Formula.eval.

Chamamos as fórmulas que são sempre verdade para qualquer valoração de suas variáveis proposicionais de tautologias, ou, simplesmente, fórmulas válidas. Se α é uma tautologia, significa que ⊨ α, não depende de nenhuma hipótese para ser verdade. As fórmulas que são sempre falsas para toda valoração são chamadas de contradições (ou insatisfatíveis). Uma fórmula é satisfatível se há pelo menos uma valoração que a torna verdadeira. Uma fórmula é contingente se existe pelo menos uma valoração que torna a fórmula verdadeira e pelo menos uma que a torna falsa. Podemos concluir que se α é uma contradição, então ⊨ ¬ α (sua negação é válida). Toda tautologia é satisfatível, mas nem toda fórmula satisfatível é uma tautologia.

A seguir, definimos a função allVals que gera a lista de todas as valorações possíveis sobre o vocabulário de uma Formula.

Com estas funções, podemos construir a tabela verdade de uma fórmula.

Para decidir se uma fórmula é tautologia, satisfatível ou contradição, podemos percorrer todas as valorações possíveis, que são finitas, porque uma fórmula tem finitos átomos.

E como já sabemos da seção pl-lean, podemos mostrar que form3 é uma tautologia.

A seguir, escrevemos implies para a relação de consequência lógica, chamando atenção para a relação entre P ⊨ Q e ⊨ P → Q. Uma proposição Q é consequência lógica de P se, e somente se, a implicação P → Q é uma tautologia. Se P → Q ≡ ¬ P ∨ Q ≡ ¬ (P ∧ ¬ Q) então podemos também dizer que P ⊧ Q se e somente se ⊨ ¬ (P ∧ ¬ Q).

Podemos estender para uma consequência lógica de fórmulas {P₁, …, Pₙ} ⊧ α, indicando que toda valoração que torna as fórmulas P₁, …, Pₙ verdadeiras também torna α verdadeira. O que equivale afirmar que a implicação da conjunção das premissas na conclusão é válida ⊧ (P₁ ∧ … ∧ Pₙ) → α.

Duas fórmulas α e β são logicamente equivalentes, escrevemos α ≡ β, se têm o mesmo valor de verdade para toda valoração possível. Segue da definição que todas as tautologias são logicamente equivalentes entre si, e o mesmo vale para as contradições.

A semântica da lógica proposicional também pode ser dada na forma de atualizações sobre valorações. Fixe primeiro um conjunto de valorações como estado corrente e depois defina uma função de atualização que deixa apenas as valorações que satisfazem uma dada fórmula.

Atualizar o estado de todas as valorações com uma contradição não deixa nada; atualizar com uma tautologia não tira nada. Atualizar com uma fórmula contingente tira alguma coisa, e atualizar com sua negação tira o complemento.

3.2.4. Traduzindo Formula para Prop🔗

Dadas as definições da sintaxe e semântica de PL, Podemos provar alguns meta-teoremas sobre elas. Nos capítulos seguintes, estes resultados não serão necessariamente úteis, mas mostram que nossas definições estão consistentes. Os teoremas a seguir estão no nível da linguagem Lean, isto quer dizer que não são teoremas na linguagem PL mas sobre a linguagem PL. Abaixo provamos dois teoremas. O teorema top_equiv_taut diz que toda tautologia é equivalente a Formula.top. O teorema neg_taut_is_contradiction diz que se uma fórmula é uma tautologia, sua negação é uma contradição.

E também podemos provar o princípio da contraposição. Temos que F₁ ⊧ F₂ se e somente se ¬ F₂ ⊧ ¬F₁. Expandindo a definição de Formula.implies e Formula.satisfiable, temos o enunciado do teorema contraposition_principle₁. A prova dele é direta, corresponde a avaliação da definição de Formula.eval seguida da aplicação da comutativade da conjunção boleana. Mas ele não é o princípio diretamente.

O teorema contraposition_principle₂, por outro lado, corresponde exatamente ao enunciado do princípio. Mas, para prová-lo, precisamos de alguns passos adicionais. Primeiro precisamos provar que todas as valorações possíveis para F₁ coincidem com as de F₂. esta é nossa hipótese hv. Também precisamos mostrar que se duas listas são permutações entre si, então ordená-las irá produzir a mesma lista. Este é o teorema auxiliar mergeSort_eq_of_perm. A notação List.perm_append_comm.dedup corresponde a uma composição de provas. Lean resolve para a composição de List.Perm.dedup com List.perm_append_comm. Como o leitor pode imaginar, estes resultados auxiliares combinados com alguns outros teoremas adicionais, seriam suficientes para melhor automação da prova de contraposition_principle₂ e outros teoremas ainda mais relevantes sobre PL. Mas nosso objetivo é somente ilustrar a capacidade de Lean em provar estes resultados. Finalmente, sugerimos que o leitor consulte  (FRO, 2026)Lean FRO (2026). “The Lean Language Reference”. Manuscrito não publicado. . ou navegue pelas definições no seu editor, se desejar entender os todos os teoremas e tácticas usadas nas provas a seguir.

Finalmente, o mapeamento de Formula em Prop pode ser definido como uma função que interpreta cada fórmula como a proposição que ela afirma, dado um mapeamento de átomos em Bool.

Repare no que cada caso faz: ele troca um construtor de Formula pelo conectivo correspondente de Prop. O Formula.conj do dado vira o ∧ da proposição, o Formula.neg vira o ¬. O teorema que fecha o capítulo diz que as duas leituras concordam. Dada uma valoração, computar o valor verdade de uma fórmula resulta em true exatamente quando a proposição resultande da fórmula para a mesma valoração tem prova.