Universal Quantifier $\forall$ and Generalized Conjunction $\bigwedge$ in intuitionistic logic

constructive-mathematicsfirst-order-logicintuitionistic-logiclogic

I have a question about $\forall xA(x)$ and $\bigwedge\! A(a_i)$ (= $A(a_1)\wedge…\wedge A(a_n)$). In classical logic, the universal statement $\forall xA(x)$ can be understood as a generalized conjunction of $A(a_i)$ if the universe of discourse is finite, say, $\{a_1,…,a_n\}$. I wonder if this generalizes to intuitionistic logic?

The concrete problem that I meet is as follows. I assume that this generalizes, then we have
$$\forall xA(x)\leftrightarrow\bigwedge\! A(a_i).\quad\quad(*)$$
However, putting $\neg\neg$ before $\forall xA(x)$, $\neg\neg\forall xA(x)\rightarrow\forall x\neg\neg A(x)$ is intuitionistically valid, but the converse is not. But putting $\neg\neg$ before $\bigwedge\! A(a_i)$, $\neg\neg\bigwedge\! A(a_i)\leftrightarrow\bigwedge\! \neg\neg A(a_i)$ (note: both directions) is intuitionistically valid. Why is there such a difference? Does this signal that $(*)$ does not hold in intuitionistic logic? Thanks!

Best Answer

In general, $(*)$ is the wrong way to think about the universal quantifier. In both classical and intuitionistic logic, the power of the universal quantifier $\forall x$ is that it allows $x$ to range over an arbitrary, unspecified domain. There is no sense in which $(*)$ is a valid sentence in either classical or intuitionistic logic.

If you want to restrict your semantics to a fixed finite domain, you need to introduce an axiom. Let $\varphi$ be the sentence: $$\forall x\, \bigvee_{i=1}^n (x = a_i).$$ Then we indeed have $$\varphi\vdash (\forall x\,\psi(x)\leftrightarrow \bigwedge_{i=1}^n \psi(a_i))$$ for all formulas $\psi(x)$, both classically and intuitionistically. But also $$\varphi\vdash \forall x\, \lnot\lnot \psi(x) \leftrightarrow \lnot \lnot \forall x\, \psi(x)$$ for all formulas $\psi(x)$, both classically and intuitionistically. So your concerns vanish in this restricted setting.

Related Question