# A first order logic extended with binding terms like the familiar set descriptors $\{x:\varphi\}$

First order logic comes equipped with two kinds of terms:

1. Variable: those terms of the form $$x$$ for some variable $$x$$, of which there are infinite.
2. Function application: those terms of the form $$f(t_1,\dots,t_n)$$ for some $$n$$-place function symbol $$f$$, of which there are infinite, and some $$n$$ terms $$t_1, \dots, t_n$$.

In practice, one more kind of term is commonly used informally in the context of set theory: set descriptors of the form $$\{x:\varphi\}$$, where $$x$$ is a variable, and $$\varphi$$ is a first order well-formed formula. This term cannot be rewritten as a function application, since $$\varphi$$ is not a term. This term creates a scope in which the variable $$x$$ is bound, similar to the way the quantified formulas of the form $$\forall x\varphi$$ and $$\exists x\varphi$$ work.

One way to introduce set descriptor terms into the logic, which then will no longer be a first order logic, so lets call it extended first order logic, is by introducing an infinite set of binding term constructors that is disjoint from the the first order logic vocabulary (consisting of logical symbols, variables, function symbols, and relation symbols), and a new way of forming terms: $$Cx\varphi$$, for every binding term constructor $$C$$, every variable $$x$$, and every extended first order well-formed formula $$\varphi$$ (the definition of function application and of a well-formed formula should be modified to accomodate this new kind of term). Let's call such terms binding terms.

We can now set aside one of the new-fangled binding term constructors, say $$\sigma$$, and interpret every binding term of the form $$\sigma x\varphi$$ as $$\{x:\varphi\}$$.

Set descriptors are probably the most familiar example of binding terms, but two others that I know of have been proposed in the past by mainstream mathematicians, likewise in the context of set theory: Hilbert's epsilon operator and Bourbaki's $$\tau$$ operator, which, though similar, are not the same operator, as they satisfy slightly different axioms.

Note that extending first order logic with binding terms necessitates a corresponding extension of the inference system, say Gentzen's Natural Deduction.

Has the combination of extended first order logic with a corresponding inference system been studied? Does it have a name? Where can I read more about it?

• There is a large literature for dealing with issues like this and building practical extensions to logics in the computer science literature. Nominal techniques and logical frameworks are two entryways into it. – Derek Elkins left SE Jul 19 '19 at 22:55
• @DerekElkins Could you add a couple citations? This is certainly a topic about which I know nothing (and I suspect I'm not alone in that); I think this is a situation where a lot of logicians are suffering from unfamiliarity with the CS literature. – Noah Schweber Jul 19 '19 at 23:42
• @NoahSchweber While not up-to-date, the Name Binding Blog has a fairly extensive list of topics from 2010 and earlier. There is certainly work from after 2010 like the work in contextual modal type theory which was incorporated into Beluga for example. – Derek Elkins left SE Jul 19 '19 at 23:48

This is an excellent question, and is something which should be explicitly treated in basic logic texts (and in my experience, isn't). Disappointingly or satisfyingly depending on what you're looking for, first-order logic is already enough - at least, initially (see below the fold).

All the constructors you're talking about are definable in an appropriate sense, and so they can be implemented in standard first-order logic by just tweaking the syntax appropriately: basically, we'd add infinitely many new function symbols, each corresponding to an instance of the desired constructor, and axioms saying how they work. In all of the examples you've described, this can be done without difficulty.

For example, let's look at the Hilbert $$\epsilon$$-operator. Rather than have a single $$\epsilon$$, we'll have a separate $$\epsilon_A$$ for each formula $$A$$ with at least one free variable, and these will behave as follows:

• The simplest case is for single-variable (so, parameter-free) $$A$$. In this case, $$\epsilon_A$$ is nullary - it's just a constant. And our corresponding axiom is $$\exists xA(x)\implies A(\epsilon_A).$$

• Now let's look at the case where $$A$$ has two free variables, $$x$$ and $$y$$. We might now want to write something which for each $$b$$ picks some $$a$$ such that $$A(a,b)$$ holds (if such an $$a$$ exists). So our $$\epsilon_A$$ is now a unary function, and the corresponding axiom is $$\forall y(\exists xA(x,y)\implies A(\epsilon_A(y),y)).$$

• More generally, an $$(n+1)$$-ary $$A$$ yields an $$n$$-ary $$\epsilon_A$$, with corresponding axiom $$\forall y_1,...,y_n(\exists xA(x,y_1,...,y_n)\implies A(\epsilon_A(y_1,...,y_n), y_1,...,y_n)).$$

Note the similarity between this kind of implementation and Skolem functions - it's exactly the same idea. Incidentally, it is at this point arguably better to adopt a version of first-order logic which allows for partial functions and empty structures, just for simplicity; the deductive apparatus of course gets more annoying, but very manageably so, and it might clean things up in certain respects. But that's not an essential point.

Of course, there's a more general question here which the above fails to address: what if we're looking for a general theory which allows for (essentially) arbitrary ways to build terms out of formulas?

In this case it seems that there is actually not too much literature out there. I asked an MO question about this a while back, since this is a topic I've already started working on and I wanted to avoid reinventing the wheel. Some basic model theory for the resulting logic is easy enough to whip up, but it seems not to have been done explicitly yet; the existing work seems to be on the computer science side, and not focused on those topics. (Incidentally, Andrej's answer to that question is a great example of how logicians should pay attention to computer science.)

If you're interested, I can tell you what I know about the resulting logic. But that gets a bit far afield for this answer, so I'll stop here for now.

(Incidentally, it looks like I forgot to mention the specific motivation at that question; briefly, I was - and am - playing around with abstract Godel numbering notions in the context of generalized recursion theory.)

• "what if we're looking for a general theory which allows for (essentially) arbitrary ways to build terms out of formulas?" That's the thing that I though plural logic addressed, but I suppose that's not considered satisfactory. – Simone Jul 19 '19 at 18:42
• @Simone I don't believe so. At best, plural logic captures one particular notion of such an assignment - namely, set(like-object)s to formulas. But I do mean arbitrary - e.g. Godel numbering constitutes such an operation, and plural logic isn't helpful there. – Noah Schweber Jul 19 '19 at 18:45
• ah! so we're looking for an hauptsatz for formulas that can be turned into Godel numbering (or something similar)? – Simone Jul 19 '19 at 18:50
• @Simone I'm not sure what a "hauptsatz" is (is that a cut elimination theorem?), so probably not; I'm just interested in a general model theory treating structures in the broader sense described in my MO question. – Noah Schweber Jul 19 '19 at 18:51
• @Simone Ah. No, my primary interest is the semantic side. But of course a satisfactory proof theory would be the natural next goal. (As to cut, I honestly don't care about cut elimination for its own sake - it's a useful tool if you have it, but even then only for some sorts of questions. If the system is sound and complete, I'm happy.) – Noah Schweber Jul 19 '19 at 19:04

In plural logic they do a similar thing but without the singularism which is inherent in set notation. The extension works by adding plural terms ( "the solutions to $$x^2 - 4 = 0$$", "nation states", " the soldiers surrounding the fort").

What's especially interesting is the natural expansion of descriptors: besides the notorious Russel's definite (singular) description, they add exhaustive description $$x:\phi x$$ ( in your example "the $$x$$s that singularly $$\phi$$), plural definite description and plural exhaustive description.