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?