📐 Dimostrazioni di logica proposizionale con Lean 4: una guida pratica 🔗

Questo articolo offre un percorso tecnico attraverso i concetti fondamentali della logica proposizionale e la loro implementazione formale utilizzando il linguaggio di programmazione e dimostratore di teoremi (theorem prover) Lean 4.

Che tu sia un matematico interessato a formalizzare dimostrazioni o un programmatore che si addentra nella teoria dei tipi, questa guida ricostruisce la logica a partire dai principi primi. Partiremo dalle costanti logiche di base ed esploreremo come Lean 4 modelli elegantemente i costrutti logici utilizzando l’isomorfismo di Curry-Howard — il principio secondo cui le proposizioni sono tipi e le dimostrazioni sono programmi.

📑 Indice 🔗

⚙️ Il preambolo: preparare l’ambiente 🔗

Prima di definire i nostri connettivi logici, dobbiamo configurare un ambiente di base. In Lean 4, questo viene solitamente fatto utilizzando due comandi specifici per controllare lo scope e il comportamento computazionale.

namespace Basic

noncomputable section

• namespace Basic: Questo comando raggruppa le nostre definizioni, evitando conflitti di nomi con la libreria integrata di Lean (il Prelude). Ci consente di ridefinire da zero strutture fondamentali come True, False e And a scopo didattico.
• noncomputable section: Lean 4 è sia un dimostratore di teoremi sia un linguaggio di programmazione funzionale. Per impostazione predefinita, cerca di generare bytecode eseguibile per ogni definizione. Contrassegnare una sezione come noncomputable indica al compilatore di saltare questo passaggio, una pratica comune nella logica formale dove ci interessano le proprietà matematiche piuttosto che l’esecuzione a runtime.

🧩 I connettivi logici fondamentali 🔗

In questa sezione definiremo gli elementi fondanti della logica, mappando la notazione matematica standard sul codice Lean 4.

✅ 1. Vero (⊤) 🔗

La proposizione più semplice è quella universalmente valida dal punto di vista logico. In termini di programmazione, $\top$ si comporta come un tipo Unit — ha esattamente uno stato e non trasporta dati aggiuntivi.

Definizione:

inductive True : Prop where
  | intro : True

Poiché è definito con un singolo costruttore (intro), l’unico modo per “dimostrare” True è fornire esattamente questo costruttore.

Esempi:

-- Dimostrare True incondizionatamente
example : True := True.intro

-- Qualsiasi proposizione 'a' implica banalmente True
example {a : Prop} : a → True := fun _ => True.intro

❌ 2. Falso (⊥) 🔗

Mentre True è definito dalla banale esistenza di una dimostrazione, False è definito dalla totale assenza di essa. È un tipo vuoto (Empty type o Void type).

Definizione:

inductive False : Prop

Poiché False non ha costruttori, non è mai possibile istanziarlo dal nulla. Rappresenta una contraddizione logica.

Il principio di esplosione (Ex Falso Quodlibet): Se ti ritrovi mai in possesso di una dimostrazione di False, la logica crolla e puoi dimostrare qualsiasi cosa. Lean gestisce questo caso usando il ricorsore False.elim.

-- Dal falso segue qualsiasi proposizione 'a' (⊥ → a)
def False.elim {a : Prop} (false_proof : False) : a := 
  false_proof.rec

🔄 3. Negazione (¬) 🔗

In Lean 4, la negazione non è un concetto primitivo integrato. Viene invece definita funzionalmente usando l’implicazione e False. Per dimostrare che la proposizione $a$ è falsa (indicata con $\neg a$), devi mostrare una funzione in cui assumere $a$ porta direttamente a una contraddizione ($\bot$).

Definizione:

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

Teoremi chiave:

-- Dimostrare la negazione: se assumere 'a' dimostra False, allora Not 'a' è vero.
theorem Not.intro {a : Prop} (h : a → False) : Not a := 
  fun ha => h ha

-- Introduzione della doppia negazione (a → ¬¬a)
theorem not_not_intro {a : Prop} (ha : a) : Not (Not a) := 
  fun na => na ha  -- 'na' ha tipo (a → False), quindi passare 'ha' produce False.

-- Modus Tollens: se (a → b) e (¬b), allora (¬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. Implicazione (→) 🔗

Poiché Lean si basa sulla teoria dei tipi, l’implicazione logica ($a \to b$) viene trattata letteralmente come una funzione. Per dimostrare che $a$ implica $b$, devi scrivere una funzione che prenda una dimostrazione arbitraria di $a$ e restituisca una dimostrazione di $b$.

Esempio di implicazione concatenata: Se puoi trasformare $c$ in $a$ e trasformare $b$ in $d$, puoi trasformare una funzione da $a \to b$ in una da $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. Congiunzione (∧) 🔗

La congiunzione logica, che richiede che sia $a$ sia $b$ siano vere, è modellata come una structure. In termini di programmazione, si tratta di un tipo Prodotto (una struct o una tupla) che contiene due prove distinte.

Definizione:

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

Schemi di dimostrazione chiave:

-- Introduzione: creare un And
example {a b : Prop} (ha : a) (hb : b) : And a b := 
  And.intro ha hb

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

🔀 6. Disgiunzione (∨) 🔗

La disgiunzione logica richiede che almeno una delle proposizioni sia vera. A differenza di And, Or è un tipo Somma induttivo (una tagged union), poiché esistono due modi distinti e alternativi per costruire una dimostrazione.

Definizione:

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

Per dimostrare $a \lor b$, racchiudi una dimostrazione di $a$ nel costruttore inl (inject-left), oppure una dimostrazione di $b$ nel costruttore inr (inject-right).

Esempio:

-- Simmetria: 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. Equivalenza logica (↔) 🔗

La doppia implicazione, o “se e solo se” (Iff), indica che due proposizioni sono logicamente equivalenti. È definita come una struttura che contiene implicazioni in entrambe le direzioni.

Definizione:

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

Esempio di riflessività:

-- Ogni proposizione è equivalente a se stessa (a ↔ a)
theorem Iff.refl {a : Prop} : Iff a a :=
  Iff.intro (fun ha => ha) (fun ha => ha)

🎯 Conclusione e punti chiave 🔗

Ricostruendo la logica proposizionale da zero in Lean 4, sveliamo la bellezza meccanica dei sistemi formali:

1. Costruttivo per impostazione predefinita: Definiamo cosa significa possedere una prova di una verità, piuttosto che limitarci ad affermare che qualcosa è vero.
2. Proposizioni come tipi: Attraverso la corrispondenza di Curry-Howard, i connettivi logici corrispondono direttamente alle strutture di programmazione standard: l’implicazione è una funzione, And è una struct, Or è un enum, True è unit e False è void.
3. Dimostrazioni come programmi: Scrivere una dimostrazione matematica in Lean equivale esattamente a scrivere una funzione type-safe che soddisfa una firma specifica.

Padroneggiare questi mattoni fondamentali fornisce le basi indispensabili per affrontare teoremi matematici più complessi, la logica dei predicati e la verifica di sistemi software complessi.