De Morgan in algebra di Heyting

thedarkhero
La legge di De Morgan $\notX ^^ \notY \vdash \not(XvvY)$ si traduce in un algebra di Heyting come $(x->0)^^(y->0)<=(xvvy)->0$ (in un'algebra di Heyting l'implicazione tra $a$ e $b$ è quell'elemento $a->b$ tale che per ogni $c$ vale $c^^a<=b$ se e solo se $c<=a->b$).
Come posso dimostrare algebricamente che in un'algebra di Heyting tale relazione è vera?

Risposte
killing_buddha
Anzitutto serve un

Lemma. Se \((P,\le)\) è un insieme parzialmente ordinato, e \(\downarrow\!\!(a)\) indica il segmento iniziale di $a$ in $P$, cioè
\[
\downarrow\!\!(a) = \{x\in P\mid x\le a\}
\]
allora la funzione \(P \to {\bf 2}^P\) che manda $a$ in \(\downarrow\!\!(a)\) è iniettiva.

Proof. Facile: se \(\downarrow\!\!(a)=\downarrow\!\!(b)\) allora \(a\in \downarrow\!\!(b)\), e dunque $a\le b$. Viceversa, si conclude.

Mostriamo allora che, se \(\mathcal{H}\) è un'algebra di Heyting gli elementi \(\lnot(x\vee y)\) e \(\lnot x \land \lnot y\) hanno gli stessi segmenti iniziali:
\[
\begin{array}{c}
z\le (x\vee y \to 0) \\\hline
z\land(x\vee y) \le 0\\\hline
(z\land x)\vee(z\land y) \le 0\\\hline
(z\land x \le 0) \& (z\land y\le 0)\\\hline
(z \le x \to 0) \& (z\le y\to 0)\\\hline
z\le (x\to 0)\land (y\to 0).
\end{array}
\]
La cosa più interessante comunque è che questo risultato vale in una categoria cartesiana chiusa cocompleta \(\mathcal{C}\), con la stessa dimostrazione (l'iniettività della funzione che manda $a$ nel suo segmento iniziale è il lemma di Yoneda, \(\land\) è il prodotto e \(\vee\) il coprodotto in \(\mathcal{C}\)). Un'algebra di Heyting è un caso particolare di queste strutture.

thedarkhero
Grazie mille!

Vedendo la tua soluzione mi è venuto in mente che si potrebbe dimostrare questa legge di De Morgan senza ricorrere al lemma di Yoneda (pur perdendo un po di generalità): ponendo $z=(xvvy)->0$ e leggendo la dimostrazione dall'alto verso il basso (come l'hai scritta tu) si prova che $(xvvy)->0<=(x->0)^^(y->0)$ mentre ponendo $z=(x->0)^^(y->0)$ e leggendo la dimostrazione dal basso verso l'alto (è invertibile) si prova che $(x->0)^^(y->0)<=(xvvy)->0$.

Rispondi
Per rispondere a questa discussione devi prima effettuare il login.