[Gödel's speed up theorems](https://plato.stanford.edu/entries/goedel/#SpeUpThe) seem to say that higher order logics offer shorter shortest proofs of various propositions in number theory. Explicitly, he gave the following



> 
> **Theorem.** 
>  Let $n>0$ be a natural number. If $f$ is a computable function, then there are infinitely many formulas $A$, provable in $S\_n$ ($n$-th order logic), such that if $k$ is the length of the shortest proof of $A$ in $S\_n$ and $l$ is the length of the shortest proof of $A$ in $S\_{n+1}$, then $k>f(l)$.
> 
> 
> 


I am not well versed in computable functions but I believe the identity function is computable, so the above inequality would simplify to tell us that the shortest proofs get shorter as we move into higher logics.


How does this reconcile with the following quote from Bell and Machover's "A course in Mathematical Logic":



> 
> However, most logicians agree that [second and higher order] languages are, at least in principle, dispensable. Indeed, let $\mathfrak{U}$ be any structure and let $\mathfrak{B}$ be a structure obtained from $\mathfrak{U}$ in the following way. The universe of $\mathfrak{B}$ consists of all undividuals of $\mathfrak{U}$ plus all sets of individuals of $\mathfrak{U}$. The basic operations of $\mathfrak{B}$ are defined in such a way that when they are restricted to the universe of $\mathfrak{U}$ they behave exactly as the corresponding basic operations of $\mathfrak{U}$. Finally, the basic relations of $\mathfrak{B}$ are all the basic relations of $\mathfrak{U}$ plus two additional relations: the property of being an individual of $\mathfrak{U}$, and the relation of membership between an individual of $\mathfrak{U}$ and a set of individuals of $\mathfrak{U}$. Then any statement about $\mathfrak{U}$ expressed in a second-order language with set variables, can easily be "translated" into a statement about $\mathfrak{B}$ in first order language. A similar argument applies to other higher-order languages. We therefore do not lose much by confining our attention to first order languages only.
> 
> 
> 


From the argument they outline it seems they lose nothing by restricting their attention to first order languages, but this goes against the grain of the speed up theorems unless I'm missing something - does the "translation" from a second order statement over $\mathfrak{U}$ to a first order statement over $\mathfrak{B}$ require more symbols? This goes against what seems to be the implied translation, where we interpret the symbols for subsets of the universe of $\mathfrak{U}$ as the symbols in $\mathfrak{B}$ added to denote these subsets, which seems like it would yield a translation of equal length.


Giorgio Mossa's answer [here](https://mathoverflow.net/questions/90863/what-is-the-relationship-between-fopl-and-higher-order-logics) seems to indicate that the difference lies in the standard semantics of the languages in question, not their syntax, but this is somewhat unclear to me as the semantics of a language are fixed as soon as we choose a structure to interpret the language in, which it seems has been done in the above quote. Any assistance is greatly appreciated.



What do we gain with higher order logics?
Your error is simply assuming that there is only one kind of higher-order logic (HOL). Contrary to your last paragraph, there are at least 2 major kinds, corresponding to 2 different semantics:


In **full semantics**, once you fix the domain (of individuals), you can no longer choose the interpretation of the higher-order sorts (starting with the subsets of individuals), because that is determined by the iterated power-sets of the domain (more precisely what the meta-system thinks are the power-sets). By the incompleteness theorem for PA, even second-order logic (SOL) with full semantics cannot be captured by a computable formal system.


In **general semantics**, you not only must choose the domain but also must choose the interpretation of each higher-order sort, and typically the only restriction is that it must respect the comprehension axioms that you want to have. For example if you want to have full higher-order comprehension, then you have the axiom ( $∃x∈S\_{k+1}\ ∀t∈S\_k\ ( t∈x ⇔ φ(t) )$ ) for each (higher-order) property $φ$ with one parameter from $S\_k$, where $S\_k$ denotes the level-$k$ sort. In SOL we usually require just predicative comprehension, namely where $φ$ only quantifies over $S\_0$ (i.e. the individuals), which correspond to the first-order definable subsets of the domain.


Note that HOL with general semantics can be captured by multi-sorted FOL, and hence by one-sorted FOL (simply by using predicate-symbols to represent the sorts). It is in this precise technical sense that we "do not lose much by confining our attention to first order languages only". But it is wrong to infer that "it would yield a translation of equal length". Even merely extending an FOL system to the SOL system with predicative comprehension is equivalent to having internal [definitorial expansion](https://math.stackexchange.com/a/1864310/21820), which allows one to avoid repetition of long formulae.


Note that multi-sorted FOL (and the one-sorted translation) is semantically complete for HOL with general semantics, but of course not semantically complete for HOL with full semantics. Moreover, the Henkin construction shows that if a countable HOL system $T$ (i.e. with countable language) has a general model, then it also has a countable general model.


Furthermore, the speedup theorem you linked to does not actually show a speedup attributable to the use of HOL over FOL! Note that the proof in that SEP article uses additional assumptions, namely the higher-order induction schema instead of just the first-order induction schema. That speedup is due to the ω-incompleteness of PA rather than anything to do with HOL, as shown clearly by the proof. This is also obvious from the fact that if PA proves Q then PA+Q is still an FOL system and proves Q with a very short proof...


