But, importantly, this assumption cannot in fact be implemented in a
reasoning system, as higher-order logics are semantically incomplete:
given any proposed reasoning method for a second- or higher-order
logic, there will be logically valid arguments whose validity cannot it
cannot demonstrated by that method.
I made that statement.
There are many, many (in fact MOST practical) applications which don’t require completeness.
True, well known and entirely beside the point. The sole purpose of my post was simply to qualify a remark that Doug Foxvog had made about the complexity of reasoning over properties. This was a purely theoretical point.
So the notion of incompleteness seems to be almost archaic in modern systems.
The practical upshot of incompleteness — or, perhaps more to the point, undecidability — is an interesting and complex issue. But even if its practical upshot is negligible, as you suggest (but hardly demonstrate), to say the notion itself is "archaic" is like saying the notion of a prime number is archaic. Semantic incompleteness is a mathematical property of certain logical systems, not something that is subject to trends, whims, or modern technology.