Il teorema di dualità

Il teorema di dualizzazione dice che date due formule F1 ed F2, se le due formule sono equivalenti (F1 ≡ F2) allora anche le loro dualizzate lo sono (dualize F1 ≡ dualize F2).

L'ingrediente principale è la funzione di dualizzazione di una formula F:

• Scambia FTop con FBot e viceversa

• Scambia il connettivo FAnd con FOr e viceversa

• Sostituisce il connettivo FImpl con FAnd e nega la prima sottoformula.

  Ad esempio la formula A → (B ∧ ⊥) viene dualizzata in ¬A ∧ (B ∨ ⊤).

Per dimostrare il teorema di dualizzazione in modo agevole è necessario definire altre nozioni:

• La funzione negate che presa una formula F ne nega gli atomi. Ad esempio la formula (A ∨ (⊤ → B)) deve diventare ¬A ∨ (⊤ → ¬B).

• La funzione invert permette di invertire un mondo v. Ovvero, per ogni indice di atomo i, se v i restituisce 1 allora (invert v) i restituisce 0 e viceversa.

La libreria di Matita

Gli strumenti per la dimostrazione assistita sono corredati da librerie di teoremi già dimostrati. Per portare a termine l'esercitazione sono necessari i seguenti lemmi:

• lemma sem_le_1 : ∀F,v. [[ F ]]_v ≤ 1

  Il lemma stabilisce che per ogni formula e per ogni valutazione v, la semantica della formula è un valore minore o uguale a 1

• lemma min_1_1 : ∀x. x ≤ 1 → 1 - (1 - x) = x

  Il lemma afferma che se x è un numero minore o uguale a 1 (x è 0 oppure 1) allora (1 - (1 - x) = x)

• lemma min_bool : ∀n. min n 1 = 0 ∨ min n 1 = 1

  Il lemma afferma che gli unici due valori ammessi dalla funzione minimo fra un generico numero n e 1 sono solo 0 oppure 1

• lemma min_max : ∀F,G,v.min (1 - [[F]]_v) (1 - [[G]]_v) = 1 - max [[F]]_v [[G]]_v

  Il lemma stabilisce che min (1- *, 1- +) = 1 - max ( * , +)

• lemma max_min : ∀F,G,v.max (1 - [[F]]_v) (1 - [[G]]_v) = 1 - min [[F]]_v [[G]]_v

  Il lemma stabilisce che max (1- *, 1- +) = 1 - min ( * , +)

• lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3

  Il lemma traduce una sorta di proprietà transitiva: se F1 ≡ F2 e F1 ≡ F3 allora F2 ≡ F3.

Il linguaggio di dimostrazione di Matita

Per dimostrare il lemma negate_invert in modo agevole è necessario utilizzare il seguente comando:

• by H1, H2 we proved P (H)

  Il comando by ... we proved visto nella scorsa esercitazione permette di utilizzare più ipotesi o lemmi alla volta separandoli con una virgola.

La prova del teorema di dualità

Il teorema di dualità accennato a lezione dice che se due formule F1 ed F2 sono equivalenti, allora anche le formule duali lo sono.

∀F1,F2:Formula. F1 ≡ F2 → dualize F1 ≡ dualize F2.

Per dimostrare tale teorema è bene suddividere la prova in lemmi intermedi

1. lemma negate_invert, dimostrato per induzione su F, utilizzando min_bool

   ∀F:Formula.∀v:ℕ→ℕ.[[ negate F ]]_v=[[ F ]]_(invert v).
   

2. lemma negate_fun, conseguenza di negate_invert

   ∀F,G:Formula. F ≡ G → negate F ≡ negate G.
   

3. lemma not_dualize_eq_negate, dimostrato per induzione su F, utilizzando max_min e min_max

   ∀F:Formula. negate F ≡ FNot (dualize F)
   

4. lemma not_inj, conseguenza di sem_bool

   ∀F,G:Formula. FNot F ≡ FNot G → F ≡ G
   

Una volta dimostrati tali lemmi la prova del teorema di dualità procede come di seguito:

1. Assume l'ipotesi

   F1 ≡ F2
   

2. Utilizza negate_fun per ottenere

   negate F1 ≡ negate F2
   

3. Utilizzando due volte il lemma not_dualize_eq_negate e il lemma equiv_rewrite ottiene

   FNot (dualize F1) ≡ FNot (dualize F2)
   

4. Conclude utilizzando il lemma not_inj per ottenere la tesi

   dualize F1 ≡ dualize F2