What do we gain with higher order logics?

Question

Gödel's speed up theorems 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 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.

Answer 1

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, 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...

Answer 2

The debate about first-order and higher-order logics is a bit of a religious issue. There are many ways to argue one way or the other: first-order logic has very nice meta-theoretical properties, higher-order logic achieves categoricity, etc., and one can always produce an argument in one's favor.

The Stanford Encyclopedia on the Emergence of First-order Logic makes a point that the logicians who established the importance of first-order logic used higher-order logic for many years after first-order logic was identified as an object of interest. When the fundamental meta-theoretic theorems about first-order logic were discovered, they were sometimes taken as evidence of deficiency of first-order logic. While today many think it is obvious that first-order logic is the One True Logic to rule them all (as I said, it's a religious issue), this was not the case in the past.

It really depends on what you want to do with logic.

If you're a logician who wants to study meta-theoretic properties of formal systems, then first-order logic is a sweet spot. It is very expressive, but it also has extremely good meta-theoretic features (completeness theorem, compactness theorem, Lindström's theorem). Higher-order logic is even more expressive, but lacks some of the nice properties of first-order logic.

If you're a categorical logician, then you are interested in the connections between formal systems and structure, as perceived in category theory. In this case your view might be that logic is dictated by semantics. For example, the internal language of toposes is fully higher-order, while the internal logic of algebraic varieties is regular logic (just equations, conjunctions, and $\exists$). And if you only care about Grothendieck toposes and geometric morphism, geometric logic is for you.

If you're a mathematician, you probably care mostly about using logic as a tool, in which case the primary concern is expressivity. You do not want to be told that some very natural mathematical idea cannot be stated formally, so you would naturally gravitate towards higher-order logics. However, it is known that such needs for expressivity can largely be met by combining first-order logic with set theory. And since logic and set theory are typically taught by logicians, who prefer first-order logic for their own purposes, the prevalent formal system advocated today is first-order logic with set theory. But ultimately, for an ordinary mathematician it does not matter much which one they use.

Computer-scientists have their own ideas about logic and typically take an engineering point of view: use the tool that is appropriate for the situation at hand. For example, when we formalize mathematics with a proof assistant (software that aids and oversees writing of formal proofs), we seek a formalism that allows us to get the job done as directly as possible. For large scale projects the overriding concern becomes proof engineering: how to organize large libraries of definitions and theorems, how to search them, how to write proofs so that they are robust with respect to small changes, etc. Traditional logic has almost nothing to say about these topics, and consequently does not influence much the choice of formalism used in proof assistants. So many proof assistants use type theory, which could be characterized as "predicative higher-order", a reasonable middle ground between first-order and unrestricted higher-order.

Answer 3

Bell and Machover don't say (in the quote) anything about statement length, so this doesn't necessarily contradict Gödel.

I can't speak about (universal) shortest proof, but "translating" between higher and lower logics can become unwieldy. This paper by Shapiro [1] might be of general interest to the question, but also specifically an example by Boolos discussed on page 46 (I don't have access to the Boolos paper [2])

If the logic were complete, it might be natural to assume that the mathematician proceeds, or could proceed (or should proceed), by deducing consequences of the axiomatization. This would weigh in favor of first-order logic, since it is complete. However, this natural thought is problematic. Boolos [1987] gives an example of a valid argument $I$ in a first-order language and sketches a short derivation of the conclusion of $I$ from its premises in a second-order deductive system. A slight variation on the argument would yield a model-theoretic proof that $I$ is valid in the model-theoretic semantics. Since $I$ is first-order, and first-order logic is complete, there is a derivation of the conclusion of $I$ from its premises in a standard first-order deductive system. Boolos shows, however, that the shortest first-order derivation of $I$ has more lines than there are particles in the known universe.$^1$ We cannot know that $I$ is valid via a derivation of it in a first-order deductive system. Boolos concludes that

... the fact that we so readily recognize the validity of $I$ would seem to provide as strong a proof as could be reasonably be asked for that no standard first-order logical system can be taken to be a satisfactory idealization of the... processes... whereby we recognize (first-order!) logical consequences.

Clearly, if a first-order argument is valid then in principle an epistemic agent can learn this via a derivation in a standard, first-order deductive system. However, examples like these should make one wary of the epistemic significance of these 'in principle' declarations

$^1$ See my [Foundations without Foundationalism] Chapter 5, Section 5.3.4 for this and other cases of 'speed-up'

I think Shapiro and Boolos have different views ("cannot know") related to finitism than Bell and Machover ("We therefore do not lose much"), but that's getting a bit off topic. The example, I think, is still relevant though.

Of course, the one example does not mean all such statements "blow up" in a similar manner.

[1] Stewart Shapiro. "Do Not Claim Too Much: Second-order Logic and First-order Logic" Philosophia Mathematica, Volume 7, Issue 1, February 1999, Pages 42–64, https://doi.org/10.1093/philmat/7.1.42

[2] Boolos, G. [1987]: "The consistency of Frege's Foundations of Arithmetic" in Judith Jarvis Thompson (ed.), On being and saying: Essays for Richard Cartwright.Cambridge, Massachusetts: MIT Press, pp. 3-20.

Answer 4

Some of these answers want to convince you HOL is more expressive. That's true in a certain sense but it's easily misleading.

Specifically, let's be careful to distinguish two different notions that people refer to as a logic. The first is a set of rules for writing down formula and proving results about them (might not be best name but it's what unfamiliar people often mean.). The second is really a metamathematical conception that specifies a semantics of the language, i.e., specifies what models count as satisfying a collection of sentences.

In terms of the first notion there is nothing HOL expresses that FOL can't express. Indeed, if you only consider a linear hierarchy of types the theory is most naturally presented as a many sorted first order language. If you get fancier and allow types to be formed in some more complex fashion, e.g., as per the typed lambda calculus, you can still formulate a first order theory which proves the same theorems.

Basically, both approaches need to deal with the problem of avoiding Russell's paradox. Set theory deals with this by adopting the cumulative hierarchy approach and limiting comprehension to the elements of an existing set. In contrast, HOL logic requires that each variable be assigned a type. The connection between HOL and type theory offers certain advantages in computer applications (you can recycle your logic as your type theory for handling computation with a certain kind of elegance). However, if you just want to do mathematics imo FOL tends to be the more elegant choice -- though of course you could just ignore all your higher types in HOL and mimic the FOL approach -- since it gets difficult to model certain kinds of reasoning in HOL as a result of the need to assign everything a type. Whenever you have long sequences of sets (each being an element of the next) or want to impredicatively quantify over all sets in it gets tough/inelegant to do in HOL.

[Though you can always split the difference and work in Quine's New Foundations]

This brings us to the sense in which HOL is more expressive. In the standard semantics, discussed in the first answer, models of HOL are constrained to actually consider quantification over the type representing sets of individuals to range over the full powerset of individuals. That means you can say that HOL is more expressive since, for instance, you can write down a sentence that's only satisfied by the intended model of the natural numbers.

But that's not really an advantage, it comes at the cost of giving up a complete and effective proof system and it's really no different than just working in first order ZFC and saying "I intend to work in the true universe of sets V."

Ultimately, I don't find much to recommend HOL as a logic in the epistemic sense -- a way to justify our reasoning via some minimal clearly valid system of inferences -- and while it has some interesting applications in CS my personal belief is that computer assisted theorem proving is being held back by the allure of using your type system as your proof system since it creates too much of an impedance gap with how mathematicians are likely to think of their proofs.

Answer 5

I think my dissertation topic gives a distinction from the perspective of a functional type. Although it is a specialization, it seems to me a natural one. For a poster which expands on some details, see http://arxiv.org/abs/1408.2784 .

One can express hyperassociativity, the statement "All term operations are associative", by means of a hyperidentity, which is a (in a linguistic sense) compact object in a certain second order language, and this will apply to various classes of universal algebras. In the case that the corresponding first order language has only one binary operation symbol, there is another compact representation: the conjunction of the five sentences that assert that the five binary term operations b(x,x), b(x,y), b(x,b(x,y)),b(x,b(y,y)), and b(x,b(y,x)) are associative. There is also a similar and less interesting version when the language has only finitely many unary function symbols.

However, if the language incorporates more function symbols, we no longer have this: hyperassociativity is not logically equivalent to a finite set of first order identities. There does not appear to be a compact way to present hyperassociativity for these kinds of structures. So second order here means shorter in a significant way.

Gerhard "The Many Ways Of Hyperassociativity" Paseman, 2019.05.30.

Answer 6

I think the difference lies in the specific structures.

What the second statement says is

"For any second order formula $\phi$, there is some first order formula $\hat\phi$ such that $(\mathfrak U, R_0...R_n)\vDash\phi \leftrightarrow (\mathfrak V, Q_0...Q_n,\in,\mathfrak U)\vDash\hat\phi$."

This is easy enough to verify, as $\mathfrak U\vDash R_n(x_0...x_n) \leftrightarrow\mathfrak B\vDash Q_n(x_0...x_n)\land x_0\in\mathfrak U...x_n\in\mathfrak U$.

What the first statement says is that second order logic can provide proofs for theorems in first order logic in general faster. This would be confusing if $\mathfrak U$ and $\mathfrak B$ were the same structures, yet they are different. A proof using the relation symbols of $\mathfrak U$ is not nesscarily as fast as a proof using the relation symbols of $\mathfrak B$, as $\mathfrak B$ has the additional unary predicate $\mathfrak U$ and the relation symbol $x\in X$.

The point of the second quote, is that for a larger structure $(\mathfrak W,E)$ such that $E$ can interpret $Q_0...Q_n,\in,\mathfrak U$, $(V,\in)$ for example, every second order statement about $(\mathfrak U, R_0...R_n)$ can be reduced to a first order statement about $(\mathfrak V, Q_0...Q_n,\in,\mathfrak U)$. However, from the perspective of $(\mathfrak V, Q_0...Q_n,\in,\mathfrak U)$, it is much larger then $(\mathfrak U, R_0...R_n)$.