📐 Provas de Lógica Proposicional Usando Lean 4: Um Guia Prático 🔗

Este post oferece um passo a passo técnico dos conceitos fundamentais da lógica proposicional e sua implementação formal usando a linguagem de programação e assistente de provas (theorem prover) Lean 4.

Seja você um matemático buscando formalizar demonstrações ou um programador mergulhando na teoria dos tipos, este guia reconstrói a lógica a partir dos primeiros princípios. Começaremos com constantes lógicas básicas e exploraremos como o Lean 4 modela construções lógicas com elegância usando o Isomorfismo de Curry-Howard — o princípio de que proposições são tipos e provas são programas.

📑 Índice 🔗

⚙️ O Preâmbulo: Preparando o Terreno 🔗

Antes de definir nossos conectivos lógicos, precisamos configurar um ambiente base. No Lean 4, isso geralmente é feito usando dois comandos específicos para controlar o escopo e o comportamento computacional.

namespace Basic

noncomputable section

• namespace Basic: Este comando agrupa nossas definições, evitando conflitos de nomes com a biblioteca padrão do Lean (o Prelude). Ele nos permite redefinir estruturas fundamentais como True, False e And do zero para fins educacionais.
• noncomputable section: O Lean 4 é tanto um assistente de provas quanto uma linguagem de programação funcional. Por padrão, ele tenta gerar bytecode executável para cada definição. Marcar uma seção como noncomputable diz ao compilador para pular essa etapa, o que é comum na lógica formal, onde nos importamos com propriedades matemáticas em vez de execução em tempo de execução (runtime).

🧩 Conectivos Lógicos Fundamentais 🔗

Nesta seção, definiremos os elementos fundamentais da lógica, mapeando a notação matemática padrão para código em Lean 4.

✅ 1. Verdadeiro / True (⊤) 🔗

A proposição mais simples é aquela que é universalmente válida do ponto de vista lógico. Em termos de programação, $\top$ se comporta como um tipo Unidade (Unit type) — possui exatamente um estado e não carrega dados adicionais.

Definição:

inductive True : Prop where
  | intro : True

Como é definido com um único construtor (intro), a única maneira de “provar” True é fornecer exatamente esse construtor.

Exemplos:

-- Proving True unconditionally
example : True := True.intro

-- Any proposition 'a' trivially implies True
example {a : Prop} : a → True := fun _ => True.intro

❌ 2. Falso / False (⊥) 🔗

Enquanto True é definido pela existência trivial de uma prova, False é definido pela ausência total de uma. É um tipo Vazio (Empty type ou Void type).

Definição:

inductive False : Prop

Como False não possui construtores, você nunca pode instanciá-lo do nada. Ele representa uma contradição lógica.

O Princípio da Explosão (Ex Falso Quodlibet): Se você algum dia se encontrar com uma prova de False em mãos, a lógica entra em colapso e você pode provar qualquer coisa. O Lean lida com isso usando o recursor False.elim.

-- From a falsehood, any proposition 'a' follows (⊥ → a)
def False.elim {a : Prop} (false_proof : False) : a := 
  false_proof.rec

🔄 3. Negação (¬) 🔗

No Lean 4, a negação não é um conceito primitivo embutido. Em vez disso, ela é definida funcionalmente usando implicação e False. Para provar que a proposição $a$ é falsa (denotada por $\neg a$), você deve demonstrar uma função na qual assumir $a$ leva diretamente a uma contradição ($\bot$).

Definição:

def Not (a : Prop) : Prop := a → False

Teoremas Principais:

-- Proving Negation: If assuming 'a' proves False, then Not 'a' is true.
theorem Not.intro {a : Prop} (h : a → False) : Not a := 
  fun ha => h ha

-- Double Negation Introduction (a → ¬¬a)
theorem not_not_intro {a : Prop} (ha : a) : Not (Not a) := 
  fun na => na ha  -- 'na' has type (a → False), so passing 'ha' yields False.

-- Modus Tollens: If (a → b) and (¬b), then (¬a)
theorem Not.imp {a b : Prop} (nb : Not b) (ab : a → b) : Not a := 
  fun ha => 
    have hb : b := ab ha
    nb hb

➡️ 4. Implicação (→) 🔗

Como o Lean se baseia na teoria dos tipos, a implicação lógica ($a \to b$) é tratada literalmente como uma função. Para provar que $a$ implica $b$, você deve escrever uma função que recebe uma prova arbitrária de $a$ e retorna uma prova de $b$.

Exemplo de Implicação Encadeada: Se você consegue transformar $c$ em $a$, e transformar $b$ em $d$, você pode transformar uma função de $a \to b$ em uma de $c \to d$.

theorem imp_imp_imp {a b c d : Prop} 
  (ca : c → a) (bd : b → d) : (a → b) → (c → d) := 
  fun ab => fun hc => 
    have ha : a := ca hc
    have hb : b := ab ha
    bd hb

🔗 5. Conjunção (∧) 🔗

A conjunção lógica, que exige que tanto $a$ quanto $b$ sejam verdadeiros, é modelada como uma structure. Em termos de programação, trata-se de um tipo Produto (Product type) (uma struct ou tupla) que armazena duas evidências separadas.

Definição:

structure And (a b : Prop) : Prop where
  intro ::
  left : a
  right : b

Padrões Principais de Prova:

-- Introduction: Creating an And
example {a b : Prop} (ha : a) (hb : b) : And a b := 
  And.intro ha hb

-- Symmetry: a ∧ b → b ∧ a
theorem And.symm {a b : Prop} (h : And a b) : And b a := 
  And.intro h.right h.left

🔀 6. Disjunção (∨) 🔗

A disjunção lógica exige que pelo menos uma das proposições seja verdadeira. Ao contrário de And, Or é um tipo Soma (Sum type) indutivo (uma tagged union), porque existem duas maneiras distintas e alternativas de construir uma prova.

Definição:

inductive Or (a b : Prop) : Prop where
  | inl (h : a) : Or a b
  | inr (h : b) : Or a b

Para provar $a \lor b$, você encapsula uma prova de $a$ no construtor inl (inject-left), ou uma prova de $b$ no construtor inr (inject-right).

Exemplo:

-- Symmetry: a ∨ b → b ∨ a
theorem Or.symm {a b : Prop} (h : Or a b) : Or b a :=
  match h with
  | Or.inl ha => Or.inr ha
  | Or.inr hb => Or.inl hb

↔️ 7. Equivalência Lógica (↔) 🔗

A bi-implicação, ou “se e somente se” (Iff), representa que duas proposições são logicamente equivalentes. Ela é definida como uma estrutura que armazena implicações em ambas as direções.

Definição:

structure Iff (a b : Prop) : Prop where
  intro ::
  mp : a → b
  mpr : b → a

Exemplo de Reflexividade:

-- Every proposition is equivalent to itself (a ↔ a)
theorem Iff.refl {a : Prop} : Iff a a :=
  Iff.intro (fun ha => ha) (fun ha => ha)

🎯 Conclusão e Principais Lições 🔗

Ao reconstruir a lógica proposicional do zero no Lean 4, revelamos a beleza mecânica dos sistemas formais:

1. Construtivo por Padrão: Definimos o que significa possuir uma evidência de uma verdade, em vez de meramente afirmar que algo é verdadeiro.
2. Proposições como Tipos: Por meio do mapeamento de Curry-Howard, os conectivos lógicos correspondem diretamente a estruturas padrão de programação: a implicação é uma função, And é uma struct, Or é um enum, True é unit e False é void.
3. Provas como Programas: Escrever uma prova matemática no Lean é idêntico a escrever uma função com segurança de tipos (type-safe) que satisfaz uma assinatura específica.

Dominar esses blocos de construção fundamentais fornece a base essencial para encarar teoremas matemáticos mais complexos, lógica de predicados e a verificação formal de sistemas de software complexos.