Is the internal language of a topos complete, sound and effective?

Question

The internal language of a topos is higher order intuitionistic typed logic. Now according to this article in wikipedia higher order classical logic with full semantics is never complete, sound or effective.

Is this also true for higher order intuitionistic typed logic?

Is there an nice characterisation of when a topos does have these properties in a categorical fashion?

Presumably its not enough to make the topos classical. Can we do it by somehow asserting Henkin style semantics which according to the previous article makes a classical higher logic a typed first order logic - which then has the properties required?

Answer 1

I asked the same question on Mathoverflow which was answered by Andrej Bauer:

The undesirable properties of higher-order logic are created by an insufficient notion of model. That is, we cannot have all three, soundness, completeness and effectivness (decidability of proof checking), if we insist that formulas be interpreted in the "standard" set-theoretic way. Henkin semantics does not suffer from this defficiency.

What this says is not that something is wrong with higher-order logic, but that something is wrong with those who refuse to look at semantic models, even when they are right in front of their faces, because these models are "unintended", "philosophically unacceptable", "not what mathematicians think", etc. This phenomenon of refusing to accept new interpretations of old theories is quite persistent, and always very harmful. Didn't someone stall progress in noneuclidean geometry because it was unthinkable that there would be strange new models? Aren't imaginary numbers so called because they were unthinkable and did not "really exist"? Doesn't higher-order classical logic suffer because it is being denied its natural notion of models on the grounds that they are non-standard?

The natural notion of model for intuitionistic higher-order logic (IHOL) is that of a topos. With respect to topos semantics, it is a standard result that IHOL enjoys soundness, completeness and effectivness.

We may specialize this standard fact to classical higher-order logic (CHOL). The result then is that, with respect to Boolean topos semantics, CHOL enjoys soundness, completeness and effectivness. From here on, we may prove various technical theorems which allow us to cut down on the class of Boolean toposes which is stil sufficient for completeness. And then it is not much of a surprise that we cannot cut down just to a single topos known as classical sets, which is called "Paradise" by its prisioners.