Definizione di valutazione delle proposizioni in un'algebra di Heyting

[thedarkhero]

Consideriamo un linguaggio proposizionale $L$ costituito da un insieme di variabili proposizionali $A, B, C,...$, dai connettivi congiunzione $\wedge$, disgiunzione $\vee$, implicazione $\rightarrow$ e negazione $\neg$ e dalle parentesi $($ e $)$.
Indichiamo con $Frm(L)$ l'insieme delle formule ben formate del linguaggio proposizionale $L$.
Consideriamo un'algebra di Heyting $(H, \wedge, \vee, \rightarrow, \neg, \top, \bot)$, dove l'operazione $\neg$ definita ponendo $\neg x = x \rightarrow \bot$ è lo pseudocomplemento.

Una valutazione delle proposizioni del linguaggio $L$ nell'algebra di Heyting $(H, \wedge, \vee, \rightarrow, \neg, \top, \bot)$ è una funzione $V : Frm(L) \to H$ tale che:
1) $V(\top)=\top$;
2) $V(\bot)=\bot$;
3) $V(\phi \wedge \psi) = V(\phi) \wedge V(\psi)$ per ogni $\phi, \psi \in Frm(L)$;
4) $V(\phi \vee \psi) = V(\phi) \vee V(\psi)$ per ogni $\phi, \psi \in Frm(L)$;
5) $V(\phi \rightarrow \psi) = V(\phi) \rightarrow V(\psi)$ per ogni $\phi, \psi \in Frm(L)$;
6) $V(\neg \phi) = \neg V(\phi)$ per ogni $\phi \in Frm(L)$.

Mi domando se questa definizione di valutazione è ridondante o meno.
In particolare, visto che sia in logica classica che in logica intuizionista si ha che $\top \equiv \neg \bot$ e che $\neg \phi \equiv \phi \rightarrow \bot$, penso che si potrebbero rimuovere dalla definizione le condizioni 1) e 6) in quanto:
$V(\top)=V(\neg \bot)=V(\bot \rightarrow \bot)=V(\bot) \rightarrow V(\bot)=\bot \rightarrow \bot=\top$ e
$V(\neg \phi)=V(\phi \rightarrow \bot)=V(\phi) \rightarrow V(\bot)=V(\phi) \rightarrow \bot=\neg V(\phi)$.

Quello che sto affermando è corretto?

[megas_archon]

Sì, 1 e 6 si derivano da 2 e 5.

[thedarkhero]

Grazie!

Invece la proprietà 5) si può ricavare dalle altre proprietà?

Mi verrebbe da dire di no ma non mi viene in mente un esempio di funzione che soddisfa le proprietà 2), 3) e 4) ma non la 5)...

[megas_archon]

No, in generale no (credo che una condizione sufficiente sia che V preservi i sup arbitrari, e penso sia anche necessaria).

[megas_archon]

Il motivo è che in ogni algebra di Heyting (e più in generale in ogni quantale), si può caratterizzare \(a\to b\) mediante una proprietà universale: \[a\to b = \bigvee_{x\land a\le b} x\] Te lo lascio dimostrare per non toglierti il piacere.

[thedarkhero]

La proprietà universale che hai scritto dovrebbe discendere direttamente dal fatto che $x \wedge a \le b$ se e solo se $x \le a \rightarrow b$, ovvero dalla definizione di implicazione.

Ma perchè questa è una condizione sufficiente affinchè V rispetti l'implicazione?