Finding a formula in intuitionist logic

Question

I am looking for a formula which is true semantically but not syntactically in propositional intuitionist logic.

Does it exist? If yes what's that?

Thanks for your help.

Answer 1

If with "true semantically" you are referring to Kripke semantics for intuitionistic logic, there is no such formula, because

Kripke's Soundness and Completeness Theorems establish that a sentence of [the language ] $L$ is provable in intuitionistic predicate logic if and only if it is forced by every node of every Kripke structure [i.e. it is valid].

---

If, instead, with "semantically true" you mean true with the "classical semantic" (e.g truth tables for propositional logic), then $P∨¬P$ is the simplest example of a formula which is (classically) true but underivable in intuitionsitic logic, because, due to Kripke's Sondness and Completeness Theorem, is not valid according to Kripke's semantic.