36
$\begingroup$

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.

$\endgroup$
2
  • 3
    $\begingroup$ The historic perspective about first-order logic is quite interesting, I recommend the writeup The Emergence of First-Order Logic at the Stanford Encyclopedia of Philosophy. $\endgroup$ May 31, 2019 at 8:57
  • $\begingroup$ @AndrejBauer Interesting indeed, much appreciated Andrej. $\endgroup$
    – Alec Rhea
    May 31, 2019 at 9:29

5 Answers 5

17
$\begingroup$

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

$\endgroup$
1
  • 1
    $\begingroup$ The clarification is much appreciated user21820. $\endgroup$
    – Alec Rhea
    Jun 1, 2019 at 23:02
36
$\begingroup$

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.

$\endgroup$
13
  • 2
    $\begingroup$ perhaps one could also mention that there are mathematical results, such as various transfer principles, where a mathematician must be careful that 1st order theories are used. So it might matter for a mathematician using model theory. $\endgroup$ May 31, 2019 at 10:50
  • 9
    $\begingroup$ For proof assistants, the logic the mathematician uses to write proofs should be as expressive as feasible, to make it easier for the human. However, people also often want to not write proofs (i.e., they want the computer to search for proofs), and in this case the logic should be as inexpressive as possible, because weak logics make it easier for computers to find proofs. Managing this divide erodes the cultural divide between "mathematics" and "logic" in a very satisfying way -- proof theory and model theory become ordinary proof techniques, no different from linear algebra. $\endgroup$ May 31, 2019 at 11:52
  • 2
    $\begingroup$ Andrej, excuse me, what I don't understand in the discussions like this are the foundations. Are higher order logics axiomatized? The first order logic is. $\endgroup$ Jun 1, 2019 at 6:31
  • 2
    $\begingroup$ @SergeiAkbarov: of course they are formalized (I think "formalized" is a better word than "axiomatized" because "axioms" are a specific notion within logic), why wouldn't they be? For instance, you can look up higher-order logic in Lambek and Scott's "Introduction to Higher-Order Categorical Logic", and I am pretty sure Bart Jacobs's "Categorical Logic and Type Theory" also addresses higher-order logics. (Sorry, I am not familiar with "classical" treatments of higher-order logic.) $\endgroup$ Jun 1, 2019 at 21:25
  • 2
    $\begingroup$ Let’s just prove everything about everything. haha only serious $\endgroup$ Jun 7, 2019 at 2:22
9
$\begingroup$

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.

$\endgroup$
1
  • 2
    $\begingroup$ It seems like we (with finite lifespans) might lose quite a bit when only paying attention to $1$st order logic, the reference and explanation are much appreciated Ben. $\endgroup$
    – Alec Rhea
    Jun 2, 2019 at 2:40
3
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Very interesting Gerhard, thank you -- I'll take a look and try to comprehend your reference. $\endgroup$
    – Alec Rhea
    May 31, 2019 at 8:53
3
$\begingroup$

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)$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.