[Logica intuizionista] Legge di De Morgan generalizzata

[thedarkhero]

Si può dimostrare in logica intuizionista il sequente $\forall x \neg A(x) \vdash \neg \exists x A(x)$?

[megas_archon]

"thedarkhero":Si può dimostrare in logica intuizionista il sequente $\forall x \neg A(x) \vdash \neg \exists x A(x)$?

Sì, è sufficiente scriverlo come \(\forall x .(A(x) \to \perp) \vdash (\exists x A(x))\to\, \perp)\), cioè \(\forall x .(A(x) \to \,\perp) \land (\exists x A(x))\vdash \,\perp\).

[thedarkhero]

Grazie!
E per quanto riguarda il sequente "inverso", cioè $\neg \exists x A(x) \vdash \forall x \neg A(x)$?

[megas_archon]

"thedarkhero":Grazie!
E per quanto riguarda il sequente "inverso", cioè $\neg \exists x A(x) \vdash \forall x \neg A(x)$?

No, non si può.