Come si dimostra l’iniettività e si usa il quantificatore esistenziale nella logica formale

Nel contesto della dimostrazione formale, una funzione è iniettiva se ogni elemento del codominio ha al più un elemento corrispondente nel dominio. Dimostrare l’iniettività di funzioni elementari, come la traslazione $x \mapsto x + c$ o la moltiplicazione per un valore reale non nullo $x \mapsto c \cdot x$ , richiede spesso l’introduzione di variabili e l’uso di proprietà algebriche elementari. Per esempio, l’iniettività di $x \mapsto x + c$ si dimostra introducendo due elementi $x_1, x_2$ tali che la loro immagine coincide e deducendo che $x_1 = x_2$ tramite la proprietà dell’addizione. Analogamente, la composizione di due funzioni iniettive si dimostra iniettiva grazie alla proprietà transitiva della definizione: se $f$ e $g$ sono iniettive, allora la funzione composta $g \circ f$ conserva l’iniettività.

Il quantificatore esistenziale $\exists$ , che esprime l’esistenza di almeno un elemento che soddisfa una certa proprietà, è fondamentale nella formalizzazione matematica. Esso si utilizza, per esempio, per affermare che esiste un numero reale compreso tra 2 e 3, scritto formalmente come $\exists x \in \mathbb{R}, 2 < x \wedge x < 3$ . Dimostrare un’affermazione esistenziale si realizza in modo canonico mostrando un esempio esplicito dell’elemento richiesto, come il numero 2.5. Tale strategia è espressa nel sistema Lean tramite la tattica "use", che consente di fornire direttamente un valore candidato e lascia come obiettivo la dimostrazione della sua proprietà.

Quando si utilizza un quantificatore esistenziale in un’ipotesi, è necessario "smontare" o decomporre l’asserzione per poter ragionare con l’elemento esistente e le sue proprietà. Lean fornisce diversi modi per questo: la tattica "rcases" permette di estrarre le componenti di un’esistenza espressa come coppia o struttura, assegnandole a variabili locali. Questa tecnica è essenziale per ragionamenti matematici dove si suppone l’esistenza di un oggetto con proprietà note e si vuole derivare ulteriori conseguenze.

Ad esempio, consideriamo funzioni reali $f$ e $g$ dotate di un limite superiore (ossia esistono $a$ e $b$ tali che $f(x) \leq a$ e $g(x) \leq b$ per ogni $x$ ). Si può dimostrare che anche la funzione somma $f + g$ ha un limite superiore, dato da $a + b$ . Il metodo consiste nel "smontare" le ipotesi di esistenza del limite superiore di $f$ e $g$ , per poi costruire esplicitamente il limite superiore della somma.

Lean offre inoltre diverse alternative per la decomposizione di dati esistenziali, come "obtain" o il costrutto "cases", che rispecchiano il pattern matching comune nei linguaggi funzionali. Questo riflette la natura computazionale della logica formale, dove le prove sono oggetti con struttura interna analizzabile e manipolabile.

Oltre alla dimostrazione dell’esistenza, è importante saper usare la notazione e le tattiche per combinare oggetti esistenti in nuove costruzioni, come nel caso della moltiplicazione di funzioni per scalari non negativi o della composizione di funzioni iniettive. Le tecniche di destrutturazione degli oggetti esistenziali sono il cuore del ragionamento formale e matematico, poiché permettono di trasformare informazioni implicite in dati espliciti e utilizzabili.

Infine, la comprensione profonda di queste tecniche è cruciale per chi si avvicina alla formalizzazione della matematica: il passaggio dall’esistenza astratta alla manipolazione concreta degli elementi esistenti è ciò che rende possibile lo sviluppo di teorie più complesse e l’automatizzazione delle dimostrazioni. Questi strumenti rappresentano un ponte tra la matematica tradizionale e la sua formalizzazione computazionale, ampliando gli orizzonti della ricerca e dell’applicazione.

È importante notare che la pratica di "smontare" dati esistenziali va oltre la pura tecnica: essa incarna il principio di rendere esplicite le informazioni implicite, un processo che sottende gran parte del pensiero matematico rigoroso e che consente di gestire in modo sistematico la complessità delle prove. In più, il riconoscimento della funzione compositiva come un’operazione che conserva proprietà come l’iniettività sottolinea come la struttura e le proprietà matematiche siano spesso preservate da operazioni naturali, un concetto centrale nello studio delle funzioni e delle loro applicazioni.

Come si dimostra un'uguaglianza logica e come si lavora con congiunzioni, bi-implicazioni e disgiunzioni in Lean?

In Lean, la dimostrazione di enunciati logici segue una metodologia rigorosa che si avvicina molto alla manipolazione formale delle proposizioni, ma con una sintassi e un meccanismo propri. Ad esempio, una bi-implicazione $A \leftrightarrow B$ non è definita semplicemente come $(A \to B) \wedge (B \to A)$ , anche se il comportamento è molto simile. Infatti, Lean consente di accedere direttamente alle due direzioni della bi-implicazione con i metodi .mp e .mpr, o semplicemente .1 e .2, corrispondenti ai due sensi della definizione.

La dimostrazione di un'uguaglianza logica, o di un enunciato se e solo se, si può realizzare utilizzando il comando constructor, che consente di dividere il problema in due sotto-obiettivi: la dimostrazione di $A \to B$ e la dimostrazione di $B \to A$ . Questo ricorda la prova di una congiunzione, perché la bi-implicazione può essere vista come una congiunzione di due implicazioni.

Un esempio emblematico è la dimostrazione che $\neg (y \leq x) \leftrightarrow x \neq y$ , che si può affrontare con tecniche come la contrapositiva e l'uso della proprietà antisimmmetrica del rapporto d'ordine $\leq$ . La dimostrazione formale di queste proprietà si basa sul riconoscimento che $\leq$ è una relazione parziale d'ordine, che soddisfa riflessività, transitività e antisimmmetria.

Un altro aspetto fondamentale è la capacità di riscrivere enunciati usando equivalenze note, per esempio trasformando espressioni con valori assoluti tramite il teorema abs_lt, che trasforma $|x| < y$ in $-y < x \wedge x < y$ . Allo stesso modo, si può riscrivere una proprietà sulla divisibilità come $m \mid \gcd(n,k)$ nell'equivalente $m \mid n \wedge m \mid k$ usando Nat.dvd_gcd_iff. Queste tecniche di riscrittura, basate su equivalenze, sono potenti per semplificare le dimostrazioni e riorganizzare i problemi in forme più maneggevoli.

L'uso delle negazioni in Lean richiede attenzione particolare. Ad esempio, la negazione di una proprietà come la monotonia può essere espressa con una doppia negazione trasformata in esistenza di un controesempio tramite la riscrittura con il teorema not_monotone_iff, che porta a una forma che implica l'esistenza di due valori $x,y$ tali che $x \leq y$ ma $f(x) > f(y)$ .

Si evidenzia anche la distinzione tra preordine e ordine parziale. Un preordine è solo riflessivo e transitivo, mentre l'ordine parziale è anche antisimmmetrico. Questa differenza si riflette nelle proprietà degli ordini stretti derivati, che si definiscono come $a < b \leftrightarrow a \leq b \wedge \neg (b \leq a)$ . Nei preordini, si possono ancora dimostrare proprietà come l'irriflessività e la transitività dell'ordine stretto, anche senza antisimmmetria.

Passando alla disgiunzione, la strategia canonica è di dimostrare almeno uno dei due membri della disgiunzione $A \vee B$ . In Lean, si usano i comandi left e right per scegliere rispettivamente $A$ o $B$ . Quando si scrive un termine di prova, si possono usare le forme esplicite Or.inl e Or.inr che indicano l'introduzione a sinistra o a destra della disgiunzione. È importante notare che Lean non può indovinare quale disgiunto si vuole dimostrare senza questa esplicita indicazione.

Per lavorare con ipotesi di forma disgiuntiva si utilizza la tecnica del "proof by cases" tramite il comando rcases, che genera due obiettivi distinti: uno con $A$ assunto vero, l'altro con $B$ assunto vero. In questo modo si può ragionare separatamente in ciascun caso, mantenendo il flusso logico chiaro e organizzato.

Lean permette anche di utilizzare la sintassi di pattern matching tipica della programmazione funzionale per manipolare le disgiunzioni, rendendo le dimostrazioni più leggibili e controllate. I comandi cases con case inl e case inr permettono di nominare esplicitamente i casi, facilitando la gestione di dimostrazioni che si basano su un'analisi a casi.

Nel trattamento degli ordini e delle relazioni, è essenziale riconoscere il ruolo delle proprietà riflessive, transitive e antisimmmetriche. Queste proprietà sono le fondamenta per la definizione di ordini parziali e preordini e condizionano le modalità con cui si possono dimostrare proprietà come l'irriflessività dell'ordine stretto o la sua transitività. Inoltre, la capacità di riscrivere e scomporre enunciati in forme equivalenti è uno strumento fondamentale per affrontare e semplificare problemi complessi in Lean.

Oltre alle tecniche esposte, è utile comprendere come la formalizzazione di queste proprietà logiche nel sistema Lean permetta di collegare la logica matematica con la programmazione e la verifica formale. Questo ponte tra logica e programmazione consente di sfruttare Lean non solo come ambiente di prova matematica, ma anche come strumento per lo sviluppo di software affidabile, dove le proprietà logiche sono garantite formalmente.

Il lettore dovrebbe inoltre tener presente che, sebbene Lean offra strumenti potenti come rw, constructor, cases, e rcases, la loro efficacia dipende dall'approfondita comprensione delle strutture logiche sottostanti, dalla natura delle relazioni che si stanno trattando, e dalla strategia di riscrittura o scomposizione adottata. La padronanza di queste tecniche richiede pratica, ma apre la porta a dimostrazioni precise, automatizzabili e altamente affidabili in ambito matematico e informatico.

Come si dimostrano proprietà fondamentali degli insiemi usando Lean e la teoria dei tipi

Nel contesto della teoria degli insiemi formalizzata in Lean, l’intersezione, l’unione e la differenza tra insiemi sono trattate come proprietà logiche, dove un insieme è definito come una funzione che associa a un elemento un predicato, ossia una proposizione. Questo approccio fonda tutta la teoria su una base intensamente logica e funzionale, piuttosto che su una semplice collezione di elementi.

L’esempio classico di distribuzione dell’intersezione rispetto all’unione, $s \cap (t \cup u) \subseteq (s \cap t) \cup (s \cap u)$ , può essere dimostrato tramite il metodo di analisi dei casi (cases tactic) in Lean, il quale suddivide l’appartenenza a $t \cup u$ nelle due possibilità $t$ o $u$ . La dimostrazione si avvale di una decomposizione sistematica degli elementi, utilizzando ipotesi di appartenenza agli insiemi e ricostruendo l’appartenenza agli insiemi target tramite costruttori logici.

Lean permette inoltre di abbreviare queste dimostrazioni sfruttando la notazione $rintro$ , che permette un’introduzione combinata di variabili e pattern matching sulle disgiunzioni, rendendo più compatte e leggibili le prove. La flessibilità di Lean si esprime anche nella gestione di insiemi con operazioni come la differenza tra insiemi, definita tramite la negazione di appartenenza e la congiunzione con l’appartenenza a un altro insieme.

Un aspetto centrale nell’uso di Lean è il principio di estensionalità degli insiemi: due insiemi sono uguali se e solo se hanno gli stessi elementi. Questo principio è formalizzato con il tactic $ext$ , che riduce l’uguaglianza tra insiemi alla doppia inclusione. In alternativa, la libreria di Lean offre teoremi come $Subset.antisymm$ , che permette di dimostrare l’uguaglianza tra insiemi dimostrando le inclusioni reciproche, offrendo una via strutturata e modulare alla formalizzazione.

La rappresentazione degli insiemi in Lean è profondamente radicata nella teoria dei tipi: un insieme è una funzione che associa a ciascun elemento un predicato, quindi l’appartenenza $x \in s$ si traduce nell’espressione $s(x)$ . Questo spiega anche come la notazione $\{ y \mid P(y) \}$ sia un modo di costruire insiemi tramite proprietà, sfruttando la semplificazione logica per passare dalla definizione formale alle applicazioni concrete.

La definizione di insiemi tramite proprietà consente di esprimere insiemi come quelli dei numeri pari o dispari, o di definire l’insieme universo e l’insieme vuoto tramite predicati costantemente veri o falsi. Questa astrazione favorisce una gestione elegante delle operazioni insiemistiche, traducendole in manipolazioni di predicati logici.

Un elemento essenziale nella formalizzazione in Lean è la gestione dei quantificatori limitati, $\forall x \in s$ e $\exists x \in s$ , che permettono di esprimere proprietà e esistenza relative a insiemi specifici. Questi quantificatori limitati facilitano l’uso di teoremi e tattiche specifiche che lavorano su insiemi riducendo i domini di quantificazione, semplificando notevolmente le dimostrazioni complesse.

Gli indici usati per unioni o intersezioni infinite o generalizzate sono anch’essi incorporati nel formalismo, potendo sostituire $\mathbb{N}$ con qualsiasi tipo arbitrario $I$ . Questo amplia la versatilità del sistema nel trattare famiglie di insiemi indicizzati, cruciale nelle dimostrazioni che coinvolgono strutture matematiche più complesse.

È importante sottolineare che, nella pratica della dimostrazione assistita, l’attenzione a dettagli come la necessità di parentesi in alcuni pattern matching, o la scelta di tattiche più compatte come $rintro$ e $use$ , influisce profondamente sulla chiarezza e sulla efficacia della dimostrazione stessa. L’approccio logico-funzionale di Lean, con la sua enfasi su pattern matching e costruttori logici, richiede una mentalità precisa, ma permette una formalizzazione rigorosa e trasparente.

Inoltre, la capacità di usare tecniche come la riscrittura con assunzioni ( $rwa$ ) rende la gestione delle ipotesi più fluida, facilitando l’applicazione di equivalenze tra concetti matematici, come nel caso delle diverse definizioni di primalità nei numeri naturali. Questa sinergia tra definizioni e strategie di prova è centrale per la padronanza del sistema.

L’interconnessione tra teoria degli insiemi e logica predicativa, messa in evidenza dall’approccio di Lean, offre al lettore un’importante prospettiva: la teoria degli insiemi non è semplicemente una raccolta di elementi, ma una teoria di proprietà e predicati. Comprendere questa visione permette di apprezzare la profondità degli strumenti formali utilizzati e le loro implicazioni nella costruzione di teorie matematiche rigorose.

È veramente irrazionale la radice quadrata di due?

Affermare che la radice quadrata di due è irrazionale implica innanzitutto un'affermazione circa la natura dei numeri razionali: nessun numero esprimibile come quoziente di due interi può coincidere con √2. Una tale proposizione, sebbene classica, necessita di un rigore formale nel contesto della formalizzazione matematica, specialmente in ambienti computazionali come Lean. È importante comprendere che la radice quadrata di due, pur essendo definita all'interno dei numeri reali (e complessi), ha un significato specifico a seconda della struttura numerica in cui ci si muove.

In sistemi formali come Mathlib, le diverse categorie numeriche — numeri naturali, interi, razionali, reali e complessi — sono rappresentate da tipi distinti, ognuno con proprie regole e metodi di inferenza. Questa separazione, se da un lato complica la transizione da un dominio all'altro, dall’altro permette di sfruttare al meglio le caratteristiche peculiari di ciascuna struttura: per esempio, l'induzione è agevolmente applicabile ai numeri naturali, mentre la divisibilità è trattata più efficacemente nel dominio degli interi, isolando i reali.

Il ragionamento che porta a dimostrare l’irrazionalità di √2 si basa su un’analisi profonda delle proprietà dei numeri interi e dei loro divisori. Per esempio, se si assume che √2 sia razionale, allora esistono due interi a e b tali che √2 = a / b e la frazione sia in forma ridotta. Elevando al quadrato si ottiene 2 = a² / b², ovvero a² = 2b². Da qui segue che a deve essere pari, e quindi si può scrivere a = 2k. Sostituendo, si ottiene (2k)² = 4k² = 2b², ovvero b² = 2k², il che implica che anche b è pari — in contraddizione con l’assunzione che a e b siano coprimi. Questa dimostrazione, ben nota, assume però nei formalismi un significato più profondo, poiché richiede una gestione rigorosa delle strutture coinvolte.

La teoria può essere ulteriormente rafforzata: se r è un numero positivo la cui radice k-esima è razionale, allora r deve essere una potenza k-esima. Questo risultato richiede una teoria ben sviluppata dei prodotti e delle somme su insiemi finiti. A tal fine, Mathlib offre strumenti per ragionare su insiemi finiti e operazioni su tali insiemi attraverso il tipo Finset, una rappresentazione formale degli insiemi finiti che permette di definire e manipolare somme (Σ) e prodotti (Π) in modo strutturato.

Tornando ai numeri naturali, è essenziale comprendere la loro costruzione formale tramite tipi induttivi. In Lean, Nat è definito come un tipo induttivo con due costruttori: zero e succ. Questo significa che ogni numero naturale può essere costruito applicando un numero finito di volte il costruttore succ a zero. Questa costruzione "libera" garantisce che il successore sia un'applicazione iniettiva e che zero non sia il successore di alcun numero. Inoltre, l’induzione e la ricorsione su Nat derivano direttamente dalla sua definizione.

Questa definizione induttiva permette di costruire funzioni per ricorsione, come nel caso della funzione fattoriale:

lean
def fac : ℕ → ℕ 
| 0       => 1
| n + 1   => (n + 1) * fac n

Qui il caso base è fac 0 = 1, e l'induzione viene usata per definire i casi successivi. Tale funzione, già disponibile nella libreria come Nat.factorial, può essere utilizzata per dimostrare proprietà numeriche come la positività di ogni fattoriale, o per costruire argomenti combinatori.

Un altro esempio interessante di applicazione dell’induzione riguarda il teorema secondo cui ogni numero positivo i minore o uguale a n divide il fattoriale di n. Questa proprietà è alla base di molte costruzioni aritmetiche e combinatorie, e la sua dimostrazione fa uso dell’induzione, sfruttando il fatto che se i ≤ n, allora i divide n!, essendo presente come fattore.

Infine, l’espressione di somme e prodotti finiti è gestita attraverso Finset.sum e Finset.prod. Queste espressioni permettono di manipolare identità come:

lean
example (f : ℕ → ℕ) : Σ x ∈ range 0, f x = 0

example (f : ℕ → ℕ) (n : ℕ) : Σ x ∈ range (n+1), f x = Σ x ∈ range n, f x + f n

Le identità per somme e prodotti su intervalli di numeri naturali sono fondamentali per l’analisi combinatoria e la teoria dei numeri elementare. Permettono di costruire argomenti su proprietà numeriche di funzioni definite sui naturali, e in particolare sono strumenti imprescindibili nella generalizzazi

Cosmopolitismo in crisi? Comprendere il disincanto politico nell’epoca di Brexit e Trump
Come Allineare Correttamente il Raggio Centrale nelle Proiezioni Craniche: Tecniche e Correzioni
Quali sono le sfide e le opportunità della sostenibilità nella chimica dei materiali?
Qual è la strategia più vantaggiosa: il rischio calcolato o l'approccio prudente?