0

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$?

effezeta
  • 445
  • Off the top of my head: what if $D = \mathbb{N}$, $H$ is the free Heyting algebra on generators $p_1, p_2, \ldots$, $A(n) = p_n$, and $F$ is the filter generated by ${ p_1 \land \cdots \land p_n \mid n \in \mathbb{N} }$? – Daniel Schepler Apr 14 '22 at 00:19
  • @DanielSchepler: thanks! So my conjecture is false. – effezeta Apr 15 '22 at 14:27

0 Answers0