Filter on Heyting algebra

64 Views Asked by At

Consider the first order intuitionistic logic.

Let $H$ be an Heyting algebra, let $F$ be a filter on $H$ and let $V:\text{Frm} \rightarrow H$ be an evaluation function.

Suppose that $b \rightarrow V^{[x:=d]}(A(x)) \in F$ for every $d \in D$ ($D$ is the domain). Can I prove that $b \rightarrow \bigwedge_{d \in D}V^{[x:=d]}(A(x)) \in F$?