$ \bigcap _{i \in I} (A\cup S_i) \subset A\cup \bigcap _{i \in I} S_i $ on the intutionistic logic

Question

I want to prove below for nonempty I on the intuitionistic logic. $$ \bigcap_{i\in I} (A\cup S_i) \subset A \cup\bigcap_{i \in I} S_i $$ This is equivalent to next. $$ (\forall x)(\phi\lor\psi_x)\rightarrow\phi\lor(\forall x)(\psi_x) $$ I had proved on the G.

If it cannot be proved, I want to prove IPC+above $\rightarrow$ G.

Thank you for your apply

Answer 1

Consider the Kripke frame roughly given by the below diagram (with partial order given by left nodes $\le$ right nodes).

S_0  ---  S_0, A
I={0}     I={0,1}
     \--  S_0, S_1  ---  S_0, S_1, A
          I={0,1}        I={0,1,2}
                    \--  S_0, S_1, S_2  ---  ...
                         I={0,1,2}
                                        \--  ...

In this diagram, the annotations on $I$ define the "presheaf" $I$ as a subpresheaf of the constant presheaf $\mathbb{N}$. (Or, if you insist on sticking to vanilla Kripke frames, then replace $I$ in each node with $K$ to define the domain of discourse, and in the below arguments, replace $\forall i \in I$ with plain $\forall i$.) In this diagram, we have that $0 \in I$ is globally true, so the base node forces the proposition that $I$ is nonempty.

However, we have that the base node $\Vdash \forall i\in I, A \lor S_i$ since every node in which $n \in I$ has either $S_0, S_1, \ldots, S_{n-1}, A$ true (so the left case holds) or else $S_0, S_1, \ldots, S_{n-1}, S_n$ all true (so the right case holds). On the other hand, the base node $\not\Vdash A \lor (\forall i \in I, S_i)$ since it does not force $A$, and for each $n \in \mathbb{N}$, we have the node $S_0, S_1, \ldots, S_{n-1}, A$ at which $n \in I$ but we do not have that node forcing $S_n$, meaning that the base node also does not force $\forall i \in I, S_i$.

Therefore, this Kripke frame gives a counterexample to show that $[\forall i\in I, (A \vee S_i)] \rightarrow [A \vee (\forall i \in I, S_i)]$ is not a theorem of intuitionistic logic.