Does every intuitionistic formula have disjunctive or conjuctive normal form?

Question

As in title - does every intuitionistic formula have disjunctive and conjuctive normal form? I guess that this is correct but I couldn't find any information on that.

Answer 1

I don't know of anywhere this is proven, offhand. It's one of those "well-known facts" that becomes intuitively obvious once you have a good amount of experience with intuitionistic logic, but I don't know if I've ever even seen a proof for it. I wouldn't say it isn't proven in your book because it is too elementary (it is oftentimes really hard to prove you can't do something in logic, even when it is clear that you can't), but rather just it's not that important, and it's more efficient to disallow you from doing something by never proving that you can, rather than proving that you can't, unless the curiosity is too great.

I'm not sure the following argument is complete, but I'll try and give you some reasoning for why $A\to B$ is not equivalent to any DNF. Consider a DNF, and without loss of generality, assume none of the literals are $\top$ or $\bot,$ and only are $A,B$ $\lnot A$ or $\lnot B.$ Unlike in classical logic, if we can prove $A\to B$ implies some disjunction, we can prove that it implies one of the clauses. This clause is the conjunction of some literals, and so (like in classical logic) we can prove $A\to B$ implies each of the literals. But, it is not provable (even classically) that $A\to B$ implies any of $A,$ $B$, $\lnot A$ or $\lnot B.$