Is the intuitionistic valid_of_provable sound?

[jmaessen]

I was working through the intuitionistic soundness theorem and came up with a proof, but had a critical insight when I trying to understand the mechanics of completeness. It looks like the soundness theorem works equally well for terms that denote false – for which the only satisfying value will be ⊥. That's fine and even expected for soundness – we can prove false things by putting falsehoods into Γ, and indeed any proof of a tautology of the form ~A will do exactly this.

But for valid_of_provable it seems like we need something stronger – that ∅ ⊨ A is non-bottom for any valuation, in some Heyting algebra H (perhaps every non-trivial Heyting algebra H). We'll need something similar for completeness as well.

[fpvandoorn]

I'm not sure what you're asking/claiming. ∅ ⊨ A states that eval φ A is the top element in any Heyting-algebra, so for every non-trivial Heyting algebra it will not be the bottom element.