10
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ No . $\endgroup$
    – Emil Jeřábek
    Aug 22, 2012 at 14:01
  • 4
    $\begingroup$ There is no important syntactic difference between second-order and first-order logic. Any syntax that works in second-order logic would work equally well in a suitable first-order logic. However, I agree this question is better suited for math.stackexchange.org. If you can ask it there, I will write a longer answer. $\endgroup$
    – Carl Mummert
    Aug 22, 2012 at 15:27
  • 9
    $\begingroup$ Please don't close the question. The question is a symptom of logicians' always preferring single-sorted theories over multi-sorted ones. So everyone ends up thinking that functions must necessarily involve second-order logic, which is false. $\endgroup$
    – Andrej Bauer
    Aug 22, 2012 at 16:15
  • $\begingroup$ A related question on MSE: math.stackexchange.com/questions/23799/… $\endgroup$
    – Kaveh
    Aug 22, 2012 at 23:18

2 Answers 2

Reset to default
22
$\begingroup$

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.

Improve this answer
$\endgroup$
4
  • 2
    $\begingroup$ Thanks. So do you know why is the common answer to what is a higher-order logic, like you pointed out, is that any logic in which we intend to have quantifiers over "functions" or "sets"? Is it a special case? $\endgroup$
    – kate_r
    Aug 22, 2012 at 20:12
  • 4
    $\begingroup$ Historically, the distinction between first-order logic and higher-order logic was not very well understood, and it took a long time before it was clear. The idea that one could arbitrarily change the semantics of a logic would have been very strange in the early 20th century. Henkin's new proof method for the completeness theorem, which applied to type theory with first order semantics, was not obtained until the 1950s. As with many things, older terminology is still used by convention even though it is not the terminology that we would pick today. $\endgroup$
    – Carl Mummert
    Aug 22, 2012 at 20:51
  • $\begingroup$ I see. So, to confirm my understanding, in FOL, we can quantify over variables of type, e.g., $A \to B \to ...$ as long as the individuals of the domain are of type $A \to B \to ...$? If so, is this the reason why ZF is a first-order theory even some axioms quantify over sets, e.g., Axiom of union, i.e. the individuals are sets? $\endgroup$
    – kate_r
    Aug 22, 2012 at 20:57
  • 3
    $\begingroup$ My point is "what you can quantify over" is independent of whether you use FOL or higher order logic. But you should not say "in FOL" because there are many different first order logics, and they have somewhat different syntaxes. In some of them you can directly quantify over functions, in others you cannot. First-order ZFC is somewhat different in that you cannot directly quantify over functions at the level of the logic That is, there is just one kind of universal and one kind of existential quantifier in the logic used for ZFC, while in other FOLs there are multiple kinds of $\exists$. $\endgroup$
    – Carl Mummert
    Aug 22, 2012 at 21:30
14
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • $\begingroup$ Thanks. Just to clarify my understanding: the quantification of variables of type $A \to B$ is valid in FOL because the elements of the domain in question are of type $A \to B$. If so, how come the quantification over $(A \to B) \to (A \to B)$ is still valid in FOL? $\endgroup$
    – kate_r
    Aug 22, 2012 at 17:14
  • 1
    $\begingroup$ I voted for this earlier, but I feel obliged to say I think my answer is just a more detailed explanation of some ideas expressed in this one. $\endgroup$
    – Carl Mummert
    Aug 23, 2012 at 2:32
  • 1
    $\begingroup$ @kate_r: The essential thing to graps is that there can be many domains, even infinitely many ones. So you can quantify over any domain you like. In your case the domains would correspond to simple types, so they would be $A \to B$, $(A \to B) \to (A \to B)$, etc., whatever you like. Have a look at $\mathrm{HA}^\omega$, higher-order Heyting arithmetic. It is an example of a first-order theory with arbitrarily complex domains of the form $\mathbb{N} \to \mathbb{N}$, $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$, $((\mathbb{N} \to \mathbb{N}) \to \mathbb{N}) \to \mathbb{N}$, etc. $\endgroup$
    – Andrej Bauer
    Aug 23, 2012 at 7:35

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.