[cruegge]

I see. Checking the formulation of the incompleteness theorem again, I noticed that I probably misunderstood something here: it indeed essentially requires proofs to be verifyable, which second order theories do not provide. So second order PA can (and in fact does) have a proof of every statement or its negation, without contradicting incompleteness, but provability is somewhat useless in this case. For theories that fit the conditions you listed, unprovability is indeed due to multiple models. Does that make sense?

Edit: however, consistent second order theories don't always have a model. In first order, if S is an undecideable statement in theory T, then both T+S and T+!S have models, both of which are models for T, so undecideable statements always come from multiple models. But that does not need to be the case in second order, so your claim "it is independent from the axioms, i.e. there exist multiple models" is not neccessarily true, i.e. there may be cases when decideability of some statement fails in a theory with a unique model. Or is there another argument for your claim?

Forgive me for spamming questions, I just try to understand how these things fit together. But maybe we should just stick to first order, since everything else is too weird anyway.

[cruegge]

Ok, the more I try to understand this, the more confused I get. Probably just scrap everything I said, I'll need to do some more reading.

[bo1024]

This was all a helpful/interesting discussion!