Second-order term in first-order logic?

Question

Could a function in FOL take functions as arguments? FOL only limits on the order of the individuals being quantified, but if an expression does not involve quantifying over second-order or higher terms, would it still be valid in FOL? Say, $f(g)$ where $f : (A \to B) \to C$ and $g : A \to B$.

So another way to put my question is that does the rule of formation in FOL say that $f(g)$ is valid as long as $g$ is in the domain of $f$, despite the type of $f$? Could $f$ be a 4th order function and would still be valid in FOL?

Answer 1

I think that the spirit of this question, combined with the clarifications in comments, is:

What is it that makes first-order logic "first order"?

Unfortunately, the terms "first order" and "second order" get used to mean various things.

A formal but unsatisfying answer would say that first-order logic is a specific logic defined in, say, Mendelson's textbook, and any other logic is not "first order logic" strictly speaking. This is unsatisfying because we know there are many inessential variations of first-order logic - really there are many first-order logics that share a certain core. The question I quoted asks for a characterization of that core.

One common answer is that any logic in which we intend to have quantifiers over "functions" or "sets" is higher order. This is unsatisfying because, as Andrej Bauer points out, such theories can be syntactically expressed in multi-sorted first-order logic. There are many theories of "second order arithmetic", for example, which allow us to express set and function quantification but which are treated as first-order theories. Unfortunately, the terminology "second order" is established for these theories and cannot be avoided.

Recall that a logic consists of both a syntax and a semantics. The truly defining feature of a first-order logic is the semantics. First-order semantics begins with the notion of a structure (also called a model), as defined in every introductory textbook on first-order logic.

Consider how we would express function quantification in (multi-sorted) first-order logic, as in Andrej's answer. Each structure must interpret two sorts. It uses a set of individuals for the quantifiers over individuals and a separate set of functions for the quantifiers over functions. This set of functions, in an arbitrary structure, might be a proper subset of the collection of all functions on the set of individuals; nothing in the definition of a structure requires otherwise. Indeed some structures will have an infinite set of individuals but a finite set of functions.

Full second order semantics changes the class of allowable structures so that only those whose function set includes all the functions are allowed. This does not affect the syntax in any way, but it deeply changes the semantics. Because fewer structures are being considered, more formulas will be logically valid, and fewer will be satisfiable. Thus there are more categorical theories in these semantics, such as the well known categorical second-order axiomatizations of the natural numbers. Those same axiomatizations are syntactically fine in first-order logic, where the simple difference is that they are no longer categorical.

Thus the key difference between function quantification in multi-sorted first order logic (or type theory) and function quantification in full second-order semantics is not the existence of syntactic quantifier symbols that allow quantification over functions. The difference is in the meaning of those quantifiers, which derives from the way the semantics are defined. In the first-order case, we have little control over the range of quantifiers. In full second-order semantics, once the set of individuals is fixed, the range of the function quantifiers is also fixed. This distinction is only visible at the meta level, when we are studying the logic from the outside and can specify which interpretations are permissible. Nothing in the syntax of the logic tells us what collection of structures will be used to interpret it.

Answer 2

While this question is not research-level, I think many mathematicians would not know how to answer it. I propose we keep it.

In usual logic texts first-order logic is done over a single sort, i.e., we assume a fixed universe of discourse. Terms denote elements of the single universe. For example, in the theory of a group the universe is the group, in set-theory it is the class of all sets, etc.

But this need not be so, we can have a first-order logic with many sorts. A typical example is the theory of a module, where the two sorts are the ring and the module. Another example is the theory of a graph, where the two sorts are the vertices and the edges. In classical logic various tricks may be played that allow us to replace the sorts with their disjoint union (define operations arbitrarily when they don't make sense and fix the axioms appropriately). If one studies first-order theories in general this is a very useful trick, which is why logicians always stick to singe-sorted theories. But in particular cases it makes little sense to replace several natural sorts with a single unnatural one.

However, in computer-sciency applications such tricks are unacceptable. Therefore we keep many sorts. In fact we go a step further and organize sorts into a type theory (and call the sorts types). It is common for a type theory to have type constructors that generate infinitely many types.

To answer your question, suppose we want a first-order logic in which we are allowed to speak about functions $A \to B$ as well as functionals $(A \to B) \to C$. Then we work in simple type theory, whose type constructors are the cartesian products $\times$ and the function space $\to$. Only well-typed terms are admitted, and all quantifiers must range over specific types. Thus we can write things like $\forall F : (A \to B) \to (A \to B) . \exists f : A \to B . F(f) = f$. This is still first-order logic on top of a type theory.

Such a logic would become higher-order if we included a type $\Omega$ of truth values and axioms which related formulas and functions mapping into $\Omega$. One would expect a comprehension-style schema which related formulas $\phi(x)$ with $x$ of type $A$ and functions $f : A \to \Omega$. Second-order quantification $\forall F . F(\dots)$ can then be expressed as $\forall f : A \to \Omega . f(\dots)$.

You can read more about this kind of formal systems in Bart Jacobs's book "Categorical Logic and Type Theory". Constructive mathematicians also prefer formalizations of this sort, for example Peter Aczel has been advocating logic-enriched type-theory for a while.